Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10

5 files changed, 47 insertions, 244 deletions

diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 1df1ab7..148d6d7 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -783,7 +783,6 @@ Module Atom.
    | BO_BVor (_: N)
    | BO_BVxor (_: N)
    | BO_BVadd (_: N)
-   | BO_BVsubst (_: N)
    | BO_BVmult (_: N)
    | BO_BVult (_: N)
    | BO_BVslt (_: N)
@@ -852,7 +851,6 @@ Module Atom.
    | BO_BVor s1, BO_BVor s2
    | BO_BVxor s1, BO_BVxor s2
    | BO_BVadd s1, BO_BVadd s2
-   | BO_BVsubst s1, BO_BVsubst s2
    | BO_BVmult s1, BO_BVmult s2 => N.eqb s1 s2
    | BO_BVult s1, BO_BVult s2 => N.eqb s1 s2
    | BO_BVslt s1, BO_BVslt s2 => N.eqb s1 s2
@@ -952,8 +950,8 @@ Module Atom.
 
   Lemma reflect_bop_eqb : forall o1 o2, reflect (o1 = o2) (bop_eqb o1 o2).
   Proof.
-    intros [ | | | | | | | A1|s1|s1 |s1 | s1 | s1 | s1 | s1 | s1 | s1 | s1 | s1 | I1 E1 | I1 E1 ]
-           [ | | | | | | | A2|s2|s2| s2 | s2 | s2 | s2 | s2 | s2 | s2 | s2 | s2 |I2 E2 | I2 E2 ];
+    intros [ | | | | | | | A1|s1|s1 |s1 | s1 | s1 | s1 | s1 | s1 | s1 | s1 | I1 E1 | I1 E1 ]
+           [ | | | | | | | A2|s2|s2| s2 | s2 | s2 | s2 | s2 | s2 | s2 | s2 |I2 E2 | I2 E2 ];
       simpl;try (constructor;trivial;discriminate).
    - preflect (Typ.reflect_eqb A1 A2).
      constructor;subst;trivial.
@@ -971,8 +969,6 @@ Module Atom.
      constructor;subst;trivial.
    - preflect (N.eqb_spec s1 s2).
      constructor;subst;trivial.
-   - preflect (N.eqb_spec s1 s2).
-     constructor;subst;trivial.
    - intros.
      preflect (N.eqb_spec s1 s2).
      preflect (N.eqb_spec n n0).
@@ -1116,7 +1112,6 @@ Qed.
         | BO_BVor s   => ((Typ.TBV s,Typ.TBV s), Typ.TBV s)
         | BO_BVxor s   => ((Typ.TBV s,Typ.TBV s), Typ.TBV s)
         | BO_BVadd s   => ((Typ.TBV s,Typ.TBV s), Typ.TBV s)
-        | BO_BVsubst s   => ((Typ.TBV s,Typ.TBV s), Typ.TBV s)
         | BO_BVmult s   => ((Typ.TBV s,Typ.TBV s), Typ.TBV s)
         | BO_BVult s   => ((Typ.TBV s,Typ.TBV s), Typ.Tbool)
         | BO_BVconcat s1 s2   => ((Typ.TBV s1,Typ.TBV s2), (Typ.TBV (s1 + s2)))
@@ -1369,12 +1364,6 @@ Qed.
           right. intros. rewrite andb_false_r. easy.
           right. intros. rewrite andb_false_r. easy.
           right. intros. rewrite andb_false_r. easy.
-        (*additional case for BO_BVsubst*)
-        (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)).
-          left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy.
-          right. intros. rewrite andb_false_r. easy.
-          right. intros. rewrite andb_false_r. easy.
-          right. intros. rewrite andb_false_r. easy.
         (*additional case for BO_BVmult*)
         (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)).
           left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy.
@@ -1544,8 +1533,6 @@ Qed.
            apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_xor s)
          | BO_BVadd s =>
            apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_add s)
-         | BO_BVsubst s =>
-           apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_subt s)
          | BO_BVmult s =>
            apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_mult s)
          | BO_BVult s =>
@@ -1788,7 +1775,7 @@ Qed.
         rewrite Hb. intros.
         exists (@BITVECTOR_LIST.bv_sextn n n0 y); auto. rewrite Typ.cast_refl; auto.
   (* Binary operators *)
