Define substitution conformly to SMT-LIB

1 files changed, 3 insertions, 3 deletions

diff --git a/src/spl/Operators.v b/src/spl/Operators.v
index f0aba15..d9fd40a 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.