From 25f99b87cc2beb20aaa74a3a28a147f3afdf9467 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 28 Jan 2020 14:23:31 +0100 Subject: Hints in databases --- src/Misc.v | 82 +++--- src/SMT_terms.v | 18 +- src/Trace.v | 116 ++++----- src/array/FArray.v | 290 +++++++++++---------- src/bva/BVList.v | 2 + src/bva/Bva_checker.v | 2 +- src/euf/Euf.v | 134 +++++----- src/lia/Lia.v | 208 +++++++-------- src/spl/Arithmetic.v | 4 +- src/spl/Operators.v | 128 +++++---- src/versions/standard/Array/PArray_standard.v | 2 + src/versions/standard/Int63/Int63Native_standard.v | 1 + 12 files changed, 481 insertions(+), 506 deletions(-) diff --git a/src/Misc.v b/src/Misc.v index b675599..952985f 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -763,26 +763,26 @@ Section List2. | In2_hd : forall l, In j l -> In2 i j (i::l) | In2_tl : forall k l, In2 i j l -> In2 i j (k::l). - Local Hint Constructors In2. + Local Hint Constructors In2 : smtcoq_in2. Lemma In2_app : forall i j l m, In2 i j (l ++ m) <-> In2 i j l \/ (In i l /\ In j m) \/ In2 i j m. Proof. - intros i j; induction l as [ |t l IHl]; simpl; intro m; split; auto. - intros [H|[[H _]|H]]; auto. + intros i j; induction l as [ |t l IHl]; simpl; intro m; split; auto with smtcoq_in2. + intros [H|[[H _]|H]]; auto with smtcoq_in2. inversion H. elim H. intro H; inversion H; clear H. - subst i l0; rewrite in_app_iff in H1; destruct H1 as [H1|H1]; auto. - subst k l0; rewrite IHl in H1; destruct H1 as [H1|[[H1 H2]|H1]]; auto. + subst i l0; rewrite in_app_iff in H1; destruct H1 as [H1|H1]; auto with smtcoq_in2. + subst k l0; rewrite IHl in H1; destruct H1 as [H1|[[H1 H2]|H1]]; auto with smtcoq_in2. intros [H|[[[H|H] H1]|H]]. inversion H; clear H. - subst i l0; constructor 1; rewrite in_app_iff; auto. - subst k l0; constructor 2; rewrite IHl; left; auto. - subst t; constructor 1; rewrite in_app_iff; auto. - constructor 2; rewrite IHl; right; left; auto. - constructor 2; rewrite IHl; right; right; auto. + subst i l0; constructor 1; rewrite in_app_iff; auto with smtcoq_in2. + subst k l0; constructor 2; rewrite IHl; left; auto with smtcoq_in2. + subst t; constructor 1; rewrite in_app_iff; auto with smtcoq_in2. + constructor 2; rewrite IHl; right; left; auto with smtcoq_in2. + constructor 2; rewrite IHl; right; right; auto with smtcoq_in2. Qed. @@ -796,17 +796,17 @@ Section List2. Lemma In2_rev_aux : forall i j l acc, In2 i j (rev_aux acc l) <-> In2 i j acc \/ (In i l /\ In j acc) \/ In2 j i l. Proof. - intros i j; induction l as [ |t q IHq]; simpl; intro acc; split; auto. - intros [H|[[H _]|H]]; auto. + intros i j; induction l as [ |t q IHq]; simpl; intro acc; split; auto with smtcoq_in2. + intros [H|[[H _]|H]]; auto with smtcoq_in2. elim H. inversion H. - rewrite IHq; clear IHq; intros [H|[[H1 H2]|H]]; auto. - inversion H; auto. - inversion H2; auto; clear H2; subst t; right; right; auto. - intros [H|[[[H1|H1] H2]|H]]; rewrite IHq; clear IHq; auto. - subst t; auto. - right; left; split; auto; constructor 2; auto. - inversion H; clear H; auto; subst j l; right; left; split; auto; constructor 1; auto. + rewrite IHq; clear IHq; intros [H|[[H1 H2]|H]]; auto with smtcoq_in2. + inversion H; auto with smtcoq_in2. + inversion H2; auto with smtcoq_in2; clear H2; subst t; right; right; auto with smtcoq_in2. + intros [H|[[[H1|H1] H2]|H]]; rewrite IHq; clear IHq; auto with smtcoq_in2. + subst t; auto with smtcoq_in2. + right; left; split; auto with smtcoq_in2; constructor 2; auto with smtcoq_in2. + inversion H; clear H; auto with smtcoq_in2; subst j l; right; left; split; auto with smtcoq_in2; constructor 1; auto with smtcoq_in2. Qed. @@ -815,7 +815,7 @@ Section List2. Lemma In2_rev : forall i j l, In2 i j (rev l) <-> In2 j i l. Proof. - intros i j l; unfold rev; rewrite In2_rev_aux; split; auto; intros [H|[[_ H]|H]]; auto; inversion H. + intros i j l; unfold rev; rewrite In2_rev_aux; split; auto with smtcoq_in2; intros [H|[[_ H]|H]]; auto with smtcoq_in2; inversion H. Qed. @@ -825,15 +825,15 @@ Section List2. intros [H1 H2]; generalize H1 H2; clear H1 H2; induction l as [ |t q IHq]. intro H1; inversion H1. intros H1 H2; inversion H1; clear H1. - subst t; inversion H2; auto; elim H; auto. + subst t; inversion H2; auto with smtcoq_in2; elim H; auto with smtcoq_in2. inversion H2; clear H2. - subst t; auto. - destruct (IHq H0 H1) as [H2|H2]; auto. + subst t; auto with smtcoq_in2. + destruct (IHq H0 H1) as [H2|H2]; auto with smtcoq_in2. intros [H1|H1]; induction H1 as [H1|t q H1 [IH1 IH2]]. - split; [constructor 1|constructor 2]; auto. - split; constructor 2; auto. - split; [constructor 2|constructor 1]; auto. - split; constructor 2; auto. + split; [constructor 1|constructor 2]; auto with smtcoq_in2. + split; constructor 2; auto with smtcoq_in2. + split; [constructor 2|constructor 1]; auto with smtcoq_in2. + split; constructor 2; auto with smtcoq_in2. Qed. End List2. @@ -892,32 +892,32 @@ Section Distinct. distinct_aux acc' q end. - Local Hint Constructors In2. + Local Hint Constructors In2 : smtcoq_in2. Lemma distinct_aux_spec : forall l acc, distinct_aux acc l = true <-> acc = true /\ (forall i j, In2 i j l -> eq i j = false). Proof. induction l as [ |t q IHq]; simpl. intro acc; split. - intro H; split; auto; intros i j H1; inversion H1. - intros [H _]; auto. + intro H; split; auto with smtcoq_in2; intros i j H1; inversion H1. + intros [H _]; auto with smtcoq_in2. intro acc; rewrite (IHq (distinct_aux2 acc t q)), distinct_aux2_spec; split. - intros [[H1 H2] H3]; split; auto; intros i j H; inversion H; auto. - intros [H1 H2]; repeat split; auto. + intros [[H1 H2] H3]; split; auto with smtcoq_in2; intros i j H; inversion H; auto with smtcoq_in2. + intros [H1 H2]; repeat split; auto with smtcoq_in2. Qed. Lemma distinct_aux_spec_neg : forall l acc, distinct_aux acc l = false <-> acc = false \/ (exists i j, In2 i j l /\ eq i j = true). Proof. induction l as [ |t q IHq]; simpl. - intro acc; split; auto; intros [H|[i [j [H _]]]]; auto; inversion H. + intro acc; split; auto with smtcoq_in2; intros [H|[i [j [H _]]]]; auto with smtcoq_in2; inversion H. intro acc; rewrite (IHq (distinct_aux2 acc t q)), distinct_aux2_spec_neg; split. - intros [[H|[i [H1 H2]]]|[i [j [H1 H2]]]]; auto. - right; exists t; exists i; auto. - right; exists i; exists j; auto. - intros [H|[i [j [H1 H2]]]]; auto; inversion H1; clear H1. - subst i l; left; right; exists j; auto. - subst k l; right; exists i; exists j; auto. + intros [[H|[i [H1 H2]]]|[i [j [H1 H2]]]]; auto with smtcoq_in2. + right; exists t; exists i; auto with smtcoq_in2. + right; exists i; exists j; auto with smtcoq_in2. + intros [H|[i [j [H1 H2]]]]; auto with smtcoq_in2; inversion H1; clear H1. + subst i l; left; right; exists j; auto with smtcoq_in2. + subst k l; right; exists i; exists j; auto with smtcoq_in2. Qed. Definition distinct := distinct_aux true. @@ -925,13 +925,13 @@ Section Distinct. Lemma distinct_spec : forall l, distinct l = true <-> (forall i j, In2 i j l -> eq i j = false). Proof. - unfold distinct; intro l; rewrite distinct_aux_spec; split; auto; intros [_ H]; auto. + unfold distinct; intro l; rewrite distinct_aux_spec; split; auto with smtcoq_in2; intros [_ H]; auto with smtcoq_in2. Qed. Lemma distinct_false_spec : forall l, distinct l = false <-> (exists i j, In2 i j l /\ eq i j = true). Proof. - unfold distinct; intro l; rewrite distinct_aux_spec_neg; split; auto; intros [H|H]; auto; discriminate. + unfold distinct; intro l; rewrite distinct_aux_spec_neg; split; auto with smtcoq_in2; intros [H|H]; auto with smtcoq_in2; discriminate. Qed. End Distinct. diff --git a/src/SMT_terms.v b/src/SMT_terms.v index a85804c..1df1ab7 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -18,7 +18,7 @@ Local Open Scope list_scope. Local Open Scope array_scope. Local Open Scope int63_scope. -Hint Unfold is_true. +Hint Unfold is_true : smtcoq_core. (* Remark: I use Notation instead of Definition du eliminate conversion check during the type checking *) @@ -125,11 +125,11 @@ Module Form. destruct h;simpl;intros;trivial; try (apply afold_left_eq;unfold is_true in H0; rewrite PArray.forallb_spec in H0;intros; - auto using Lit.interp_eq_compat). + auto using Lit.interp_eq_compat with smtcoq_core). - f_equal;auto using Lit.interp_eq_compat. - apply afold_right_eq;unfold is_true in H0; rewrite PArray.forallb_spec in H0;intros; - auto using Lit.interp_eq_compat. + auto using Lit.interp_eq_compat with smtcoq_core. - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; rewrite !(Lit.interp_eq_compat f1 f2);auto. - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; @@ -138,7 +138,7 @@ Module Form. rewrite !(Lit.interp_eq_compat f1 f2);auto. - replace (List.map (Lit.interp f2) l) with (List.map (Lit.interp f1) l); auto. unfold is_true in H0. rewrite List.forallb_forall in H0. - apply List_map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto. + apply List_map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto with smtcoq_core. Qed. Definition wf := PArray.forallbi lt_form t_form. @@ -589,11 +589,11 @@ Module Typ. (* TODO : Move this *) Lemma not_false : ~ false. Proof. intro;discriminate. Qed. - Hint Resolve not_false. + Hint Resolve not_false : smtcoq_core. Lemma is_true_true : true. Proof. reflexivity. Qed. - Hint Resolve is_true_true. + Hint Resolve is_true_true : smtcoq_core. Lemma not_is_true_eq_false : forall b:bool, ~ b <-> b = false. Proof. exact not_true_iff_false. Qed. @@ -1231,8 +1231,8 @@ Qed. intros [op|op h|op h1 h2|op ha i i0|f args | i e ]; simpl. (* Constants *) left; destruct op; simpl. - exists Typ.Tpositive; auto. - exists Typ.TZ; auto. + exists Typ.Tpositive; auto with smtcoq_core. + exists Typ.TZ; auto with smtcoq_core. exists (Typ.TBV n); now rewrite N.eqb_refl. (* Unary operators *) destruct op; simpl; @@ -1440,7 +1440,7 @@ Qed. right. intros. rewrite andb_false_r. easy. (* N-ary operators *) destruct f as [ty]; simpl; case (List.forallb (fun t1 : int => Typ.eqb (get_type t1) ty) args). - left; exists Typ.Tbool; auto. + left; exists Typ.Tbool; auto with smtcoq_core. right; intro T; rewrite andb_false_r; auto. (* Application *) case (v_type Typ.ftype interp_ft (t_func .[ i])); intros; apply check_args_dec. diff --git a/src/Trace.v b/src/Trace.v index e7c7d22..86250a2 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -280,7 +280,7 @@ Module Cnf_Checker. checker_b t_form l b c = true -> Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l = b. Proof. - unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto; rewrite Lit.interp_neg, H1; auto. + unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto with smtcoq_core; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto with smtcoq_core; rewrite Lit.interp_neg, H1; auto with smtcoq_core. Qed. Definition checker_eq t_form l1 l2 l (c:certif) := @@ -297,8 +297,8 @@ Module Cnf_Checker. Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2. Proof. unfold checker_eq; intros t_var t_form l1 l2 l c; rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form). - unfold checker in H3; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) _ H3) as [[Ht1 Ht2] Ht3]; split; auto. - destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2); intro Heq2; auto; elim (checker_correct H3 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto. + unfold checker in H3; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) _ H3) as [[Ht1 Ht2] Ht3]; split; auto with smtcoq_core. + destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2); intro Heq2; auto with smtcoq_core; elim (checker_correct H3 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_core; rewrite Heq; simpl; rewrite Heq1, Heq2; auto with smtcoq_core. Qed. End Cnf_Checker. @@ -433,49 +433,49 @@ Inductive step := |pos orig1 orig2 res|pos orig1 orig2 res |pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res |pos cl |pos orig res |pos orig res |pos orig res | pos orig1 orig2 res | pos orig1 orig2 res |pos res|pos res - |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto. - - apply S.valid_set_resolve; auto. - - apply S.valid_set_weaken; auto. - - apply valid_check_flatten; auto; intros h1 h2 H. - + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto. - + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto. - - apply valid_check_True; auto. - - apply valid_check_False; auto. - - apply valid_check_BuildDef; auto. - - apply valid_check_BuildDef2; auto. - - apply valid_check_BuildProj; auto. - - apply valid_check_ImmBuildDef; auto. - - apply valid_check_ImmBuildDef2; auto. - - apply valid_check_ImmBuildProj; auto. - - apply valid_check_trans; auto. - - apply valid_check_congr; auto. - - apply valid_check_congr_pred; auto. - - apply valid_check_micromega; auto. - - apply valid_check_diseq; auto. - - apply valid_check_spl_arith; auto. - - apply valid_check_distinct_elim; auto. - - eapply valid_check_bbVar; eauto. - - apply valid_check_bbConst; auto. - - apply valid_check_bbOp; auto. - - apply valid_check_bbNot; auto. - - apply valid_check_bbNeg; auto. - - apply valid_check_bbAdd; auto. - - apply valid_check_bbConcat; auto. - - apply valid_check_bbMult; auto. - - apply valid_check_bbUlt; auto. - - apply valid_check_bbSlt; auto. - - apply valid_check_bbEq; auto. - - apply valid_check_bbDiseq; auto. - - apply valid_check_bbExtract; auto. - - apply valid_check_bbZextend; auto. - - apply valid_check_bbSextend; auto. - - apply valid_check_bbShl; auto. - - apply valid_check_bbShr; auto. - - apply valid_check_roweq; auto. - - apply valid_check_rowneq; auto. - - apply valid_check_ext; auto. - - apply valid_check_hole; auto. - - apply valid_check_forall_inst with lemma; auto. + |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto with smtcoq_core. + - apply S.valid_set_resolve; auto with smtcoq_core. + - apply S.valid_set_weaken; auto with smtcoq_core. + - apply valid_check_flatten; auto with smtcoq_core; intros h1 h2 H. + + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto with smtcoq_core. + + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto with smtcoq_core. + - apply valid_check_True; auto with smtcoq_core. + - apply valid_check_False; auto with smtcoq_core. + - apply valid_check_BuildDef; auto with smtcoq_core. + - apply valid_check_BuildDef2; auto with smtcoq_core. + - apply valid_check_BuildProj; auto with smtcoq_core. + - apply valid_check_ImmBuildDef; auto with smtcoq_core. + - apply valid_check_ImmBuildDef2; auto with smtcoq_core. + - apply valid_check_ImmBuildProj; auto with smtcoq_core. + - apply valid_check_trans; auto with smtcoq_core. + - apply valid_check_congr; auto with smtcoq_core. + - apply valid_check_congr_pred; auto with smtcoq_core. + - apply valid_check_micromega; auto with smtcoq_core. + - apply valid_check_diseq; auto with smtcoq_core. + - apply valid_check_spl_arith; auto with smtcoq_core. + - apply valid_check_distinct_elim; auto with smtcoq_core. + - eapply valid_check_bbVar; eauto with smtcoq_core. + - apply valid_check_bbConst; auto with smtcoq_core. + - apply valid_check_bbOp; auto with smtcoq_core. + - apply valid_check_bbNot; auto with smtcoq_core. + - apply valid_check_bbNeg; auto with smtcoq_core. + - apply valid_check_bbAdd; auto with smtcoq_core. + - apply valid_check_bbConcat; auto with smtcoq_core. + - apply valid_check_bbMult; auto with smtcoq_core. + - apply valid_check_bbUlt; auto with smtcoq_core. + - apply valid_check_bbSlt; auto with smtcoq_core. + - apply valid_check_bbEq; auto with smtcoq_core. + - apply valid_check_bbDiseq; auto with smtcoq_core. + - apply valid_check_bbExtract; auto with smtcoq_core. + - apply valid_check_bbZextend; auto with smtcoq_core. + - apply valid_check_bbSextend; auto with smtcoq_core. + - apply valid_check_bbShl; auto with smtcoq_core. + - apply valid_check_bbShr; auto with smtcoq_core. + - apply valid_check_roweq; auto with smtcoq_core. + - apply valid_check_rowneq; auto with smtcoq_core. + - apply valid_check_ext; auto with smtcoq_core. + - apply valid_check_hole; auto with smtcoq_core. + - apply valid_check_forall_inst with lemma; auto with smtcoq_core. Qed. Definition euf_checker (* t_atom t_form *) s t := @@ -490,8 +490,8 @@ Inductive step := ~ (S.valid rho s). Proof. unfold euf_checker; intros (* t_i t_func t_atom t_form *) rho H1 H2 H10; apply _checker__correct. - intros c H; apply C.is_false_correct; auto. - apply step_checker_correct; auto. + intros c H; apply C.is_false_correct; auto with smtcoq_core. + apply step_checker_correct; auto with smtcoq_core. Qed. Inductive certif := @@ -516,11 +516,11 @@ Inductive step := forall s d used_roots, S.valid rho s -> valid t_func t_atom t_form d -> S.valid rho (add_roots s d used_roots). Proof. - intros (* t_i t_func t_atom t_form *) rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ _ _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H]; auto); case used_roots. - intro ur; apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; case_eq (ur .[ i] < length d). - intro; unfold C.valid; simpl; rewrite H5; auto. - intros; apply C.interp_true; auto. - apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; unfold C.valid; simpl; rewrite H5; auto. + intros (* t_i t_func t_atom t_form *) rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ _ _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H]; auto with smtcoq_core); case used_roots. + intro ur; apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto with smtcoq_core; intros a i H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; case_eq (ur .[ i] < length d). + intro; unfold C.valid; simpl; rewrite H5; auto with smtcoq_core. + intros; apply C.interp_true; auto with smtcoq_core. + apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto with smtcoq_core; intros a i H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; unfold C.valid; simpl; rewrite H5; auto with smtcoq_core. Qed. Definition checker (* t_i t_func t_atom t_form *) d used_roots (c:certif) := @@ -711,7 +711,7 @@ Inductive step := checker (* t_i t_func t_atom t_form *) d used_roots c = true -> ~ (valid t_func t_atom t_form d). Proof. - unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H4]; auto. + unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H4]; auto with smtcoq_core. Qed. Definition checker_b (* t_i t_func t_atom t_form *) l (b:bool) (c:certif) := @@ -723,7 +723,7 @@ Inductive step := checker_b (* t_func t_atom t_form *) l b c = true -> Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l = b. Proof. - unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto. + unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l); auto with smtcoq_core; intros H1; elim (checker_correct H2); auto with smtcoq_core; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto with smtcoq_core; rewrite Lit.interp_neg, H1; auto with smtcoq_core. Qed. Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) := @@ -741,8 +741,8 @@ Inductive step := Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2. Proof. unfold checker_eq; intros (* t_i t_func t_atom t_form *) l1 l2 l (nclauses, t, confl); rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form). - unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H3) as [[Ht1 Ht2] Ht3]; split; auto. - destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2); intro Heq2; auto; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto. + unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H3) as [[Ht1 Ht2] Ht3]; split; auto with smtcoq_core. + destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2); intro Heq2; auto with smtcoq_core; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_core; rewrite Heq; simpl; rewrite Heq1, Heq2; auto with smtcoq_core. Qed. @@ -762,7 +762,7 @@ Inductive step := forall t_i t_func, Atom.wt t_i t_func t_atom -> ~ valid t_func t_atom t_form d. Proof. - unfold checker_ext; intros t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[H1 H2] H3]; intros t_i t_func H10 H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto. + unfold checker_ext; intros t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[H1 H2] H3]; intros t_i t_func H10 H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto with smtcoq_core. Qed. *) diff --git a/src/array/FArray.v b/src/array/FArray.v index a17817f..8048e60 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -44,7 +44,7 @@ Module Raw. Lemma eqb_elt_eq x y : eqb_elt x y = true <-> x = y. Proof. unfold eqb_elt. case (eq_dec x y); split; easy. Qed. - Hint Immediate eqb_key_eq eqb_elt_eq. + Hint Immediate eqb_key_eq eqb_elt_eq : smtcoq_array. Definition farray := list (key * elt). @@ -57,8 +57,8 @@ Module Raw. (* Definition ltke (a b : (key * elt)) := *) (* lt (fst a) (fst b) \/ ( (fst a) = (fst b) /\ lt (snd a) (snd b)). *) - Hint Unfold ltk (* ltke *) eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. + Hint Unfold ltk (* ltke *) eqk eqke : smtcoq_array. + Hint Extern 2 (eqke ?a ?b) => split : smtcoq_array. Global Instance lt_key_strorder : StrictOrder (lt : key -> key -> Prop). Proof. apply StrictOrder_OrdType. Qed. @@ -95,7 +95,7 @@ Module Raw. Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. - Hint Immediate ltk_right_r ltk_right_l. + Hint Immediate ltk_right_r ltk_right_l : smtcoq_array. Notation Sort := (sort ltk). Notation Inf := (lelistA (ltk)). @@ -105,7 +105,7 @@ Module Raw. Notation NoDupA := (NoDupA eqk). - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : smtcoq_array. (* Instance ke_ord: OrdType (key * elt). *) (* Proof. *) @@ -154,52 +154,52 @@ Module Raw. (* eqk, eqke are equalities *) Lemma eqk_refl : forall e, eqk e e. - Proof. auto. Qed. + Proof. auto with smtcoq_array. Qed. Lemma eqke_refl : forall e, eqke e e. - Proof. auto. Qed. + Proof. auto with smtcoq_array. Qed. Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. - Proof. auto. Qed. + Proof. auto with smtcoq_array. Qed. Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. Proof. unfold eqke; intuition. Qed. Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. - Proof. eauto. Qed. + Proof. eauto with smtcoq_array. Qed. Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. Proof. - unfold eqke; intuition; [ eauto | congruence ]. + unfold eqke; intuition; [ eauto with smtcoq_array | congruence ]. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. eauto with smtcoq_array. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. - Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto. Qed. + Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto with smtcoq_array. Qed. Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. unfold eqke, ltk; intuition; simpl in *; subst. - apply lt_not_eq in H. auto. + apply lt_not_eq in H. auto with smtcoq_array. Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. - Hint Immediate eqk_sym eqke_sym. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : smtcoq_array. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : smtcoq_array. + Hint Immediate eqk_sym eqke_sym : smtcoq_array. Global Instance eqk_equiv : Equivalence eqk. - Proof. split; eauto. Qed. + Proof. split; eauto with smtcoq_array. Qed. Global Instance eqke_equiv : Equivalence eqke. - Proof. split; eauto. Qed. + Proof. split; eauto with smtcoq_array. Qed. Global Instance ltk_strorder : StrictOrder ltk. Proof. split. unfold Irreflexive, Reflexive, complement. - intros. apply lt_not_eq in H; auto. + intros. apply lt_not_eq in H; auto with smtcoq_array. unfold Transitive. intros x y z. apply lt_trans. Qed. @@ -207,13 +207,13 @@ Module Raw. (* Proof. *) (* split. *) (* unfold Irreflexive, Reflexive, complement. *) - (* intros. apply lt_not_eq in H; auto. *) + (* intros. apply lt_not_eq in H; auto with smtcoq_array. *) (* unfold Transitive. apply lt_trans. *) (* Qed. *) Global Instance eq_equiv : @Equivalence (key * elt) eq. Proof. - split; auto. + split; auto with smtcoq_array. unfold Transitive. apply eq_trans. Qed. @@ -230,13 +230,13 @@ Module Raw. Global Instance ltk_compatk : Proper (eqk==>eqk==>iff) ltk. Proof. intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute. - compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto with smtcoq_array. Qed. Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk. Proof. intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute. - compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto with smtcoq_array. Qed. Global Instance ltk_asym : Asymmetric ltk. @@ -251,8 +251,8 @@ Module Raw. destruct x, x'. simpl in *. intro. symmetry in H. - apply lt_not_eq in H. auto. - subst. auto. + apply lt_not_eq in H. auto with smtcoq_array. + subst. auto with smtcoq_array. Qed. Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''. @@ -265,8 +265,8 @@ Module Raw. intros (k,e) (k',e') (k'',e''). unfold ltk, eqk; simpl; intros; subst; trivial. Qed. - Hint Resolve eqk_not_ltk. - Hint Immediate ltk_eqk eqk_ltk. + Hint Resolve eqk_not_ltk : smtcoq_array. + Hint Immediate ltk_eqk eqk_ltk : smtcoq_array. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. @@ -274,19 +274,19 @@ Module Raw. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : smtcoq_array. (* Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. *) (* Proof. *) - (* intros; apply InA_eqA with p; auto with *. *) + (* intros; apply InA_eqA with p; auto with smtcoq_array with *. *) (* Qed. *) (* Lemma In_eq : forall l x y, eq x y -> InA eqke x l -> InA eqke y l. *) - (* Proof. intros. rewrite <- H; auto. Qed. *) + (* Proof. intros. rewrite <- H; auto with smtcoq_array. Qed. *) (* Lemma ListIn_In : forall l x, List.In x l -> InA eqk x l. *) - (* Proof. apply In_InA. split; auto. unfold Transitive. *) - (* unfold eqk; intros. rewrite H, <- H0. auto. *) + (* Proof. apply In_InA. split; auto with smtcoq_array. unfold Transitive. *) + (* unfold eqk; intros. rewrite H, <- H0. auto with smtcoq_array. *) (* Qed. *) (* Lemma Inf_lt : forall l x y, ltk x y -> Inf y l -> Inf x l. *) @@ -300,12 +300,12 @@ Module Raw. Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof. firstorder. - exists x; auto. + exists x; auto with smtcoq_array. induction H. destruct y. - exists e; auto. + exists e; auto with smtcoq_array. destruct IHInA as [e H0]. - exists e; auto. + exists e; auto with smtcoq_array. Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. @@ -315,7 +315,7 @@ Module Raw. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. Proof. - destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. + destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto with smtcoq_array. Qed. Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. @@ -324,8 +324,8 @@ Module Raw. Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. + Hint Immediate Inf_eq : smtcoq_array. + Hint Resolve Inf_lt : smtcoq_array. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -339,11 +339,11 @@ Module Raw. intros; red; intros. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto. - red; simpl; auto. + eapply Sort_Inf_In; eauto with smtcoq_array. + red; simpl; auto with smtcoq_array. Qed. - Hint Resolve Sort_Inf_NotIn. + Hint Resolve Sort_Inf_NotIn : smtcoq_array. Lemma Sort_NoDupA: forall l, Sort l -> NoDupA l. Proof. @@ -352,14 +352,14 @@ Module Raw. Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. Proof. - inversion 1; intros; eapply Sort_Inf_In; eauto. + inversion 1; intros; eapply Sort_Inf_In; eauto with smtcoq_array. Qed. Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - inversion_clear 2; auto. - left; apply Sort_In_cons_1 with l; auto. + inversion_clear 2; auto with smtcoq_array. + left; apply Sort_In_cons_1 with l; auto with smtcoq_array. Qed. Lemma Sort_In_cons_3 : @@ -372,7 +372,7 @@ Module Raw. Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. inversion 1. - inversion_clear H0; eauto. + inversion_clear H0; eauto with smtcoq_array. destruct H1; simpl in *; intuition. Qed. @@ -388,7 +388,7 @@ Module Raw. inversion_clear 1; compute in H0; intuition. Qed. - Hint Resolve In_inv_2 In_inv_3. + Hint Resolve In_inv_2 In_inv_3 : smtcoq_array. (** * FMAPLIST interface implementaion *) @@ -405,11 +405,11 @@ Module Raw. intro abs. inversion abs. Qed. - Hint Resolve empty_1. + Hint Resolve empty_1 : smtcoq_array. Lemma empty_sorted : Sort empty. Proof. - unfold empty; auto. + unfold empty; auto with smtcoq_array. Qed. Lemma MapsTo_inj : forall x e e' l (Hl:Sort l), @@ -441,7 +441,7 @@ Module Raw. + unfold eqk in H, H0. simpl in *. subst. inversion_clear HH. inversion_clear HH0. - unfold eqke in *. simpl in *. destruct H, H1; subst; auto. + unfold eqke in *. simpl in *. destruct H, H1; subst; auto with smtcoq_array. apply InA_eqke_eqk in H1. inversion_clear Hl. specialize (Sort_Inf_In H2 H3 H1). @@ -460,15 +460,15 @@ Module Raw. Proof. unfold Empty, MapsTo. intros m. - case m;auto. + case m;auto with smtcoq_array. intros (k,e) l inlist. - absurd (InA eqke (k, e) ((k, e) :: l));auto. + absurd (InA eqke (k, e) ((k, e) :: l));auto with smtcoq_array. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. Proof. intros m. - case m;auto. + case m;auto with smtcoq_array. intros p l abs. inversion abs. Qed. @@ -494,15 +494,15 @@ Module Raw. - simpl. case_eq (compare x k'); trivial. + intros _x0 e0. absurd (In x ((k', _x) :: l));try assumption. - apply Sort_Inf_NotIn with _x;auto. + apply Sort_Inf_NotIn with _x;auto with smtcoq_array. + intros _x0 e0. apply IHb. - elim (sort_inv sorted);auto. - elim (In_inv belong1);auto. + elim (sort_inv sorted);auto with smtcoq_array. + elim (In_inv belong1);auto with smtcoq_array. intro abs. - absurd (eq x k'); auto. + absurd (eq x k'); auto with smtcoq_array. symmetry in abs. - apply lt_not_eq in abs; auto. + apply lt_not_eq in abs; auto with smtcoq_array. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. @@ -510,10 +510,10 @@ Module Raw. intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo. induction m as [ |[k' _x] l IHb]; intros sorted hyp;try ((inversion hyp);fail). revert hyp. simpl. case_eq (compare x k'); intros _x0 e0 hyp;try ((inversion hyp);fail). - - exists _x; auto. - - induction IHb; auto. - + exists x0; auto. - + inversion_clear sorted; auto. + - exists _x; auto with smtcoq_array. + - induction IHb; auto with smtcoq_array. + + exists x0; auto with smtcoq_array. + + inversion_clear sorted; auto with smtcoq_array. Qed. Lemma mem_3 : forall m (Hm:Sort m) x, mem x m = false -> ~ In x m. @@ -539,8 +539,8 @@ Module Raw. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold MapsTo. - induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto). - case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto. + induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto with smtcoq_array). + case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto with smtcoq_array. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. @@ -551,11 +551,11 @@ Module Raw. - case_eq (compare x k'); intros _x0 e1; subst. + inversion_clear 2. * clear e1;compute in H0; destruct H0. - apply lt_not_eq in H; auto. now contradict H. + apply lt_not_eq in H; auto with smtcoq_array. now contradict H. * clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. (* order. *) intros. - apply (lt_trans k') in _x0; auto. + apply (lt_trans k') in _x0; auto with smtcoq_array. apply lt_not_eq in _x0. now contradict _x0. + clear e1;inversion_clear 2. @@ -564,7 +564,7 @@ Module Raw. (* order. *) intros. apply lt_not_eq in H. now contradict H. - + clear e1; do 2 inversion_clear 1; auto. + + clear e1; do 2 inversion_clear 1; auto with smtcoq_array. compute in H2; destruct H2. (* order. *) subst. apply lt_not_eq in _x0. now contradict _x0. @@ -587,7 +587,7 @@ Module Raw. Proof. intros m x y e; generalize y; clear y. unfold MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto with smtcoq_array. Qed. Lemma add_2 : forall m x y e e', @@ -595,14 +595,14 @@ Module Raw. Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto; clear e0. - subst;auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto with smtcoq_array; clear e0. + subst;auto with smtcoq_array. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. (* order. *) subst. now contradict eqky'. - auto. - auto. + auto with smtcoq_array. + auto with smtcoq_array. intros y' e'' eqky'; inversion_clear 1; intuition. Qed. @@ -611,10 +611,10 @@ Module Raw. Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];simpl; intros. - apply (In_inv_3 H0); compute; auto. - apply (In_inv_3 H0); compute; auto. - constructor 2; apply (In_inv_3 H0); compute; auto. - inversion_clear H0; auto. + apply (In_inv_3 H0); compute; auto with smtcoq_array. + apply (In_inv_3 H0); compute; auto with smtcoq_array. + constructor 2; apply (In_inv_3 H0); compute; auto with smtcoq_array. + inversion_clear H0; auto with smtcoq_array. Qed. Lemma add_Inf : forall (m:farray)(x x':key)(e e':elt), @@ -628,7 +628,7 @@ Module Raw. compute in H0,H1. simpl; case (compare x x''); intuition. Qed. - Hint Resolve add_Inf. + Hint Resolve add_Inf : smtcoq_array. Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). Proof. @@ -636,9 +636,9 @@ Module Raw. simpl; intuition. intros. destruct a as (x',e'). - simpl; case (compare x x'); intuition; inversion_clear Hm; auto. - constructor; auto. - apply Inf_eq with (x',e'); auto. + simpl; case (compare x x'); intuition; inversion_clear Hm; auto with smtcoq_array. + constructor; auto with smtcoq_array. + apply Inf_eq with (x',e'); auto with smtcoq_array. Qed. (** * [remove] *) @@ -661,22 +661,22 @@ Module Raw. red; inversion 1; inversion H0. - apply Sort_Inf_NotIn with x0; auto. + apply Sort_Inf_NotIn with x0; auto with smtcoq_array. clear e0. inversion Hm. subst. - apply Sort_Inf_NotIn with x0; auto. + apply Sort_Inf_NotIn with x0; auto with smtcoq_array. (* clear e0;inversion_clear Hm. *) - (* apply Sort_Inf_NotIn with x0; auto. *) - (* apply Inf_eq with (k',x0);auto; compute; apply eq_trans with x; auto. *) + (* apply Sort_Inf_NotIn with x0; auto with smtcoq_array. *) + (* apply Inf_eq with (k',x0);auto with smtcoq_array; compute; apply eq_trans with x; auto with smtcoq_array. *) clear e0;inversion_clear Hm. - assert (notin:~ In y (remove y l)) by auto. + assert (notin:~ In y (remove y l)) by auto with smtcoq_array. intros (x1,abs). inversion_clear abs. compute in H1; destruct H1. subst. apply lt_not_eq in _x; now contradict _x. - apply notin; exists x1; auto. + apply notin; exists x1; auto with smtcoq_array. Qed. @@ -684,41 +684,41 @@ Module Raw. ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m). Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto; + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. - inversion_clear 3; auto. + inversion_clear 3; auto with smtcoq_array. compute in H1; destruct H1. subst; now contradict H. - inversion_clear 1; inversion_clear 2; auto. + inversion_clear 1; inversion_clear 2; auto with smtcoq_array. Qed. Lemma remove_3 : forall m (Hm:Sort m) x y e, MapsTo y e (remove x m) -> MapsTo y e m. Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto. - inversion_clear 1; inversion_clear 1; auto. + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array. + inversion_clear 1; inversion_clear 1; auto with smtcoq_array. Qed. Lemma remove_4_aux : forall m (Hm:Sort m) x y, ~ eq x y -> In y m -> In y (remove x m). Proof. intros m Hm x y; generalize Hm; clear Hm. - induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto; + induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. rewrite In_alt. - inversion_clear 3; auto. + inversion_clear 3; auto with smtcoq_array. inversion H2. unfold eqk in H3. simpl in H3. subst. now contradict H0. apply In_alt. - exists x. auto. + exists x. auto with smtcoq_array. apply lt_not_eq in _x. intros. inversion_clear Hm. @@ -729,27 +729,27 @@ Module Raw. destruct (eq_dec k' y). exists x0. apply InA_cons_hd. - split; simpl; auto. + split; simpl; auto with smtcoq_array. inversion H3. unfold eqk in H4. simpl in H4; subst. now contradict n. assert ((exists e : elt, MapsTo y e (remove x l)) -> (exists e : elt, MapsTo y e ((k', x0) :: remove x l))). intros. destruct H6. exists x2. - apply InA_cons_tl. auto. + apply InA_cons_tl. auto with smtcoq_array. apply H6. - apply IHf; auto. + apply IHf; auto with smtcoq_array. apply In_alt. - exists x1. auto. + exists x1. auto with smtcoq_array. Qed. Lemma remove_4 : forall m (Hm:Sort m) x y, ~ eq x y -> In y m <-> In y (remove x m). Proof. split. - apply remove_4_aux; auto. + apply remove_4_aux; auto with smtcoq_array. revert H. generalize Hm; clear Hm. - induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto; + induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac @@ -758,7 +758,7 @@ Module Raw. (* rewrite In_alt in *. *) destruct H0 as (e, H0). exists e. - apply InA_cons_tl. auto. + apply InA_cons_tl. auto with smtcoq_array. intros. apply lt_not_eq in _x0. inversion_clear Hm. @@ -766,11 +766,11 @@ Module Raw. destruct H0. (* destruct (eq_dec k' y). *) exists _x. - apply InA_cons_hd. split; simpl; auto. + apply InA_cons_hd. split; simpl; auto with smtcoq_array. specialize (IHb H1 H H0). inversion IHb. exists x0. - apply InA_cons_tl. auto. + apply InA_cons_tl. auto with smtcoq_array. Qed. Lemma remove_Inf : forall (m:farray)(Hm : Sort m)(x x':key)(e':elt), @@ -784,9 +784,9 @@ Module Raw. compute in H0. simpl; case (compare x x''); intuition. inversion_clear Hm. - apply Inf_lt with (x'',e''); auto. + apply Inf_lt with (x'',e''); auto with smtcoq_array. Qed. - Hint Resolve remove_Inf. + Hint Resolve remove_Inf : smtcoq_array. Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). Proof. @@ -794,7 +794,7 @@ Module Raw. simpl; intuition. intros. destruct a as (x',e'). - simpl; case (compare x x'); intuition; inversion_clear Hm; auto. + simpl; case (compare x x'); intuition; inversion_clear Hm; auto with smtcoq_array. Qed. (** * [elements] *) @@ -804,25 +804,25 @@ Module Raw. Lemma elements_1 : forall m x e, MapsTo x e m -> InA eqke (x,e) (elements m). Proof. - auto. + auto with smtcoq_array. Qed. Lemma elements_2 : forall m x e, InA eqke (x,e) (elements m) -> MapsTo x e m. Proof. - auto. + auto with smtcoq_array. Qed. Lemma elements_3 : forall m (Hm:Sort m), sort ltk (elements m). Proof. - auto. + auto with smtcoq_array. Qed. Lemma elements_3w : forall m (Hm:Sort m), NoDupA (elements m). Proof. intros. apply Sort_NoDupA. - apply elements_3; auto. + apply elements_3; auto with smtcoq_array. Qed. (** * [fold] *) @@ -836,7 +836,7 @@ Module Raw. Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. - intros; revert i; induction m as [ |[k e]]; simpl; auto. + intros; revert i; induction m as [ |[k e]]; simpl; auto with smtcoq_array. Qed. (** * [equal] *) @@ -860,7 +860,7 @@ Module Raw. Equivb cmp m m' -> equal cmp m m' = true. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto; unfold Equivb; intuition; subst. + revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto with smtcoq_array; unfold Equivb; intuition; subst. - destruct (H0 x') as [_ H3]. assert (H2: In x' nil). { @@ -873,53 +873,53 @@ Module Raw. apply H3. exists e. now constructor. } elim H2. intros x0 Hx0. inversion Hx0. - - case_eq (compare x x'); simpl; subst;auto; unfold Equivb; + - case_eq (compare x x'); simpl; subst;auto with smtcoq_array; unfold Equivb; intuition; subst. + destruct (H0 x). assert (In x ((x',e')::l')). - apply H2; auto. - exists e; auto. + apply H2; auto with smtcoq_array. + exists e; auto with smtcoq_array. destruct (In_inv H4). (* order. *) clear H. apply lt_not_eq in l0; now contradict l0. inversion_clear Hm'. assert (Inf (x,e) l'). - apply Inf_lt with (x',e'); auto. + apply Inf_lt with (x',e'); auto with smtcoq_array. elim (Sort_Inf_NotIn H6 H8 H5). + match goal with H: compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). - apply H1 with x'; auto. + apply H1 with x'; auto with smtcoq_array. rewrite cmp_e_e'; simpl. - apply IHl; auto. - inversion_clear Hm; auto. - inversion_clear Hm'; auto. + apply IHl; auto with smtcoq_array. + inversion_clear Hm; auto with smtcoq_array. + inversion_clear Hm'; auto with smtcoq_array. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x',e) ::l)). - destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H2 H4)); auto. + destruct H as (e'', hyp); exists e''; auto with smtcoq_array. + destruct (In_inv (H2 H4)); auto with smtcoq_array. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). - destruct H as (e'', hyp); exists e''; auto. - apply MapsTo_eq with k; auto. + destruct H as (e'', hyp); exists e''; auto with smtcoq_array. + apply MapsTo_eq with k; auto with smtcoq_array. destruct (H0 k). assert (In k ((x',e') ::l')). - destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H3 H4)); auto. + destruct H as (e'', hyp); exists e''; auto with smtcoq_array. + destruct (In_inv (H3 H4)); auto with smtcoq_array. subst. inversion_clear Hm'. now elim (Sort_Inf_NotIn H5 H6). - apply H1 with k; destruct (eq_dec x' k); auto. + apply H1 with k; destruct (eq_dec x' k); auto with smtcoq_array. + destruct (H0 x'). assert (In x' ((x,e)::l)). - apply H3; auto. - exists e'; auto. + apply H3; auto with smtcoq_array. + exists e'; auto with smtcoq_array. destruct (In_inv H4). (* order. *) clear H; subst; apply lt_not_eq in l0; now contradict l0. inversion_clear Hm. assert (Inf (x',e') l). - apply Inf_lt with (x,e); auto. + apply Inf_lt with (x,e); auto with smtcoq_array. elim (Sort_Inf_NotIn H6 H8 H5). Qed. @@ -927,7 +927,7 @@ Module Raw. equal cmp m m' = true -> Equivb cmp m m'. Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. - revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto; unfold Equivb; + revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto with smtcoq_array; unfold Equivb; intuition; try discriminate; subst; try match goal with H: compare _ _ = _ |- _ => clear H end. - inversion H0. @@ -936,19 +936,19 @@ Module Raw. destruct (andb_prop _ _ H); clear H. destruct (IHl _ H1 H4 H7). destruct (In_inv H0). - exists e'; constructor; split; trivial; apply eq_trans with x; auto. + exists e'; constructor; split; trivial; apply eq_trans with x; auto with smtcoq_array. destruct (H k). destruct (H10 H9) as (e'',hyp). - exists e''; auto. + exists e''; auto with smtcoq_array. - revert H; case_eq (compare x x'); intros _x _ H; try inversion H. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHl _ H1 H4 H7). destruct (In_inv H0). - exists e; constructor; split; trivial; apply eq_trans with x'; auto. + exists e; constructor; split; trivial; apply eq_trans with x'; auto with smtcoq_array. destruct (H k). destruct (H11 H9) as (e'',hyp). - exists e''; auto. + exists e''; auto with smtcoq_array. - revert H; case_eq (compare x x'); intros _x _ H; [inversion H| |inversion H]. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. @@ -956,16 +956,16 @@ Module Raw. inversion_clear H0. + destruct H9; simpl in *; subst. inversion_clear H1. - * destruct H0; simpl in *; subst; auto. + * destruct H0; simpl in *; subst; auto with smtcoq_array. * elim (Sort_Inf_NotIn H4 H5). - exists e'0; apply MapsTo_eq with x'; auto. + exists e'0; apply MapsTo_eq with x'; auto with smtcoq_array. (* order. *) + inversion_clear H1. - * destruct H0; simpl in *; subst; auto. + * destruct H0; simpl in *; subst; auto with smtcoq_array. elim (Sort_Inf_NotIn H2 H3). - exists e0; apply MapsTo_eq with x'; auto. + exists e0; apply MapsTo_eq with x'; auto with smtcoq_array. (* order. *) - * apply H8 with k; auto. + * apply H8 with k; auto with smtcoq_array. Qed. (** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *) @@ -979,18 +979,18 @@ Module Raw. inversion H0; subst. destruct x; destruct y; compute in H1, H2. split; intros. - apply equal_2; auto. + apply equal_2; auto with smtcoq_array. simpl. case (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). rewrite H2; simpl. - apply equal_1; auto. - apply equal_2; auto. + apply equal_1; auto with smtcoq_array. + apply equal_2; auto with smtcoq_array. generalize (equal_1 H H0 H3). simpl. case (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). - rewrite H2; simpl; auto. + rewrite H2; simpl; auto with smtcoq_array. Qed. End Array. @@ -1580,7 +1580,7 @@ Section FArray. intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff. apply add_neq_mapsto_iff; auto. Qed. - Hint Resolve add_neq_o. + Hint Resolve add_neq_o : smtcoq_array. Lemma MapsTo_fun : forall m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'. @@ -1838,6 +1838,8 @@ Arguments extensionnality2 {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. Arguments select_at_diff {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _. +Declare Scope farray_scope. + Notation "a '[' i ']'" := (select a i) (at level 1, format "a [ i ]") : farray_scope. Notation "a '[' i '<-' v ']'" := (store a i v) (at level 1, format "a [ i <- v ]") : farray_scope. diff --git a/src/bva/BVList.v b/src/bva/BVList.v index a53970b..6d64190 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -2684,6 +2684,8 @@ Qed. End RAWBITVECTOR_LIST. +Declare Scope bv_scope. + Module BITVECTOR_LIST <: BITVECTOR. Include RAW2BITVECTOR(RAWBITVECTOR_LIST). diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 84df9bd..0f5bc1a 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -1554,7 +1554,7 @@ Proof. intros l a H. rewrite H. unfold RAWBITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.size, RAWBITVECTOR_LIST.bits in *. - rewrite RAWBITVECTOR_LIST.List_eq_refl; auto. + rewrite RAWBITVECTOR_LIST.List_eq_refl; auto with smtcoq_core. apply inj_iff in wf0. now do 2 rewrite id' in wf0. Qed. diff --git a/src/euf/Euf.v b/src/euf/Euf.v index 7818246..5b4fa93 100644 --- a/src/euf/Euf.v +++ b/src/euf/Euf.v @@ -180,7 +180,7 @@ Section certif. apply C.interp_true. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial. Qed. - Hint Resolve valid_C_true. + Hint Resolve valid_C_true : smtcoq_euf. Local Notation interp := (Atom.interp t_i t_func t_atom). @@ -210,9 +210,9 @@ Section certif. C.interp rho (get_eq (Lit.blit l) f). Proof. intros l f Hf;unfold get_eq. - case_eq (t_form.[Lit.blit l]);trivial;intros. - case_eq (t_atom.[i]);trivial;intros. - destruct b;trivial. + case_eq (t_form.[Lit.blit l]);trivial with smtcoq_euf;intros. + case_eq (t_atom.[i]);trivial with smtcoq_euf;intros. + destruct b;trivial with smtcoq_euf. generalize wt_t_atom;unfold Atom.wt;unfold is_true; rewrite PArray.forallbi_spec;intros. assert (i < length t_atom). @@ -279,48 +279,48 @@ Section certif. C.interp rho (check_trans_aux t1 t2 eqs res c). Proof. induction eqs;simpl;intros. - apply get_eq_interp;intros. + - apply get_eq_interp;intros. match goal with |- context [if ?b then _ else _] => case_eq b end; - intros;trivial. + intros;trivial with smtcoq_euf. simpl;rewrite Lit.interp_lit;unfold Var.interp. - destruct H1;[ | rewrite H1,orb_true_r;auto]. + destruct H1;[ | rewrite H1,orb_true_r;auto with smtcoq_euf smtcoq_core]. rewrite orb_true_iff, !andb_true_iff in H7;destruct H7 as [[H7 H8] | [H7 H8]]. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. - tunicity. subst t. rewrite H4, H1;auto. + tunicity. subst t. rewrite H4, H1;auto with smtcoq_euf smtcoq_core. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. - tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto. - apply get_eq_interp;intros. + tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto with smtcoq_euf smtcoq_core. + - apply get_eq_interp;intros. destruct (Int63Properties.reflect_eqb t2 b);subst;tunicity; try subst t. - apply (IHeqs u);trivial. + + apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. rewrite interp_binop_eqb_sym;trivial. - destruct (Int63Properties.reflect_eqb t2 a0); subst;tunicity; try subst t. - apply (IHeqs u);trivial. + + destruct (Int63Properties.reflect_eqb t2 a0); subst;tunicity; try subst t. + * apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. - destruct (Int63Properties.reflect_eqb t1 b);subst;tunicity; try subst t. - apply (IHeqs u);trivial. + * destruct (Int63Properties.reflect_eqb t1 b);subst;tunicity; try subst t. + -- apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (5:= H1);trivial. - destruct (Int63Properties.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto]. + -- destruct (Int63Properties.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto with smtcoq_euf smtcoq_core]. apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. - (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *) + (* Warning: here, we use decidability of equality over u *) case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (5:= H1);trivial. @@ -332,9 +332,9 @@ Section certif. C.interp rho (check_trans res eqs). Proof. unfold check_trans;intros res [ | leq eqs]. - apply get_eq_interp;intros. + - apply get_eq_interp;intros. destruct (Int63Properties.reflect_eqb a b). - unfold C.interp; simpl; rewrite orb_false_r. + + unfold C.interp; simpl; rewrite orb_false_r. unfold Lit.interp; simpl; rewrite Lit.is_pos_lit. unfold Var.interp; simpl; rewrite Lit.blit_lit. rewrite H1. @@ -344,12 +344,12 @@ Section certif. unfold Atom.interp_hatom. rewrite HHb;simpl;rewrite Typ.cast_refl;simpl. apply Typ.i_eqb_refl. - auto. - apply get_eq_interp;intros. + + auto with smtcoq_euf. + - apply get_eq_interp;intros. apply check_trans_aux_correct with t;trivial. simpl;rewrite Lit.interp_nlit;unfold Var.interp. rewrite <- H1. (* Attention ici on utilise la decidabilit'e de l'egalit'e sur t *) - destruct (rho (Lit.blit leq));auto. + destruct (rho (Lit.blit leq));auto with smtcoq_core. Qed. Inductive Forall2 A B (P:A->B->Prop) : list A -> list B -> Prop := @@ -362,16 +362,16 @@ Section certif. (Forall2 _ _ (fun a b => interp_hatom a = interp_hatom b) l r -> C.interp rho c) -> C.interp rho (build_congr lp l r c). Proof. - induction lp;destruct l;destruct r;simpl;trivial;intros. + induction lp;destruct l;destruct r;simpl;trivial with smtcoq_euf smtcoq_core;intros. apply H;constructor. destruct a. apply get_eq_interp;intros. match goal with |- context [if ?x then _ else _] => - case_eq x;intros;auto end. + case_eq x;intros;auto with smtcoq_euf smtcoq_core end. apply IHlp;simpl;intros. rewrite Lit.interp_nlit;unfold Var.interp. - case_eq (rho (Lit.blit i1));intros;simpl;[ | auto]. - apply H;constructor;trivial. + case_eq (rho (Lit.blit i1));intros;simpl;[ | auto with smtcoq_euf smtcoq_core]. + apply H;constructor;trivial with smtcoq_euf smtcoq_core. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H3. rewrite Typ.eqb_spec in H4. unfold Atom.get_type in H3, H4. rewrite H3,H4. intros [va HHa] [vb HHb]. revert H7;rewrite H2;unfold Atom.apply_binop; simpl. unfold Atom.interp_hatom. @@ -381,11 +381,11 @@ Section certif. rewrite orb_true_iff, !andb_true_iff in H5;destruct H5 as [ [H5 H7] | [H5 H7]]. rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst. - rewrite HHa, HHb;trivial. + rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core. rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst. - rewrite HHa, HHb;trivial. - destruct (Int63Properties.reflect_eqb i i0);[subst | auto]. - apply IHlp;intros;apply H;constructor;auto. + rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core. + destruct (Int63Properties.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core]. + apply IHlp;intros;apply H;constructor;auto with smtcoq_euf smtcoq_core. Qed. Lemma valid_check_congr : @@ -393,71 +393,71 @@ Section certif. C.interp rho (check_congr leq eqs). Proof. unfold check_congr;intros leq eqs;apply get_eq_interp;intros. - case_eq (t_atom .[ a]);intros;auto; - case_eq (t_atom .[ b]);intros;auto. + case_eq (t_atom .[ a]);intros;auto with smtcoq_euf smtcoq_core; + case_eq (t_atom .[ b]);intros;auto with smtcoq_euf smtcoq_core. (* uop *) - destruct (Atom.reflect_uop_eqb u u0);[subst | auto]. + destruct (Atom.reflect_uop_eqb u u0);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl. rewrite HHb, HHa. simpl. - rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa. - rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb. + rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. + rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). inversion H6;subst. unfold Atom.interp_hatom in H10. - rewrite <- HHa; rewrite <- HHb, H10;trivial. + rewrite <- HHa; rewrite <- HHb, H10;trivial with smtcoq_euf smtcoq_core. inversion H7. - apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial. + apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. - intros x y;destruct (Typ.reflect_eqb x y);auto. + intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. (* bop *) - destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto]. + destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop. unfold Atom.interp_hatom;simpl. rewrite HHb, HHa;simpl. - rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa. - rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb. + rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. + rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). inversion H6;clear H6;subst. inversion H12;clear H12;subst. unfold Atom.interp_hatom in H10, H8. - rewrite <- HHa. rewrite <- HHb, H10, H8;trivial. + rewrite <- HHa. rewrite <- HHb, H10, H8;trivial with smtcoq_euf smtcoq_core. inversion H7. - apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial. + apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. - intros x y;destruct (Typ.reflect_eqb x y);auto. + intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. (* op *) - destruct (Int63Properties.reflect_eqb i i0);[subst | auto]. + destruct (Int63Properties.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl. rewrite HHb, HHa;simpl. - rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa. - rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb. + rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. + rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). rewrite <- HHa;rewrite <- HHb;destruct (t_func.[i0]). apply f_equal;clear HHa HHb va vb H5 H4. - induction H6;simpl;trivial. + induction H6;simpl;trivial with smtcoq_euf smtcoq_core. unfold Atom.interp_hatom in H4. - rewrite IHForall2, H4;trivial. + rewrite IHForall2, H4;trivial with smtcoq_euf smtcoq_core. inversion H7. - apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial. + apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. - intros x y;destruct (Typ.reflect_eqb x y);auto. + intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. Qed. Lemma valid_check_congr_pred : @@ -465,11 +465,11 @@ Section certif. C.interp rho (check_congr_pred lpa lpb eqs). Proof. unfold check_congr_pred;intros. - case_eq (t_form.[Lit.blit lpa]);auto. - case_eq (t_form.[Lit.blit lpb]);auto;intros. - case_eq (t_atom.[i0]);auto; case_eq (t_atom.[i]);auto;intros. + case_eq (t_form.[Lit.blit lpa]);auto with smtcoq_euf smtcoq_core. + case_eq (t_form.[Lit.blit lpb]);auto with smtcoq_euf smtcoq_core;intros. + case_eq (t_atom.[i0]);auto with smtcoq_euf smtcoq_core; case_eq (t_atom.[i]);auto with smtcoq_euf smtcoq_core;intros. (* uop *) - destruct (Atom.reflect_uop_eqb u0 u);[subst | auto]. + destruct (Atom.reflect_uop_eqb u0 u);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). @@ -485,12 +485,12 @@ Section certif. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. - rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial. + rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. apply f_equal;apply f_equal. - inversion H3;clear H3;subst;trivial. + inversion H3;clear H3;subst;trivial with smtcoq_euf smtcoq_core. (* bop *) - destruct (Atom.reflect_bop_eqb b0 b);[subst | auto]. + destruct (Atom.reflect_bop_eqb b0 b);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). @@ -506,13 +506,13 @@ Section certif. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. - rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial. + rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. inversion H3;clear H3;subst. inversion H11;clear H11;subst. - apply f_equal; apply f_equal2;trivial. + apply f_equal; apply f_equal2;trivial with smtcoq_euf smtcoq_core. (* op *) - destruct (Int63Properties.reflect_eqb i2 i1);[subst | auto]. + destruct (Int63Properties.reflect_eqb i2 i1);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;simpl;intros. rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp. replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)). @@ -528,11 +528,11 @@ Section certif. rewrite H2, def_t_atom;discriminate. apply H4 in H5;apply H4 in H6;clear H4. unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl. - rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial. + rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core. apply f_equal;destruct (t_func.[i1]);apply f_equal. clear H H0 H1 H2 H5 H6. - induction H3;simpl;trivial. - unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial. + induction H3;simpl;trivial with smtcoq_euf smtcoq_core. + unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial with smtcoq_euf smtcoq_core. Qed. End Proof. diff --git a/src/lia/Lia.v b/src/lia/Lia.v index c214c3b..46bbc5d 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -113,7 +113,7 @@ Section certif. | Some z => (vm, PEc z) | None => let (vm,p) := find_var vm h in - (vm,PEX Z p) + (vm,PEX p) end end. @@ -157,7 +157,7 @@ Section certif. Section Build_form. Definition build_not2 i f := - fold (fun f' => N (N (A:=Formula Z) f')) 1 i f. + fold (fun f' : BFormula (Formula Z) => N (N f')) 1 i f. Variable build_var : vmap -> var -> option (vmap*BFormula (Formula Z)). @@ -166,11 +166,11 @@ Section certif. match f with | Form.Fatom h => match build_formula vm h with - | Some (vm,f) => Some (vm, A f) + | Some (vm,f) => Some (vm, A f tt) | None => None end - | Form.Ftrue => Some (vm, TT (Formula Z)) - | Form.Ffalse => Some (vm, FF (Formula Z)) + | Form.Ftrue => Some (vm, TT) + | Form.Ffalse => Some (vm, FF) | Form.Fnot2 i l => match build_var vm (Lit.blit l) with | Some (vm, f) => @@ -181,7 +181,7 @@ Section certif. end | Form.Fand args => let n := length args in - if n == 0 then Some (vm,TT (Formula Z)) + if n == 0 then Some (vm,TT) else foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,Cj f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in match build_var vm (Lit.blit l) with @@ -190,7 +190,7 @@ Section certif. end) | Form.For args => let n := length args in - if n == 0 then Some (vm,FF (Formula Z)) + if n == 0 then Some (vm,FF) else foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,D f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in match build_var vm (Lit.blit l) with @@ -211,7 +211,7 @@ Section certif. end | Form.Fimp args => let n := length args in - if n == 0 then Some (vm,TT (Formula Z)) + if n == 0 then Some (vm,TT) else if n <= 1 then let l := args.[0] in match build_var vm (Lit.blit l) with @@ -219,7 +219,7 @@ Section certif. | None => None end else - foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,I f2' f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in + foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,I f2' None f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in match build_var vm (Lit.blit l) with | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) | None => None @@ -295,7 +295,7 @@ Section certif. Definition build_clause vm cl := match build_clause_aux vm cl with - | Some (vm, bf) => Some (vm, I bf (FF _)) + | Some (vm, bf) => Some (vm, I bf None FF) | None => None end. @@ -479,11 +479,11 @@ Section certif. Fixpoint bounded_bformula (p:positive) (bf:BFormula (Formula Z)) := match bf with - | @TT _ | @FF _ | @X _ _ => true - | A f => bounded_formula p f + | @TT _ | @FF _ | @X _ _ _ _ _ => true + | A f _ => bounded_formula p f | Cj bf1 bf2 | D bf1 bf2 - | I bf1 bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 + | I bf1 _ bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 | N bf => bounded_bformula p bf end. @@ -523,7 +523,7 @@ Section certif. check_atom h Typ.TZ -> match build_z_atom h with | Some z => (vm, PEc z) - | None => let (vm0, p) := find_var vm h in (vm0, PEX Z p) + | None => let (vm0, p) := find_var vm h in (vm0, PEX p) end = (vm', pe) -> wf_vmap vm -> wf_vmap vm' /\ @@ -1020,13 +1020,15 @@ Transparent build_z_atom. intros;apply build_formula_atom_correct with (get_type t_i t_func t_atom h);trivial. unfold wt, is_true in wt_t_atom;rewrite forallbi_spec in wt_t_atom. - case_eq (h < length t_atom);intros Heq;unfold get_type;auto. + case_eq (h < length t_atom);intros Heq;unfold get_type;auto with smtcoq_core. unfold get_type'. rewrite !PArray.get_outofbound, default_t_interp, def_t_atom;trivial; try reflexivity. rewrite length_t_interp;trivial. Qed. + Local Notation eval_f := (eval_f (fun x => x)). + Lemma build_not2_pos_correct : forall vm f l i, bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (build_not2 i f)). Proof. @@ -1083,7 +1085,7 @@ Transparent build_z_atom. Proof. intros vm vm' Hnth. unfold is_true;induction bf;simpl;try tauto. - destruct a;unfold bounded_formula;simpl. + destruct t;unfold bounded_formula;simpl. rewrite andb_true_iff;intros (H1, H2). rewrite !(interp_pexpr_le _ _ Hnth);tauto. rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto. @@ -1123,12 +1125,12 @@ Transparent build_z_atom. (* Ftrue *) intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 4 split; auto. (* Ffalse *) - intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 3 (split; auto); discriminate. + intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate. (* Fnot2 *) case_eq (build_var vm (Lit.blit l)); try discriminate; intros [vm0 f] Heq H H1; inversion H; subst vm0; subst bf; destruct (Hbv _ _ _ _ Heq H1) as [H2 [H3 [H4 [H5 H6]]]]; do 3 (split; auto); case_eq (Lit.is_pos l); [apply build_not2_pos_correct|apply build_not2_neg_correct]; auto. (* Fand *) simpl; unfold afold_left; case (length l == 0). - intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto). + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core). revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. @@ -1136,104 +1138,76 @@ Transparent build_z_atom. intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split. intros p H15; rewrite H7; auto; apply H12; eauto with arith. split. - simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto. - simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite andb_true_r; try rewrite andb_false_r; try (intros; split; auto); try discriminate; intros [H20 H21]; auto. + simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto with smtcoq_core. + simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite andb_true_r; try rewrite andb_false_r; try (intros; split; auto with smtcoq_core); try discriminate; intros [H20 H21]; auto with smtcoq_core. (* For *) simpl; unfold afold_left; case (length l == 0). - intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto); discriminate. + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate. revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). - intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split. + intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. - intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto; intro H4; elim H3; rewrite <- H14; auto. - intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split. - intros p H15; rewrite H7; auto; apply H12; eauto with arith. + intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core. + intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split. + intros p H15; rewrite H7; auto with smtcoq_core; apply H12; eauto with smtcoq_core arith. split. - simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto. - simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite orb_false_r; try rewrite orb_true_r; auto; try (intros [H20|H20]; auto; discriminate); right; intro H20; discriminate. + simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto with smtcoq_core. + simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite orb_false_r; try rewrite orb_true_r; auto with smtcoq_core; try (intros [H20|H20]; auto with smtcoq_core; discriminate); right; intro H20; discriminate. (* Fimp *) simpl; unfold afold_right; case (length l == 0). - intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto). + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core). case (length l <= 1). - case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H3 [H4 [H5 [H6 H7]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split. + case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H3 [H4 [H5 [H6 H7]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H8 H9; rewrite <- H7 in H9; rewrite H9 in H8; discriminate. - intro H8; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto; intro H9; rewrite H7 in H9; elim H8; auto. + intro H8; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H9; rewrite H7 in H9; elim H8; auto with smtcoq_core. revert vm' bf; apply (foldi_down_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). - intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ length l - 1]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ length l - 1])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split. + intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ length l - 1]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ length l - 1])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. - intro H3; case_eq (Var.interp rho (Lit.blit (l .[ length l - 1]))); auto; intro H4; elim H3; rewrite <- H14; auto. - intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split. - intros p H15; rewrite H7; auto; apply H12; eauto with arith. + intro H3; case_eq (Var.interp rho (Lit.blit (l .[ length l - 1]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core. + intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split. + intros p H15; rewrite H7; auto with smtcoq_core; apply H12; eauto with smtcoq_core arith. split. - simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto. - simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); auto; try discriminate; simpl; intro H; apply H; discriminate. + simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto with smtcoq_core. + simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); auto with smtcoq_core; try discriminate; simpl; intro H; apply H; discriminate. (* Fxor *) - simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto; split; [eauto with arith| ]; split. - intros p H18; rewrite H5; auto; rewrite H10; eauto with arith. + simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split. + intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith. split. - case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto. - simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto; try discriminate; simpl. - intros [_ [H20|H20]]; elim H20; reflexivity. - intros _; split; [left; reflexivity|right; intro H20; discriminate]. - intros _; split; [right; reflexivity|left; intro H20; discriminate]. - intros [[H20|H20] _]; discriminate. - intros [_ [H20|H20]]; elim H20; [reflexivity|discriminate]. - intros [[H20|H20] _]; [discriminate|elim H20; reflexivity]. - intros _; split; [right|left]; discriminate. - intros [[H20|H20] _]; [elim H20; reflexivity|discriminate]. - intros [_ [H20|H20]]; elim H20; [discriminate|reflexivity]. - intros _; split; [left|right]; discriminate. - intros [[H20|H20] _]; elim H20; reflexivity. - intros _; split; [right; discriminate|left; intro H21; apply H21; reflexivity]. - intros _; split; [left; discriminate|right; intro H21; apply H21; reflexivity]. - intros [_ [H20|H20]]; elim H20; discriminate. + case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto with smtcoq_core. + simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition. (* Fiff *) - simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto; split; [eauto with arith| ]; split. - intros p H18; rewrite H5; auto; rewrite H10; eauto with arith. + simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split. + intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith. split. - case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto. - simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto; try discriminate; simpl. - intros [_ [H20|H20]]; [elim H20; reflexivity|discriminate]. - intros [[H20|H20] _]; [discriminate|elim H20; reflexivity]. - intros _; split; [right|left]; discriminate. - intros [_ [H20|H20]]; elim H20; reflexivity. - intros _; split; [left; reflexivity|right; discriminate]. - intros _; split; [right; intro H20; apply H20; reflexivity|left; discriminate]. - intros [[H20|H20] _]; [ |elim H20]; discriminate. - intros [[H20|H20] _]; elim H20; reflexivity. - intros _; split; [right; discriminate|left; intro H20; apply H20; reflexivity]. - intros _; split; [left; discriminate|right; reflexivity]. - intros [_ [H20|H20]]; [elim H20| ]; discriminate. - intros [[H20|H20] _]; elim H20; [reflexivity|discriminate]. - intros [_ [H20|H20]]; elim H20; [discriminate|reflexivity]. - intros _; split; [left|right]; discriminate. + case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto with smtcoq_core. + simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition. (* Fite *) - simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2; case_eq (build_var vm2 (Lit.blit c)); try discriminate; intros [vm3 f3] Heq3 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; destruct (Hbv _ _ _ _ Heq3 H8) as [H13 [H14 [H15 [H16 H17]]]]; split; auto; split; [eauto with arith| ]; split. - intros p H18; rewrite H5; auto; rewrite H10; eauto with arith. - assert (H18: (Pos.to_nat (fst vm1) <= Pos.to_nat (fst vm3))%nat) by eauto with arith. + simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2; case_eq (build_var vm2 (Lit.blit c)); try discriminate; intros [vm3 f3] Heq3 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; destruct (Hbv _ _ _ _ Heq3 H8) as [H13 [H14 [H15 [H16 H17]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split. + intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith. + assert (H18: (Pos.to_nat (fst vm1) <= Pos.to_nat (fst vm3))%nat) by eauto with smtcoq_core arith. split. - case (Lit.is_pos a); case (Lit.is_pos b); case (Lit.is_pos c); simpl; rewrite H16; rewrite (bounded_bformula_le _ _ H14 _ H11); rewrite (bounded_bformula_le _ _ H18 _ H6); auto. - simpl; rewrite (interp_bformula_le _ _ H15 _ H11) in H12; rewrite (interp_bformula_le _ vm3) in H7; [ |intros p Hp; rewrite H10; eauto with arith|auto]; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; case_eq (Lit.is_pos c); intro Hc; unfold Lit.interp; rewrite Ha, Hb, Hc; simpl; rewrite <- H17; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); [case (Var.interp rho (Lit.blit b))|case (Var.interp rho (Lit.blit c))]); split; auto; try discriminate; try (intros [[H20 H21]|[H20 H21]]; auto); try (intros _; left; split; auto; discriminate); try (intros _; right; split; auto; discriminate); try (elim H20; discriminate); try (elim H21; discriminate); try (simpl; intro H; left; split; auto; discriminate); try (revert H; case (Var.interp rho (Lit.blit c)); discriminate); try (revert H; case (Var.interp rho (Lit.blit b)); discriminate); try (intro H20; rewrite H20 in H; discriminate); simpl. - intro H; right; split; auto. - intro H; right; split; auto. - intro H; right; split; auto. + case (Lit.is_pos a); case (Lit.is_pos b); case (Lit.is_pos c); simpl; rewrite H16; rewrite (bounded_bformula_le _ _ H14 _ H11); rewrite (bounded_bformula_le _ _ H18 _ H6); auto with smtcoq_core. + simpl; rewrite (interp_bformula_le _ _ H15 _ H11) in H12; rewrite (interp_bformula_le _ vm3) in H7; [ |intros p Hp; rewrite H10; eauto with smtcoq_core arith|auto with smtcoq_core]; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; case_eq (Lit.is_pos c); intro Hc; unfold Lit.interp; rewrite Ha, Hb, Hc; simpl; rewrite <- H17; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); [case (Var.interp rho (Lit.blit b))|case (Var.interp rho (Lit.blit c))]); split; auto with smtcoq_core; try discriminate; try (intros [[H20 H21]|[H20 H21]]; auto with smtcoq_core); try (intros _; left; split; auto with smtcoq_core; discriminate); try (intros _; right; split; auto with smtcoq_core; discriminate); try (elim H20; discriminate); try (elim H21; discriminate); try (simpl; intro H; left; split; auto with smtcoq_core; discriminate); try (revert H; case (Var.interp rho (Lit.blit c)); discriminate); try (revert H; case (Var.interp rho (Lit.blit b)); discriminate); try (intro H20; rewrite H20 in H; discriminate); simpl. + intro H; right; split; auto with smtcoq_core. + intro H; right; split; auto with smtcoq_core. + intro H; right; split; auto with smtcoq_core. intro H20; rewrite H20 in H; discriminate. - revert H21; case (Var.interp rho (Lit.blit c)); auto. - right; split; auto; intro H20; rewrite H20 in H; discriminate. - revert H21; case (Var.interp rho (Lit.blit c)); auto. - intro H; right; split; auto. - intro H; right; split; auto. + revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core. + right; split; auto with smtcoq_core; intro H20; rewrite H20 in H; discriminate. + revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core. + intro H; right; split; auto with smtcoq_core. + intro H; right; split; auto with smtcoq_core. intro H; left; split; try discriminate; revert H; case (Var.interp rho (Lit.blit b)); discriminate. - revert H21; case (Var.interp rho (Lit.blit b)); auto. + revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core. intro H; left; split; try discriminate; revert H; case (Var.interp rho (Lit.blit b)); discriminate. - revert H21; case (Var.interp rho (Lit.blit b)); auto. - intro H; right; split; auto; revert H; case (Var.interp rho (Lit.blit c)); discriminate. - revert H21; case (Var.interp rho (Lit.blit c)); auto. - intro H; right; split; auto; revert H; case (Var.interp rho (Lit.blit c)); discriminate. - revert H21; case (Var.interp rho (Lit.blit c)); auto. - intro H; left; split; auto; revert H; case (Var.interp rho (Lit.blit b)); discriminate. - revert H21; case (Var.interp rho (Lit.blit b)); auto. - intro H; left; split; auto; revert H; case (Var.interp rho (Lit.blit b)); discriminate. - revert H21; case (Var.interp rho (Lit.blit b)); auto. + revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core. + intro H; right; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit c)); discriminate. + revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core. + intro H; right; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit c)); discriminate. + revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core. + intro H; left; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit b)); discriminate. + revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core. + intro H; left; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit b)); discriminate. + revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core. Qed. @@ -1251,8 +1225,8 @@ Transparent build_z_atom. Proof. unfold build_var; apply foldi_down_cont_ind; try discriminate. intros i cont _ Hlen Hrec v vm vm' bf; unfold is_true; intros H1 H2; replace (Var.interp rho v) with (Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[v])). - apply (build_hform_correct cont); auto. - unfold Var.interp; rewrite <- wf_interp_form; auto. + apply (build_hform_correct cont); auto with smtcoq_core. + unfold Var.interp; rewrite <- wf_interp_form; auto with smtcoq_core. Qed. @@ -1285,17 +1259,17 @@ Transparent build_z_atom. unfold build_nlit; intros l vm vm' bf; case_eq (build_form vm (t_form .[ Lit.blit (Lit.neg l)])); try discriminate. intros [vm1 f] Heq H1 H2; inversion H1; subst vm1; subst bf; case_eq (Lit.is_pos (Lit.neg l)); intro Heq2. replace (negb (Lit.interp rho l)) with (Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form .[ Lit.blit (Lit.neg l)])). - apply build_form_correct; auto. + apply build_form_correct; auto with smtcoq_core. unfold Lit.interp; replace (Lit.is_pos l) with false. - rewrite negb_involutive; unfold Var.interp; rewrite <- wf_interp_form; auto; rewrite Lit.blit_neg; auto. - rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate. - simpl; destruct (build_form_correct (t_form .[ Lit.blit (Lit.neg l)]) vm vm' f Heq H2) as [H3 [H4 [H5 [H6 [H7 H8]]]]]; do 4 (split; auto); split. + rewrite negb_involutive; unfold Var.interp; rewrite <- wf_interp_form; auto with smtcoq_core; rewrite Lit.blit_neg; auto with smtcoq_core. + rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto with smtcoq_core; intro H; rewrite H in Heq2; discriminate. + simpl; destruct (build_form_correct (t_form .[ Lit.blit (Lit.neg l)]) vm vm' f Heq H2) as [H3 [H4 [H5 [H6 [H7 H8]]]]]; do 4 (split; auto with smtcoq_core); split. intros H9 H10; pose (H11 := H8 H10); unfold Lit.interp in H9; replace (Lit.is_pos l) with true in H9. - unfold Var.interp in H9; rewrite <- wf_interp_form in H11; auto; rewrite Lit.blit_neg in H11; rewrite H11 in H9; discriminate. - rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate. - intro H9; case_eq (Lit.interp rho l); intro Heq3; auto; elim H9; apply H7; unfold Lit.interp in Heq3; replace (Lit.is_pos l) with true in Heq3. - unfold Var.interp in Heq3; rewrite <- wf_interp_form; auto; rewrite Lit.blit_neg; auto. - rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate. + unfold Var.interp in H9; rewrite <- wf_interp_form in H11; auto with smtcoq_core; rewrite Lit.blit_neg in H11; rewrite H11 in H9; discriminate. + rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto with smtcoq_core; intro H; rewrite H in Heq2; discriminate. + intro H9; case_eq (Lit.interp rho l); intro Heq3; auto with smtcoq_core; elim H9; apply H7; unfold Lit.interp in Heq3; replace (Lit.is_pos l) with true in Heq3. + unfold Var.interp in Heq3; rewrite <- wf_interp_form; auto with smtcoq_core; rewrite Lit.blit_neg; auto with smtcoq_core. + rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto with smtcoq_core; intro H; rewrite H in Heq2; discriminate. Qed. @@ -1403,7 +1377,7 @@ Transparent build_z_atom. rewrite H0, def_t_atom;discriminate. apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2. rewrite !andb_true_iff in H2;decompose [and] H2;clear H2. - apply Hf with (2:= H0);trivial. auto. + apply Hf with (2:= H0);trivial. auto with smtcoq_core. rewrite wf_interp_form, H;simpl. unfold Atom.interp_form_hatom, Atom.interp_hatom at 1;simpl. rewrite Atom.t_interp_wf, H0;simpl;trivial. @@ -1434,7 +1408,7 @@ Transparent build_z_atom. rewrite H0, def_t_atom;discriminate. apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2. rewrite !andb_true_iff in H2;decompose [and] H2;clear H2. - simpl; apply Hf with (2:= H0);trivial. auto. + simpl; apply Hf with (2:= H0);trivial. auto with smtcoq_core. rewrite wf_interp_form, H;simpl. unfold Atom.interp_form_hatom, Atom.interp_hatom at 1;simpl. rewrite Atom.t_interp_wf, H0;simpl;trivial. @@ -1480,7 +1454,7 @@ Transparent build_z_atom. case_eq (build_clause empty_vmap cl). intros (vm1, bf) Heq. destruct (build_clause_correct _ _ _ _ Heq). - red;simpl;auto. + red;simpl;auto with smtcoq_core. decompose [and] H0. case_eq (ZTautoChecker bf c);intros Heq2. unfold C.valid;rewrite H5. @@ -1512,11 +1486,11 @@ Transparent build_z_atom. rewrite wf_interp_form, H;simpl. case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])). intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19. - apply (afold_left_orb_true int 0); subst; auto. + apply (afold_left_orb_true int 0); subst; auto with smtcoq_core. apply ltb_spec;rewrite H0;compute;trivial. - apply (afold_left_orb_true int 1); auto. + apply (afold_left_orb_true int 1); auto with smtcoq_core. apply ltb_spec;rewrite H0;compute;trivial. - apply (afold_left_orb_true int 2); auto. + apply (afold_left_orb_true int 2); auto with smtcoq_core. apply ltb_spec;rewrite H0;compute;trivial. intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19. unfold Lit.interp in H19. @@ -1534,7 +1508,7 @@ Transparent build_z_atom. destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) Typ.TZ) as [H12|H12]; [intros _|discriminate]. generalize H6. clear H6. destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) t) as [H6|H6]; [intros _|discriminate]. - rewrite <- H6. auto. + rewrite <- H6. auto with smtcoq_core. rewrite H26 in H19. case_eq (interp_atom (t_atom .[ b1])); intros t1 v1 Heq1. assert (H50: t1 = Typ.TZ). @@ -1560,11 +1534,11 @@ Transparent build_z_atom. rewrite wf_interp_form, H;simpl. case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])). intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19. - apply (afold_left_orb_true int 0); auto. + apply (afold_left_orb_true int 0); auto with smtcoq_core. apply ltb_spec;rewrite H0;compute;trivial. - apply (afold_left_orb_true int 1); auto. + apply (afold_left_orb_true int 1); auto with smtcoq_core. apply ltb_spec;rewrite H0;compute;trivial. - apply (afold_left_orb_true int 2); auto. + apply (afold_left_orb_true int 2); auto with smtcoq_core. apply ltb_spec;rewrite H0;compute;trivial. intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19. unfold Lit.interp in H19. @@ -1581,7 +1555,7 @@ Transparent build_z_atom. unfold Var.interp in H23; rewrite H10 in H23. rewrite <-H22, <- H20 in H21. assert (t = Typ.TZ). - rewrite Typ.eqb_spec in H6; rewrite Typ.eqb_spec in H18; subst; auto. + rewrite Typ.eqb_spec in H6; rewrite Typ.eqb_spec in H18; subst; auto with smtcoq_core. rewrite H26 in H19. case_eq (interp_atom (t_atom .[ b0])); intros t1 v1 Heq1. assert (H50: t1 = Typ.TZ). diff --git a/src/spl/Arithmetic.v b/src/spl/Arithmetic.v index 05c999d..3f5cd16 100644 --- a/src/spl/Arithmetic.v +++ b/src/spl/Arithmetic.v @@ -63,8 +63,6 @@ Section Arith. Let wf_rho : Valuation.wf rho. Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto. Qed. - Hint Immediate wf_rho. - Lemma valid_check_spl_arith : forall orig, C.valid rho orig -> @@ -76,7 +74,7 @@ Section Arith. (* List with one element *) intros H res l; case_eq (build_clause Lia.empty_vmap (Lit.neg li :: res :: nil)); [ |intros; apply C.interp_true; auto]. intros (vm1, bf) Heq; destruct (Lia.build_clause_correct _ _ _ t_func ch_atom ch_form wt_t_atom _ _ _ _ Heq) as [H1 H0]. - red; simpl; auto. + red; simpl; auto with smtcoq_core. decompose [and] H0; case_eq (ZTautoChecker bf l); [intros Heq3|intros; apply C.interp_true; auto]. unfold C.valid; replace (C.interp rho (res :: nil)) with (C.interp rho (Lit.neg li :: res :: nil)). rewrite H6; apply ZTautoChecker_sound with l;trivial. diff --git a/src/spl/Operators.v b/src/spl/Operators.v index f0aba15..fb3e379 100644 --- a/src/spl/Operators.v +++ b/src/spl/Operators.v @@ -279,28 +279,28 @@ intros. destruct H0; now contradict H0. Lemma wf_t_form : wf t_form. Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[_ H] _]; auto. Qed. - Local Hint Immediate wf_t_atom default_t_atom default_t_form wf_t_form. + Local Hint Immediate wf_t_atom default_t_atom default_t_form wf_t_form : smtcoq_spl_op. Lemma interp_check_distinct : forall ha diseq, check_distinct ha diseq = true -> interp_form_hatom ha = afold_left bool int true andb (Lit.interp rho) diseq. Proof. - intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H2]]]; rewrite check_diseqs_spec in H2; destruct H2 as [H2 H3]; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl. + intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H2]]]; rewrite check_diseqs_spec in H2; destruct H2 as [H2 H3]; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl. intros l H4; case_eq (distinct (Typ.i_eqb t_i A) (rev l)). - rewrite distinct_spec; intro H5; symmetry; apply afold_left_andb_true; intros i Hi; destruct (H2 _ Hi) as [H9 [a [H10 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite H10; simpl; rewrite Atom.t_interp_wf; auto; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H11: a < length t_atom). - case_eq (a < length t_atom); auto; intro H11; rewrite (get_outofbound _ _ _ H11) in H6; rewrite default_t_atom in H6; inversion H6. - generalize (wt_t_atom _ H11); rewrite H6; simpl; rewrite !andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h1) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h1) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h2) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h2) A)); rewrite !Typ.eqb_spec; intros [[_ H13] H12]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h1); rewrite H13; intros [v1 HH1]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h2); rewrite H12; intros [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; simpl; destruct H8 as [H8|H8]; [ |rewrite Typ.i_eqb_sym]; rewrite H5; auto; rewrite H4; [exists h2; exists h1|exists h1; exists h2]; auto. - rewrite distinct_false_spec; intros [v2 [v1 [H5 H6]]]; rewrite H4 in H5; destruct H5 as [a [b [H5 [H7 H8]]]]; clear H4; change (Typ.i_eqb t_i A v2 v1 = true) with (is_true (Typ.i_eqb t_i A v2 v1)) in H6; rewrite Typ.i_eqb_spec in H6; subst v2; clear H2; destruct (H3 _ _ H5) as [i [H2 [H4 [hb [H6 [H9 H10]]]]]]; clear H3; symmetry; apply (afold_left_andb_false _ i); auto; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite H6; simpl; rewrite Atom.t_interp_wf; auto; destruct H10 as [H10|H10]; rewrite H10; simpl; rewrite H7, H8; simpl; rewrite Typ.cast_refl; simpl; replace (Typ.i_eqb t_i A v1 v1) with true; auto; symmetry; change (is_true (Typ.i_eqb t_i A v1 v1)); rewrite Typ.i_eqb_spec; auto. + rewrite distinct_spec; intro H5; symmetry; apply afold_left_andb_true; intros i Hi; destruct (H2 _ Hi) as [H9 [a [H10 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H10; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H11: a < length t_atom). + case_eq (a < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H11; rewrite (get_outofbound _ _ _ H11) in H6; rewrite default_t_atom in H6; inversion H6. + generalize (wt_t_atom _ H11); rewrite H6; simpl; rewrite !andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h1) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h1) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h2) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h2) A)); rewrite !Typ.eqb_spec; intros [[_ H13] H12]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h1); rewrite H13; intros [v1 HH1]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h2); rewrite H12; intros [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; simpl; destruct H8 as [H8|H8]; [ |rewrite Typ.i_eqb_sym]; rewrite H5; auto with smtcoq_spl_op smtcoq_core; rewrite H4; [exists h2; exists h1|exists h1; exists h2]; auto with smtcoq_spl_op smtcoq_core. + rewrite distinct_false_spec; intros [v2 [v1 [H5 H6]]]; rewrite H4 in H5; destruct H5 as [a [b [H5 [H7 H8]]]]; clear H4; change (Typ.i_eqb t_i A v2 v1 = true) with (is_true (Typ.i_eqb t_i A v2 v1)) in H6; rewrite Typ.i_eqb_spec in H6; subst v2; clear H2; destruct (H3 _ _ H5) as [i [H2 [H4 [hb [H6 [H9 H10]]]]]]; clear H3; symmetry; apply (afold_left_andb_false _ i); auto with smtcoq_spl_op smtcoq_core; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; destruct H10 as [H10|H10]; rewrite H10; simpl; rewrite H7, H8; simpl; rewrite Typ.cast_refl; simpl; replace (Typ.i_eqb t_i A v1 v1) with true; auto with smtcoq_spl_op smtcoq_core; symmetry; change (is_true (Typ.i_eqb t_i A v1 v1)); rewrite Typ.i_eqb_spec; auto with smtcoq_spl_op smtcoq_core. intros [a [H20 H21]]; assert (H4: ha < length t_atom). - case_eq (ha < length t_atom); auto; intro Heq; generalize H1; rewrite get_outofbound; auto; rewrite default_t_atom; discriminate. - unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; generalize (wt_t_atom _ H4); rewrite H1; simpl; rewrite andb_true_iff, forallb_forall; intros [_ H5]; assert (H6 := H5 _ H20); generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a); intros [va Ha]; rewrite Ha in H21; simpl in H21; elim H21; apply Typ.eqb_spec; auto. + case_eq (ha < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate. + unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; generalize (wt_t_atom _ H4); rewrite H1; simpl; rewrite andb_true_iff, forallb_forall; intros [_ H5]; assert (H6 := H5 _ H20); generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a); intros [va Ha]; rewrite Ha in H21; simpl in H21; elim H21; apply Typ.eqb_spec; auto with smtcoq_spl_op smtcoq_core. Qed. Lemma interp_check_distinct_two_args : forall f1 f2, check_distinct_two_args f1 f2 = true -> rho f1 = negb (rho f2). Proof. - intros f1 f2; rewrite check_distinct_two_args_spec; intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; unfold Form.interp_state_var; assert (H5: f1 < length t_form) by (case_eq (f1 < length t_form); auto; intro Heq; generalize H1; rewrite get_outofbound; auto; rewrite default_t_form; discriminate); assert (H6: f2 < length t_form) by (case_eq (f2 < length t_form); auto; intro Heq; generalize H2; rewrite get_outofbound; auto; rewrite default_t_form; discriminate); rewrite !Form.t_interp_wf; auto; rewrite H1, H2; simpl; unfold Atom.interp_form_hatom, Atom.interp_hatom; rewrite !Atom.t_interp_wf; auto; rewrite H3, H4; simpl; unfold Atom.wt,is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H7: hb < length t_atom) by (case_eq (hb < length t_atom); auto; intro Heq; generalize H4; rewrite get_outofbound; auto; rewrite default_t_atom; discriminate); generalize (wt_t_atom _ H7); rewrite H4; simpl; case (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) hb); try discriminate; simpl; rewrite andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A)); rewrite !Typ.eqb_spec; intros [H8 H9]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom x), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom y); rewrite H8, H9; intros [v1 HH1] [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; auto; rewrite Typ.i_eqb_sym; auto. + intros f1 f2; rewrite check_distinct_two_args_spec; intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; unfold Form.interp_state_var; assert (H5: f1 < length t_form) by (case_eq (f1 < length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); assert (H6: f2 < length t_form) by (case_eq (f2 < length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H2; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); rewrite !Form.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H1, H2; simpl; unfold Atom.interp_form_hatom, Atom.interp_hatom; rewrite !Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H3, H4; simpl; unfold Atom.wt,is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H7: hb < length t_atom) by (case_eq (hb < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H4; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate); generalize (wt_t_atom _ H7); rewrite H4; simpl; case (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) hb); try discriminate; simpl; rewrite andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A)); rewrite !Typ.eqb_spec; intros [H8 H9]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom x), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom y); rewrite H8, H9; intros [v1 HH1] [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; auto with smtcoq_spl_op smtcoq_core; rewrite Typ.i_eqb_sym; auto with smtcoq_spl_op smtcoq_core. Qed. @@ -308,13 +308,13 @@ intros. destruct H0; now contradict H0. (* check_distinct ha diseq -> *) (* interp_form_hatom ha -> afold_left bool int true andb (Lit.interp rho) diseq. *) (* Proof. *) - (* intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H]]]; rewrite check_diseqs_spec in H; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl. *) - (* intros l H2; unfold is_true; rewrite distinct_spec; intro H3; apply afold_left_andb_true; intros i Hi; destruct (H _ Hi) as [H4 [a [H5 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite H5; simpl; rewrite Atom.t_interp_wf; auto; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H10: a < length t_atom). *) - (* case_eq (a < length t_atom); auto; intro H10; rewrite (get_outofbound _ _ _ H10) in H6; rewrite default_t_atom in H6; inversion H6. *) - (* generalize (wt_t_atom _ H10); rewrite H6; simpl; rewrite !andb_true_iff. change (Typ.eqb (Atom.get_type t_i t_func t_atom h1) A = true) with (is_true (Typ.eqb (Atom.get_type t_i t_func t_atom h1) A)); change (Typ.eqb (Atom.get_type t_i t_func t_atom h2) A = true) with (is_true (Typ.eqb (Atom.get_type t_i t_func t_atom h2) A)); rewrite !Typ.eqb_spec; intros [[_ H11] H12]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h1); rewrite H11; intros [v1 HH1]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h2); rewrite H12; intros [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; simpl; destruct H8 as [H8|H8]; [ |rewrite Typ.i_eqb_sym]; rewrite H3; auto; rewrite H2; [exists h2; exists h1|exists h1; exists h2]; auto. *) + (* intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H]]]; rewrite check_diseqs_spec in H; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl. *) + (* intros l H2; unfold is_true; rewrite distinct_spec; intro H3; apply afold_left_andb_true; intros i Hi; destruct (H _ Hi) as [H4 [a [H5 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H5; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H10: a < length t_atom). *) + (* case_eq (a < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H10; rewrite (get_outofbound _ _ _ H10) in H6; rewrite default_t_atom in H6; inversion H6. *) + (* generalize (wt_t_atom _ H10); rewrite H6; simpl; rewrite !andb_true_iff. change (Typ.eqb (Atom.get_type t_i t_func t_atom h1) A = true) with (is_true (Typ.eqb (Atom.get_type t_i t_func t_atom h1) A)); change (Typ.eqb (Atom.get_type t_i t_func t_atom h2) A = true) with (is_true (Typ.eqb (Atom.get_type t_i t_func t_atom h2) A)); rewrite !Typ.eqb_spec; intros [[_ H11] H12]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h1); rewrite H11; intros [v1 HH1]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h2); rewrite H12; intros [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; simpl; destruct H8 as [H8|H8]; [ |rewrite Typ.i_eqb_sym]; rewrite H3; auto with smtcoq_spl_op smtcoq_core; rewrite H2; [exists h2; exists h1|exists h1; exists h2]; auto with smtcoq_spl_op smtcoq_core. *) (* intros [a [H2 H3]] _; assert (H4: ha < length t_atom). *) - (* case_eq (ha < length t_atom); auto; intro Heq; generalize H1; rewrite get_outofbound; auto; rewrite default_t_atom; discriminate. *) - (* unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; generalize (wt_t_atom _ H4); rewrite H1; simpl; rewrite andb_true_iff, forallb_forall; intros [_ H5]; assert (H6 := H5 _ H2); generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a); intros [va Ha]; rewrite Ha in H3; simpl in H3; elim H3; apply Typ.eqb_spec; auto. *) + (* case_eq (ha < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate. *) + (* unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; generalize (wt_t_atom _ H4); rewrite H1; simpl; rewrite andb_true_iff, forallb_forall; intros [_ H5]; assert (H6 := H5 _ H2); generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a); intros [va Ha]; rewrite Ha in H3; simpl in H3; elim H3; apply Typ.eqb_spec; auto with smtcoq_spl_op smtcoq_core. *) (* Qed. *) End Valid1. @@ -382,18 +382,18 @@ intros. destruct H0; now contradict H0. check_lit l1 l2 -> Lit.interp rho l1 = Lit.interp rho l2. Proof. unfold check_lit; intros l1 l2; unfold is_true; rewrite !orb_true_iff, !andb_true_iff; intros [[H1|[H1 H2]]|[H1 H2]]. - rewrite eqb_spec in H1; rewrite H1; auto. - rewrite Bool.eqb_true_iff in H1; unfold Lit.interp; rewrite H1, (interp_check_var _ _ H2); auto. - generalize H1; unfold Lit.interp; case (Lit.is_pos l1); case (Lit.is_pos l2); try discriminate; intros _; unfold Var.interp; rewrite (interp_check_distinct_two_args _ t_func ch_atom ch_form wt_t_atom _ _ H2); auto; case (rho (Lit.blit l2)); auto. + rewrite eqb_spec in H1; rewrite H1; auto with smtcoq_core. + rewrite Bool.eqb_true_iff in H1; unfold Lit.interp; rewrite H1, (interp_check_var _ _ H2); auto with smtcoq_core. + generalize H1; unfold Lit.interp; case (Lit.is_pos l1); case (Lit.is_pos l2); try discriminate; intros _; unfold Var.interp; rewrite (interp_check_distinct_two_args _ t_func ch_atom ch_form wt_t_atom _ _ H2); auto with smtcoq_core; case (rho (Lit.blit l2)); auto with smtcoq_core. Qed. (* Lemma interp_check_lit : forall l1 l2, *) (* check_lit l1 l2 -> Lit.interp rho l1 -> Lit.interp rho l2 = true. *) (* Proof. *) (* unfold check_lit; intros l1 l2; unfold is_true; rewrite !orb_true_iff, !andb_true_iff; intros [[H1|[[H1 H2] H3]]|[[H1 H2] H3]]. *) - (* rewrite Int63Properties.eqb_spec in H1; subst l1; auto. *) - (* unfold Lit.interp; rewrite H1, H2; apply interp_check_var; auto. *) - (* unfold Lit.interp; case_eq (Lit.is_pos l1); intro Heq; rewrite Heq in H1; try discriminate; clear Heq H1; case_eq (Lit.is_pos l2); intro Heq; rewrite Heq in H2; try discriminate; clear Heq H2; case_eq (Var.interp rho (Lit.blit l1)); try discriminate; intros H4 _; case_eq (Var.interp rho (Lit.blit l2)); auto; intro H5; rewrite (interp_check_var _ _ H3 H5) in H4; discriminate. *) + (* rewrite Int63Properties.eqb_spec in H1; subst l1; auto with smtcoq_core. *) + (* unfold Lit.interp; rewrite H1, H2; apply interp_check_var; auto with smtcoq_core. *) + (* unfold Lit.interp; case_eq (Lit.is_pos l1); intro Heq; rewrite Heq in H1; try discriminate; clear Heq H1; case_eq (Lit.is_pos l2); intro Heq; rewrite Heq in H2; try discriminate; clear Heq H2; case_eq (Var.interp rho (Lit.blit l1)); try discriminate; intros H4 _; case_eq (Var.interp rho (Lit.blit l2)); auto with smtcoq_core; intro H5; rewrite (interp_check_var _ _ H3 H5) in H4; discriminate. *) (* Qed. *) (* Local Hint Resolve interp_check_lit. *) @@ -402,72 +402,72 @@ intros. destruct H0; now contradict H0. check_form_aux a b -> Form.interp interp_form_hatom interp_form_hatom_bv t_form a = Form.interp interp_form_hatom interp_form_hatom_bv t_form b. Proof. - intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3|a l1] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3|b m1]; simpl; try discriminate;auto. + intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3|a l1] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3|b m1]; simpl; try discriminate;auto with smtcoq_core. (* Atom *) - unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto. + unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto with smtcoq_core. (* Interesting case *) - apply interp_check_distinct; auto. + apply interp_check_distinct; auto with smtcoq_core. (* Double negation *) - unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; subst j1. rewrite (interp_check_lit _ _ H2). auto. + unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; subst j1. rewrite (interp_check_lit _ _ H2). auto with smtcoq_core. (* Conjunction *) - unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto; intros i Hi; apply interp_check_lit; auto. + unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto with smtcoq_core; intros i Hi; apply interp_check_lit; auto with smtcoq_core. (* Disjunction *) - unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto; intros i Hi; apply interp_check_lit; auto. + unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto with smtcoq_core; intros i Hi; apply interp_check_lit; auto with smtcoq_core. (* Implication *) - unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_right_eq; auto; intros i Hi; apply interp_check_lit; auto. + unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_right_eq; auto with smtcoq_core; intros i Hi; apply interp_check_lit; auto with smtcoq_core. (* Xor *) - unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto. + unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto with smtcoq_core. (* Iff *) - unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto. + unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto with smtcoq_core. (* Ite *) - unfold is_true; rewrite !andb_true_iff; intros [[H1 H2] H3]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2), (interp_check_lit _ _ H3); auto. + unfold is_true; rewrite !andb_true_iff; intros [[H1 H2] H3]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2), (interp_check_lit _ _ H3); auto with smtcoq_core. Qed. (* Lemma interp_check_lit_equiv : forall l1 l2, *) (* check_lit l1 l2 -> check_lit l2 l1 -> *) (* Lit.interp rho l1 = Lit.interp rho l2. *) (* Proof. *) - (* intros l1 l2 H1 H2; generalize (interp_check_lit _ _ H1) (interp_check_lit _ _ H2); case (Lit.interp rho l1); case (Lit.interp rho l2); auto; symmetry; auto. *) + (* intros l1 l2 H1 H2; generalize (interp_check_lit _ _ H1) (interp_check_lit _ _ H2); case (Lit.interp rho l1); case (Lit.interp rho l2); auto with smtcoq_core; symmetry; auto with smtcoq_core. *) (* Qed. *) (* Lemma interp_check_form_aux : forall a b, *) (* check_form_aux a b -> *) (* Form.interp interp_form_hatom t_form a -> Form.interp interp_form_hatom t_form b. *) (* Proof. *) - (* intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3]; simpl; try discriminate;auto. *) + (* intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3]; simpl; try discriminate;auto with smtcoq_core. *) (* (* Atom *) *) - (* unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto. *) + (* unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto with smtcoq_core. *) (* (* Interesting case *) *) - (* apply interp_check_distinct; auto. *) + (* apply interp_check_distinct; auto with smtcoq_core. *) (* (* Double negation *) *) (* unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; subst j1; apply (fold_ind2 _ _ (fun x y => x = true -> y = true)). *) - (* apply interp_check_lit; auto. *) - (* intros a b; case a; try discriminate; intros H _; rewrite H; auto. *) + (* apply interp_check_lit; auto with smtcoq_core. *) + (* intros a b; case a; try discriminate; intros H _; rewrite H; auto with smtcoq_core. *) (* (* Conjunction *) *) - (* unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite forallbi_spec in H2; intro H3; assert (H4 := afold_left_andb_true_inv _ _ _ H3); clear H3; apply afold_left_andb_true; rewrite <- H1; intros i Hi; eapply interp_check_lit; eauto. *) + (* unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite forallbi_spec in H2; intro H3; assert (H4 := afold_left_andb_true_inv _ _ _ H3); clear H3; apply afold_left_andb_true; rewrite <- H1; intros i Hi; eapply interp_check_lit; eauto with smtcoq_core. *) (* (* Disjunction *) *) (* unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite forallbi_spec in H2; intro H3; assert (H4 := afold_left_orb_true_inv _ _ _ H3); clear H3; destruct H4 as [i [H3 H4]]; eapply afold_left_orb_true. *) - (* rewrite <- H1; eauto. *) - (* eapply interp_check_lit; eauto. *) + (* rewrite <- H1; eauto with smtcoq_core. *) + (* eapply interp_check_lit; eauto with smtcoq_core. *) (* (* Implication *) *) (* unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite forallbi_spec in H2; intro H3; apply afold_right_implb_true; case_eq (length a1 == 0); intro Heq. *) - (* left; rewrite eqb_spec in Heq; rewrite <- H1; auto. *) + (* left; rewrite eqb_spec in Heq; rewrite <- H1; auto with smtcoq_core. *) (* destruct (afold_right_implb_true_inv _ _ _ H3) as [H4|[[i [H4 H5]]|H4]]. *) (* rewrite H4 in Heq; discriminate. *) - (* right; left; exists i; rewrite <- H1; split; auto; case_eq (Lit.interp rho (a2 .[ i])); auto; intro H6; assert (H7: i < length a1 = true). *) - (* rewrite ltb_spec in *; rewrite eqb_false_spec in Heq; rewrite to_Z_sub_1_diff in H4; auto; omega. *) - (* generalize (H2 _ H7); rewrite H4; intro H8; rewrite (interp_check_lit _ _ H8 H6) in H5; auto. *) + (* right; left; exists i; rewrite <- H1; split; auto with smtcoq_core; case_eq (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; intro H6; assert (H7: i < length a1 = true). *) + (* rewrite ltb_spec in *; rewrite eqb_false_spec in Heq; rewrite to_Z_sub_1_diff in H4; auto with smtcoq_core; omega. *) + (* generalize (H2 _ H7); rewrite H4; intro H8; rewrite (interp_check_lit _ _ H8 H6) in H5; auto with smtcoq_core. *) (* right; case_eq (existsbi (fun i l => (i < length a2 - 1) && (negb (Lit.interp rho l))) a2). *) - (* rewrite existsbi_spec; intros [i [_ H5]]; rewrite andb_true_iff in H5; destruct H5 as [H5 H6]; left; exists i; split; auto; generalize H6; case (Lit.interp rho (a2 .[ i])); auto; discriminate. *) + (* rewrite existsbi_spec; intros [i [_ H5]]; rewrite andb_true_iff in H5; destruct H5 as [H5 H6]; left; exists i; split; auto with smtcoq_core; generalize H6; case (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; discriminate. *) (* rewrite existsbi_false_spec; intro H; right; intros i Hi; assert (Hi' := Hi); rewrite <- H1 in Hi'; generalize (H2 _ Hi') (H _ Hi); rewrite <- H1; case (i < length a1 - 1); simpl. *) - (* intros _; case (Lit.interp rho (a2 .[ i])); auto; discriminate. *) - (* intros H5 _; apply (interp_check_lit _ _ H5); apply H4; auto. *) + (* intros _; case (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; discriminate. *) + (* intros H5 _; apply (interp_check_lit _ _ H5); apply H4; auto with smtcoq_core. *) (* (* Xor *) *) - (* unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto. *) + (* unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto with smtcoq_core. *) (* (* Iff *) *) - (* unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto. *) + (* unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto with smtcoq_core. *) (* (* Ite *) *) - (* unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2); case (Lit.interp rho j1); apply interp_check_lit; auto. *) + (* unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2); case (Lit.interp rho j1); apply interp_check_lit; auto with smtcoq_core. *) (* Qed. *) End AUX. @@ -505,50 +505,46 @@ intros. destruct H0; now contradict H0. Let wf_rho : Valuation.wf rho. - Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto. Qed. + Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto with smtcoq_core. Qed. Let default_t_form : default t_form = Ftrue. - Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[H _] _]; auto. Qed. + Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[H _] _]; auto with smtcoq_core. Qed. Let wf_t_form : wf t_form. - Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[_ H] _]; auto. Qed. - - Local Hint Immediate wf_rho default_t_form wf_t_form. + Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[_ H] _]; auto with smtcoq_core. Qed. Lemma interp_check_hform : forall h1 h2, check_hform h1 h2 -> Var.interp rho h1 = Var.interp rho h2. Proof. unfold check_hform; apply foldi_down_cont_ind; try discriminate. intros i cont _ _ Hrec h1 h2. unfold is_true; rewrite orb_true_iff; intros [H|H]. - rewrite Int63Properties.eqb_spec in H; rewrite H; auto. - unfold Var.interp; rewrite !wf_interp_form; auto; eapply interp_check_form_aux; eauto. + rewrite Int63Properties.eqb_spec in H; rewrite H; auto with smtcoq_core. + unfold Var.interp; rewrite !wf_interp_form; auto with smtcoq_core; eapply interp_check_form_aux; eauto with smtcoq_core. Qed. - Local Hint Resolve interp_check_hform. - Lemma interp_check_form : forall a b, check_form a b -> Form.interp interp_form_hatom interp_form_hatom_bv t_form a = Form.interp interp_form_hatom interp_form_hatom_bv t_form b. - Proof. apply interp_check_form_aux, interp_check_hform; auto. Qed. + Proof. apply interp_check_form_aux, interp_check_hform; auto with smtcoq_core. Qed. Lemma interp_check_lit' : forall l res, check_lit' l res -> Lit.interp rho l = Lit.interp rho res. - Proof. apply interp_check_lit, interp_check_hform; auto. Qed. + Proof. apply interp_check_lit, interp_check_hform; auto with smtcoq_core. Qed. Lemma valid_check_distinct_elim : forall input, C.valid rho input -> forall res, C.valid rho (check_distinct_elim input res). Proof. - induction input as [ |l c IHc]; auto; simpl; unfold C.valid; simpl; rewrite orb_true_iff; intros [H|H] res. + induction input as [ |l c IHc]; auto with smtcoq_core; simpl; unfold C.valid; simpl; rewrite orb_true_iff; intros [H|H] res. case_eq (check_lit' l res); intro Heq; simpl. - rewrite <- (interp_check_lit' _ _ Heq), H; auto. - rewrite H; auto. + rewrite <- (interp_check_lit' _ _ Heq), H; auto with smtcoq_core. + rewrite H; auto with smtcoq_core. case (check_lit' l res). - simpl; rewrite H, orb_true_r; auto. - simpl; rewrite (IHc H), orb_true_r; auto. + simpl; rewrite H, orb_true_r; auto with smtcoq_core. + simpl; rewrite (IHc H), orb_true_r; auto with smtcoq_core. Qed. End Valid. diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index e116339..ee0dd96 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -14,6 +14,8 @@ trees *) +Declare Scope array_scope. + Require Import Int31. Require Export Int63. Require FMapAVL. diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v index a5a931b..abb91ee 100644 --- a/src/versions/standard/Int63/Int63Native_standard.v +++ b/src/versions/standard/Int63/Int63Native_standard.v @@ -20,6 +20,7 @@ Definition size := size. Notation int := int31. +Declare Scope int63_scope. Delimit Scope int63_scope with int. Bind Scope int63_scope with int. -- cgit