-        destruct op as [ | | | | | | | A |s1|s2| s3 | s4 | s5 | s6 | s7 | s8 | s9 | s10 | n m | ti te | ti te];
+        destruct op as [ | | | | | | | A |s1|s2| s3 | s4 | s6 | s7 | s8 | s9 | s10 | n m | ti te | ti te];
           [ intros [ ti' te' | i | | | |s ] |
             intros [ ti' te' | i | | | |s ] |
             intros [ ti' te' | i | | | |s ] |
@@ -1806,7 +1793,6 @@ Qed.
             intros [ ti' te' | i | | | |s ] |
             intros [ ti' te' | i | | | |s ] |
             intros [ ti' te' | i | | | |s ] |
-            intros [ ti' te' | i | | | |s ] |
             intros [ ti' te' | i | | | |s ] | |
             ];
         simpl; try discriminate; unfold is_true;
@@ -1895,20 +1881,6 @@ Qed.
         rewrite Hb, Hc. intros y1 Hy1 y2 Hy2.
         rewrite Typ.cast_refl.
         exists (BITVECTOR_LIST.bv_add y1 y2); auto.
-        (*BO_BVsubt*)
-        simpl in s.
-        intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc).
-        apply Typ.eqb_spec in Hb.
-        apply Typ.eqb_spec in Hc.
-        rewrite N.eqb_eq in Ha.
-        revert Hb Hc. rewrite Ha in *. intros.
-
-        destruct (check_aux_interp_hatom h1) as [x1 Hx1].
-        rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl.
-        revert x1 Hx1 x2 Hx2.
-        rewrite Hb, Hc. intros y1 Hy1 y2 Hy2.
-        rewrite Typ.cast_refl.
-        exists (BITVECTOR_LIST.bv_subt y1 y2); auto.
         (*BO_BVmult*)
         simpl in s.
         intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc).
@@ -2156,15 +2128,6 @@ Qed.
           apply Typ.cast_diff in H. now rewrite H.
           apply Typ.cast_diff in H. rewrite H.
           case (Typ.cast (get_type h1) (Typ.TBV n)); auto.
-        (*BVsubt*)
-        specialize (H (Typ.TBV n)). simpl in H.
-        apply andb_false_iff in H. destruct H.
-        specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros.
-        rewrite andb_false_iff in H. destruct H as [ H | H ].
-          rewrite N.eqb_refl in H. now contradict H.
-          apply Typ.cast_diff in H. now rewrite H.
-          apply Typ.cast_diff in H. rewrite H.
-          case (Typ.cast (get_type h1) (Typ.TBV n)); auto.
         (*BVmult*)
         specialize (H (Typ.TBV n)). simpl in H.
         apply andb_false_iff in H. destruct H.
@@ -2448,7 +2411,7 @@ Qed.
         simpl; [ | exists true; auto]. intro k. exists (BITVECTOR_LIST.bv_sextn i0 (k interp_t x)) ; auto.
 
        (* Binary operators *)
-        intros [ | | | | | | |A | | | | | | | | | | | | ti te| ti te] h1 h2; simpl; rewrite andb_true_iff; intros [H1 H2]; destruct (IH h1 H1) as [x Hx]; destruct (IH h2 H2) as [y Hy]; rewrite Hx, Hy; simpl.
+        intros [ | | | | | | |A | | | | | | | | | | | ti te| ti te] h1 h2; simpl; rewrite andb_true_iff; intros [H1 H2]; destruct (IH h1 H1) as [x Hx]; destruct (IH h2 H2) as [y Hy]; rewrite Hx, Hy; simpl.
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x + k2 interp_t y)%Z; auto.
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x - k2 interp_t y)%Z; auto.
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x * k2 interp_t y)%Z; auto.
@@ -2478,10 +2441,6 @@ Qed.
         intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TBV n)) as [k2| ];
         simpl; try (exists true; reflexivity); exists (BITVECTOR_LIST.bv_add (k1 interp_t x) (k2 interp_t y));
         auto.
-        (*BO_BVsubst*)
-        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) (Typ.TBV n)); simpl; try (exists true; auto);
-        intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TBV n)) as [k2| ];
-        simpl; try (exists true; reflexivity); exists (BITVECTOR_LIST.bv_subt (k1 interp_t x) (k2 interp_t y)); auto.
         (*BO_BVmult*)
         case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) (Typ.TBV n)); simpl; try (exists true; auto);
         intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TBV n)) as [k2| ];
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index 0540855..da0f6f2 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -206,9 +206,9 @@ Section certif.
       case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
       intros a Heq2.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq3; try (intros; now apply C.interp_true).
+      intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq3; try (intros; now apply C.interp_true).
       case_eq (t_atom .[ a1]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq4; try (intros; now apply C.interp_true).
+      intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq4; try (intros; now apply C.interp_true).
       case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true).
       intros [ ] c1 c2 c3 Heq5.
       (* roweq *)
