diff options
| -rw-r--r-- | cfrontend/SimplExprproof.v | 4 | ||||
| -rw-r--r-- | common/Memdata.v | 10 | ||||
| -rw-r--r-- | common/Switch.v | 8 | ||||
| -rw-r--r-- | lib/Coqlib.v | 6 | ||||
| -rw-r--r-- | lib/Iteration.v | 3 |
5 files changed, 18 insertions, 13 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 2aed0cdf..04afe4da 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1974,7 +1974,7 @@ Ltac NOTIN := exploit tr_simple_rvalue; eauto. simpl; intro SL1. subst sl0; simpl Kseqlist. econstructor; split. - right; split. apply star_refl. simpl. apply plus_lt_compat_r. + right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r. apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. apply S. eapply tr_expr_monotone; eauto. @@ -1996,7 +1996,7 @@ Ltac NOTIN := auto. + (* for effects *) econstructor; split. - right; split. apply star_refl. simpl. apply plus_lt_compat_r. + right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r. apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1. diff --git a/common/Memdata.v b/common/Memdata.v index 1bd87169..7622cab3 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -426,7 +426,7 @@ Lemma check_inj_value: Proof. induction n; simpl. auto. unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_true. - rewrite <- beq_nat_refl. simpl; auto. + rewrite Nat.eqb_refl. simpl; auto. Qed. Lemma proj_inj_value: @@ -719,7 +719,7 @@ Proof. { induction n; destruct mvs; simpl; intros; try discriminate. contradiction. - destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst. + destruct m; try discriminate. InvBooleans. apply Nat.eqb_eq in H4. subst. destruct H0. subst mv. exists n0; split; auto. lia. eapply IHn; eauto. lia. } @@ -738,7 +738,7 @@ Proof. destruct (quantity_eq q q0); auto. destruct (Nat.eqb sz n) eqn:EQN; auto. destruct (check_value sz v q mvl) eqn:CHECK; auto. - simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. + simpl. apply Nat.eqb_eq in EQN. subst n q0. constructor. auto. destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. congruence. intros. eapply B; eauto. lia. @@ -797,9 +797,9 @@ Lemma check_value_inject: Proof. induction 1; intros; destruct n; simpl in *; auto. inv H; auto. - InvBooleans. assert (n = n0) by (apply beq_nat_true; auto). subst v1 q0 n0. + InvBooleans. assert (n = n0) by (apply Nat.eqb_eq; auto). subst v1 q0 n0. replace v2 with v'. - unfold proj_sumbool; rewrite ! dec_eq_true. rewrite <- beq_nat_refl. simpl; eauto. + unfold proj_sumbool; rewrite ! dec_eq_true. rewrite Nat.eqb_refl. simpl; eauto. inv H2; try discriminate; inv H4; congruence. discriminate. Qed. diff --git a/common/Switch.v b/common/Switch.v index 70d1da15..23f9dd3e 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -271,7 +271,7 @@ Lemma validate_jumptable_correct_rec: Proof. induction tbl; simpl; intros. - unfold list_length_z in H0. simpl in H0. extlia. -- InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. +- InvBooleans. rewrite list_length_z_cons in H0. apply Nat.eqb_eq in H1. destruct (zeq v 0). + replace (base + v) with base by lia. congruence. + replace (base + v) with (Z.succ base + Z.pred v) by lia. @@ -308,13 +308,13 @@ Proof. intros default v VRANGE. induction t; simpl; intros until hi. - (* base case *) destruct cases as [ | [key1 act1] cases1]; intros. -+ apply beq_nat_true in H. subst act. reflexivity. -+ InvBooleans. apply beq_nat_true in H2. subst. simpl. ++ apply Nat.eqb_eq in H. subst act. reflexivity. ++ InvBooleans. apply Nat.eqb_eq in H2. subst. simpl. destruct (zeq v hi). auto. extlia. - (* eq node *) destruct (split_eq key cases) as [optact others] eqn:EQ. intros. destruct optact as [act1|]; InvBooleans; try discriminate. - apply beq_nat_true in H. + apply Nat.eqb_eq in H. rewrite (split_eq_prop v default _ _ _ _ EQ). destruct (zeq v key). + congruence. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 045fb03a..9b8f2abb 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -406,6 +406,12 @@ Qed. (** Properties of Euclidean division and modulus. *) +Lemma Z_div_mod_eq: forall a b, + b > 0 -> a = (b * (a / b) + a mod b). +Proof. + intros. apply Z.div_mod. lia. +Qed. + Lemma Zmod_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x mod y = b. diff --git a/lib/Iteration.v b/lib/Iteration.v index 34471826..50672069 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -204,7 +204,6 @@ End PrimIter. Require Import Classical. Require Import ClassicalDescription. -Require Import Max. Module GenIter. @@ -280,7 +279,7 @@ Lemma converges_to_unique: Proof. intros a b [n C] b' [n' C']. rewrite <- (C (max n n')). rewrite <- (C' (max n n')). auto. - apply le_max_r. apply le_max_l. + apply Nat.le_max_r. apply Nat.le_max_l. Qed. Lemma converges_to_exists_uniquely: |