diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-07-07 16:26:42 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-07-07 16:26:42 +0200 |
commit | 0a5ce82066855bae205f9536c008715eebb470f2 (patch) | |
tree | d07ce5a99b4d680c31e2e43f635ad4d37dff8945 /src/bva | |
parent | c7f38ea3b96ee0e52f0e1f20ccfabd3206ff6ad2 (diff) | |
parent | 0a0dc47da1916c2a850610cfb80ba04c17e64549 (diff) | |
download | smtcoq-0a5ce82066855bae205f9536c008715eebb470f2.tar.gz smtcoq-0a5ce82066855bae205f9536c008715eebb470f2.zip |
Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13
Diffstat (limited to 'src/bva')
-rw-r--r-- | src/bva/BVList.v | 32 | ||||
-rw-r--r-- | src/bva/Bva_checker.v | 92 |
2 files changed, 56 insertions, 68 deletions
diff --git a/src/bva/BVList.v b/src/bva/BVList.v index 9e22f98..5c707f6 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -435,7 +435,7 @@ Fixpoint beq_listP (l m : list bool) {struct l} := Lemma bv_mk_eq l1 l2 : bv_eq l1 l2 = beq_list l1 l2. Proof. unfold bv_eq, size, bits. - case_eq (Nat_eqb (length l1) (length l2)); intro Heq. + case_eq (Nat.eqb (length l1) (length l2)); intro Heq. - now rewrite (EqNat.beq_nat_true _ _ Heq), N.eqb_refl. - replace (N.of_nat (length l1) =? N.of_nat (length l2)) with false. * revert l2 Heq. induction l1 as [ |b1 l1 IHl1]; intros [ |b2 l2]; simpl in *; auto. @@ -696,7 +696,7 @@ Definition bvmult_bool (a b: list bool) (n: nat) : list bool := Definition mult_list a b := bvmult_bool a b (length a). Definition bv_mult (a b : bitvector) : bitvector := - if ((@size a) =? (@size b)) + if ((@size a) =? (@size b))%N then mult_list a b else zeros (@size a). @@ -710,11 +710,11 @@ Proof. intro n. Qed. Definition _of_bits (a:list bool) (s: N) := -if (N.of_nat (length a) =? s) then a else zeros s. +if (N.of_nat (length a) =? s)%N then a else zeros s. Lemma _of_bits_size l s: (size (_of_bits l s)) = s. Proof. unfold of_bits, size. unfold _of_bits. - case_eq ( N.of_nat (length l) =? s). + case_eq ( N.of_nat (length l) =? s)%N. intros. now rewrite N.eqb_eq in H. intros. unfold zeros. rewrite length_mk_list_false. now rewrite N2Nat.id. @@ -800,7 +800,7 @@ Qed. Lemma bv_eq_reflect a b : bv_eq a b = true <-> a = b. Proof. - unfold bv_eq. case_eq (size a =? size b); intro Heq; simpl. + unfold bv_eq. case_eq (size a =? size b)%N; intro Heq; simpl. - apply List_eq. - split; try discriminate. intro H. rewrite H, N.eqb_refl in Heq. discriminate. @@ -1880,11 +1880,11 @@ Qed. Lemma bv_ult_B2P: forall x y, bv_ult x y = true <-> bv_ultP x y. Proof. intros. split; intros; unfold bv_ult, bv_ultP in *. - case_eq (size x =? size y); intros; + case_eq (size x =? size y)%N; intros; rewrite H0 in H; unfold ult_listP. now rewrite H. now contradict H. unfold ult_listP in *. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. rewrite H0 in H. case_eq (ult_list x y); intros. easy. rewrite H1 in H. now contradict H. @@ -1893,11 +1893,11 @@ Qed. Lemma bv_slt_B2P: forall x y, bv_slt x y = true <-> bv_sltP x y. Proof. intros. split; intros; unfold bv_slt, bv_sltP in *. - case_eq (size x =? size y); intros; + case_eq (size x =? size y)%N; intros; rewrite H0 in H; unfold slt_listP. now rewrite H. now contradict H. unfold slt_listP in *. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. rewrite H0 in H. case_eq (slt_list x y); intros. easy. rewrite H1 in H. now contradict H. @@ -1962,28 +1962,28 @@ Qed. Lemma bv_ult_not_eqP : forall x y, bv_ultP x y -> x <> y. Proof. intros x y. unfold bv_ultP. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply ult_list_not_eqP in H0. - now contradict H0. Qed. Lemma bv_slt_not_eqP : forall x y, bv_sltP x y -> x <> y. Proof. intros x y. unfold bv_sltP. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply slt_list_not_eqP in H0. - now contradict H0. Qed. Lemma bv_ult_not_eq : forall x y, bv_ult x y = true -> x <> y. Proof. intros x y. unfold bv_ult. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply ult_list_not_eq in H0. - now contradict H0. Qed. Lemma bv_slt_not_eq : forall x y, bv_slt x y = true -> x <> y. Proof. intros x y. unfold bv_slt. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply slt_list_not_eq in H0. - now contradict H0. Qed. @@ -2258,7 +2258,7 @@ Qed. size a = n1 -> size (@bv_extr i n0 n1 a) = n0%N. Proof. intros. unfold bv_extr, size in *. - case_eq (n1 <? n0 + i). + case_eq (n1 <? n0 + i)%N. intros. now rewrite length_mk_list_false, N2Nat.id. intros. specialize (@length_extract a i (n0 + i)). intros. @@ -2455,7 +2455,7 @@ Qed. (** bit-vector extension *) Definition bv_shl (a b : bitvector) : bitvector := - if ((@size a) =? (@size b)) + if ((@size a) =? (@size b))%N then shl_be a b else zeros (@size a). @@ -2510,7 +2510,7 @@ Qed. (** bit-vector extension *) Definition bv_shr (a b : bitvector) : bitvector := - if ((@size a) =? (@size b)) + if ((@size a) =? (@size b))%N then shr_be a b else zeros (@size a). diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 0518992..a7743b2 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -12,7 +12,7 @@ (** A small checker for bit-vectors bit-blasting *) -Require Import Int63 Int63Properties PArray SMT_classes ZArith. +Require Import Int63 PArray SMT_classes ZArith. Require Import Misc State SMT_terms BVList Psatz. Require Import Bool List BoolEq NZParity Nnat. @@ -87,7 +87,7 @@ Section Checker. Fixpoint check_bb (a: int) (bs: list _lit) (i n: nat) := match bs with - | nil => Nat_eqb i n (* We go up to n *) + | nil => Nat.eqb i n (* We go up to n *) | b::bs => if Lit.is_pos b then match get_form (Lit.blit b) with @@ -95,10 +95,10 @@ Section Checker. match get_atom a' with | Auop (UO_BVbitOf N p) a' => (* TODO: - Do not need to check [Nat_eqb l (N.to_nat N)] at every iteration *) + Do not need to check [Nat.eqb l (N.to_nat N)] at every iteration *) if (a == a') (* We bit blast the right bv *) - && (Nat_eqb i p) (* We consider bits after bits *) - && (Nat_eqb n (N.to_nat N)) (* The bv has indeed type BV n *) + && (Nat.eqb i p) (* We consider bits after bits *) + && (Nat.eqb n (N.to_nat N)) (* The bv has indeed type BV n *) then check_bb a bs (S i) n else false | _ => false @@ -262,7 +262,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := if Lit.is_pos bres then match get_form (Lit.blit bres) with | Fand args => - match PArray.to_list args with + match to_list args with | bres :: bsres => if Lit.is_pos bres then let ires := @@ -530,7 +530,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := end. Definition check_mult (bs1 bs2 bsres: list _lit) : bool := - if Nat_eqb (length bs1) (length bs2)%nat then + if Nat.eqb (length bs1) (length bs2)%nat then let bvm12 := bblast_bvmult bs1 bs2 (length bs1) in forallb2 eq_carry_lit bvm12 bsres else false. @@ -1080,7 +1080,7 @@ Definition shr_lit_be (a: list _lit) (b: list bool): list _lit := Let rho_interp : forall x : int, rho x = Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[ x]). Proof. intros x;apply wf_interp_form;trivial. Qed. - Definition wf := PArray.forallbi lt_form t_form. + Definition wf := aforallbi lt_form t_form. Hypothesis wf_t_i : wf. Variable interp_bvatom : atom -> forall s, BITVECTOR_LIST.bitvector s. @@ -1125,17 +1125,6 @@ Qed. Lemma le_le_S_eq : forall (n m: nat), (n <= m)%nat -> (S n <= m)%nat \/ n = m. Proof le_lt_or_eq. -Lemma Nat_eqb_eq: forall n m, Nat_eqb n m = true -> n = m. -Proof. induction n. - intros n Hm. simpl in Hm. case_eq n. reflexivity. - intros. rewrite H in Hm. now contradict H. - intros m Hm. - case_eq m. intros. rewrite H in Hm. simpl in Hm. - now contradict Hm. - intros. rewrite H in Hm. simpl in Hm. - specialize (@IHn n0 Hm). now rewrite IHn. -Qed. - Lemma diseq_neg_eq: forall (la lb: list bool), List_diseqb la lb = true -> negb (RAWBITVECTOR_LIST.beq_list la lb) = true. Proof. intro la. @@ -1218,7 +1207,7 @@ Proof. rewrite Typ.N_cast_refl. simpl. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. (* a *) pose proof (H a). @@ -1327,7 +1316,7 @@ Proof. intros a bs. case_eq u; try (intro Heq'; rewrite Heq' in H0; now contradict H0). intros. rewrite H2 in H0. - case_eq ((a == i2) && Nat_eqb i n1 && Nat_eqb n (N.to_nat n0)). intros Hif. + case_eq ((a == i2) && Nat.eqb i n1 && Nat.eqb n (N.to_nat n0)). intros Hif. rewrite Hif in H0. do 2 rewrite andb_true_iff in Hif. destruct Hif as ((Hif0 & Hif1) & Hif2). specialize (@IHys a (S i) n). @@ -1362,7 +1351,7 @@ Proof. intros a bs. rewrite Hif0. rewrite <- Hd. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. assert (i1 < PArray.length t_atom). { apply PArray.get_not_default_lt. @@ -1412,8 +1401,8 @@ Proof. intros a bs. apply Typ.eqb_spec in H7. inversion H7. easy. - now apply Nat_eqb_eq in Hif2. - now apply Nat_eqb_eq in Hif1. + now apply Nat.eqb_eq in Hif2. + now apply Nat.eqb_eq in Hif1. lia. destruct H1. @@ -1525,7 +1514,7 @@ Proof. unfold Lit.interp. unfold Var.interp. destruct wf_rho. simpl. unfold Lit.blit. cut (0 >> 1 = 0). intros Heq0. rewrite Heq0. exact H. - now rewrite lsr_0_l. + now rewrite lsr0_l. apply is_even_0. Qed. @@ -1759,7 +1748,7 @@ Proof. + simpl in Hcheck; now contradict Hcheck. + simpl in Hlen. inversion Hlen as [Hlen']. simpl in Hcheck. rewrite andb_true_iff in Hcheck; destruct Hcheck as (Hcheck1, Hcheck2). - apply Int63Properties.eqb_spec in Hcheck1; rewrite Hcheck1. + apply Int63.eqb_spec in Hcheck1; rewrite Hcheck1. simpl. rewrite Lit.interp_neg. apply f_equal. apply IHbs; auto. Qed. @@ -1804,7 +1793,7 @@ Proof. rewrite !andb_true_iff in Hc. destruct Hc as ((Ha, Hcheck), Hlen). rewrite N.eqb_eq in Hlen. - apply Int63Properties.eqb_spec in Ha. + apply Int63.eqb_spec in Ha. generalize (Hs pos). rewrite Hpos, Hnil. unfold C.valid, C.interp; simpl; rewrite !orb_false_r. @@ -1820,7 +1809,7 @@ Proof. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H r). assert (r < PArray.length t_atom). @@ -1933,12 +1922,11 @@ Qed. Lemma to_list_two: forall {A:Type} (a: PArray.array A), PArray.length a = 2 -> (to_list a) = a .[0] :: a .[1] :: nil. Proof. intros A a H. - rewrite to_list_to_list_ntr. unfold to_list_ntr. + unfold to_list. rewrite H. - cut (0 == 2 = false). intro H1. - rewrite H1. - unfold foldi_ntr. rewrite foldi_cont_lt; auto. - auto. + rewrite 2!foldi_lt_r by reflexivity. + rewrite foldi_ge by reflexivity. + reflexivity. Qed. Lemma check_symopp_and: forall ibs1 ibs2 xbs1 ybs2 ibsres zbsres N, @@ -3236,7 +3224,7 @@ Proof. rewrite Atom.t_interp_wf; trivial. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -3569,7 +3557,7 @@ Proof. rewrite Atom.t_interp_wf; trivial. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -3901,7 +3889,7 @@ Proof. rewrite Atom.t_interp_wf; trivial. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -4529,7 +4517,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres). rewrite wf_interp_form; trivial. rewrite Heq8. simpl. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a3). assert (a3 < PArray.length t_atom). @@ -5185,7 +5173,7 @@ Proof. rewrite wf_interp_form; trivial. rewrite Heq8. simpl. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a3). assert (a3 < PArray.length t_atom). @@ -5410,7 +5398,7 @@ Proof. rewrite wf_interp_form; trivial. rewrite Heq8. simpl. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a3). assert (a3 < PArray.length t_atom). @@ -5822,7 +5810,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -6270,7 +6258,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -6302,7 +6290,7 @@ Proof. do 2 rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq10, Heq11). destruct Heq10 as (Heq10a1 & Heq10a2). - rewrite Int63Properties.eqb_spec in Heq10a1; rewrite Heq10a1 in *. + rewrite Int63.eqb_spec in Heq10a1; rewrite Heq10a1 in *. (* interp_form_hatom_bv a = interp_bv t_i (interp_atom (t_atom .[a])) *) @@ -6556,8 +6544,8 @@ Proof. intros bs1. + unfold check_mult in H. now contradict H. - intros. unfold check_mult in H. - case_eq (Nat_eqb (Datatypes.length (a :: bs1)) ((Datatypes.length bs2))). - intros. now apply Nat_eqb_eq in H0. + case_eq (Nat.eqb (Datatypes.length (a :: bs1)) ((Datatypes.length bs2))). + intros. now apply Nat.eqb_eq in H0. intros. rewrite H0 in H. now contradict H. Qed. @@ -6581,7 +6569,7 @@ Lemma prop_main: forall bs1 bs2 bsres, map interp_carry (bblast_bvmult bs1 bs2 (Datatypes.length (map (Lit.interp rho) bs1))) = map (Lit.interp rho) bsres. Proof. intros. unfold check_mult in H. - case_eq (Nat_eqb (Datatypes.length bs1) (Datatypes.length bs2)). intros. + case_eq (Nat.eqb (Datatypes.length bs1) (Datatypes.length bs2)). intros. rewrite H0 in H. apply prop_eq_carry_lit2 in H. rewrite map_length. now rewrite H. @@ -6620,7 +6608,7 @@ Proof. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -6925,7 +6913,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -7241,7 +7229,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -7501,7 +7489,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -7747,7 +7735,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -8071,7 +8059,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). @@ -8401,7 +8389,7 @@ Proof. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. - rewrite PArray.forallbi_spec;intros. + rewrite aforallbi_spec;intros. pose proof (H a). assert (a < PArray.length t_atom). |