@@ -415,13 +415,13 @@ Section certif.
         case_eq (t_form .[ Lit.blit j]); try (intros; now apply C.interp_true).
         intros b Heq4.
         case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq5; try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq5; try (intros; now apply C.interp_true).
         case_eq (t_atom .[ b]); try (intros; now apply C.interp_true).
-        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq6; try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq6; try (intros; now apply C.interp_true).
         case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true).
-        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq7; try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq7; try (intros; now apply C.interp_true).
         case_eq (t_atom .[ b2]); try (intros; now apply C.interp_true).
-        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq8; try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq8; try (intros; now apply C.interp_true).
         case_eq (Typ.eqb t t1 && Typ.eqb t t3 && Typ.eqb t0 t2 && Typ.eqb t0 t4); 
           try (intros; now apply C.interp_true). intros Heq9.
 
@@ -906,18 +906,18 @@ Section certif.
     case_eq (t_form .[ Lit.blit (a .[1])]); try (intros; now apply C.interp_true).
     intros c Heq6.
     case_eq (t_atom .[ b]); try (intros; now apply C.interp_true).
-    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq7; try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq7; try (intros; now apply C.interp_true).
     case_eq t; try (intros; now apply C.interp_true). intros t0 t1 Heq8.
     case_eq (t_atom .[ c]); try (intros; now apply C.interp_true).
-    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq9; try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq9; try (intros; now apply C.interp_true).
     case_eq (Typ.eqb t1 t2); [ intros Heq10 | intros Heq10; now apply C.interp_true].
     case_eq (t_atom .[ c1]); try (intros; now apply C.interp_true).
-    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq11; try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq11; try (intros; now apply C.interp_true).
     case_eq (t_atom .[ c2]); try (intros; now apply C.interp_true).
-    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] e1 e2 Heq12; try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] e1 e2 Heq12; try (intros; now apply C.interp_true).
     case_eq (t_atom .[ d2]);
       try (intros; rewrite !andb_false_r; simpl; now apply C.interp_true).
