diff options
Diffstat (limited to 'src/bva/Bva_checker.v')
| -rw-r--r-- | src/bva/Bva_checker.v | 302 |
1 files changed, 151 insertions, 151 deletions
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 24917a8..5c14bab 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -96,7 +96,7 @@ Section Checker. | Auop (UO_BVbitOf N p) a' => (* TODO: Do not need to check [Nat.eqb l (N.to_nat N)] at every iteration *) - if (a == a') (* We bit blast the right bv *) + 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 *) then check_bb a bs (S i) n @@ -133,7 +133,7 @@ Section Checker. Fixpoint check_not (bs br : list _lit) := match bs, br with | nil, nil => true - | b::bs, r::br => (r == Lit.neg b) && check_not bs br + | b::bs, r::br => (r =? Lit.neg b) && check_not bs br | _, _ => false end. @@ -146,7 +146,7 @@ Section Checker. | FbbT a bs, FbbT r br => match get_atom r with | Auop (UO_BVnot N) a' => - if (a == a') && check_not bs br && + if (a =? a') && check_not bs br && (N.of_nat (length bs) =? N)%N then lres::nil else C._true @@ -174,25 +174,25 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_form (Lit.blit bres), bvop with | Fand args, BO_BVand n => - ((if PArray.length args == 2 then + ((if PArray.length args =? 2 then let a1 := args.[0] in let a2 := args.[1] in - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) else false), BO_BVand (n-1)) | For args, BO_BVor n => - ((if PArray.length args == 2 then + ((if PArray.length args =? 2 then let a1 := args.[0] in let a2 := args.[1] in - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) else false), BO_BVor (n-1)) | Fxor a1 a2, BO_BVxor n => - (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)), + (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)), BO_BVxor (n-1)) | Fiff a1 a2, (BO_eq (Typ.TBV n)) => - (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)), + (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)), BO_eq (Typ.TBV n)) | _, _ => (false, bvop) @@ -218,21 +218,21 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVand n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (@check_symopp bs1 bs2 bsres (BO_BVand n)) && (N.of_nat (length bs1) =? n)%N then lres::nil else C._true | Abop (BO_BVor n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_symopp bs1 bs2 bsres (BO_BVor n)) && (N.of_nat (length bs1) =? n)%N then lres::nil else C._true | Abop (BO_BVxor n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_symopp bs1 bs2 bsres (BO_BVxor n)) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -268,7 +268,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := let ires := match get_form (Lit.blit bres) with | Fiff a1 a2 => - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) | _ => false end in if ires then check_eq bs1 bs2 bsres @@ -284,7 +284,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := let ires := match get_form (Lit.blit bres) with | Fiff a1 a2 => - ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)) + ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) | _ => false end in if ires then check_eq bs1 bs2 bsres @@ -306,7 +306,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Fatom a, _ (* | _, Fatom a *) => match get_atom a with | Abop (BO_eq (Typ.TBV n)) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_eq bs1 bs2 [lbb]) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -340,12 +340,12 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := Fixpoint eq_carry_lit (carry : carry) (c : _lit) := if Lit.is_pos c then match carry with - | Clit l => l == c + | Clit l => l =? c | Cand c1 c2 => match get_form (Lit.blit c) with | Fand args => - if PArray.length args == 2 then + if PArray.length args =? 2 then (eq_carry_lit c1 (args.[0]) && eq_carry_lit c2 (args.[1])) (* || (eq_carry_lit c1 (args.[1]) && eq_carry_lit c2 (args.[0])) *) else false @@ -363,7 +363,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Cor c1 c2 => match get_form (Lit.blit c) with | For args => - if PArray.length args == 2 then + if PArray.length args =? 2 then (eq_carry_lit c1 (args.[0]) && eq_carry_lit c2 (args.[1])) (* || (eq_carry_lit c1 (args.[1]) && eq_carry_lit c2 (args.[0])) *) else false @@ -381,7 +381,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := else (* c can be negative only when it is literal false *) match carry with - | Clit l => l == c + | Clit l => l =? c | _ => false end. @@ -400,7 +400,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := (* This is the way LFSC computes carries *) let carry' := Cor (Cand (Clit b1) (Clit b2)) (Cand (Cxor (Clit b1) (Clit b2)) carry) in - (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1))) + (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1))) && eq_carry_lit carry c && check_add bs1 bs2 bsres carry' | _ => false @@ -422,7 +422,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVadd n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1'))) + if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_add bs1 bs2 bsres (Clit Lit._false)) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -458,7 +458,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | FbbT a bs, FbbT r br => match get_atom r with | Auop (UO_BVneg n) a' => - if (a == a') && check_neg bs br && + if (a =? a') && check_neg bs br && (N.of_nat (length bs) =? n)%N then lres::nil else C._true @@ -545,7 +545,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVmult n) a1' a2' => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_mult bs1 bs2 bsres) && (N.of_nat (length bs1) =? n)%N then lres::nil @@ -590,7 +590,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Fatom a, _ (* | _, Fatom a *) => match get_atom a with | Abop (BO_BVult n) a1' a2' => - if ((a1 == a1') && (a2 == a2')) + if ((a1 =? a1') && (a2 =? a2')) && (check_ult bs1 bs2 lbb) && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bs2) =? n)%N @@ -636,7 +636,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | Fatom a, _ (* | _, Fatom a *) => match get_atom a with | Abop (BO_BVslt n) a1' a2' => - if ((a1 == a1') && (a2 == a2')) + if ((a1 =? a1') && (a2 =? a2')) && (check_slt bs1 bs2 lbb) && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bs2) =? n)%N @@ -691,7 +691,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Abop (BO_BVconcat n m) a1' a2' => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_concat bs1 bs2 bsres) && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bs2) =? m)%N @@ -771,7 +771,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := else false. Definition check_extract3 (bs bsres: list _lit) (i j: N) : bool := - forallb2 (fun l1 l2 => l1 == l2) (extract_lit bs (nat_of_N i) (nat_of_N j)) bsres. + forallb2 (fun l1 l2 => l1 =? l2) (extract_lit bs (nat_of_N i) (nat_of_N j)) bsres. (** Checker for bitvector extraction *) @@ -783,7 +783,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := | O => match j, bsres with | O, nil => true - | S j', b :: bsres' => (bx == b) && check_extract2 x' bsres' i j' + | S j', b :: bsres' => (bx =? b) && check_extract2 x' bsres' i j' | _, _ => false end | S i' => @@ -804,7 +804,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Auop (UO_BVextr i n0 n1) a1' => - if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) ) + if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_extract bs bsres i (n0 + i)) && (N.of_nat (length bs) =? n1)%N && (N.leb (n0 + i) n1) @@ -847,7 +847,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Auop (UO_BVzextn n i) a1' => - if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) ) + if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_zextend bs bsres i) && (N.of_nat (length bs) =? n)%N then lres::nil @@ -889,7 +889,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match get_atom a with | Auop (UO_BVsextn n i) a1' => - if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) ) + if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) ) && (check_sextend bs bsres i) && (N.of_nat (length bs) =? n)%N then lres::nil @@ -938,7 +938,7 @@ Definition shl_lit_be (a: list _lit) (b: list bool): list _lit := | Abop (BO_BVshl n) a1' a2' => match (get_atom a2) with | (Acop (CO_BV bv2 n2)) => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && check_shl bs1 bv2 bsres && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bv2) =? n)%N @@ -989,7 +989,7 @@ Definition shr_lit_be (a: list _lit) (b: list bool): list _lit := | Abop (BO_BVshr n) a1' a2' => match (get_atom a2) with | (Acop (CO_BV bv2 n2)) => - if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) ) + if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) ) && check_shr bs1 bv2 bsres && (N.of_nat (length bs1) =? n)%N && (N.of_nat (length bv2) =? n)%N @@ -1211,7 +1211,7 @@ Proof. (* a *) pose proof (H a). - assert (H1: a < PArray.length t_atom). + assert (H1: a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4, Heq5. easy. } specialize (@H0 H1). rewrite Heq4 in H0. simpl in H0. unfold get_type' in H0. unfold v_type in H0. @@ -1229,7 +1229,7 @@ Proof. (* b *) pose proof (H b). - assert (H4: b < PArray.length t_atom). + assert (H4: b <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6, Heq7. easy. } specialize (@H2 H4). rewrite Heq6 in H2. simpl in H2. unfold get_type' in H2. unfold v_type in H2. @@ -1247,7 +1247,7 @@ Proof. (* f *) pose proof (H f). - assert (H7: f < PArray.length t_atom). + assert (H7: f <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. } specialize (@H5 H7). rewrite Heq3 in H5. simpl in H5. unfold get_type' in H5. unfold v_type in H5. @@ -1316,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). @@ -1352,7 +1352,7 @@ Proof. intros a bs. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. - assert (i1 < PArray.length t_atom). + assert (i1 <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite Heq2. now rewrite def_t_atom. @@ -1785,7 +1785,7 @@ Proof. intros u a'. case_eq u; try (intros; now apply C.interp_true). intros n Huot Hr. - case_eq ((a == a') + case_eq ((a =? a') && check_not bs br && (N.of_nat (Datatypes.length bs) =? n)%N); try (intros; now apply C.interp_true). @@ -1812,7 +1812,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H r). - assert (r < PArray.length t_atom). + assert (r <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Hr. easy. } @@ -1914,7 +1914,7 @@ Qed. Lemma eq_head: forall {A: Type} a b (l: list A), (a :: l) = (b :: l) <-> a = b. Proof. intros A a b l; split; [intros H; inversion H|intros ->]; auto. Qed. -Lemma eqb_spec : forall x y, (x == y) = true <-> x = y. +Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y. Proof. split;auto using eqb_correct, eqb_complete. Qed. @@ -1937,9 +1937,9 @@ Proof. intros. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. exact H. now contradict H. now contradict H. @@ -1947,9 +1947,9 @@ Proof. intros. unfold check_symopp in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. apply H. now contradict H. now contradict H. @@ -1964,9 +1964,9 @@ Proof. intros. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. exact H. now contradict H. now contradict H. @@ -1974,9 +1974,9 @@ Proof. intros. unfold check_symopp in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case (PArray.length a == 2) in H. - case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2) - || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H. + case (PArray.length a =? 2) in H. + case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) + || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. apply H. now contradict H. now contradict H. @@ -1991,14 +1991,14 @@ Proof. intros. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H. + case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H. exact H. now contradict H. now contradict H. unfold check_symopp in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H. + case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H. apply H. now contradict H. now contradict H. @@ -2041,20 +2041,20 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. (* apply length_to_list in H4. *) unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_true_r. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. @@ -2100,19 +2100,19 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_true_r. intros H4. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite andb_true_r. @@ -2164,19 +2164,19 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_true_r. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite andb_true_r. @@ -2226,20 +2226,20 @@ Proof. intro bs1. intros. rewrite H3 in H1. simpl. rewrite afold_left_and. - case_eq (PArray.length a == 2). intros H5. + case_eq (PArray.length a =? 2). intros H5. rewrite H5 in H1. rewrite eqb_spec in H5. apply to_list_two in H5. unfold forallb. rewrite H5. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H6. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H6. rewrite andb_true_iff in H6. destruct H6 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold Lit.interp. rewrite Heq1, H2. unfold Var.interp. now rewrite andb_true_r. intros H6. rewrite H6 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H7. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H7. rewrite andb_true_iff in H7. destruct H7 as (H7 & H8). rewrite eqb_spec in H7, H8. rewrite H7, H8. rewrite andb_true_r. @@ -2310,12 +2310,12 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold C.interp. unfold existsb. rewrite orb_false_r. @@ -2325,7 +2325,7 @@ Proof. intro bs1. now unfold Var.interp. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. @@ -2369,21 +2369,21 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold C.interp. unfold existsb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite orb_false_r. intros H4. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite orb_false_r. @@ -2433,12 +2433,12 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros. rewrite H3 in H1. + case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold C.interp, existsb. @@ -2446,7 +2446,7 @@ Proof. intro bs1. rewrite Heq1, Heq2. unfold Var.interp. now rewrite orb_false_r. intros. rewrite H4 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite orb_false_r. @@ -2494,20 +2494,20 @@ Proof. intro bs1. intros. rewrite H3 in H1. simpl. rewrite afold_left_or. - case_eq (PArray.length a == 2). intros H5. + case_eq (PArray.length a =? 2). intros H5. rewrite H5 in H1. rewrite eqb_spec in H5. apply to_list_two in H5. unfold forallb. rewrite H5. - case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H6. + case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H6. rewrite andb_true_iff in H6. destruct H6 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold C.interp, Lit.interp, existsb. rewrite Heq1, H2. unfold Var.interp. now rewrite orb_false_r. intros H6. rewrite H6 in H1. simpl in *. - case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H7. + case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H7. rewrite andb_true_iff in H7. destruct H7 as (H7 & H8). rewrite eqb_spec in H7, H8. rewrite H7, H8. rewrite orb_false_r. @@ -2576,7 +2576,7 @@ Proof. intro bs1. try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros i Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. @@ -2585,7 +2585,7 @@ Proof. intro bs1. now unfold Var.interp. intros H4. rewrite H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. @@ -2629,14 +2629,14 @@ Proof. intro bs1. try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). intros H5. + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. @@ -2686,14 +2686,14 @@ Proof. intro bs1. intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). intros H5. + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. @@ -2740,14 +2740,14 @@ Proof. intro bs1. try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. - case_eq ((i == ibs1) && (i0 == ibs2)). intros H5. + case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. - case_eq ((i == ibs2) && (i0 == ibs1)). intros H5. + case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. @@ -2796,8 +2796,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2834,8 +2834,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2871,8 +2871,8 @@ Proof. intros bs1 bs2 bsres. now contradict H. case (Lit.is_pos xbsres) in *. case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H. - case (PArray.length a == 2) in *. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in *. + case (PArray.length a =? 2) in *. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in *. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). @@ -2924,8 +2924,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2961,8 +2961,8 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case (PArray.length a == 2) in H; try easy. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy. + case (PArray.length a =? 2) in H; try easy. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -2998,8 +2998,8 @@ Proof. intros bs1 bs2 bsres. now contradict H. case (Lit.is_pos xbsres) in *. case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H. - case (PArray.length a == 2) in *. - case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in *. + case (PArray.length a =? 2) in *. + case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in *. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). @@ -3051,7 +3051,7 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in H; try easy. + case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -3088,7 +3088,7 @@ Proof. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. - case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in H; try easy. + case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. @@ -3124,7 +3124,7 @@ Proof. intros bs1 bs2 bsres. now contradict H. case (Lit.is_pos xbsres) in *. case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H. - case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in *. + case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in *. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). @@ -3204,7 +3204,7 @@ Proof. intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVand *) - - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); + - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( @@ -3227,7 +3227,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -3537,7 +3537,7 @@ Proof. exact Heq11. (* BVor *) - - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); + - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( @@ -3560,7 +3560,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -3869,7 +3869,7 @@ Proof. exact Heq11. (** BVxor **) - - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); + - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( @@ -3892,7 +3892,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -4210,7 +4210,7 @@ Proof. intros. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). - case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H. + case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H. exact H. now contradict H. now contradict H. @@ -4228,7 +4228,7 @@ Proof. intros. case_eq (t_form .[ Lit.blit ibsres]); intros; rewrite H1 in H; try (now contradict H). specialize (@rho_interp ( Lit.blit ibsres)). rewrite H1 in rho_interp. simpl in rho_interp. - case_eq ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)). + case_eq ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)). intros. rewrite orb_true_iff in H2. destruct H2. rewrite andb_true_iff in H2. destruct H2. rewrite eqb_spec in H2, H3. rewrite H2, H3 in rho_interp. @@ -4320,7 +4320,7 @@ Proof. intro bs1. (*++*) rename i into arg1; rename i0 into arg2. unfold Lit.interp at 1, Var.interp at 1. rewrite Hposr1, Hi. repeat (rewrite andb_true_r). - case_eq ((arg1 == x1) && (arg2 == x2) || (arg1 == x2) && (arg2 == x1)). + case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)). (* ** *) intros Hif. rewrite orb_true_iff in Hif. repeat (rewrite andb_true_iff in Hif). @@ -4351,7 +4351,7 @@ Proof. intro bs1. unfold Lit.interp at 1, Var.interp at 1. rewrite Hposa1. rewrite Heqx1x2. - case_eq ((arg1 == x1) && (arg2 == x2) || (arg1 == x2) && (arg2 == x1)). + case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)). (* ** *) intros Hif. rewrite Hif in Hcheck. apply (@IHbs1 _ _ Hlen') in Hcheck. @@ -4375,11 +4375,11 @@ Proof. intro bs1. generalize (rho_interp (Lit.blit r1)); rewrite Hform_r1; simpl; intro Hi. (* ++ *) contradict Hcheck. simpl. - case ((i0 == x1) && (i1 == x2) || (i0 == x2) && (i1 == x1)); easy. + case ((i0 =? x1) && (i1 =? x2) || (i0 =? x2) && (i1 =? x1)); easy. (* ++ *) rename i0 into x1', i1 into x2', i2 into arg1, i3 into arg2. unfold Lit.interp at 1, Var.interp at 1. rewrite Hposr1, Hi. - case_eq ((arg1 == x1) && (arg2 == x2) || (arg1 == x2) && (arg2 == x1)). + case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)). (* ** *) intros Hif. rewrite Hif in Hcheck. apply (@IHbs1 _ _ Hlen') in Hcheck. simpl in Hcheck. rewrite Hcheck. @@ -4424,7 +4424,7 @@ Proof. case (Lit.is_pos i2); try easy. case (t_form .[ Lit.blit i2]); try easy. intros i3 i4. - case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)). + case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. intros _ _ i2 l0 a0. @@ -4433,7 +4433,7 @@ Proof. case (Lit.is_pos i1); try easy. case (t_form .[ Lit.blit i1]); try easy. intros i3 i4. - case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)). + case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. intros i2 l0 a0. @@ -4442,7 +4442,7 @@ Proof. case (Lit.is_pos i9); try easy. case (t_form .[ Lit.blit i9]); try easy. intros i3 i4. - case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)). + case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. intros _ _ i2 l0 a0. @@ -4451,7 +4451,7 @@ Proof. case (Lit.is_pos i9); try easy. case (t_form .[ Lit.blit i9]); try easy. intros i3 i4. - case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)). + case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. case bs1; try easy; case bs2; easy. @@ -4462,10 +4462,10 @@ Proof. simpl. easy. intros i0 l i1 i2. - case ((i1 == a) && (i2 == i) || (i1 == i) && (i2 == a)); easy. + case ((i1 =? a) && (i2 =? i) || (i1 =? i) && (i2 =? a)); easy. simpl. intros _ l i1 i2. - case ((i1 == a) && (i2 == i) || (i1 == i) && (i2 == a)); easy. + case ((i1 =? a) && (i2 =? i) || (i1 =? i) && (i2 =? a)); easy. easy. case bs1 in *; try easy; case bs2; easy. case bs1 in *; try easy; case bs2; easy. @@ -4473,13 +4473,13 @@ Proof. case bs1 in *; try easy; case bs2; try easy. case (Lit.is_pos r); try easy. case (t_form .[ Lit.blit r]); try easy. - simpl. intros x y. case ((x == a) && (y == i) || (x == i) && (y == a)); easy. + simpl. intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)); easy. case (Lit.is_pos r); try easy. case (t_form .[ Lit.blit r]); try easy. - simpl. intros x y. case ((x == a) && (y == i) || (x == i) && (y == a)); easy. + simpl. intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)); easy. case (Lit.is_pos r); try easy. case (t_form .[ Lit.blit r]); try easy. - intros x y. case ((x == a) && (y == i) || (x == i) && (y == a)). + intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)). intros x2 rbs2 xr rbrs. apply IHbs1. easy. Qed. @@ -4503,7 +4503,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres). try (intros; now apply C.interp_true). intros a1' a2' Heq9. - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); + case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq15; try (now apply C.interp_true). case_eq (check_eq bs1 bs2 [bsres] && @@ -4520,7 +4520,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres). rewrite aforallbi_spec;intros. pose proof (H a3). - assert (a3 < PArray.length t_atom). + assert (a3 <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -4887,7 +4887,7 @@ Proof. intro c. case_eq ( Lit.is_pos i). intros Hip0. rewrite Hip0 in H. case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H. - case_eq (PArray.length a == 2). intros Hl. rewrite Hl in H. + case_eq (PArray.length a =? 2). intros Hl. rewrite Hl in H. (* rewrite orb_true_iff in H; do 2 *) rewrite andb_true_iff in H. specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp. @@ -4935,7 +4935,7 @@ Proof. intro c. case_eq ( Lit.is_pos i). intros Hip0. rewrite Hip0 in H. case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H. - case_eq (PArray.length a == 2). intros Hl. rewrite Hl in H. + case_eq (PArray.length a =? 2). intros Hl. rewrite Hl in H. (* rewrite orb_true_iff in H; do 2 *) rewrite andb_true_iff in H. specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp. @@ -5158,7 +5158,7 @@ Proof. try (intros; now apply C.interp_true). intros a1' a2' Heq9. - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq15; try (now apply C.interp_true). + case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq15; try (now apply C.interp_true). case_eq (check_ult bs1 bs2 bsres && (N.of_nat (Datatypes.length bs1) =? N)%N && @@ -5176,7 +5176,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a3). - assert (a3 < PArray.length t_atom). + assert (a3 <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -5383,7 +5383,7 @@ Proof. intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq15; try (now apply C.interp_true). + case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq15; try (now apply C.interp_true). case_eq (check_slt bs1 bs2 bsres && (N.of_nat (Datatypes.length bs1) =? N)%N && @@ -5401,7 +5401,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a3). - assert (a3 < PArray.length t_atom). + assert (a3 <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -5795,7 +5795,7 @@ Proof. try (intros; now apply C.interp_true). (* BVadd *) - - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); + - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_add bs1 bs2 bsres (Clit Lit._false) && @@ -5813,7 +5813,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -6246,7 +6246,7 @@ Proof. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | | | | ] a1' Heq9; try now apply C.interp_true. - case_eq ((a1 == a1') && check_neg bs1 bsres && + case_eq ((a1 =? a1') && check_neg bs1 bsres && (N.of_nat (Datatypes.length bs1) =? n)%N); simpl; intros Heq11; try (now apply C.interp_true). @@ -6261,7 +6261,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. @@ -6591,7 +6591,7 @@ Proof. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVmult *) - - case_eq ((a1 == a1') && (a2 == a2') (* || (a1 == a2') && (a2 == a1')*) ); + - case_eq ((a1 =? a1') && (a2 =? a2') (* || (a1 =? a2') && (a2 =? a1')*) ); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( @@ -6611,7 +6611,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -6899,7 +6899,7 @@ Proof. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVconcat *) - - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true). + - case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_concat bs1 bs2 bsres && (N.of_nat (Datatypes.length bs1) =? N)%N && (N.of_nat (Datatypes.length bs2) =? n)%N @@ -6916,7 +6916,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. @@ -7215,7 +7215,7 @@ Proof. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | | | | ] a1' Heq6; try (intros; now apply C.interp_true). (* BVextract *) - - case_eq ((a1 == a1')); simpl; intros Heq7; try (now apply C.interp_true). + - case_eq ((a1 =? a1')); simpl; intros Heq7; try (now apply C.interp_true). case_eq ( check_extract bs1 bsres i (n0 + i) && (N.of_nat (Datatypes.length bs1) =? n1)%N && (n0 + i <=? n1)%N @@ -7232,7 +7232,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. easy. } specialize (@H0 H1). rewrite Heq6 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. @@ -7476,7 +7476,7 @@ Proof. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | | | | ] a1' Heq6; try (intros; now apply C.interp_true). (* BVzextend *) - - case_eq ((a1 == a1')); simpl; intros Heq7; try (now apply C.interp_true). + - case_eq ((a1 =? a1')); simpl; intros Heq7; try (now apply C.interp_true). case_eq ( check_zextend bs1 bsres i && (N.of_nat (Datatypes.length bs1) =? n)%N ); simpl; intros Heq8; try (now apply C.interp_true). @@ -7492,7 +7492,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. easy. } specialize (@H0 H1). rewrite Heq6 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. @@ -7722,7 +7722,7 @@ Proof. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | | | | ] a1' Heq6; try (intros; now apply C.interp_true). (* BVsextend *) - - case_eq ((a1 == a1')); simpl; intros Heq7; try (now apply C.interp_true). + - case_eq ((a1 =? a1')); simpl; intros Heq7; try (now apply C.interp_true). case_eq ( check_sextend bs1 bsres i && (N.of_nat (Datatypes.length bs1) =? n)%N ); simpl; intros Heq8; try (now apply C.interp_true). @@ -7738,7 +7738,7 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. easy. } specialize (@H0 H1). rewrite Heq6 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. @@ -8045,7 +8045,7 @@ Proof. case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2. case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc. (* BVshl *) - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true). + case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_shl bs1 bv2 bsres && (N.of_nat (Datatypes.length bs1) =? n)%N && (N.of_nat (Datatypes.length bv2) =? n)%N && (n0 =? n)%N @@ -8062,13 +8062,13 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. pose proof (H a2). - assert (a2 < PArray.length t_atom). + assert (a2 <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heqa2, Heqc. easy. } specialize (@H4 H5). rewrite Heqa2 in H4. simpl in H4. @@ -8375,7 +8375,7 @@ Proof. case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2. case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc. (* BVshr *) - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true). + case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_shr bs1 bv2 bsres && (N.of_nat (Datatypes.length bs1) =? n)%N && (N.of_nat (Datatypes.length bv2) =? n)%N && (n0 =? n)%N @@ -8392,13 +8392,13 @@ Proof. rewrite aforallbi_spec;intros. pose proof (H a). - assert (a < PArray.length t_atom). + assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. pose proof (H a2). - assert (a2 < PArray.length t_atom). + assert (a2 <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heqa2, Heqc. easy. } specialize (@H4 H5). rewrite Heqa2 in H4. simpl in H4. |