diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/Memdata.v | 10 | ||||
-rw-r--r-- | common/Switch.v | 8 |
2 files changed, 9 insertions, 9 deletions
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. |