-    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] f1 f2 Heq14;
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] f1 f2 Heq14;
       try (intros; rewrite !andb_false_r; simpl; now apply C.interp_true).
     case_eq (Typ.eqb t0 t3 && Typ.eqb t0 t5 && Typ.eqb t1 t4 && Typ.eqb t1 t6);
       [ intros Heq13'| intro; now apply C.interp_true].
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index c9db26b..868cf7b 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -53,28 +53,29 @@ Module Type BITVECTOR.
   (*equality*)
   Parameter bv_eq     : forall n, bitvector n -> bitvector n -> bool.
 
+  (*unary operations*)
+  Parameter bv_not    : forall n,     bitvector n -> bitvector n.
+  Parameter bv_neg    : forall n,     bitvector n -> bitvector n.
+  Parameter bv_extr   : forall (i n0 n1 : N), bitvector n1 -> bitvector n0.
+
   (*binary operations*)
   Parameter bv_concat : forall n m, bitvector n -> bitvector m -> bitvector (n + m).
   Parameter bv_and    : forall n, bitvector n -> bitvector n -> bitvector n.
   Parameter bv_or     : forall n, bitvector n -> bitvector n -> bitvector n.
   Parameter bv_xor    : forall n, bitvector n -> bitvector n -> bitvector n.
   Parameter bv_add    : forall n, bitvector n -> bitvector n -> bitvector n.
-  Parameter bv_subt   : forall n, bitvector n -> bitvector n -> bitvector n.
   Parameter bv_mult   : forall n, bitvector n -> bitvector n -> bitvector n.
   Parameter bv_ult    : forall n, bitvector n -> bitvector n -> bool.
   Parameter bv_slt    : forall n, bitvector n -> bitvector n -> bool.
 
+  Notation bv_subt bv1 bv2 := (bv_add bv1 (bv_neg bv2)).
+
   Parameter bv_ultP   : forall n, bitvector n -> bitvector n -> Prop.
   Parameter bv_sltP   : forall n, bitvector n -> bitvector n -> Prop.
 
   Parameter bv_shl    : forall n, bitvector n -> bitvector n -> bitvector n.
   Parameter bv_shr    : forall n, bitvector n -> bitvector n -> bitvector n.
 
-    (*unary operations*)
-  Parameter bv_not    : forall n,     bitvector n -> bitvector n.
-  Parameter bv_neg    : forall n,     bitvector n -> bitvector n.
-  Parameter bv_extr   : forall (i n0 n1 : N), bitvector n1 -> bitvector n0.
-
  (* Parameter bv_extr   : forall (n i j : N) {H0: n >= j} {H1: j >= i}, bitvector n -> bitvector (j - i). *)
 
   Parameter bv_zextn  : forall (n i: N), bitvector n -> bitvector (i + n).
@@ -122,6 +123,11 @@ Parameter zeros      : N -> bitvector.
 (*equality*)
 Parameter bv_eq      : bitvector -> bitvector -> bool.
 
+(*unary operations*)
+Parameter bv_not     : bitvector -> bitvector.
+Parameter bv_neg     : bitvector -> bitvector.
+Parameter bv_extr    : forall (i n0 n1: N), bitvector -> bitvector.
+
 (*binary operations*)
 Parameter bv_concat  : bitvector -> bitvector -> bitvector.
 Parameter bv_and     : bitvector -> bitvector -> bitvector.
@@ -129,7 +135,6 @@ Parameter bv_or      : bitvector -> bitvector -> bitvector.
 Parameter bv_xor     : bitvector -> bitvector -> bitvector.
 Parameter bv_add     : bitvector -> bitvector -> bitvector.
 Parameter bv_mult    : bitvector -> bitvector -> bitvector.
-Parameter bv_subt    : bitvector -> bitvector -> bitvector.
 Parameter bv_ult     : bitvector -> bitvector -> bool.
 Parameter bv_slt     : bitvector -> bitvector -> bool.
 
@@ -139,11 +144,6 @@ Parameter bv_sltP    : bitvector -> bitvector -> Prop.
 Parameter bv_shl     : bitvector -> bitvector -> bitvector.
 Parameter bv_shr     : bitvector -> bitvector -> bitvector.
 
-(*unary operations*)
-Parameter bv_not     : bitvector -> bitvector.
-Parameter bv_neg     : bitvector -> bitvector.
-Parameter bv_extr    : forall (i n0 n1: N), bitvector -> bitvector.
-
 (*Parameter bv_extr    : forall (n i j: N) {H0: n >= j} {H1: j >= i}, bitvector -> bitvector.*)
 
 Parameter bv_zextn   : forall (n i: N), bitvector -> bitvector.
@@ -160,7 +160,6 @@ Axiom bv_and_size    : forall n a b, size a = n -> size b = n -> size (bv_and a
 Axiom bv_or_size     : forall n a b, size a = n -> size b = n -> size (bv_or a b) = n.
 Axiom bv_xor_size    : forall n a b, size a = n -> size b = n -> size (bv_xor a b) = n.
 Axiom bv_add_size    : forall n a b, size a = n -> size b = n -> size (bv_add a b) = n.
-Axiom bv_subt_size   : forall n a b, size a = n -> size b = n -> size (bv_subt a b) = n.
 Axiom bv_mult_size   : forall n a b, size a = n -> size b = n -> size (bv_mult a b) = n.
 Axiom bv_not_size    : forall n a, size a = n -> size (bv_not a) = n.
 Axiom bv_neg_size    : forall n a, size a = n -> size (bv_neg a) = n.
@@ -238,6 +237,12 @@ Module RAW2BITVECTOR (M:RAWBITVECTOR) <: BITVECTOR.
 
   Definition bv_eq n (bv1 bv2:bitvector n) := M.bv_eq bv1 bv2.
 
+  Definition bv_not n (bv1: bitvector n) : bitvector n :=
+    @MkBitvector n (M.bv_not bv1) (M.bv_not_size (wf bv1)).
+
+  Definition bv_neg n (bv1: bitvector n) : bitvector n :=
+    @MkBitvector n (M.bv_neg bv1) (M.bv_neg_size (wf bv1)).
+
   Definition bv_ultP n (bv1 bv2:bitvector n) := M.bv_ultP bv1 bv2.
 
   Definition bv_sltP n (bv1 bv2:bitvector n) := M.bv_sltP bv1 bv2.
@@ -251,8 +256,7 @@ Module RAW2BITVECTOR (M:RAWBITVECTOR) <: BITVECTOR.
   Definition bv_add n (bv1 bv2:bitvector n) : bitvector n :=
     @MkBitvector n (M.bv_add bv1 bv2) (M.bv_add_size (wf bv1) (wf bv2)).
 
-  Definition bv_subt n (bv1 bv2:bitvector n) : bitvector n :=
-    @MkBitvector n (M.bv_subt bv1 bv2) (M.bv_subt_size (wf bv1) (wf bv2)).
+  Notation bv_subt bv1 bv2 := (bv_add bv1 (bv_neg bv2)).
 
   Definition bv_mult n (bv1 bv2:bitvector n) : bitvector n :=
     @MkBitvector n (M.bv_mult bv1 bv2) (M.bv_mult_size (wf bv1) (wf bv2)).
@@ -264,12 +268,6 @@ Module RAW2BITVECTOR (M:RAWBITVECTOR) <: BITVECTOR.
 
   Definition bv_slt n (bv1 bv2:bitvector n) : bool := M.bv_slt bv1 bv2.
 
-  Definition bv_not n (bv1: bitvector n) : bitvector n :=
-    @MkBitvector n (M.bv_not bv1) (M.bv_not_size (wf bv1)).
-
-  Definition bv_neg n (bv1: bitvector n) : bitvector n :=
-    @MkBitvector n (M.bv_neg bv1) (M.bv_neg_size (wf bv1)).
-
   Definition bv_concat n m (bv1:bitvector n) (bv2: bitvector m) : bitvector (n + m) :=
     @MkBitvector (n + m) (M.bv_concat bv1 bv2) (M.bv_concat_size (wf bv1) (wf bv2)).
 
@@ -575,42 +573,6 @@ Definition twos_complement b :=
   
 Definition bv_neg (a: bitvector) : bitvector := (twos_complement a).
 
-Definition subst_list' a b := add_list a (twos_complement b).
-
-Definition bv_subt' (a b : bitvector) : bitvector :=
-   match (@size a) =? (@size b) with
-     | true => (subst_list' (@bits a) (@bits b))
-     | _    => nil
-   end.
-
-Definition subst_borrow b1 b2 b :=
-  match b1, b2, b with
-    | true,  true,  true  => (true, true)
-    | true,  true,  false => (false, false)
-    | true,  false, true  => (false, false)
-    | false, true,  true  => (false, true)
-    | false, false, true  => (true, true)
-    | false, true,  false => (true, true)
-    | true,  false, false => (true, false)
-    | false, false, false => (false, false)
-  end.
-
-Fixpoint subst_list_borrow bs1 bs2 b {struct bs1} :=
-  match bs1, bs2 with
-    | nil, _               => nil
-    | _ , nil              => nil
-    | b1 :: bs1, b2 :: bs2 =>
-      let (r, b) := subst_borrow b1 b2 b in r :: (subst_list_borrow bs1 bs2 b)
-  end.
-
-Definition subst_list (a b: list bool) := subst_list_borrow a b false.
-
-Definition bv_subt (a b : bitvector) : bitvector :=
-  match (@size a) =? (@size b) with 
-    | true => subst_list (@bits a) (@bits b)
-    | _    => nil 
-  end.
-  
 (*less than*)
 
 Fixpoint ult_list_big_endian (x y: list bool) :=
@@ -1735,33 +1697,6 @@ Qed.
 
 (* bitwise SUBST properties *)
 
-Lemma subst_list_empty_empty_l: forall a, (subst_list [] a) = [].
-Proof. intro a. unfold subst_list; auto. Qed.
-
-Lemma subst_list_empty_empty_r: forall a, (subst_list a []) = [].
-Proof. intro a.
-       induction a as [ | a xs IHxs].
-       - auto.
-       - unfold subst_list; auto. 
-Qed.
-
-Lemma subst_list'_empty_empty_r: forall a, (subst_list' a []) = [].
-Proof. intro a.
-       induction a as [ | a xs IHxs].
-       - auto.
-       - unfold subst_list' in *. unfold twos_complement. simpl. reflexivity.
-Qed.
-
-Lemma subst_list_borrow_length: forall (a b: list bool) c, length a = length b -> length a = length (subst_list_borrow a b c). 
-Proof. induction a as [ | a' xs IHxs]. 
-       simpl. auto. 
-       intros [ | b ys].
-       - simpl. intros. exact H. 
-       - intros. simpl in *. 
-         case_eq (subst_borrow a' b c); intros r c0 Heq. simpl. apply f_equal. 
-         specialize (@IHxs ys). apply IHxs. inversion H; reflexivity. 
-Qed.
-
 Lemma length_twos_complement: forall (a: list bool), length a = length (twos_complement a).
 Proof. intro a.
       induction a as [ | a' xs IHxs].
@@ -1771,30 +1706,6 @@ Proof. intro a.
         rewrite length_mk_list_false. rewrite <- not_list_length. reflexivity.
 Qed.
 
-Lemma subst_list_length: forall (a b: list bool), length a = length b -> length a = length (subst_list a b). 
-Proof. intros a b H. unfold subst_list. apply (@subst_list_borrow_length a b false). exact H. Qed.
-
-Lemma subst_list'_length: forall (a b: list bool), length a = length b -> length a = length (subst_list' a b).
-Proof. intros a b H. unfold subst_list'.
-       rewrite <- (@length_add_list_eq a (twos_complement b)).
-       - reflexivity.
-       - rewrite <- (@length_twos_complement b). exact H.
-Qed.
-
-Lemma subst_list_borrow_empty_neutral: forall (a: list bool), (subst_list_borrow a (mk_list_false (length a)) false) = a.
-Proof. intro a. induction a as [ | a' xs IHxs].
-       - simpl. reflexivity.
-       - simpl.
-         cut(subst_borrow a' false false = (a', false)).
-         + intro H. rewrite H. rewrite IHxs. reflexivity.
-         + unfold subst_borrow. case a'; auto.
-Qed.
-
-Lemma subst_list_empty_neutral: forall (a: list bool), (subst_list a (mk_list_false (length a))) = a.
-Proof. intros a. unfold subst_list.
-       apply (@subst_list_borrow_empty_neutral a).
-Qed.
-
 Lemma twos_complement_cons_false: forall a, false :: twos_complement a = twos_complement (false :: a).
 Proof. intro a.
        induction a as [ | a xs IHxs]; unfold twos_complement; simpl; reflexivity.
@@ -1808,12 +1719,6 @@ Proof. intro n.
          apply f_equal. exact IHn.
 Qed.
 
-Lemma subst_list'_empty_neutral: forall (a: list bool), (subst_list' a (mk_list_false (length a))) = a.
-Proof. intros a. unfold subst_list'.
-       rewrite (@twos_complement_false_false (length a)).
-       rewrite add_list_empty_neutral_r. reflexivity.
-Qed.
-
 (* some list ult and slt properties *)
 
 Lemma ult_list_big_endian_trans : forall x y z,
@@ -2117,36 +2022,6 @@ Proof. intros.
   now apply rev_neq in H1.
 Qed.
 
-(* bitvector SUBT properties *)
-
-Lemma bv_subt_size: forall n a b, size a = n -> size b = n -> size (bv_subt a b) = n.
-Proof. intros n a b H0 H1.
-       unfold bv_subt, size, bits in *. rewrite H0, H1. rewrite N.eqb_compare.
-       rewrite N.compare_refl. rewrite <- subst_list_length. exact H0.
-       now rewrite <- Nat2N.inj_iff, H0.
-Qed.
-
-Lemma bv_subt_empty_neutral_r: forall a, (bv_subt a (mk_list_false (length (bits a)))) = a.
-Proof. intro a. unfold bv_subt, size, bits.
-       rewrite N.eqb_compare. rewrite length_mk_list_false.
-       rewrite N.compare_refl.
-       rewrite subst_list_empty_neutral. reflexivity.
-Qed.
-
-Lemma bv_subt'_size: forall n a b, (size a) = n -> (size b) = n -> size (bv_subt' a b) = n.
-Proof. intros n a b H0 H1. unfold bv_subt', size, bits in *.
-       rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
-       rewrite <- subst_list'_length. exact H0.
-       now rewrite <- Nat2N.inj_iff, H0.
-Qed.
-
-Lemma bv_subt'_empty_neutral_r: forall a, (bv_subt' a (mk_list_false (length (bits a)))) = a.
-Proof. intro a. unfold bv_subt', size, bits.
-       rewrite N.eqb_compare. rewrite length_mk_list_false.
-       rewrite N.compare_refl.
-       rewrite subst_list'_empty_neutral. reflexivity.
-Qed.
-
 (* bitwise ADD-NEG properties *)
 
 Lemma add_neg_list_carry_false: forall a b c, add_list_ingr a (add_list_ingr b c true) false = add_list_ingr a (add_list_ingr b c false) true.
@@ -2220,37 +2095,6 @@ Proof. intro a. unfold bv_add, bv_not, size, bits. rewrite not_list_length.
        rewrite Nat2N.id, not_list_length. reflexivity.
 Qed. 
 
-
-(* bitwise ADD-SUBST properties *)
-
-Lemma add_subst_list_carry_opp: forall n a b, (length a) = n -> (length b) = n -> (add_list_ingr (subst_list' a b) b false) = a.
-Proof. intros n a b H0 H1.
-       unfold subst_list', twos_complement, add_list.
-       rewrite add_neg_list_carry_false. rewrite not_list_length at 1.
-       rewrite add_list_carry_empty_neutral_r.
-       specialize (@add_list_carry_assoc a (map negb b) b true false false true).
-       intro H2. rewrite H2; try auto. rewrite add_neg_list_carry_neg_f_r.
-       rewrite H1. rewrite <- H0. rewrite add_list_carry_unit_t; reflexivity.
-Qed.
-
-Lemma add_subst_opp:  forall n a b, (length a) = n -> (length b) = n -> (add_list (subst_list' a b) b) = a.
-Proof. intros n a b H0 H1. unfold add_list, size, bits.
-       apply (@add_subst_list_carry_opp n a b); easy.
-Qed.
-
-(* bitvector ADD-SUBT properties *)
-
-Lemma bv_add_subst_opp:  forall n a b, (size a) = n -> (size b) = n -> (bv_add (bv_subt' a b) b) = a.
-Proof. intros n a b H0 H1. unfold bv_add, bv_subt', add_list, size, bits in *.
-       rewrite H0, H1.
-       rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl.
-       rewrite <- (@subst_list'_length a b). rewrite H0.
-       rewrite N.compare_refl. rewrite (@add_subst_list_carry_opp (nat_of_N n) a b); auto;
-       inversion H0; rewrite Nat2N.id; auto.
-       symmetry. now rewrite <- Nat2N.inj_iff, H0.
-        now rewrite <- Nat2N.inj_iff, H0.
-Qed.
-
  (* bitvector MULT properties *) 
 
 Lemma prop_mult_bool_step_k_h_len: forall a b c k,
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index c0fb520..e7acfa7 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -1186,7 +1186,7 @@ Proof.
         intros f Heq2.
       case_eq (t_atom .[ f]); try (intros; now apply C.interp_true).
 
-      intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N|N| | | | ];
+      intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N| | | | ];
          try (intros; now apply C.interp_true). intros a b Heq3.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
       intros c Heq4.
@@ -3215,7 +3215,7 @@ Proof.
       case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
       intros a bsres Heq8.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9;
+      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'));
@@ -4513,7 +4513,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres).
        case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10.
        case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true).
 
-       intros [ | | | | | | | [ A B | A | | | |n]|N|N|N|N|N|N|N|N|N| | | | ]; 
+       intros [ | | | | | | | [ A B | A | | | |n]|N|N|N|N|N|N|N|N| | | | ]; 
           try (intros; now apply C.interp_true).
 
        intros a1' a2' Heq9.
@@ -5168,7 +5168,7 @@ Proof.
        case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10.
        case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true).
 
-       intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ]; 
+       intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ]; 
          try (intros; now apply C.interp_true).
 
        intros a1' a2' Heq9.
@@ -5394,7 +5394,7 @@ Proof.
        case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10.
        case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true).
 
