From 7ce6bf4f7740de4c69877ec9179520bcaa0d014c Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Fri, 18 Feb 2022 17:10:13 +0100
Subject: Removed deprecated features

---
 src/bva/Bva_checker.v | 302 +++++++++++++++++++++++++-------------------------
 1 file changed, 151 insertions(+), 151 deletions(-)

(limited to 'src/bva/Bva_checker.v')

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.
 
-- 
cgit