-       intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; 
+       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).
@@ -5805,7 +5805,7 @@ Proof.
       case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
       intros a bsres Heq8.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9;
+      intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9;
         try (intros; now apply C.interp_true).
 
       (* BVadd *)
@@ -6603,7 +6603,7 @@ Proof.
       case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
       intros a bsres Heq8.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; 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')*) );
             simpl; intros Heq10; try (now apply C.interp_true).
@@ -6911,7 +6911,7 @@ Proof.
       case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
       intros a bsres Heq8.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ]  a1' a2' Heq9; 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 (
@@ -8055,7 +8055,7 @@ Proof.
       case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
       intros a bsres Heq8.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ]  a1' a2' Heq9; 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).
        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 *)
@@ -8385,7 +8385,7 @@ Proof.
       case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
       intros a bsres Heq8.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ]  a1' a2' Heq9; 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).
        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 *)
diff --git a/src/spl/Operators.v b/src/spl/Operators.v
index fb3e379..1bdf8e7 100644
--- a/src/spl/Operators.v
+++ b/src/spl/Operators.v
@@ -169,10 +169,10 @@ Section Operators.
      PArray.forallb_spec, check_diseqs_complete_spec, length_mapi; split; intros [H1 H2]; split.
     clear H2; intros i Hi; generalize (H1 _ Hi); rewrite get_mapi; 
     auto; case_eq (Lit.is_pos (diseq .[ i])); try discriminate; intro Heq1; case_eq (get_form (Lit.blit (diseq .[ i]))); 
-    try discriminate; intros a Heq2; case_eq (get_atom a); try discriminate; intros [ | | | | | | | B | | | | | | | | | | | | | ]; try discriminate; intros h1 h2 Heq3; case_eq (Typ.eqb A B); try discriminate; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try discriminate; rewrite eqb_false_spec; intro H2; case_eq (check_in h1 dist); try discriminate; case_eq (check_in h2 dist); try discriminate; rewrite !check_in_spec; intros H3 H4 _; split; try discriminate; exists a; split; auto; exists h1, h2; repeat split; auto; rewrite <- In2_In; auto.
+    try discriminate; intros a Heq2; case_eq (get_atom a); try discriminate; intros [ | | | | | | | B | | | | | | | | | | | | ]; try discriminate; intros h1 h2 Heq3; case_eq (Typ.eqb A B); try discriminate; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try discriminate; rewrite eqb_false_spec; intro H2; case_eq (check_in h1 dist); try discriminate; case_eq (check_in h2 dist); try discriminate; rewrite !check_in_spec; intros H3 H4 _; split; try discriminate; exists a; split; auto; exists h1, h2; repeat split; auto; rewrite <- In2_In; auto.
     clear H1; intros x y Hxy; destruct (H2 _ _ Hxy) as [i [H1 H4]]; clear H2; rewrite get_mapi in H4; auto; exists i; split; auto; generalize H4; 
     
-    case_eq (Lit.is_pos (diseq .[ i])); intro Heq; try (intros [H|H]; discriminate); case_eq (get_form (Lit.blit (diseq .[ i]))); [intros a| | |intros a1 a2|intros a1|intros a1|intros a1|intros a1 a2|intros a1 a2| intros a1 a2 a3|intros a ls]; intro Heq2; try (intros [H|H]; discriminate); case_eq (get_atom a); [intros a1|intros a1 a2|intros [ | | | | | | | B | | | | | | | | | | | | | ] h1 h2|intros a1 a2|intros a1 a2 | intros a1 a2]; intro Heq3; try (intros [H|H]; discriminate); try (case_eq (Typ.eqb A B); try (intros _ [H|H]; discriminate); change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try (intros _ [H|H]; discriminate); rewrite eqb_false_spec; intro H10; case (check_in h1 dist); try (intros [H|H]; discriminate); case (check_in h2 dist); try (intros [H|H]; discriminate); simpl; intro H3; split; try discriminate; exists a; split; auto; destruct H3 as [H3|H3]; inversion H3; subst; auto).
+    case_eq (Lit.is_pos (diseq .[ i])); intro Heq; try (intros [H|H]; discriminate); case_eq (get_form (Lit.blit (diseq .[ i]))); [intros a| | |intros a1 a2|intros a1|intros a1|intros a1|intros a1 a2|intros a1 a2| intros a1 a2 a3|intros a ls]; intro Heq2; try (intros [H|H]; discriminate); case_eq (get_atom a); [intros a1|intros a1 a2|intros [ | | | | | | | B | | | | | | | | | | | | ] h1 h2|intros a1 a2|intros a1 a2 | intros a1 a2]; intro Heq3; try (intros [H|H]; discriminate); try (case_eq (Typ.eqb A B); try (intros _ [H|H]; discriminate); change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try (intros _ [H|H]; discriminate); rewrite eqb_false_spec; intro H10; case (check_in h1 dist); try (intros [H|H]; discriminate); case (check_in h2 dist); try (intros [H|H]; discriminate); simpl; intro H3; split; try discriminate; exists a; split; auto; destruct H3 as [H3|H3]; inversion H3; subst; auto).
 intros. destruct H0; now contradict H0.
     
     clear H2; intros i Hi; rewrite get_mapi; auto; destruct (H1 _ Hi) as [H2 [a [H3 [h1 [h2 [H4 [H5 H6]]]]]]]; clear H1; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); rewrite H3, H4, Typ.eqb_refl; simpl; replace (h1 == h2) with false by (case_eq (h1 == h2); auto; rewrite eqb_spec; intro H; elim H5; auto); simpl; rewrite <- In2_In, <- !check_in_spec in H6; auto; destruct H6 as [H6 H7]; rewrite H6, H7; auto.
@@ -247,7 +247,7 @@ intros. destruct H0; now contradict H0.
        get_atom hb = Atom.Abop (Atom.BO_eq ty) y x).
   Proof.
     intros f1 f2; unfold check_distinct_two_args; split.
-    case (get_form f1); try discriminate; intro ha; case (get_form f2); try discriminate; intro hb; case_eq (get_atom ha); try discriminate; intros [A] [ |x [ |y [ |l]]] Heq1; try discriminate; case_eq (get_atom hb); try discriminate; intros [ | | | | | | |B | | | | | | | | | | | | | ] x' y' Heq2; try discriminate; rewrite !andb_true_iff, orb_true_iff, !andb_true_iff; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec, !Int63Properties.eqb_spec; intros [H1 [[H2 H3]|[H2 H3]]]; subst B x' y'; exists ha, hb, A, x, y; auto.
+    case (get_form f1); try discriminate; intro ha; case (get_form f2); try discriminate; intro hb; case_eq (get_atom ha); try discriminate; intros [A] [ |x [ |y [ |l]]] Heq1; try discriminate; case_eq (get_atom hb); try discriminate; intros [ | | | | | | |B | | | | | | | | | | | | ] x' y' Heq2; try discriminate; rewrite !andb_true_iff, orb_true_iff, !andb_true_iff; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec, !Int63Properties.eqb_spec; intros [H1 [[H2 H3]|[H2 H3]]]; subst B x' y'; exists ha, hb, A, x, y; auto.
     intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; rewrite H1, H2, H3, H4, Typ.eqb_refl, !eqb_refl; auto; rewrite orb_true_r; auto.
   Qed.