diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2020-07-06 12:40:48 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2020-07-06 12:40:48 +0200 |
| commit | 52621f58edcabc36e7d1cd10d9b4da8be1a08649 (patch) | |
| tree | de5831e7b1b0fb79fe459a819bbe2590e14a1682 | |
| parent | ea73755e6e1b7efea8db79b9fc0cf456ed5c640f (diff) | |
| parent | d7a33ad9b479317701eba7c787744599de134f78 (diff) | |
| download | smtcoq-52621f58edcabc36e7d1cd10d9b4da8be1a08649.tar.gz smtcoq-52621f58edcabc36e7d1cd10d9b4da8be1a08649.zip | |
Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.10
43 files changed, 896 insertions, 3223 deletions
@@ -15,13 +15,13 @@ you want to use. ## Requirements -You need to have OCaml version >= 4.04.0 and Coq version 8.9.0. +You need to have OCaml version >= 4.09.0 and Coq version 8.9.0. The easiest way to install these two pieces of software is through opam. > **Warning**: The version of Coq that you plan to use must have been compiled > with the same version of OCaml that you are going to use to compile > SMTCoq. In particular this means you want a version of Coq that was compiled -> with OCaml version >= 4.04.0. +> with OCaml version >= 4.09.0. If you want to use SMTCoq with high performance to check large proof certificates, you need to use the [version of Coq with native @@ -67,11 +67,10 @@ eval `opam config env` #### Install OCaml -Now you can install an OCaml compiler (we recommend 4.04.0 or the latest -release): +Now you can install an OCaml compiler (we recommend 4.09.0): ```bash -opam switch 4.04.0 +opam switch create ocaml-base-compiler.4.09.0 ``` #### Install Coq @@ -110,7 +109,7 @@ make install wget https://github.com/coq/coq/archive/V8.9.0.tar.gz ``` and compile it by following the instructions available in the - repository (make sure you use OCaml 4.04.0 for that). We recommand + repository (make sure you use OCaml 4.09.0 for that). We recommand that you do not install it, but only compile it in local: ```bash ./configure -local diff --git a/examples/Example.v b/examples/Example.v index 2d48776..7beed4a 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -11,7 +11,7 @@ (* [Require Import SMTCoq.SMTCoq.] loads the SMTCoq library. - If you are using native-coq instead of Coq 8.9, replace it with: + If you are using native-coq instead of Coq 8.10, replace it with: Require Import SMTCoq. *) diff --git a/examples/InsertionSort.v b/examples/InsertionSort.v index fcd5dfc..0f21e23 100644 --- a/examples/InsertionSort.v +++ b/examples/InsertionSort.v @@ -21,19 +21,19 @@ definitions - it requires too much from uninterpreted functions even when it is not needed - - it sometimes fails? (may be realted to the previous item) + - it sometimes fails (may be realted to the previous item) *) -Add Rec LoadPath "../src" as SMTCoq. - -Require Import SMTCoq. +Require Import SMTCoq.SMTCoq. Require Import ZArith List Bool. +Local Open Scope Z_scope. + -(* We should really make SMTCoq work with SSReflect! *) +(* This will improve when SMTCoq works with SSReflect! *) -Lemma impl_implb (a b:bool) : (a -> b) <-> (a --> b). +Lemma impl_implb (a b:bool) : (a -> b) <-> (a ---> b). Proof. auto using (reflect_iff _ _ (ReflectFacts.implyP a b)). Qed. @@ -76,20 +76,20 @@ Section InsertionSort. Lemma is_sorted_smaller x y ys : - (((x <=? y) && is_sorted (y :: ys)) --> is_sorted (x :: ys)). + (((x <=? y)%Z && is_sorted (y :: ys)) ---> is_sorted (x :: ys)). Proof. destruct ys as [ |z zs]. - simpl. smt. - change (is_sorted (y :: z :: zs)) with ((y <=? z)%Z && (is_sorted (z::zs))). change (is_sorted (x :: z :: zs)) with ((x <=? z)%Z && (is_sorted (z::zs))). (* [smt] or [verit] fail? *) - assert (H:forall b, (x <=? y) && ((y <=? z) && b) --> (x <=? z) && b) by smt. + assert (H:forall b, (x <=? y)%Z && ((y <=? z) && b) ---> (x <=? z) && b) by smt. apply H. Qed. Lemma is_sorted_cons x xs : - (is_sorted (x::xs)) <--> (is_sorted xs && smaller x xs). + (is_sorted (x::xs)) <---> (is_sorted xs && smaller x xs). Proof. induction xs as [ |y ys IHys]. - reflexivity. @@ -97,27 +97,27 @@ Section InsertionSort. change (smaller x (y :: ys)) with ((x <=? y)%Z && (smaller x ys)). generalize (is_sorted_smaller x y ys). revert IHys. rewrite !impl_implb. (* Idem *) - assert (H:forall a b c d, (a <--> b && c) --> - ((x <=? y) && d --> a) --> - ((x <=? y) && d <--> + assert (H:forall a b c d, (a <---> b && c) ---> + ((x <=? y) && d ---> a) ---> + ((x <=? y) && d <---> d && ((x <=? y) && c))) by smt. apply H. Qed. Lemma insert_keeps_smaller x y ys : - smaller y ys --> (y <=? x) --> smaller y (insert x ys). + smaller y ys ---> (y <=? x) ---> smaller y (insert x ys). Proof. induction ys as [ |z zs IHzs]. - simpl. smt. - simpl. case (x <=? z). + simpl. (* [smt] or [verit] require [Compec (list Z)] but they should not *) - assert (H:forall a, (y <=? z) && a --> (y <=? x) --> (y <=? x) && ((y <=? z) && a)) by smt. + assert (H:forall a, (y <=? z) && a ---> (y <=? x) ---> (y <=? x) && ((y <=? z) && a)) by smt. apply H. + simpl. revert IHzs. rewrite impl_implb. (* Idem *) - assert (H:forall a b, (a --> (y <=? x) --> b) --> (y <=? z) && a --> (y <=? x) --> (y <=? z) && b) by smt. + assert (H:forall a b, (a ---> (y <=? x) ---> b) ---> (y <=? z) && a ---> (y <=? x) ---> (y <=? z) && b) by smt. apply H. Qed. @@ -134,7 +134,7 @@ Section InsertionSort. generalize (insert_keeps_smaller x y ys). revert IHys H Heq. rewrite !impl_implb. (* Idem *) - assert (H: forall a b c d, (a --> b) --> a && c --> negb (x <=? y) --> (c --> (y <=? x) --> d) --> b && d) by smt. + assert (H: forall a b c d, (a ---> b) ---> a && c ---> negb (x <=? y) ---> (c ---> (y <=? x) ---> d) ---> b && d) by smt. apply H. Qed. diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md index b8d9d99..a61ec79 100644 --- a/src/BEST_PRACTICE.md +++ b/src/BEST_PRACTICE.md @@ -14,6 +14,9 @@ the project is named `smtcoq_core`. # Code organization +## Documentation +Every OCaml module comes with a documented interface. + ## Theories Theories are organized in sub-directories whose names are the names of diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v index ecf1be8..cb0c090 100644 --- a/src/Conversion_tactics.v +++ b/src/Conversion_tactics.v @@ -457,4 +457,4 @@ End nat_convert_type. Module nat_convert_mod := convert nat_convert_type. -Ltac nat_convert := fold Nat.add Nat.mul Nat.leb Nat.ltb Nat.eqb; nat_convert_mod.convert. +Ltac nat_convert := nat_convert_mod.convert. @@ -59,6 +59,18 @@ Proof. Qed. +Lemma minus_1_lt i : (i == 0) = false -> i - 1 < i = true. +Proof. + intro Hl. rewrite ltb_spec, (to_Z_sub_1 _ 0). + - lia. + - rewrite ltb_spec. rewrite eqb_false_spec in Hl. + assert (0%Z <> [|i|]) + by (change 0%Z with [|0|]; intro H; apply to_Z_inj in H; auto). + destruct (to_Z_bounded i) as [H1 _]. + clear -H H1. change [|0|] with 0%Z. lia. +Qed. + + Lemma foldi_down_ZInd2 : forall A (P: Z -> A -> Prop) (f:int -> A -> A) max min a, (max < min = true -> P ([|min|])%Z a) -> @@ -142,6 +154,12 @@ Proof. unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; lia. Qed. +Lemma to_list_In_eq : forall {A} (t: array A) i x, + i < length t = true -> x = t.[i] -> In x (to_list t). +Proof. + intros A t i x Hi ->. now apply to_list_In. +Qed. + Lemma In_to_list : forall {A} (t: array A) x, In x (to_list t) -> exists i, i < length t = true /\ x = t.[i]. Proof. @@ -495,6 +513,23 @@ Proof. Qed. +Lemma afold_left_and p a : + afold_left bool int true andb p a = + List.forallb p (to_list a). +Proof. + rewrite afold_left_spec; auto. + rewrite fold_left_to_list. + assert (H:forall l acc, List.fold_left (fun (a0 : bool) (v : int) => a0 && p v) l acc = + acc && List.forallb p l). + { + clear a. induction l; simpl. + - intros; now rewrite andb_true_r. + - intro acc. rewrite IHl. now rewrite andb_assoc. + } + now apply H. +Qed. + + (* Case orb *) Lemma afold_left_orb_true : forall A i a f, @@ -541,6 +576,23 @@ Proof. Qed. +Lemma afold_left_or p a : + afold_left bool int false orb p a = + List.existsb p (to_list a). +Proof. + rewrite afold_left_spec; auto. + rewrite fold_left_to_list. + assert (H:forall l acc, List.fold_left (fun (a0 : bool) (v : int) => a0 || p v) l acc = + acc || List.existsb p l). + { + clear a. induction l; simpl. + - intros; now rewrite orb_false_r. + - intro acc. rewrite IHl. now rewrite orb_assoc. + } + now apply H. +Qed. + + (* Case implb *) Lemma afold_right_implb_false : forall A a f, diff --git a/src/QInst.v b/src/QInst.v index 611973e..cb533ee 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -69,7 +69,7 @@ Ltac vauto := eapply impl_or_split_left; apply H end; apply H); - auto. + auto with smtcoq_core. diff --git a/src/State.v b/src/State.v index a3af611..4b0db6d 100644 --- a/src/State.v +++ b/src/State.v @@ -424,6 +424,13 @@ Module C. unfold valid, interp;destruct c;simpl; auto;discriminate. Qed. + Lemma Cinterp_neg rho cl : + interp rho (List.map Lit.neg cl) = negb (List.forallb (Lit.interp rho) cl). + Proof. + induction cl as [ |l cl IHcl]; auto. + simpl. now rewrite negb_andb, IHcl, Lit.interp_neg. + Qed. + End C. diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index 3a982b2..0540855 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -893,10 +893,6 @@ Section certif. apply read_over_other_write; now auto. Qed. - Axiom afold_left_or : forall a, - afold_left bool int false orb (Lit.interp rho) a = - C.interp rho (to_list a). - Lemma valid_check_ext lres : C.valid rho (check_ext lres). unfold check_ext, eq_sel_sym. case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true. diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 0f5bc1a..f066b54 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -1926,17 +1926,6 @@ Qed. Lemma eq_head: forall {A: Type} a b (l: list A), (a :: l) = (b :: l) <-> a = b. Proof. intros A a b l; split; [intros H; inversion H|intros ->]; auto. Qed. -Axiom afold_left_and : forall a, - afold_left bool int true andb (Lit.interp rho) a = List.forallb (Lit.interp rho) (to_list a). - - Axiom afold_left_or : forall a, - afold_left bool int false orb (Lit.interp rho) a = - C.interp rho (to_list a). - - Axiom afold_left_xor : forall a, - afold_left bool int false xorb (Lit.interp rho) a = - C.interp rho (to_list a). - Lemma eqb_spec : forall x y, (x == y) = true <-> x = y. Proof. split;auto using eqb_correct, eqb_complete. diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v index ec18c15..cc956b3 100644 --- a/src/cnf/Cnf.v +++ b/src/cnf/Cnf.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import PArray List Bool ZArith. +Require Import PArray List Bool ZArith Psatz. Require Import Misc State SMT_terms BVList. Import Form. @@ -53,6 +53,62 @@ Proof. rewrite ltb_spec, (to_Z_sub_1 _ _ Heq); omega. Qed. +Lemma afold_right_impb p a : + (forall x, p (Lit.neg x) = negb (p x)) -> + (PArray.length a == 0) = false -> + (afold_right bool int true implb p a) = + List.existsb p (to_list (or_of_imp a)). +Proof. + intros Hp Hl. + case_eq (afold_right bool int true implb p a); intro Heq; symmetry. + - apply afold_right_implb_true_inv in Heq. + destruct Heq as [Heq|[[i [Hi Heq]]|Heq]]. + + rewrite Heq in Hl. discriminate. + + rewrite existsb_exists. exists (Lit.neg (a .[ i])). split. + * { + apply (to_list_In_eq _ i). + - rewrite length_or_of_imp. apply (ltb_trans _ (PArray.length a - 1)); auto. + now apply minus_1_lt. + - now rewrite get_or_of_imp. + } + * now rewrite Hp, Heq. + + rewrite existsb_exists. exists (a.[(PArray.length a) - 1]). split. + * { + apply (to_list_In_eq _ (PArray.length a - 1)). + - rewrite length_or_of_imp. + now apply minus_1_lt. + - symmetry. apply get_or_of_imp2; auto. + unfold is_true. rewrite ltb_spec. rewrite eqb_false_spec in Hl. + assert (0%Z <> [|PArray.length a|]) + by (change 0%Z with [|0|]; intro H; apply to_Z_inj in H; auto). + destruct (to_Z_bounded (PArray.length a)) as [H1 _]. + clear -H H1. change [|0|] with 0%Z. lia. + } + * { + apply Heq. now apply minus_1_lt. + } + - apply afold_right_implb_false_inv in Heq. + destruct Heq as [H1 [H2 H3]]. + case_eq (existsb p (to_list (or_of_imp a))); auto. + rewrite existsb_exists. intros [x [H4 H5]]. + apply In_to_list in H4. destruct H4 as [i [H4 ->]]. + case_eq (i < PArray.length a - 1); intro Heq. + + assert (H6 := H2 _ Heq). now rewrite (get_or_of_imp Heq), Hp, H6 in H5. + + assert (H6:i = PArray.length a - 1). + { + clear -H4 Heq H1. + rewrite length_or_of_imp in H4. + apply to_Z_inj. rewrite (to_Z_sub_1 _ 0); auto. + rewrite ltb_spec in H4; auto. + rewrite ltb_negb_geb in Heq. + case_eq (PArray.length a - 1 <= i); intro H2; rewrite H2 in Heq; try discriminate. + clear Heq. rewrite leb_spec in H2. rewrite (to_Z_sub_1 _ 0) in H2; auto. + lia. + } + rewrite get_or_of_imp2 in H5; auto. + rewrite H6, H3 in H5. discriminate. +Qed. + Section CHECKER. @@ -91,6 +147,7 @@ Section CHECKER. else l :: PArray.to_list args | Fimp args => if Lit.is_pos l then C._true + else if PArray.length args == 0 then C._true else let args := or_of_imp args in l :: PArray.to_list args @@ -128,6 +185,7 @@ Section CHECKER. if Lit.is_pos l then PArray.to_list args else C._true | Fimp args => + if PArray.length args == 0 then C._true else if Lit.is_pos l then let args := or_of_imp args in PArray.to_list args @@ -287,31 +345,19 @@ Section CHECKER. match goal with |- context [Lit.interp rho ?x] => destruct (Lit.interp rho x);trivial end. - Axiom afold_left_and : forall a, - afold_left bool int true andb (Lit.interp rho) a = - List.forallb (Lit.interp rho) (to_list a). - - Axiom afold_left_or : forall a, - afold_left bool int false orb (Lit.interp rho) a = - C.interp rho (to_list a). - - Axiom afold_right_impb : forall a, - (afold_right bool int true implb (Lit.interp rho) a) = - C.interp rho (to_list (or_of_imp a)). - - Axiom Cinterp_neg : forall cl, - C.interp rho (map Lit.neg cl) = negb (forallb (Lit.interp rho) cl). - Lemma valid_check_BuildDef : forall l, C.valid rho (check_BuildDef l). Proof. unfold check_BuildDef,C.valid;intros l. case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true; - case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; - unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl; - tauto_check. - rewrite afold_left_and, Cinterp_neg;apply orb_negb_r. - rewrite afold_left_or, orb_comm;apply orb_negb_r. - rewrite afold_right_impb, orb_comm;apply orb_negb_r. + case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; + try (unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl; + tauto_check). + - rewrite afold_left_and, C.Cinterp_neg;apply orb_negb_r. + - rewrite afold_left_or, orb_comm;apply orb_negb_r. + - case_eq (PArray.length a == 0); auto using C.interp_true. + intro Hl; simpl. + unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl. + rewrite (afold_right_impb (Lit.interp_neg _) Hl), orb_comm;try apply orb_negb_r. Qed. Lemma valid_check_BuildDef2 : forall l, C.valid rho (check_BuildDef2 l). @@ -328,30 +374,60 @@ Section CHECKER. unfold check_BuildProj,C.valid;intros l i. case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true; case_eq (i < PArray.length a);intros Hlt;auto using C.interp_true;simpl. - - rewrite Lit.interp_nlit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. - simpl;rewrite afold_left_and. - case_eq (forallb (Lit.interp rho) (to_list a));trivial. - rewrite forallb_forall;intros Heq;rewrite Heq;trivial. - apply to_list_In; auto. - rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. - simpl;rewrite afold_left_or. - - unfold C.interp;case_eq (existsb (Lit.interp rho) (to_list a));trivial. - rewrite <-not_true_iff_false, existsb_exists, Lit.interp_neg. - case_eq (Lit.interp rho (a .[ i]));trivial. - intros Heq Hex;elim Hex;exists (a.[i]);split;trivial. - apply to_list_In; auto. - case_eq (i == PArray.length a - 1);intros Heq;simpl; - rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, H;simpl; - rewrite afold_right_impb; case_eq (C.interp rho (to_list (or_of_imp a)));trivial; - unfold C.interp;rewrite <-not_true_iff_false, existsb_exists; - try rewrite Lit.interp_neg; case_eq (Lit.interp rho (a .[ i]));trivial; - intros Heq' Hex;elim Hex. - exists (a.[i]);split;trivial. - assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63Properties.eqb_spec in Heq; rewrite <- (get_or_of_imp2 H1 Heq); apply to_list_In; rewrite length_or_of_imp; auto. - exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq';split;trivial. - assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq, to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. + - rewrite Lit.interp_nlit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. + simpl;rewrite afold_left_and. + case_eq (forallb (Lit.interp rho) (to_list a));trivial. + rewrite forallb_forall;intros Heq;rewrite Heq;trivial. + apply to_list_In; auto. + - rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. + simpl;rewrite afold_left_or. + unfold C.interp;case_eq (existsb (Lit.interp rho) (to_list a));trivial. + rewrite <-not_true_iff_false, existsb_exists, Lit.interp_neg. + case_eq (Lit.interp rho (a .[ i]));trivial. + intros Heq Hex;elim Hex;exists (a.[i]);split;trivial. + apply to_list_In; auto. + - assert (Hl : (PArray.length a == 0) = false) + by (rewrite eqb_false_spec; intro H1; rewrite H1 in Hlt; now elim (ltb_0 i)). + case_eq (i == PArray.length a - 1);intros Heq;simpl; + rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, H;simpl. + + rewrite Lit.interp_neg, orb_false_r. + rewrite (afold_right_impb (Lit.interp_neg _) Hl). + case_eq (Lit.interp rho (a .[ i])); intro Hi. + * rewrite orb_false_r, existsb_exists. + exists (a .[ i]). split; auto. + { + apply (to_list_In_eq _ i). + - now rewrite length_or_of_imp. + - symmetry. apply get_or_of_imp2. + + clear -Hl. rewrite eqb_false_spec in Hl. + unfold is_true. rewrite ltb_spec. change [|0|] with 0%Z. + assert (H:[|PArray.length a|] <> 0%Z) + by (intro H; apply Hl; now apply to_Z_inj). + destruct (to_Z_bounded (PArray.length a)) as [H1 _]. + lia. + + now rewrite Int63Properties.eqb_spec in Heq. + } + * now rewrite orb_true_r. + + rewrite orb_false_r. + case_eq (Lit.interp rho (a .[ i])); intro Hi. + * now rewrite orb_true_r. + * rewrite (afold_right_impb (Lit.interp_neg _) Hl). + rewrite orb_false_r, existsb_exists. + exists (Lit.neg (a .[ i])). + { + split. + - apply (to_list_In_eq _ i). + + now rewrite length_or_of_imp. + + symmetry. apply get_or_of_imp. + clear -Hlt Heq. + unfold is_true. rewrite ltb_spec. rewrite (to_Z_sub_1 _ i); auto. + rewrite eqb_false_spec in Heq. + assert (H:[|i|] <> ([|PArray.length a|] - 1)%Z) + by (intro H; apply Heq, to_Z_inj; rewrite (to_Z_sub_1 _ i); auto). + clear Heq. + rewrite ltb_spec in Hlt. lia. + - now rewrite Lit.interp_neg, Hi. + } Qed. Hypothesis Hs : S.valid rho s. @@ -366,9 +442,11 @@ Section CHECKER. destruct (t_form.[Lit.blit l]);auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; tauto_check. - rewrite afold_left_and, Cinterp_neg, orb_false_r;trivial. - rewrite afold_left_or, orb_false_r;trivial. - rewrite afold_right_impb, orb_false_r;trivial. + - rewrite afold_left_and, C.Cinterp_neg, orb_false_r;trivial. + - rewrite afold_left_or, orb_false_r;trivial. + - case_eq (PArray.length a == 0); auto using C.interp_true. + intro Hl. now rewrite orb_false_r, (afold_right_impb (Lit.interp_neg _) Hl). + - case_eq (PArray.length a == 0); auto using C.interp_true. Qed. Lemma valid_check_ImmBuildDef2 : forall cid, C.valid rho (check_ImmBuildDef2 cid). @@ -392,23 +470,26 @@ Section CHECKER. case_eq (i < PArray.length a); intros Hlt;auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; rewrite !orb_false_r. - rewrite afold_left_and. - rewrite forallb_forall;intros H;apply H;auto. - apply to_list_In; auto. - rewrite negb_true_iff, <-not_true_iff_false, afold_left_or. - unfold C.interp;rewrite existsb_exists, Lit.interp_neg. - case_eq (Lit.interp rho (a .[ i]));trivial. - intros Heq' Hex;elim Hex;exists (a.[i]);split;trivial. - apply to_list_In; auto. - rewrite negb_true_iff, <-not_true_iff_false, afold_right_impb. - case_eq (i == PArray.length a - 1);intros Heq';simpl; - unfold C.interp;simpl;try rewrite Lit.interp_neg;rewrite orb_false_r, - existsb_exists;case_eq (Lit.interp rho (a .[ i]));trivial; - intros Heq2 Hex;elim Hex. - exists (a.[i]);split;trivial. - assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63Properties.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto. - exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial. - assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. + - rewrite afold_left_and. + rewrite forallb_forall;intros H;apply H;auto. + apply to_list_In; auto. + - rewrite negb_true_iff, <-not_true_iff_false, afold_left_or. + unfold C.interp;rewrite existsb_exists, Lit.interp_neg. + case_eq (Lit.interp rho (a .[ i]));trivial. + intros Heq' Hex;elim Hex;exists (a.[i]);split;trivial. + apply to_list_In; auto. + - rewrite negb_true_iff, <-not_true_iff_false. + assert (Hl:(PArray.length a == 0) = false) + by (rewrite eqb_false_spec; intro H; rewrite H in Hlt; now apply (ltb_0 i)). + rewrite (afold_right_impb (Lit.interp_neg _) Hl). + case_eq (i == PArray.length a - 1);intros Heq';simpl; + unfold C.interp;simpl;try rewrite Lit.interp_neg;rewrite orb_false_r, + existsb_exists;case_eq (Lit.interp rho (a .[ i]));trivial; + intros Heq2 Hex;elim Hex. + exists (a.[i]);split;trivial. + assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63Properties.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto. + exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial. + assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. Qed. End CHECKER. diff --git a/src/lfsc/ast.ml b/src/lfsc/ast.ml index 454bc0a..36c2f79 100644 --- a/src/lfsc/ast.ml +++ b/src/lfsc/ast.ml @@ -198,7 +198,7 @@ let compare_symbol s1 s2 = match s1.sname, s2.sname with | Name n1, Name n2 -> Hstring.compare n1 n2 | Name _, _ -> -1 | _, Name _ -> 1 - | S_Hole i1, S_Hole i2 -> Pervasives.compare i1 i2 + | S_Hole i1, S_Hole i2 -> Stdlib.compare i1 i2 let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with @@ -250,7 +250,7 @@ let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with | SideCond (_, _, _, t), _ -> compare_term ~mod_eq t t2 | _, SideCond (_, _, _, t) -> compare_term ~mod_eq t1 t - | Hole i1, Hole i2 -> Pervasives.compare i1 i2 + | Hole i1, Hole i2 -> Stdlib.compare i1 i2 and compare_term_list ?(mod_eq=false) l1 l2 = match l1, l2 with diff --git a/src/lfsc/builtin.ml b/src/lfsc/builtin.ml index 86899df..75ea11e 100644 --- a/src/lfsc/builtin.ml +++ b/src/lfsc/builtin.ml @@ -616,7 +616,7 @@ let cong s1 s2 a1 b1 a2 b2 u1 u2 = module MInt = Map.Make (struct type t = int - let compare = Pervasives.compare + let compare = Stdlib.compare end) module STerm = Set.Make (Term) diff --git a/src/lfsc/shashcons.mli b/src/lfsc/shashcons.mli index 049ec5f..ca46efa 100644 --- a/src/lfsc/shashcons.mli +++ b/src/lfsc/shashcons.mli @@ -47,6 +47,7 @@ module type S = val iter : (t -> unit) -> unit (** [iter f] iterates [f] over all elements of the table . *) + val stats : unit -> int * int * int * int * int * int (** Return statistics on the table. The numbers are, in order: table length, number of entries, sum of bucket lengths, @@ -83,6 +84,7 @@ module type S_consed = val iter : (key hash_consed -> unit) -> unit (** [iter f] iterates [f] over all elements of the table . *) + val stats : unit -> int * int * int * int * int * int (** Return statistics on the table. The numbers are, in order: table length, number of entries, sum of bucket lengths, diff --git a/src/lia/lia.ml b/src/lia/lia.ml index d546559..8dce3e8 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -13,9 +13,7 @@ (*** Linking SMT Terms to Micromega Terms ***) open Util open Structures.Micromega_plugin_Micromega -open Structures.Micromega_plugin_Coq_micromega -open SmtMisc open SmtForm open SmtAtom @@ -29,14 +27,6 @@ let rec pos_of_int i = then XO(pos_of_int (i lsr 1)) else XI(pos_of_int (i lsr 1)) -let z_of_int i = - if i = 0 - then Z0 - else - if i > 0 - then Zpos (pos_of_int i) - else Zneg (pos_of_int (-i)) - type my_tbl = {tbl:(hatom,int) Hashtbl.t; mutable count:int} @@ -117,8 +107,6 @@ let smt_Atom_to_micromega_formula tbl ha = (* specialized fold *) -let default_constr = Structures.econstr_of_constr (mkInt 0) -let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0 (* morphism for general formulas *) let binop_array g tbl op def t = @@ -135,12 +123,10 @@ let binop_array g tbl op def t = let rec smt_Form_to_coq_micromega_formula tbl l = let v = match Form.pform l with - | Fatom ha -> - A (smt_Atom_to_micromega_formula tbl ha, - default_tag,default_constr) + | Fatom ha -> A (smt_Atom_to_micromega_formula tbl ha, Tt) | Fapp (Ftrue, _) -> TT | Fapp (Ffalse, _) -> FF - | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> C (x,y)) TT l + | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Cj (x,y)) TT l | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> D (x,y)) FF l | Fapp (Fxor, l) -> failwith "todo:Fxor" | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> I (x,None,y)) TT l @@ -162,49 +148,184 @@ let binop_list tbl op def l = | [] -> def | f::l -> List.fold_left (fun x y -> op x (smt_Form_to_coq_micromega_formula tbl y)) (smt_Form_to_coq_micromega_formula tbl f) l +let smt_clause_to_coq_micromega_formula tbl cl = + binop_list tbl (fun x y -> Cj (x,y)) TT (List.map Form.neg cl) -(* let rec binop_list tbl op def l = *) -(* match l with *) -(* | [] -> def *) -(* | [f] -> smt_Form_to_coq_micromega_formula tbl f *) -(* | f::l -> *) -(* op (smt_Form_to_coq_micromega_formula tbl f) (binop_list tbl op def l) *) - -(* and smt_Form_to_coq_micromega_formula tbl l = *) -(* let v = *) -(* match Form.pform l with *) -(* | Fatom ha -> *) -(* A (smt_Atom_to_micromega_formula tbl ha, *) -(* default_tag,default_constr) *) -(* | Fapp (Ftrue, _) -> TT *) -(* | Fapp (Ffalse, _) -> FF *) -(* | Fapp (Fand, l) -> binop_list tbl (fun x y -> C (x,y)) TT l *) -(* | Fapp (For, l) -> binop_list tbl (fun x y -> D (x,y)) FF l *) -(* | Fapp (Fxor, l) -> failwith "todo:Fxor" *) -(* | Fapp (Fimp, l) -> binop_list tbl (fun x y -> I (x,None,y)) TT l *) -(* | Fapp (Fiff, l) -> failwith "todo:Fiff" *) -(* | Fapp (Fite, l) -> failwith "todo:Fite" *) -(* | Fapp (Fnot2 _, l) -> smt_Form_to_coq_micromega_formula tbl l *) -(* in *) -(* if Form.is_pos l then v *) -(* else N(v) *) +(* backported from Coq *) +type ('option,'a,'prf,'model) prover = { + name : string ; (* name of the prover *) + get_option : unit ->'option ; (* find the options of the prover *) + prover : ('option * 'a list) -> ('prf, 'model) Structures.Micromega_plugin_Certificate.res ; (* the prover itself *) + hyps : 'prf -> Structures.Micromega_plugin_Mutils.ISet.t ; (* extract the indexes of the hypotheses really used in the proof *) + compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *) + pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *) + pp_f : out_channel -> 'a -> unit (* pretty printing of the formulas (polynomials)*) +} -let smt_clause_to_coq_micromega_formula tbl cl = - binop_list tbl (fun x y -> C(x,y)) TT (List.map Form.neg cl) +let lia_enum = ref true +let max_depth = max_int +let lia_proof_depth = ref max_depth +let get_lia_option () = + (!Structures.Micromega_plugin_Certificate.use_simplex,!lia_enum,!lia_proof_depth) + +let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Structures.Micromega_plugin_Micromega.denorm e , o) l) + +module CacheZ = Structures.Micromega_plugin_Persistent_cache.PHashtable(struct + type prover_option = bool * bool* int + type t = prover_option * ((Structures.Micromega_plugin_Micromega.z Structures.Micromega_plugin_Micromega.pol * Structures.Micromega_plugin_Micromega.op1) list) + let equal = (=) + let hash = Hashtbl.hash +end) + +let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Structures.Micromega_plugin_Certificate.lia ce b) s) + +let xhyps_of_cone base acc prf = + let rec xtract e acc = + match e with + | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> acc + | Structures.Micromega_plugin_Micromega.PsatzIn n -> let n = (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) in + if n >= base + then Structures.Micromega_plugin_Mutils.ISet.add (n-base) acc + else acc + | Structures.Micromega_plugin_Micromega.PsatzMulC(_,c) -> xtract c acc + | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in + + xtract prf acc + +let hyps_of_pt pt = + + let rec xhyps base pt acc = + match pt with + | Structures.Micromega_plugin_Micromega.DoneProof -> acc + | Structures.Micromega_plugin_Micromega.RatProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) + | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) + | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) -> + let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in + List.fold_left (fun s x -> xhyps (base + 1) x s) s l in + + xhyps 0 pt Structures.Micromega_plugin_Mutils.ISet.empty + +let compact_cone prf f = + let np n = Structures.Micromega_plugin_Mutils.CamlToCoq.nat (f (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n)) in + + let rec xinterp prf = + match prf with + | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> prf + | Structures.Micromega_plugin_Micromega.PsatzIn n -> Structures.Micromega_plugin_Micromega.PsatzIn (np n) + | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) -> Structures.Micromega_plugin_Micromega.PsatzMulC(e,xinterp c) + | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzAdd(xinterp e1,xinterp e2) + | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzMulE(xinterp e1,xinterp e2) in + + xinterp prf + +let compact_pt pt f = + let translate ofset x = + if x < ofset then x + else (f (x-ofset) + ofset) in + + let rec compact_pt ofset pt = + match pt with + | Structures.Micromega_plugin_Micromega.DoneProof -> Structures.Micromega_plugin_Micromega.DoneProof + | Structures.Micromega_plugin_Micromega.RatProof(c,pt) -> Structures.Micromega_plugin_Micromega.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) + | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> Structures.Micromega_plugin_Micromega.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) + | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) -> Structures.Micromega_plugin_Micromega.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)), + Structures.Micromega_plugin_Micromega.map (fun x -> compact_pt (ofset+1) x) l) in + compact_pt 0 pt + +let pp_nat o n = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) + +let pp_positive o x = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.positive x) + +let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (Structures.Micromega_plugin_Mutils.CoqToCaml.z_big_int x)) + +let pp_list op cl elt o l = + let rec _pp o l = + match l with + | [] -> () + | [e] -> Printf.fprintf o "%a" elt e + | e::l -> Printf.fprintf o "%a ,%a" elt e _pp l in + Printf.fprintf o "%s%a%s" op _pp l cl + +let pp_pol pp_c o e = + let rec pp_pol o e = + match e with + | Structures.Micromega_plugin_Micromega.Pc n -> Printf.fprintf o "Pc %a" pp_c n + | Structures.Micromega_plugin_Micromega.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol + | Structures.Micromega_plugin_Micromega.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in + pp_pol o e + +let pp_psatz pp_z o e = + let rec pp_cone o e = + match e with + | Structures.Micromega_plugin_Micromega.PsatzIn n -> + Printf.fprintf o "(In %a)%%nat" pp_nat n + | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) -> + Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c + | Structures.Micromega_plugin_Micromega.PsatzSquare e -> + Printf.fprintf o "(%a^2)" (pp_pol pp_z) e + | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) -> + Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 + | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> + Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 + | Structures.Micromega_plugin_Micromega.PsatzC p -> + Printf.fprintf o "(%a)%%positive" pp_z p + | Structures.Micromega_plugin_Micromega.PsatzZ -> + Printf.fprintf o "0" in + pp_cone o e + +let rec pp_proof_term o = function + | Structures.Micromega_plugin_Micromega.DoneProof -> Printf.fprintf o "D" + | Structures.Micromega_plugin_Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst + | Structures.Micromega_plugin_Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst + | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,rst) -> + Printf.fprintf o "EP[%a,%a,%a]" + (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 + (pp_list "[" "]" pp_proof_term) rst + +let linear_Z = { + name = "lia"; + get_option = get_lia_option; + prover = memo_zlinear_prover ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) +} + +let find_witness p polys1 = + let polys1 = List.map fst polys1 in + match p.prover (p.get_option (), polys1) with + | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model m + | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown + | Structures.Micromega_plugin_Certificate.Prf prf -> Structures.Micromega_plugin_Certificate.Prf(prf,p) + +let witness_list prover l = + let rec xwitness_list l = + match l with + | [] -> Structures.Micromega_plugin_Certificate.Prf [] + | e :: l -> + match xwitness_list l with + | Structures.Micromega_plugin_Certificate.Model (m,e) -> Structures.Micromega_plugin_Certificate.Model (m,e) + | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown + | Structures.Micromega_plugin_Certificate.Prf l -> + match find_witness prover e with + | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model (m,e) + | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown + | Structures.Micromega_plugin_Certificate.Prf w -> Structures.Micromega_plugin_Certificate.Prf (w::l) in + xwitness_list l + +let witness_list_tags = witness_list -(* backported from Coq-8.8.2 *) -(* val tauto_lia : Mc.z formula -> Certificate.Mc.zArithProof list option *) let tauto_lia ff = let prover = linear_Z in - let cnf_ff,_ = cnf Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce ff in - match witness_list_tags [prover] cnf_ff with - | None -> None - | Some l -> Some (List.map fst l) + let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in + match witness_list_tags prover cnf_ff with + | Structures.Micromega_plugin_Certificate.Prf l -> Some (List.map fst l) + | _ -> None (* call to micromega solver *) let build_lia_certif cl = let tbl = create_tbl 13 in let f = I(smt_clause_to_coq_micromega_formula tbl cl, None, FF) in - tbl, f, tauto_lia f - + tauto_lia f diff --git a/src/lia/lia.mli b/src/lia/lia.mli index 9d4ee6b..fb58db8 100644 --- a/src/lia/lia.mli +++ b/src/lia/lia.mli @@ -10,60 +10,6 @@ (**************************************************************************) -val pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive -val z_of_int : int -> Structures.Micromega_plugin_Micromega.z -type my_tbl -val get_atom_var : my_tbl -> SmtAtom.hatom -> int -val create_tbl : int -> my_tbl -val smt_Atom_to_micromega_pos : - SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.positive -val smt_Atom_to_micromega_Z : - SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.z -val smt_Atom_to_micromega_pExpr : - my_tbl -> - SmtAtom.hatom -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Micromega.pExpr -val smt_binop_to_micromega_formula : - my_tbl -> - SmtAtom.bop -> - SmtAtom.hatom -> - SmtAtom.hatom -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Micromega.formula -val smt_Atom_to_micromega_formula : - my_tbl -> - SmtAtom.hatom -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Micromega.formula -val binop_array : - ('a -> 'b -> 'c) -> 'a -> ('c -> 'c -> 'c) -> 'c -> 'b array -> 'c -val smt_Form_to_coq_micromega_formula : - my_tbl -> - SmtAtom.Form.t -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula -val binop_list : - my_tbl -> - (Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula) -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula -> - SmtAtom.Form.t list -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula -val smt_clause_to_coq_micromega_formula : - my_tbl -> - SmtAtom.Form.t list -> - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula val build_lia_certif : SmtAtom.Form.t list -> - my_tbl * - Structures.Micromega_plugin_Micromega.z - Structures.Micromega_plugin_Coq_micromega.formula * Structures.Micromega_plugin_Certificate.Mc.zArithProof list option diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index f938671..7e58aa3 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -111,7 +111,7 @@ let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym) let declare_fun_from_name rt ro s tyl ty = let coqTy = List.fold_right (fun typ c -> - Term.mkArrow (interp_to_coq rt typ) c) + Structures.mkArrow (interp_to_coq rt typ) c) tyl (interp_to_coq rt ty) in let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in let op = Op.declare ro cons_v (Array.of_list tyl) ty None in diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml index 8ae7202..aee9a81 100644 --- a/src/smtlib2/smtlib2_solver.ml +++ b/src/smtlib2/smtlib2_solver.ml @@ -95,7 +95,7 @@ let read_check_result s = let send_command s cmd read = eprintf "%s@." cmd; - let err_p1 = Unix.((fstat s.stderr).st_size) in + (* let err_p1 = Unix.((fstat s.stderr).st_size) in *) try let in_ch = Unix.out_channel_of_descr s.stdin in let fmt = formatter_of_out_channel in_ch in @@ -103,16 +103,18 @@ let send_command s cmd read = pp_print_newline fmt (); read s with e -> - let err_p2 = Unix.((fstat s.stderr).st_size) in - let len = err_p2 - err_p1 in - (* Was something written to stderr? *) - if len <> 0 then begin - let buf = Bytes.create err_p2 in - Unix.read s.stderr buf 0 err_p2 |> ignore; - let err_msg = Bytes.sub_string buf err_p1 len in - Structures.error ("Solver error: "^err_msg); - end - else (kill s; raise e) + (* After the exception, the file descriptor is invalid *) + (* let err_p2 = Unix.((fstat s.stderr).st_size) in + * let len = err_p2 - err_p1 in + * (\* Was something written to stderr? *\) + * if len <> 0 then begin + * let buf = Bytes.create err_p2 in + * Unix.read s.stderr buf 0 err_p2 |> ignore; + * let err_msg = Bytes.sub_string buf err_p1 len in + * Structures.error ("Solver error: "^err_msg); + * end + * else (kill s; raise e) *) + kill s; raise e let set_option s name b = diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index ad5ec1d..a1b6765 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -10,7 +10,6 @@ (**************************************************************************) -open Coqlib open SmtMisc @@ -25,9 +24,9 @@ let ceq63 = gen_constant Structures.int63_modules "eqb" let carray = gen_constant Structures.parray_modules "array" (* nat *) -let cnat = gen_constant init_modules "nat" -let cO = gen_constant init_modules "O" -let cS = gen_constant init_modules "S" +let cnat = gen_constant Structures.init_modules "nat" +let cO = gen_constant Structures.init_modules "O" +let cS = gen_constant Structures.init_modules "S" (* Positive *) let positive_modules = [["Coq";"Numbers";"BinNums"]; @@ -72,49 +71,49 @@ let ceqbZ = gen_constant z_modules "eqb" (* Booleans *) let bool_modules = [["Coq";"Bool";"Bool"]] -let cbool = gen_constant init_modules "bool" -let ctrue = gen_constant init_modules "true" -let cfalse = gen_constant init_modules "false" -let candb = gen_constant init_modules "andb" -let corb = gen_constant init_modules "orb" -let cxorb = gen_constant init_modules "xorb" -let cnegb = gen_constant init_modules "negb" -let cimplb = gen_constant init_modules "implb" +let cbool = gen_constant Structures.init_modules "bool" +let ctrue = gen_constant Structures.init_modules "true" +let cfalse = gen_constant Structures.init_modules "false" +let candb = gen_constant Structures.init_modules "andb" +let corb = gen_constant Structures.init_modules "orb" +let cxorb = gen_constant Structures.init_modules "xorb" +let cnegb = gen_constant Structures.init_modules "negb" +let cimplb = gen_constant Structures.init_modules "implb" let ceqb = gen_constant bool_modules "eqb" let cifb = gen_constant bool_modules "ifb" -let ciff = gen_constant init_modules "iff" +let ciff = gen_constant Structures.init_modules "iff" let creflect = gen_constant bool_modules "reflect" (* Lists *) -let clist = gen_constant init_modules "list" -let cnil = gen_constant init_modules "nil" -let ccons = gen_constant init_modules "cons" -let clength = gen_constant init_modules "length" +let clist = gen_constant Structures.init_modules "list" +let cnil = gen_constant Structures.init_modules "nil" +let ccons = gen_constant Structures.init_modules "cons" +let clength = gen_constant Structures.init_modules "length" (* Option *) -let coption = gen_constant init_modules "option" -let cSome = gen_constant init_modules "Some" -let cNone = gen_constant init_modules "None" +let coption = gen_constant Structures.init_modules "option" +let cSome = gen_constant Structures.init_modules "Some" +let cNone = gen_constant Structures.init_modules "None" (* Pairs *) -let cpair = gen_constant init_modules "pair" -let cprod = gen_constant init_modules "prod" +let cpair = gen_constant Structures.init_modules "pair" +let cprod = gen_constant Structures.init_modules "prod" (* Dependent pairs *) -let csigT = gen_constant init_modules "sigT" -(* let cprojT1 = gen_constant init_modules "projT1" *) -(* let cprojT2 = gen_constant init_modules "projT2" *) -(* let cprojT3 = gen_constant init_modules "projT3" *) +let csigT = gen_constant Structures.init_modules "sigT" +(* let cprojT1 = gen_constant Structures.init_modules "projT1" *) +(* let cprojT2 = gen_constant Structures.init_modules "projT2" *) +(* let cprojT3 = gen_constant Structures.init_modules "projT3" *) -(* let csigT2 = gen_constant init_modules "sigT2" *) -(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *) +(* let csigT2 = gen_constant Structures.init_modules "sigT2" *) +(* let csigT_of_sigT2 = gen_constant Structures.init_modules "sigT_of_sigT2" *) (* Logical Operators *) -let cnot = gen_constant init_modules "not" -let ceq = gen_constant init_modules "eq" -let crefl_equal = gen_constant init_modules "eq_refl" -let cconj = gen_constant init_modules "conj" -let cand = gen_constant init_modules "and" +let cnot = gen_constant Structures.init_modules "not" +let ceq = gen_constant Structures.init_modules "eq" +let crefl_equal = gen_constant Structures.init_modules "eq_refl" +let cconj = gen_constant Structures.init_modules "conj" +let cand = gen_constant Structures.init_modules "and" (* Bit vectors *) let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]] diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 16d9bdb..ae44b8d 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -649,25 +649,9 @@ module Atom = to_smt_atom (atom h) and to_smt_atom = function - | Acop (CO_BV bv) -> Format.fprintf fmt "#b%a" bv_to_smt bv + | Acop (CO_BV bv) -> if List.length bv = 0 then Structures.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv | Acop _ as a -> to_smt_int fmt (compute_int a) - | Auop (UO_Zopp,h) -> - Format.fprintf fmt "(- "; - to_smt fmt h; - Format.fprintf fmt ")" - | Auop (UO_BVbitOf (_, i), h) -> - Format.fprintf fmt "(bitof %d %a)" i to_smt h - | Auop (UO_BVnot _, h) -> - Format.fprintf fmt "(bvnot %a)" to_smt h - | Auop (UO_BVneg _, h) -> - Format.fprintf fmt "(bvneg %a)" to_smt h - | Auop (UO_BVextr (i, n, _), h) -> - Format.fprintf fmt "((_ extract %d %d) %a)" (i+n-1) i to_smt h - | Auop (UO_BVzextn (_, n), h) -> - Format.fprintf fmt "((_ zero_extend %d) %a)" n to_smt h - | Auop (UO_BVsextn (_, n), h) -> - Format.fprintf fmt "((_ sign_extend %d) %a)" n to_smt h - | Auop _ as a -> to_smt_int fmt (compute_int a) + | Auop (op,h) -> to_smt_uop op h | Abop (op,h1,h2) -> to_smt_bop op h1 h2 | Atop (op,h1,h2,h3) -> to_smt_top op h1 h2 h3 | Anop (op,a) -> to_smt_nop op a @@ -694,6 +678,28 @@ module Atom = SmtBtype.to_smt fmt bt; Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t)) + and to_smt_uop op h = + match op with + | UO_Zpos -> + Format.fprintf fmt "%a" to_smt h + | UO_Zneg -> + Format.fprintf fmt "(- %a)" to_smt h + | UO_Zopp -> + Format.fprintf fmt "(- %a)" to_smt h + | UO_BVbitOf (_, i) -> + Format.fprintf fmt "(bitof %d %a)" i to_smt h + | UO_BVnot _ -> + Format.fprintf fmt "(bvnot %a)" to_smt h + | UO_BVneg _ -> + Format.fprintf fmt "(bvneg %a)" to_smt h + | UO_BVextr (i, n, _) -> + Format.fprintf fmt "((_ extract %d %d) %a)" (i+n-1) i to_smt h + | UO_BVzextn (_, n) -> + Format.fprintf fmt "((_ zero_extend %d) %a)" n to_smt h + | UO_BVsextn (_, n) -> + Format.fprintf fmt "((_ sign_extend %d) %a)" n to_smt h + | _ -> to_smt_int fmt (compute_int (Auop (op, h))) + and to_smt_bop op h1 h2 = let s = match op with | BO_Zplus -> "+" @@ -738,41 +744,6 @@ module Atom = let to_smt (fmt:Format.formatter) h = to_smt_named fmt h - exception NotWellTyped of atom - - let check a = - (* Format.eprintf "Checking %a @." to_smt_atom a; *) - match a with - | Acop _ -> () - | Auop(op,h) -> - if not (SmtBtype.equal (Op.u_type_arg op) (type_of h)) then - raise (NotWellTyped a) - | Abop(op,h1,h2) -> - let (t1,t2) = Op.b_type_args op in - if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2)) - then (Format.eprintf "1. Wanted %a, got %a@.2. Wanted %a, got %a@." - SmtBtype.to_smt t1 SmtBtype.to_smt (type_of h1) - SmtBtype.to_smt t2 SmtBtype.to_smt (type_of h2); - raise (NotWellTyped a)) - | Atop(op,h1,h2,h3) -> - let (t1,t2,t3) = Op.t_type_args op in - if not (SmtBtype.equal t1 (type_of h1) && - SmtBtype.equal t2 (type_of h2) && - SmtBtype.equal t3 (type_of h3)) - then raise (NotWellTyped a) - | Anop(op,ha) -> - let ty = Op.n_type_args op in - Array.iter - (fun h -> if not (SmtBtype.equal ty (type_of h)) then - raise (NotWellTyped a)) ha - | Aapp(op,args) -> - let tparams = Op.i_type_args op in - Array.iteri (fun i t -> - if not (SmtBtype.equal t (type_of args.(i))) then - (Format.eprintf "Wanted %a, got %a@." - SmtBtype.to_smt t SmtBtype.to_smt (type_of args.(i)); - raise (NotWellTyped a))) tparams - type reify_tbl = { mutable count : int; tbl : hatom HashAtom.t @@ -789,19 +760,68 @@ module Atom = reify.count <- 0; HashAtom.clear reify.tbl + let declare reify a = - check a; let res = {index = reify.count; hval = a} in HashAtom.add reify.tbl a res; reify.count <- reify.count + 1; res - let get ?declare:(decl=true) reify a = + let rec get ?declare:(decl=true) reify a = if decl then try HashAtom.find reify.tbl a - with Not_found -> declare reify a + with Not_found -> + (let a = check reify a in + try HashAtom.find reify.tbl a + with Not_found -> + declare reify a) else {index = -1; hval = a} + and check reify a = + (* Format.eprintf "Checking %a @." to_smt_atom a; *) + + let check_one t h = + let th = type_of h in + if SmtBtype.equal t th then + h + else if t == TZ && th == Tpositive then + (* Special case: the SMT solver cannot distinguish Z from + positive, we have to add the injection back *) + get reify (Auop(UO_Zpos, h)) + else ( + Format.eprintf "Incorrect type: wanted %a, got %a@." + SmtBtype.to_smt t SmtBtype.to_smt th; + failwith (Format.asprintf "Atom %a is not of the expected type" to_smt h) + ) + in + + let a = + match a with + | Acop _ -> a + | Auop(op,h) -> + let t = Op.u_type_arg op in + Auop(op, check_one t h) + | Abop(op,h1,h2) -> + let (t1,t2) = Op.b_type_args op in + let h1 = check_one t1 h1 in + let h2 = check_one t2 h2 in + Abop(op, h1, h2) + | Atop(op,h1,h2,h3) -> + let (t1,t2,t3) = Op.t_type_args op in + let h1 = check_one t1 h1 in + let h2 = check_one t2 h2 in + let h3 = check_one t3 h3 in + Atop(op, h1, h2, h3) + | Anop(op,ha) -> + let ty = Op.n_type_args op in + Anop(op, Array.map (check_one ty) ha) + | Aapp(op,args) -> + let tparams = Op.i_type_args op in + Aapp(op, Array.mapi (fun i -> check_one tparams.(i)) args) + in + a + + let mk_eq reify ?declare:(decl=true) ty h1 h2 = let op = BO_eq ty in try diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index a6a1761..f076cb8 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -121,8 +121,6 @@ module Atom : val to_smt : Format.formatter -> t -> unit - exception NotWellTyped of atom - type reify_tbl val create : unit -> reify_tbl diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index e64a131..b1f2666 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) = let tf = Hashtbl.create 17 in let rec interp = function | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|] - | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in + | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in interp prem diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 12aef5a..044ff4c 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -80,11 +80,11 @@ module type FORM = val clear : reify -> unit val get : ?declare:bool -> reify -> pform -> t - (** Give a coq term, build the corresponding formula *) + (** Given a coq term, build the corresponding formula *) val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t - (** Flattening of [Fand] and [For], removing of [Fnot2] *) + (* Flattening of [Fand] and [For], removing of [Fnot2] *) val flatten : reify -> t -> t (** Turn n-ary [Fand] and [For] into their right-associative @@ -100,10 +100,10 @@ module type FORM = val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array val interp_tbl : reify -> Structures.constr * Structures.constr val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation - of a formula *) - (** [interp_atom] map [hatom] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation + of a formula *) + (* [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) val interp_to_coq : (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> t -> Structures.constr @@ -589,9 +589,9 @@ module Make (Atom:ATOM) = (mkInt i, Structures.mkArray (Lazy.force cform, t)) let nvars reify = reify.count - (** Producing a Coq term corresponding to the interpretation of a formula *) - (** [interp_atom] map [Atom.t] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation of a formula *) + (* [interp_atom] map [Atom.t] to coq term, it is better if it produce + shared terms. *) let interp_to_coq interp_atom form_tbl f = let rec interp_form f = let l = to_lit f in diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index ad7d2ca..fead657 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -97,10 +97,10 @@ module type FORM = val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array val interp_tbl : reify -> Structures.constr * Structures.constr val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation - of a formula *) - (** [interp_atom] map [hatom] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation + of a formula *) + (* [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) val interp_to_coq : (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> t -> Structures.constr diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 92f0f09..607ebe7 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -46,7 +46,7 @@ type logic_item = module SL = Set.Make (struct type t = logic_item - let compare = Pervasives.compare + let compare = Stdlib.compare end) type logic = SL.t diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index f397826..ef017a7 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -159,7 +159,7 @@ let order_roots init_index first = r := n | _ -> failwith "root value has unexpected form" end done; - let _, lr = List.sort (fun (i1, _) (i2, _) -> Pervasives.compare i1 i2) !acc + let _, lr = List.sort (fun (i1, _) (i2, _) -> Stdlib.compare i1 i2) !acc |> List.split in let link_to c1 c2 = let curr_id = c2.id -1 in @@ -476,7 +476,7 @@ let to_coq to_lit interp (cstep, let concl' = out_cl [concl] in let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in let app_var = Structures.mkVar app_name in - let app_ty = Term.mkArrow clemma (interp ([], [concl])) in + let app_ty = Structures.mkArrow clemma (interp ([], [concl])) in cuts := (app_name, app_ty)::!cuts; mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|] end diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 17a230f..39f60c0 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -185,20 +185,27 @@ let call_verit _ rt ro ra' rf' first lsmt = let win = open_in wname in - let raise_warnings () = + let raise_warnings_errors () = try while true do let l = input_line win in + let n = String.length l in if l = "warning : proof_done: status is still open" then raise Unknown + else if l = "Invalid memory reference" then + Structures.warning "verit-warning" ("veriT outputted the warning: " ^ l) + else if n >= 7 && String.sub l 0 7 = "warning" then + Structures.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7))) + else if n >= 8 && String.sub l 0 8 = "error : " then + Structures.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8))) else - Structures.warning "verit-warning" ("Verit.call_verit: command " ^ command ^ " outputs the warning: " ^ l); + Structures.error ("veriT failed with the error: " ^ l) done with End_of_file -> () in try if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code); - raise_warnings (); + raise_warnings_errors (); let res = import_trace ra' rf' logfilename (Some first) lsmt in close_in win; Sys.remove wname; res with x -> close_in win; Sys.remove wname; diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index b1a6304..862a628 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -150,7 +150,7 @@ let mkCongrPred p = (* Linear arithmetic *) let mkMicromega cl = - let _tbl, _f, cert = Lia.build_lia_certif cl in + let cert = Lia.build_lia_certif cl in let c = match cert with | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this" @@ -168,7 +168,7 @@ let mkSplArith orig cl = match orig.value with | Some [orig'] -> orig' | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in - let _tbl, _f, cert = Lia.build_lia_certif [Form.neg orig';res] in + let cert = Lia.build_lia_certif [Form.neg orig';res] in let c = match cert with | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this" diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index ee0dd96..99a7e65 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -112,12 +112,14 @@ Axiom get_init : forall A f size (def:A) i, Axiom default_init : forall A f size (def:A), default (init size f def) = def. -(* Rename this ? *) +(* Not true in this implementation (see #71, many thanks to Andres Erbsen) *) +(* Axiom get_ext : forall A (t1 t2:array A), length t1 = length t2 -> (forall i, i < length t1 = true -> t1.[i] = t2.[i]) -> default t1 = default t2 -> t1 = t2. +*) (* Definition *) Definition to_list {A:Type} (t:array A) := @@ -366,6 +368,7 @@ Definition eqb {A:Type} (Aeqb: A->A->bool) (t1 t2:array A) := Aeqb (default t1) (default t2) && forallbi (fun i a1 => Aeqb a1 (t2.[i])) t1. +(* Lemma reflect_eqb : forall (A:Type) (Aeqb:A->A->bool), (forall a1 a2, reflect (a1 = a2) (Aeqb a1 a2)) -> forall t1 t2, reflect (t1 = t2) (eqb Aeqb t1 t2). @@ -385,6 +388,7 @@ Proof. intros i _; rewrite <- (reflect_iff _ _ (HA _ _));trivial. rewrite <- not_true_iff_false, <- (reflect_iff _ _ (HA _ _)) in H0;apply H0;trivial. Qed. +*) (* diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local index 045af88..8abc72c 100644 --- a/src/versions/standard/Makefile.local +++ b/src/versions/standard/Makefile.local @@ -5,16 +5,19 @@ test : - cd ../unit-tests; make + cd ../unit-tests; make cleanvo; make ztest : - cd ../unit-tests; make zchaff + cd ../unit-tests; make cleanvo; make zchaff vtest : - cd ../unit-tests; make verit + cd ../unit-tests; make cleanvo; make verit lfsctest : - cd ../unit-tests; make lfsc + cd ../unit-tests; make cleanvo; make lfsc + +paralleltest : + cd ../unit-tests; make parallel clean:: cd ../unit-tests; make clean diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject index 396a5ba..d7cffca 100644 --- a/src/versions/standard/_CoqProject +++ b/src/versions/standard/_CoqProject @@ -38,9 +38,6 @@ versions/standard/Int63/Int63Axioms.v versions/standard/Int63/Int63Properties.v versions/standard/Array/PArray.v -versions/standard/mutils_full.ml -versions/standard/mutils_full.mli -versions/standard/coq_micromega_full.ml versions/standard/Structures.v versions/standard/structures.ml versions/standard/structures.mli diff --git a/src/versions/standard/coq_micromega_full.ml b/src/versions/standard/coq_micromega_full.ml deleted file mode 100644 index d957110..0000000 --- a/src/versions/standard/coq_micromega_full.ml +++ /dev/null @@ -1,2215 +0,0 @@ -(*** This file is taken from Coq-8.9.0 to expose more functions than - coq_micromega.mli does. - See https://github.com/coq/coq/issues/9749 . ***) - - -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(* *) -(* Micromega: A reflexive tactic using the Positivstellensatz *) -(* *) -(* ** Toplevel definition of tactics ** *) -(* *) -(* - Modules ISet, M, Mc, Env, Cache, CacheZ *) -(* *) -(* Frédéric Besson (Irisa/Inria) 2006-20011 *) -(* *) -(************************************************************************) - -open Pp -open Names -open Goptions -open Mutils_full -open Constr -open Tactypes - -module Micromega = Micromega_plugin.Micromega -module Certificate = Micromega_plugin.Certificate -module Sos_types = Micromega_plugin.Sos_types -module Mfourier = Micromega_plugin.Mfourier - -(** - * Debug flag - *) - -let debug = false - -(* Limit the proof search *) - -let max_depth = max_int - -(* Search limit for provers over Q R *) -let lra_proof_depth = ref max_depth - - -(* Search limit for provers over Z *) -let lia_enum = ref true -let lia_proof_depth = ref max_depth - -let get_lia_option () = - (!lia_enum,!lia_proof_depth) - -let get_lra_option () = - !lra_proof_depth - - - -let _ = - - let int_opt l vref = - { - optdepr = false; - optname = List.fold_right (^) l ""; - optkey = l ; - optread = (fun () -> Some !vref); - optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v)) - } in - - let lia_enum_opt = - { - optdepr = false; - optname = "Lia Enum"; - optkey = ["Lia2";"Enum"]; - optread = (fun () -> !lia_enum); - optwrite = (fun x -> lia_enum := x) - } in - let _ = declare_int_option (int_opt ["Lra2"; "Depth"] lra_proof_depth) in - let _ = declare_int_option (int_opt ["Lia2"; "Depth"] lia_proof_depth) in - let _ = declare_bool_option lia_enum_opt in - () - -(** - * Initialize a tag type to the Tag module declaration (see Mutils). - *) - -type tag = Tag.t - -(** - * An atom is of the form: - * pExpr1 \{<,>,=,<>,<=,>=\} pExpr2 - * where pExpr1, pExpr2 are polynomial expressions (see Micromega). pExprs are - * parametrized by 'cst, which is used as the type of constants. - *) - -type 'cst atom = 'cst Micromega.formula - -(** - * Micromega's encoding of formulas. - * By order of appearance: boolean constants, variables, atoms, conjunctions, - * disjunctions, negation, implication. -*) - -type 'cst formula = - | TT - | FF - | X of EConstr.constr - | A of 'cst atom * tag * EConstr.constr - | C of 'cst formula * 'cst formula - | D of 'cst formula * 'cst formula - | N of 'cst formula - | I of 'cst formula * Names.Id.t option * 'cst formula - -(** - * Formula pretty-printer. - *) - -let rec pp_formula o f = - match f with - | TT -> output_string o "tt" - | FF -> output_string o "ff" - | X c -> output_string o "X " - | A(_,t,_) -> Printf.fprintf o "A(%a)" Tag.pp t - | C(f1,f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2 - | D(f1,f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2 - | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)" - pp_formula f1 - (match n with - | Some id -> Names.Id.to_string id - | None -> "") pp_formula f2 - | N(f) -> Printf.fprintf o "N(%a)" pp_formula f - - -let rec map_atoms fct f = - match f with - | TT -> TT - | FF -> FF - | X x -> X x - | A (at,tg,cstr) -> A(fct at,tg,cstr) - | C (f1,f2) -> C(map_atoms fct f1, map_atoms fct f2) - | D (f1,f2) -> D(map_atoms fct f1, map_atoms fct f2) - | N f -> N(map_atoms fct f) - | I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2) - -let rec map_prop fct f = - match f with - | TT -> TT - | FF -> FF - | X x -> X (fct x) - | A (at,tg,cstr) -> A(at,tg,cstr) - | C (f1,f2) -> C(map_prop fct f1, map_prop fct f2) - | D (f1,f2) -> D(map_prop fct f1, map_prop fct f2) - | N f -> N(map_prop fct f) - | I(f1,o,f2) -> I(map_prop fct f1, o , map_prop fct f2) - -(** - * Collect the identifiers of a (string of) implications. Implication labels - * are inherited from Coq/CoC's higher order dependent type constructor (Pi). - *) - -let rec ids_of_formula f = - match f with - | I(f1,Some id,f2) -> id::(ids_of_formula f2) - | _ -> [] - -(** - * A clause is a list of (tagged) nFormulas. - * nFormulas are normalized formulas, i.e., of the form: - * cPol \{=,<>,>,>=\} 0 - * with cPol compact polynomials (see the Pol inductive type in EnvRing.v). - *) - -type 'cst clause = ('cst Micromega.nFormula * tag) list - -(** - * A CNF is a list of clauses. - *) - -type 'cst cnf = ('cst clause) list - -(** - * True and False are empty cnfs and clauses. - *) - -let tt : 'cst cnf = [] - -let ff : 'cst cnf = [ [] ] - -(** - * A refinement of cnf with tags left out. This is an intermediary form - * between the cnf tagged list representation ('cst cnf) used to solve psatz, - * and the freeform formulas ('cst formula) that is retrieved from Coq. - *) - -module Mc = Micromega - -type 'cst mc_cnf = ('cst Mc.nFormula) list list - -(** - * From a freeform formula, build a cnf. - * The parametric functions negate and normalize are theory-dependent, and - * originate in micromega.ml (extracted, e.g. for rnegate, from RMicromega.v - * and RingMicromega.v). - *) - -type 'a tagged_option = T of tag list | S of 'a - -let cnf - (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) - (unsat : 'cst Mc.nFormula -> bool) (deduce : 'cst Mc.nFormula -> 'cst Mc.nFormula -> 'cst Mc.nFormula option) (f:'cst formula) = - - let negate a t = - List.map (fun cl -> List.map (fun x -> (x,t)) cl) (negate a) in - - let normalise a t = - List.map (fun cl -> List.map (fun x -> (x,t)) cl) (normalise a) in - - let and_cnf x y = x @ y in - -let rec add_term t0 = function - | [] -> - (match deduce (fst t0) (fst t0) with - | Some u -> if unsat u then T [snd t0] else S (t0::[]) - | None -> S (t0::[])) - | t'::cl0 -> - (match deduce (fst t0) (fst t') with - | Some u -> - if unsat u - then T [snd t0 ; snd t'] - else (match add_term t0 cl0 with - | S cl' -> S (t'::cl') - | T l -> T l) - | None -> - (match add_term t0 cl0 with - | S cl' -> S (t'::cl') - | T l -> T l)) in - - - let rec or_clause cl1 cl2 = - match cl1 with - | [] -> S cl2 - | t0::cl -> - (match add_term t0 cl2 with - | S cl' -> or_clause cl cl' - | T l -> T l) in - - - - let or_clause_cnf t f = - List.fold_right (fun e (acc,tg) -> - match or_clause t e with - | S cl -> (cl :: acc,tg) - | T l -> (acc,tg@l)) f ([],[]) in - - - let rec or_cnf f f' = - match f with - | [] -> tt,[] - | e :: rst -> - let (rst_f',t) = or_cnf rst f' in - let (e_f', t') = or_clause_cnf e f' in - (rst_f' @ e_f', t @ t') in - - - let rec xcnf (polarity : bool) f = - match f with - | TT -> if polarity then (tt,[]) else (ff,[]) - | FF -> if polarity then (ff,[]) else (tt,[]) - | X p -> if polarity then (ff,[]) else (ff,[]) - | A(x,t,_) -> ((if polarity then normalise x t else negate x t),[]) - | N(e) -> xcnf (not polarity) e - | C(e1,e2) -> - let e1,t1 = xcnf polarity e1 in - let e2,t2 = xcnf polarity e2 in - if polarity - then and_cnf e1 e2, t1 @ t2 - else let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - | D(e1,e2) -> - let e1,t1 = xcnf polarity e1 in - let e2,t2 = xcnf polarity e2 in - if polarity - then let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - else and_cnf e1 e2, t1 @ t2 - | I(e1,_,e2) -> - let e1 , t1 = (xcnf (not polarity) e1) in - let e2 , t2 = (xcnf polarity e2) in - if polarity - then let f',t' = or_cnf e1 e2 in - (f', t1 @ t2 @ t') - else and_cnf e1 e2, t1 @ t2 in - - xcnf true f - -(** - * MODULE: Ordered set of integers. - *) - -module ISet = Set.Make(Int) - -(** - * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of - * elements of m that are at position i0,...,iN. - *) - -let selecti s m = - let rec xselecti i m = - match m with - | [] -> [] - | e::m -> if ISet.mem i s then e::(xselecti (i+1) m) else xselecti (i+1) m in - xselecti 0 m - -(** - * MODULE: Mapping of the Coq data-strustures into Caml and Caml extracted - * code. This includes initializing Caml variables based on Coq terms, parsing - * various Coq expressions into Caml, and dumping Caml expressions into Coq. - * - * Opened here and in csdpcert.ml. - *) - -module M = -struct - - (** - * Location of the Coq libraries. - *) - - let logic_dir = ["Coq";"Logic";"Decidable"] - - let mic_modules = - [ - ["Coq";"Lists";"List"]; - ["ZMicromega"]; - ["Tauto"]; - ["RingMicromega"]; - ["EnvRing"]; - ["Coq"; "micromega"; "ZMicromega"]; - ["Coq"; "micromega"; "RMicromega"]; - ["Coq" ; "micromega" ; "Tauto"]; - ["Coq" ; "micromega" ; "RingMicromega"]; - ["Coq" ; "micromega" ; "EnvRing"]; - ["Coq";"QArith"; "QArith_base"]; - ["Coq";"Reals" ; "Rdefinitions"]; - ["Coq";"Reals" ; "Rpow_def"]; - ["LRing_normalise"]] - - let coq_modules = - Coqlib.(init_modules @ - [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules) - - let bin_module = [["Coq";"Numbers";"BinNums"]] - - let r_modules = - [["Coq";"Reals" ; "Rdefinitions"]; - ["Coq";"Reals" ; "Rpow_def"] ; - ["Coq";"Reals" ; "Raxioms"] ; - ["Coq";"QArith"; "Qreals"] ; - ] - - let z_modules = [["Coq";"ZArith";"BinInt"]] - - (** - * Initialization : a large amount of Caml symbols are derived from - * ZMicromega.v - *) - - let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) - let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules - let constant = gen_constant_in_modules "ZMicromega" coq_modules - let bin_constant = gen_constant_in_modules "ZMicromega" bin_module - let r_constant = gen_constant_in_modules "ZMicromega" r_modules - let z_constant = gen_constant_in_modules "ZMicromega" z_modules - let m_constant = gen_constant_in_modules "ZMicromega" mic_modules - - let coq_and = lazy (init_constant "and") - let coq_or = lazy (init_constant "or") - let coq_not = lazy (init_constant "not") - - let coq_iff = lazy (init_constant "iff") - let coq_True = lazy (init_constant "True") - let coq_False = lazy (init_constant "False") - - let coq_cons = lazy (constant "cons") - let coq_nil = lazy (constant "nil") - let coq_list = lazy (constant "list") - - let coq_O = lazy (init_constant "O") - let coq_S = lazy (init_constant "S") - - let coq_N0 = lazy (bin_constant "N0") - let coq_Npos = lazy (bin_constant "Npos") - - let coq_xH = lazy (bin_constant "xH") - let coq_xO = lazy (bin_constant "xO") - let coq_xI = lazy (bin_constant "xI") - - let coq_Z = lazy (bin_constant "Z") - let coq_ZERO = lazy (bin_constant "Z0") - let coq_POS = lazy (bin_constant "Zpos") - let coq_NEG = lazy (bin_constant "Zneg") - - let coq_Q = lazy (constant "Q") - let coq_R = lazy (constant "R") - - let coq_Qmake = lazy (constant "Qmake") - - let coq_Rcst = lazy (constant "Rcst") - - let coq_C0 = lazy (m_constant "C0") - let coq_C1 = lazy (m_constant "C1") - let coq_CQ = lazy (m_constant "CQ") - let coq_CZ = lazy (m_constant "CZ") - let coq_CPlus = lazy (m_constant "CPlus") - let coq_CMinus = lazy (m_constant "CMinus") - let coq_CMult = lazy (m_constant "CMult") - let coq_CInv = lazy (m_constant "CInv") - let coq_COpp = lazy (m_constant "COpp") - - - let coq_R0 = lazy (constant "R0") - let coq_R1 = lazy (constant "R1") - - let coq_proofTerm = lazy (constant "ZArithProof") - let coq_doneProof = lazy (constant "DoneProof") - let coq_ratProof = lazy (constant "RatProof") - let coq_cutProof = lazy (constant "CutProof") - let coq_enumProof = lazy (constant "EnumProof") - - let coq_Zgt = lazy (z_constant "Z.gt") - let coq_Zge = lazy (z_constant "Z.ge") - let coq_Zle = lazy (z_constant "Z.le") - let coq_Zlt = lazy (z_constant "Z.lt") - let coq_Eq = lazy (init_constant "eq") - - let coq_Zplus = lazy (z_constant "Z.add") - let coq_Zminus = lazy (z_constant "Z.sub") - let coq_Zopp = lazy (z_constant "Z.opp") - let coq_Zmult = lazy (z_constant "Z.mul") - let coq_Zpower = lazy (z_constant "Z.pow") - - let coq_Qle = lazy (constant "Qle") - let coq_Qlt = lazy (constant "Qlt") - let coq_Qeq = lazy (constant "Qeq") - - let coq_Qplus = lazy (constant "Qplus") - let coq_Qminus = lazy (constant "Qminus") - let coq_Qopp = lazy (constant "Qopp") - let coq_Qmult = lazy (constant "Qmult") - let coq_Qpower = lazy (constant "Qpower") - - let coq_Rgt = lazy (r_constant "Rgt") - let coq_Rge = lazy (r_constant "Rge") - let coq_Rle = lazy (r_constant "Rle") - let coq_Rlt = lazy (r_constant "Rlt") - - let coq_Rplus = lazy (r_constant "Rplus") - let coq_Rminus = lazy (r_constant "Rminus") - let coq_Ropp = lazy (r_constant "Ropp") - let coq_Rmult = lazy (r_constant "Rmult") - let coq_Rinv = lazy (r_constant "Rinv") - let coq_Rpower = lazy (r_constant "pow") - let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (r_constant "Q2R") - - - let coq_PEX = lazy (constant "PEX" ) - let coq_PEc = lazy (constant"PEc") - let coq_PEadd = lazy (constant "PEadd") - let coq_PEopp = lazy (constant "PEopp") - let coq_PEmul = lazy (constant "PEmul") - let coq_PEsub = lazy (constant "PEsub") - let coq_PEpow = lazy (constant "PEpow") - - let coq_PX = lazy (constant "PX" ) - let coq_Pc = lazy (constant"Pc") - let coq_Pinj = lazy (constant "Pinj") - - let coq_OpEq = lazy (constant "OpEq") - let coq_OpNEq = lazy (constant "OpNEq") - let coq_OpLe = lazy (constant "OpLe") - let coq_OpLt = lazy (constant "OpLt") - let coq_OpGe = lazy (constant "OpGe") - let coq_OpGt = lazy (constant "OpGt") - - let coq_PsatzIn = lazy (constant "PsatzIn") - let coq_PsatzSquare = lazy (constant "PsatzSquare") - let coq_PsatzMulE = lazy (constant "PsatzMulE") - let coq_PsatzMultC = lazy (constant "PsatzMulC") - let coq_PsatzAdd = lazy (constant "PsatzAdd") - let coq_PsatzC = lazy (constant "PsatzC") - let coq_PsatzZ = lazy (constant "PsatzZ") - - let coq_TT = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "TT") - let coq_FF = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "FF") - let coq_And = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "Cj") - let coq_Or = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "D") - let coq_Neg = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "N") - let coq_Atom = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "A") - let coq_X = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "X") - let coq_Impl = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "I") - let coq_Formula = lazy - (gen_constant_in_modules "ZMicromega" - [["Coq" ; "micromega" ; "Tauto"];["Tauto"]] "BFormula") - - (** - * Initialization : a few Caml symbols are derived from other libraries; - * QMicromega, ZArithRing, RingMicromega. - *) - - let coq_QWitness = lazy - (gen_constant_in_modules "QMicromega" - [["Coq"; "micromega"; "QMicromega"]] "QWitness") - - let coq_Build = lazy - (gen_constant_in_modules "RingMicromega" - [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] - "Build_Formula") - let coq_Cstr = lazy - (gen_constant_in_modules "RingMicromega" - [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula") - - (** - * Parsing and dumping : transformation functions between Caml and Coq - * data-structures. - * - * dump_* functions go from Micromega to Coq terms - * parse_* functions go from Coq to Micromega terms - * pp_* functions pretty-print Coq terms. - *) - - exception ParseError - - (* A simple but useful getter function *) - - let get_left_construct sigma term = - match EConstr.kind sigma term with - | Construct((_,i),_) -> (i,[| |]) - | App(l,rst) -> - (match EConstr.kind sigma l with - | Construct((_,i),_) -> (i,rst) - | _ -> raise ParseError - ) - | _ -> raise ParseError - - (* Access the Micromega module *) - - (* parse/dump/print from numbers up to expressions and formulas *) - - let rec parse_nat sigma term = - let (i,c) = get_left_construct sigma term in - match i with - | 1 -> Mc.O - | 2 -> Mc.S (parse_nat sigma (c.(0))) - | i -> raise ParseError - - let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n) - - let rec dump_nat x = - match x with - | Mc.O -> Lazy.force coq_O - | Mc.S p -> EConstr.mkApp(Lazy.force coq_S,[| dump_nat p |]) - - let rec parse_positive sigma term = - let (i,c) = get_left_construct sigma term in - match i with - | 1 -> Mc.XI (parse_positive sigma c.(0)) - | 2 -> Mc.XO (parse_positive sigma c.(0)) - | 3 -> Mc.XH - | i -> raise ParseError - - let rec dump_positive x = - match x with - | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_positive p |]) - | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_positive p |]) - - let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) - - let dump_n x = - match x with - | Mc.N0 -> Lazy.force coq_N0 - | Mc.Npos p -> EConstr.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) - - let parse_z sigma term = - let (i,c) = get_left_construct sigma term in - match i with - | 1 -> Mc.Z0 - | 2 -> Mc.Zpos (parse_positive sigma c.(0)) - | 3 -> Mc.Zneg (parse_positive sigma c.(0)) - | i -> raise ParseError - - let dump_z x = - match x with - | Mc.Z0 ->Lazy.force coq_ZERO - | Mc.Zpos p -> EConstr.mkApp(Lazy.force coq_POS,[| dump_positive p|]) - | Mc.Zneg p -> EConstr.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) - - let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x)) - - let dump_q q = - EConstr.mkApp(Lazy.force coq_Qmake, - [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|]) - - let parse_q sigma term = - match EConstr.kind sigma term with - | App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then - {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) } - else raise ParseError - | _ -> raise ParseError - - - let rec pp_Rcst o cst = - match cst with - | Mc.C0 -> output_string o "C0" - | Mc.C1 -> output_string o "C1" - | Mc.CQ q -> output_string o "CQ _" - | Mc.CZ z -> pp_z o z - | Mc.CPlus(x,y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y - | Mc.CMinus(x,y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y - | Mc.CMult(x,y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y - | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t - | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t - - - let rec dump_Rcst cst = - match cst with - | Mc.C0 -> Lazy.force coq_C0 - | Mc.C1 -> Lazy.force coq_C1 - | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_CQ, [| dump_q q |]) - | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_CZ, [| dump_z z |]) - | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) - | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) - - let rec dump_list typ dump_elt l = - match l with - | [] -> EConstr.mkApp(Lazy.force coq_nil,[| typ |]) - | e :: l -> EConstr.mkApp(Lazy.force coq_cons, - [| typ; dump_elt e;dump_list typ dump_elt l|]) - - let pp_list op cl elt o l = - let rec _pp o l = - match l with - | [] -> () - | [e] -> Printf.fprintf o "%a" elt e - | e::l -> Printf.fprintf o "%a ,%a" elt e _pp l in - Printf.fprintf o "%s%a%s" op _pp l cl - - let dump_var = dump_positive - - let dump_expr typ dump_z e = - let rec dump_expr e = - match e with - | Mc.PEX n -> EConstr.mkApp(Lazy.force coq_PEX,[| typ; dump_var n |]) - | Mc.PEc z -> EConstr.mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |]) - | Mc.PEadd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEadd, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEsub, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp(Lazy.force coq_PEopp, - [| typ; dump_expr e|]) - | Mc.PEmul(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEmul, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> EConstr.mkApp(Lazy.force coq_PEpow, - [| typ; dump_expr e; dump_n n|]) - in - dump_expr e - - let dump_pol typ dump_c e = - let rec dump_pol e = - match e with - | Mc.Pc n -> EConstr.mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|]) - | Mc.Pinj(p,pol) -> EConstr.mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|]) - | Mc.PX(pol1,p,pol2) -> EConstr.mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in - dump_pol e - - let pp_pol pp_c o e = - let rec pp_pol o e = - match e with - | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n - | Mc.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol - | Mc.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in - pp_pol o e - - let pp_cnf pp_c o f = - let pp_clause o l = List.iter (fun ((p,_),t) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) l in - List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause l) f - - let dump_psatz typ dump_z e = - let z = Lazy.force typ in - let rec dump_cone e = - match e with - | Mc.PsatzIn n -> EConstr.mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |]) - | Mc.PsatzMulC(e,c) -> EConstr.mkApp(Lazy.force coq_PsatzMultC, - [| z; dump_pol z dump_z e ; dump_cone c |]) - | Mc.PsatzSquare e -> EConstr.mkApp(Lazy.force coq_PsatzSquare, - [| z;dump_pol z dump_z e|]) - | Mc.PsatzAdd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzAdd, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzMulE(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzMulE, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzC p -> EConstr.mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|]) - | Mc.PsatzZ -> EConstr.mkApp(Lazy.force coq_PsatzZ,[| z|]) in - dump_cone e - - let pp_psatz pp_z o e = - let rec pp_cone o e = - match e with - | Mc.PsatzIn n -> - Printf.fprintf o "(In %a)%%nat" pp_nat n - | Mc.PsatzMulC(e,c) -> - Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c - | Mc.PsatzSquare e -> - Printf.fprintf o "(%a^2)" (pp_pol pp_z) e - | Mc.PsatzAdd(e1,e2) -> - Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 - | Mc.PsatzMulE(e1,e2) -> - Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 - | Mc.PsatzC p -> - Printf.fprintf o "(%a)%%positive" pp_z p - | Mc.PsatzZ -> - Printf.fprintf o "0" in - pp_cone o e - - let dump_op = function - | Mc.OpEq-> Lazy.force coq_OpEq - | Mc.OpNEq-> Lazy.force coq_OpNEq - | Mc.OpLe -> Lazy.force coq_OpLe - | Mc.OpGe -> Lazy.force coq_OpGe - | Mc.OpGt-> Lazy.force coq_OpGt - | Mc.OpLt-> Lazy.force coq_OpLt - - let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} = - EConstr.mkApp(Lazy.force coq_Build, - [| typ; dump_expr typ dump_constant e1 ; - dump_op o ; - dump_expr typ dump_constant e2|]) - - let assoc_const sigma x l = - try - snd (List.find (fun (x',y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) - with - Not_found -> raise ParseError - - let zop_table = [ - coq_Zgt, Mc.OpGt ; - coq_Zge, Mc.OpGe ; - coq_Zlt, Mc.OpLt ; - coq_Zle, Mc.OpLe ] - - let rop_table = [ - coq_Rgt, Mc.OpGt ; - coq_Rge, Mc.OpGe ; - coq_Rlt, Mc.OpLt ; - coq_Rle, Mc.OpLe ] - - let qop_table = [ - coq_Qlt, Mc.OpLt ; - coq_Qle, Mc.OpLe ; - coq_Qeq, Mc.OpEq - ] - - type gl = { env : Environ.env; sigma : Evd.evar_map } - - let is_convertible gl t1 t2 = - Reductionops.is_conv gl.env gl.sigma t1 t2 - - let parse_zop gl (op,args) = - let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" - - let parse_rop gl (op,args) = - let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" - - let parse_qop gl (op,args) = - (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) - - type 'a op = - | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) - | Opp - | Power - | Ukn of string - - let assoc_ops sigma x l = - try - snd (List.find (fun (x',y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) - with - Not_found -> Ukn "Oups" - - (** - * MODULE: Env is for environment. - *) - - module Env = - struct - let compute_rank_add env sigma v = - let rec _add env n v = - match env with - | [] -> ([v],n) - | e::l -> - if EConstr.eq_constr sigma e v - then (env,n) - else - let (env,n) = _add l ( n+1) v in - (e::env,n) in - let (env, n) = _add env 1 v in - (env, CamlToCoq.positive n) - - let get_rank env sigma v = - - let rec _get_rank env n = - match env with - | [] -> raise (Invalid_argument "get_rank") - | e::l -> - if EConstr.eq_constr sigma e v - then n - else _get_rank l (n+1) in - _get_rank env 1 - - - let empty = [] - - let elements env = env - - end (* MODULE END: Env *) - - (** - * This is the big generic function for expression parsers. - *) - - let parse_expr sigma parse_constant parse_exp ops_spec env term = - if debug - then ( - let _, env = Pfedit.get_current_context () in - Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); - -(* - let constant_or_variable env term = - try - ( Mc.PEc (parse_constant term) , env) - with ParseError -> - let (env,n) = Env.compute_rank_add env term in - (Mc.PEX n , env) in -*) - let parse_variable env term = - let (env,n) = Env.compute_rank_add env sigma term in - (Mc.PEX n , env) in - - let rec parse_expr env term = - let combine env op (t1,t2) = - let (expr1,env) = parse_expr env t1 in - let (expr2,env) = parse_expr env t2 in - (op expr1 expr2,env) in - - try (Mc.PEc (parse_constant term) , env) - with ParseError -> - match EConstr.kind sigma term with - | App(t,args) -> - ( - match EConstr.kind sigma t with - | Const c -> - ( match assoc_ops sigma t ops_spec with - | Binop f -> combine env f (args.(0),args.(1)) - | Opp -> let (expr,env) = parse_expr env args.(0) in - (Mc.PEopp expr, env) - | Power -> - begin - try - let (expr,env) = parse_expr env args.(0) in - let power = (parse_exp expr args.(1)) in - (power , env) - with e when CErrors.noncritical e -> - (* if the exponent is a variable *) - let (env,n) = Env.compute_rank_add env sigma term in (Mc.PEX n, env) - end - | Ukn s -> - if debug - then (Printf.printf "unknown op: %s\n" s; flush stdout;); - let (env,n) = Env.compute_rank_add env sigma term in (Mc.PEX n, env) - ) - | _ -> parse_variable env term - ) - | _ -> parse_variable env term in - parse_expr env term - - let zop_spec = - [ - coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ; - coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ; - coq_Zmult , Binop (fun x y -> Mc.PEmul (x,y)) ; - coq_Zopp , Opp ; - coq_Zpower , Power] - - let qop_spec = - [ - coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ; - coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ; - coq_Qmult , Binop (fun x y -> Mc.PEmul (x,y)) ; - coq_Qopp , Opp ; - coq_Qpower , Power] - - let rop_spec = - [ - coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ; - coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ; - coq_Rmult , Binop (fun x y -> Mc.PEmul (x,y)) ; - coq_Ropp , Opp ; - coq_Rpower , Power] - - let zconstant = parse_z - let qconstant = parse_q - - - let rconst_assoc = - [ - coq_Rplus , (fun x y -> Mc.CPlus(x,y)) ; - coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ; - coq_Rmult , (fun x y -> Mc.CMult(x,y)) ; - (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) - ] - - let rec rconstant sigma term = - match EConstr.kind sigma term with - | Const x -> - if EConstr.eq_constr sigma term (Lazy.force coq_R0) - then Mc.C0 - else if EConstr.eq_constr sigma term (Lazy.force coq_R1) - then Mc.C1 - else raise ParseError - | App(op,args) -> - begin - try - (* the evaluation order is important in the following *) - let f = assoc_const sigma op rconst_assoc in - let a = rconstant sigma args.(0) in - let b = rconstant sigma args.(1) in - f a b - with - ParseError -> - match op with - | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> - let arg = rconstant sigma args.(0) in - if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0 ; Mc.qden = Mc.XH} - then raise ParseError (* This is a division by zero -- no semantics *) - else Mc.CInv(arg) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> Mc.CQ (parse_q sigma args.(0)) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> Mc.CZ (parse_z sigma args.(0)) - | _ -> raise ParseError - end - - | _ -> raise ParseError - - - let rconstant sigma term = - let _, env = Pfedit.get_current_context () in - if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); - let res = rconstant sigma term in - if debug then - (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; - res - - - let parse_zexpr sigma = parse_expr sigma - (zconstant sigma) - (fun expr x -> - let exp = (parse_z sigma x) in - match exp with - | Mc.Zneg _ -> Mc.PEc Mc.Z0 - | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) - zop_spec - - let parse_qexpr sigma = parse_expr sigma - (qconstant sigma) - (fun expr x -> - let exp = parse_z sigma x in - match exp with - | Mc.Zneg _ -> - begin - match expr with - | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) - | _ -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError - end - | _ -> let exp = Mc.Z.to_N exp in - Mc.PEpow(expr,exp)) - qop_spec - - let parse_rexpr sigma = parse_expr sigma - (rconstant sigma) - (fun expr x -> - let exp = Mc.N.of_nat (parse_nat sigma x) in - Mc.PEpow(expr,exp)) - rop_spec - - let parse_arith parse_op parse_expr env cstr gl = - let sigma = gl.sigma in - if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); - match EConstr.kind sigma cstr with - | App(op,args) -> - let (op,lhs,rhs) = parse_op gl (op,args) in - let (e1,env) = parse_expr sigma env lhs in - let (e2,env) = parse_expr sigma env rhs in - ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env) - | _ -> failwith "error : parse_arith(2)" - - let parse_zarith = parse_arith parse_zop parse_zexpr - - let parse_qarith = parse_arith parse_qop parse_qexpr - - let parse_rarith = parse_arith parse_rop parse_rexpr - - (* generic parsing of arithmetic expressions *) - - let mkC f1 f2 = C(f1,f2) - let mkD f1 f2 = D(f1,f2) - let mkIff f1 f2 = C(I(f1,None,f2),I(f2,None,f1)) - let mkI f1 f2 = I(f1,None,f2) - - let mkformula_binary g term f1 f2 = - match f1 , f2 with - | X _ , X _ -> X(term) - | _ -> g f1 f2 - - (** - * This is the big generic function for formula parsers. - *) - - let parse_formula gl parse_atom env tg term = - let sigma = gl.sigma in - - let parse_atom env tg t = - try - let (at,env) = parse_atom env t gl in - (A(at,tg,t), env,Tag.next tg) - with e when CErrors.noncritical e -> (X(t),env,tg) in - - let is_prop term = - let sort = Retyping.get_sort_of gl.env gl.sigma term in - Sorts.is_prop sort in - - let rec xparse_formula env tg term = - match EConstr.kind sigma term with - | App(l,rst) -> - (match rst with - | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) -> - let f,env,tg = xparse_formula env tg a in - let g,env, tg = xparse_formula env tg b in - mkformula_binary mkC term f g,env,tg - | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_or) -> - let f,env,tg = xparse_formula env tg a in - let g,env,tg = xparse_formula env tg b in - mkformula_binary mkD term f g,env,tg - | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) -> - let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) - | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_iff) -> - let f,env,tg = xparse_formula env tg a in - let g,env,tg = xparse_formula env tg b in - mkformula_binary mkIff term f g,env,tg - | _ -> parse_atom env tg term) - | Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b -> - let f,env,tg = xparse_formula env tg a in - let g,env,tg = xparse_formula env tg b in - mkformula_binary mkI term f g,env,tg - | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg) - | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg) - | _ when is_prop term -> X(term),env,tg - | _ -> raise ParseError - in - xparse_formula env tg ((*Reductionops.whd_zeta*) term) - - let dump_formula typ dump_atom f = - let rec xdump f = - match f with - | TT -> EConstr.mkApp(Lazy.force coq_TT,[|typ|]) - | FF -> EConstr.mkApp(Lazy.force coq_FF,[|typ|]) - | C(x,y) -> EConstr.mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|]) - | D(x,y) -> EConstr.mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|]) - | I(x,_,y) -> EConstr.mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|]) - | N(x) -> EConstr.mkApp(Lazy.force coq_Neg,[|typ ; xdump x|]) - | A(x,_,_) -> EConstr.mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|]) - | X(t) -> EConstr.mkApp(Lazy.force coq_X,[|typ ; t|]) in - xdump f - - - let prop_env_of_formula sigma form = - let rec doit env = function - | TT | FF | A(_,_,_) -> env - | X t -> fst (Env.compute_rank_add env sigma t) - | C(f1,f2) | D(f1,f2) | I(f1,_,f2) -> - doit (doit env f1) f2 - | N f -> doit env f in - - doit [] form - - let var_env_of_formula form = - - let rec vars_of_expr = function - | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n) - | Mc.PEc z -> ISet.empty - | Mc.PEadd(e1,e2) | Mc.PEmul(e1,e2) | Mc.PEsub(e1,e2) -> - ISet.union (vars_of_expr e1) (vars_of_expr e2) - | Mc.PEopp e | Mc.PEpow(e,_)-> vars_of_expr e - in - - let vars_of_atom {Mc.flhs ; Mc.fop; Mc.frhs} = - ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in - - let rec doit = function - | TT | FF | X _ -> ISet.empty - | A (a,t,c) -> vars_of_atom a - | C(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2) - | N f -> doit f in - - doit form - - - - - type 'cst dump_expr = (* 'cst is the type of the syntactic constants *) - { - interp_typ : EConstr.constr; - dump_cst : 'cst -> EConstr.constr; - dump_add : EConstr.constr; - dump_sub : EConstr.constr; - dump_opp : EConstr.constr; - dump_mul : EConstr.constr; - dump_pow : EConstr.constr; - dump_pow_arg : Mc.n -> EConstr.constr; - dump_op : (Mc.op2 * EConstr.constr) list - } - -let dump_zexpr = lazy - { - interp_typ = Lazy.force coq_Z; - dump_cst = dump_z; - dump_add = Lazy.force coq_Zplus; - dump_sub = Lazy.force coq_Zminus; - dump_opp = Lazy.force coq_Zopp; - dump_mul = Lazy.force coq_Zmult; - dump_pow = Lazy.force coq_Zpower; - dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) zop_table - } - -let dump_qexpr = lazy - { - interp_typ = Lazy.force coq_Q; - dump_cst = dump_q; - dump_add = Lazy.force coq_Qplus; - dump_sub = Lazy.force coq_Qminus; - dump_opp = Lazy.force coq_Qopp; - dump_mul = Lazy.force coq_Qmult; - dump_pow = Lazy.force coq_Qpower; - dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table - } - -let rec dump_Rcst_as_R cst = - match cst with - | Mc.C0 -> Lazy.force coq_R0 - | Mc.C1 -> Lazy.force coq_R1 - | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_IQR, [| dump_q q |]) - | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_IZR, [| dump_z z |]) - | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |]) - | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |]) - - -let dump_rexpr = lazy - { - interp_typ = Lazy.force coq_R; - dump_cst = dump_Rcst_as_R; - dump_add = Lazy.force coq_Rplus; - dump_sub = Lazy.force coq_Rminus; - dump_opp = Lazy.force coq_Ropp; - dump_mul = Lazy.force coq_Rmult; - dump_pow = Lazy.force coq_Rpower; - dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))); - dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table - } - - - - -(** [make_goal_of_formula depxr vars props form] where - - vars is an environment for the arithmetic variables occuring in form - - props is an environment for the propositions occuring in form - @return a goal where all the variables and propositions of the formula are quantified - -*) - -let prodn n env b = - let rec prodrec = function - | (0, env, b) -> b - | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (v,t,b)) - | _ -> assert false - in - prodrec (n,env,b) - -let make_goal_of_formula sigma dexpr form = - - let vars_idx = - List.mapi (fun i v -> (v, i+1)) (ISet.elements (var_env_of_formula form)) in - - (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) - - let props = prop_env_of_formula sigma form in - - let vars_n = List.map (fun (_,i) -> (Names.Id.of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in - let props_n = List.mapi (fun i _ -> (Names.Id.of_string (Printf.sprintf "__p%i" (i+1))) , EConstr.mkProp) props in - - let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in - - let dump_expr i e = - let rec dump_expr = function - | Mc.PEX n -> EConstr.mkRel (i+(List.assoc (CoqToCaml.positive n) vars_idx)) - | Mc.PEc z -> dexpr.dump_cst z - | Mc.PEadd(e1,e2) -> EConstr.mkApp(dexpr.dump_add, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> EConstr.mkApp(dexpr.dump_sub, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp(dexpr.dump_opp, - [| dump_expr e|]) - | Mc.PEmul(e1,e2) -> EConstr.mkApp(dexpr.dump_mul, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> EConstr.mkApp(dexpr.dump_pow, - [| dump_expr e; dexpr.dump_pow_arg n|]) - in dump_expr e in - - let mkop op e1 e2 = - try - EConstr.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) - with Not_found -> - EConstr.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in - - let dump_cstr i { Mc.flhs ; Mc.fop ; Mc.frhs } = - mkop fop (dump_expr i flhs) (dump_expr i frhs) in - - let rec xdump pi xi f = - match f with - | TT -> Lazy.force coq_True - | FF -> Lazy.force coq_False - | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) - | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) - | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False) - | A(x,_,_) -> dump_cstr xi x - | X(t) -> let idx = Env.get_rank props sigma t in - EConstr.mkRel (pi+idx) in - - let nb_vars = List.length vars_n in - let nb_props = List.length props_n in - - (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) - - let subst_prop p = - let idx = Env.get_rank props sigma p in - EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in - - let form' = map_prop subst_prop form in - - (prodn nb_props (List.map (fun (x,y) -> Name.Name x,y) props_n) - (prodn nb_vars (List.map (fun (x,y) -> Name.Name x,y) vars_n) - (xdump (List.length vars_n) 0 form)), - List.rev props_n, List.rev var_name_pos,form') - - (** - * Given a conclusion and a list of affectations, rebuild a term prefixed by - * the appropriate letins. - * TODO: reverse the list of bindings! - *) - - let set l concl = - let rec xset acc = function - | [] -> acc - | (e::l) -> - let (name,expr,typ) = e in - xset (EConstr.mkNamedLetIn - (Names.Id.of_string name) - expr typ acc) l in - xset concl l - -end (** - * MODULE END: M - *) - -open M - -let coq_Node = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") -let coq_Leaf = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") -let coq_Empty = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") - -let coq_VarMap = - lazy (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") - - -let rec dump_varmap typ m = - match m with - | Mc.Empty -> EConstr.mkApp(Lazy.force coq_Empty,[| typ |]) - | Mc.Leaf v -> EConstr.mkApp(Lazy.force coq_Leaf,[| typ; v|]) - | Mc.Node(l,o,r) -> - EConstr.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) - - -let vm_of_list env = - match env with - | [] -> Mc.Empty - | (d,_)::_ -> - List.fold_left (fun vm (c,i) -> - Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env - -let rec dump_proof_term = function - | Micromega.DoneProof -> Lazy.force coq_doneProof - | Micromega.RatProof(cone,rst) -> - EConstr.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) - | Micromega.CutProof(cone,prf) -> - EConstr.mkApp(Lazy.force coq_cutProof, - [| dump_psatz coq_Z dump_z cone ; - dump_proof_term prf|]) - | Micromega.EnumProof(c1,c2,prfs) -> - EConstr.mkApp (Lazy.force coq_enumProof, - [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; - dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) - - -let rec size_of_psatz = function - | Micromega.PsatzIn _ -> 1 - | Micromega.PsatzSquare _ -> 1 - | Micromega.PsatzMulC(_,p) -> 1 + (size_of_psatz p) - | Micromega.PsatzMulE(p1,p2) | Micromega.PsatzAdd(p1,p2) -> size_of_psatz p1 + size_of_psatz p2 - | Micromega.PsatzC _ -> 1 - | Micromega.PsatzZ -> 1 - -let rec size_of_pf = function - | Micromega.DoneProof -> 1 - | Micromega.RatProof(p,a) -> (size_of_pf a) + (size_of_psatz p) - | Micromega.CutProof(p,a) -> (size_of_pf a) + (size_of_psatz p) - | Micromega.EnumProof(p1,p2,l) -> (size_of_psatz p1) + (size_of_psatz p2) + (List.fold_left (fun acc p -> size_of_pf p + acc) 0 l) - -let dump_proof_term t = - if debug then Printf.printf "dump_proof_term %i\n" (size_of_pf t) ; - dump_proof_term t - - - -let pp_q o q = Printf.fprintf o "%a/%a" pp_z q.Micromega.qnum pp_positive q.Micromega.qden - - -let rec pp_proof_term o = function - | Micromega.DoneProof -> Printf.fprintf o "D" - | Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | Micromega.EnumProof(c1,c2,rst) -> - Printf.fprintf o "EP[%a,%a,%a]" - (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 - (pp_list "[" "]" pp_proof_term) rst - -let rec parse_hyps gl parse_arith env tg hyps = - match hyps with - | [] -> ([],env,tg) - | (i,t)::l -> - let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in - try - let (c,env,tg) = parse_formula gl parse_arith env tg t in - ((i,c)::lhyps, env,tg) - with e when CErrors.noncritical e -> (lhyps,env,tg) - (*(if debug then Printf.printf "parse_arith : %s\n" x);*) - - -(*exception ParseError*) - -let parse_goal gl parse_arith env hyps term = - (* try*) - let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in - let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in - (lhyps,f,env) - (* with Failure x -> raise ParseError*) - -(** - * The datastructures that aggregate theory-dependent proof values. - *) -type ('synt_c, 'prf) domain_spec = { - typ : EConstr.constr; (* is the type of the interpretation domain - Z, Q, R*) - coeff : EConstr.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) - dump_coeff : 'synt_c -> EConstr.constr ; - proof_typ : EConstr.constr ; - dump_proof : 'prf -> EConstr.constr -} - -let zz_domain_spec = lazy { - typ = Lazy.force coq_Z; - coeff = Lazy.force coq_Z; - dump_coeff = dump_z ; - proof_typ = Lazy.force coq_proofTerm ; - dump_proof = dump_proof_term -} - -let qq_domain_spec = lazy { - typ = Lazy.force coq_Q; - coeff = Lazy.force coq_Q; - dump_coeff = dump_q ; - proof_typ = Lazy.force coq_QWitness ; - dump_proof = dump_psatz coq_Q dump_q -} - -(** Naive topological sort of constr according to the subterm-ordering *) - -(* An element is minimal x is minimal w.r.t y if - x <= y or (x and y are incomparable) *) - -(** - * Instanciate the current Coq goal with a Micromega formula, a varmap, and a - * witness. - *) - -let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) = - (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) - let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in - let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in - let vm = dump_varmap (spec.typ) (vm_of_list env) in - (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter begin fun gl -> - Tacticals.New.tclTHENLIST - [ - Tactics.change_concl - (set - [ - ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, EConstr.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); - ("__wit", cert, cert_typ) - ] - (Tacmach.New.pf_concl gl)) - ] - end - - -(** - * The datastructures that aggregate prover attributes. - *) - -type ('option,'a,'prf) prover = { - name : string ; (* name of the prover *) - get_option : unit ->'option ; (* find the options of the prover *) - prover : 'option * 'a list -> 'prf option ; (* the prover itself *) - hyps : 'prf -> ISet.t ; (* extract the indexes of the hypotheses really used in the proof *) - compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *) - pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *) - pp_f : out_channel -> 'a -> unit (* pretty printing of the formulas (polynomials)*) -} - - - -(** - * Given a list of provers and a disjunction of atoms, find a proof of any of - * the atoms. Returns an (optional) pair of a proof and a prover - * datastructure. - *) - -let find_witness provers polys1 = - let provers = List.map (fun p -> - (fun l -> - match p.prover (p.get_option (),l) with - | None -> None - | Some prf -> Some(prf,p)) , p.name) provers in - try_any provers (List.map fst polys1) - -(** - * Given a list of provers and a CNF, find a proof for each of the clauses. - * Return the proofs as a list. - *) - -let witness_list prover l = - let rec xwitness_list l = - match l with - | [] -> Some [] - | e :: l -> - match find_witness prover e with - | None -> None - | Some w -> - (match xwitness_list l with - | None -> None - | Some l -> Some (w :: l) - ) in - xwitness_list l - -let witness_list_tags = witness_list - -(** - * Prune the proof object, according to the 'diff' between two cnf formulas. - *) - -let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = - - let compact_proof (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = - let new_cl = List.mapi (fun i (f,_) -> (f,i)) new_cl in - let remap i = - let formula = try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index" in - List.assoc formula new_cl in -(* if debug then - begin - Printf.printf "\ncompact_proof : %a %a %a" - (pp_ml_list prover.pp_f) (List.map fst old_cl) - prover.pp_prf prf - (pp_ml_list prover.pp_f) (List.map fst new_cl) ; - flush stdout - end ; *) - let res = try prover.compact prf remap with x when CErrors.noncritical x -> - if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; - (* This should not happen -- this is the recovery plan... *) - match prover.prover (prover.get_option () ,List.map fst new_cl) with - | None -> failwith "proof compaction error" - | Some p -> p - in - if debug then - begin - Printf.printf " -> %a\n" - prover.pp_prf res ; - flush stdout - end ; - res in - - let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = - let hyps_idx = prover.hyps prf in - let hyps = selecti hyps_idx old_cl in - is_sublist Pervasives.(=) hyps new_cl in - - let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *) - - List.map (fun x -> - let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res - in compact_proof o p x) cnf_ff' - - -(** - * "Hide out" tagged atoms of a formula by transforming them into generic - * variables. See the Tag module in mutils.ml for more. - *) - -let abstract_formula hyps f = - let rec xabs f = - match f with - | X c -> X c - | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term) - | C(f1,f2) -> - (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_and, [|a1;a2|])) - | f1 , f2 -> C(f1,f2) ) - | D(f1,f2) -> - (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_or, [|a1;a2|])) - | f1 , f2 -> D(f1,f2) ) - | N(f) -> - (match xabs f with - | X a -> X (EConstr.mkApp(Lazy.force coq_not, [|a|])) - | f -> N f) - | I(f1,hyp,f2) -> - (match xabs f1 , hyp, xabs f2 with - | X a1 , Some _ , af2 -> af2 - | X a1 , None , X a2 -> X (EConstr.mkArrow a1 a2) - | af1 , _ , af2 -> I(af1,hyp,af2) - ) - | FF -> FF - | TT -> TT - in xabs f - - -(* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2 *) -let rec abstract_wrt_formula f1 f2 = - match f1 , f2 with - | X c , _ -> X c - | A _ , A _ -> f2 - | C(a,b) , C(a',b') -> C(abstract_wrt_formula a a', abstract_wrt_formula b b') - | D(a,b) , D(a',b') -> D(abstract_wrt_formula a a', abstract_wrt_formula b b') - | I(a,_,b) , I(a',x,b') -> I(abstract_wrt_formula a a',x, abstract_wrt_formula b b') - | FF , FF -> FF - | TT , TT -> TT - | N x , N y -> N(abstract_wrt_formula x y) - | _ -> failwith "abstract_wrt_formula" - -(** - * This exception is raised by really_call_csdpcert if Coq's configure didn't - * find a CSDP executable. - *) - -exception CsdpNotFound - - -(** - * This is the core of Micromega: apply the prover, analyze the result and - * prune unused fomulas, and finally modify the proof state. - *) - -let formula_hyps_concl hyps concl = - List.fold_right - (fun (id,f) (cc,ids) -> - match f with - X _ -> (cc,ids) - | _ -> (I(f,Some id,cc), id::ids)) - hyps (concl,[]) - - -let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 gl = - - (* Express the goal as one big implication *) - let (ff,ids) = formula_hyps_concl polys1 polys2 in - - (* Convert the aplpication into a (mc_)cnf (a list of lists of formulas) *) - let cnf_ff,cnf_ff_tags = cnf negate normalise unsat deduce ff in - - if debug then - begin - Feedback.msg_notice (Pp.str "Formula....\n") ; - let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in - let ff = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff - end; - - match witness_list_tags prover cnf_ff with - | None -> None - | Some res -> (*Printf.printf "\nList %i" (List.length `res); *) - let hyps = List.fold_left (fun s (cl,(prf,p)) -> - let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in - if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ; - (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in - TagSet.union s tags) (List.fold_left (fun s i -> TagSet.add i s) TagSet.empty cnf_ff_tags) (List.combine cnf_ff res) in - - if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout; - Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ; - - let ff' = abstract_formula hyps ff in - let cnf_ff',_ = cnf negate normalise unsat deduce ff' in - - if debug then - begin - Feedback.msg_notice (Pp.str "\nAFormula\n") ; - let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in - let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' - end; - - (* Even if it does not work, this does not mean it is not provable - -- the prover is REALLY incomplete *) - (* if debug then - begin - (* recompute the proofs *) - match witness_list_tags prover cnf_ff' with - | None -> failwith "abstraction is wrong" - | Some res -> () - end ; *) - let res' = compact_proofs cnf_ff res cnf_ff' in - - let (ff',res',ids) = (ff',res', ids_of_formula ff') in - - let res' = dump_list (spec.proof_typ) spec.dump_proof res' in - Some (ids,ff',res') - - -(** - * Parse the proof environment, and call micromega_tauto - *) - -let fresh_id avoid id gl = - Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl) - -let micromega_gen - parse_arith - (negate:'cst atom -> 'cst mc_cnf) - (normalise:'cst atom -> 'cst mc_cnf) - unsat deduce - spec dumpexpr prover tac = - Proofview.Goal.nf_enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in - try - let gl0 = { env = Tacmach.New.pf_env gl; sigma } in - let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in - let env = Env.elements env in - let spec = Lazy.force spec in - let dumpexpr = Lazy.force dumpexpr in - - match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl0 with - | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") - | Some (ids,ff',res') -> - let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in - let intro (id,_) = Tactics.introduction id in - - let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in - let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in - let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in - - let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; - micromega_order_change spec res' - (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in - - let goal_props = List.rev (prop_env_of_formula sigma ff') in - - let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in - - let arith_args = goal_props @ goal_vars in - - let kill_arith = - Tacticals.New.tclTHEN - (Tactics.keep []) - ((*Tactics.tclABSTRACT None*) - (Tacticals.New.tclTHEN tac_arith tac)) in - - Tacticals.New.tclTHENS - (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal) - [ - kill_arith; - (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map EConstr.mkVar ids)); - Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) - ] ) - ] - with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") - | CsdpNotFound -> flush stdout ; - Tacticals.New.tclFAIL 0 (Pp.str - (" Skipping what remains of this tactic: the complexity of the goal requires " - ^ "the use of a specialized external tool called csdp. \n\n" - ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" - ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end - -let micromega_gen parse_arith - (negate:'cst atom -> 'cst mc_cnf) - (normalise:'cst atom -> 'cst mc_cnf) - unsat deduce - spec prover = - (micromega_gen parse_arith negate normalise unsat deduce spec prover) - - - -let micromega_order_changer cert env ff = - (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) - let coeff = Lazy.force coq_Rcst in - let dump_coeff = dump_Rcst in - let typ = Lazy.force coq_R in - let cert_typ = (EConstr.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in - - let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in - let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in - let vm = dump_varmap (typ) (vm_of_list env) in - Proofview.Goal.nf_enter begin fun gl -> - Tacticals.New.tclTHENLIST - [ - (Tactics.change_concl - (set - [ - ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, EConstr.mkApp - (gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); - ("__wit", cert, cert_typ) - ] - (Tacmach.New.pf_concl gl))); - (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) - ] - end - -let micromega_genr prover tac = - let parse_arith = parse_rarith in - let negate = Mc.rnegate in - let normalise = Mc.rnormalise in - let unsat = Mc.runsat in - let deduce = Mc.rdeduce in - let spec = lazy { - typ = Lazy.force coq_R; - coeff = Lazy.force coq_Rcst; - dump_coeff = dump_q; - proof_typ = Lazy.force coq_QWitness ; - dump_proof = dump_psatz coq_Q dump_q - } in - Proofview.Goal.nf_enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in - - try - let gl0 = { env = Tacmach.New.pf_env gl; sigma } in - let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in - let env = Env.elements env in - let spec = Lazy.force spec in - - let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in - let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in - - match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl0 with - | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") - | Some (ids,ff',res') -> - let (ff,ids) = formula_hyps_concl - (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in - let ff' = abstract_wrt_formula ff' ff in - - let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma (Lazy.force dump_rexpr) ff' in - let intro (id,_) = Tactics.introduction id in - - let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in - let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in - let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in - - let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; - micromega_order_changer res' env' ff_arith ] in - - let goal_props = List.rev (prop_env_of_formula sigma ff') in - - let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in - - let arith_args = goal_props @ goal_vars in - - let kill_arith = - Tacticals.New.tclTHEN - (Tactics.keep []) - ((*Tactics.tclABSTRACT None*) - (Tacticals.New.tclTHEN tac_arith tac)) in - - Tacticals.New.tclTHENS - (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal) - [ - kill_arith; - (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map EConstr.mkVar ids)); - Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) - ] ) - ] - - with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") - | CsdpNotFound -> flush stdout ; - Tacticals.New.tclFAIL 0 (Pp.str - (" Skipping what remains of this tactic: the complexity of the goal requires " - ^ "the use of a specialized external tool called csdp. \n\n" - ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" - ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end - - - - -let micromega_genr prover = (micromega_genr prover) - - -let lift_ratproof prover l = - match prover l with - | None -> None - | Some c -> Some (Mc.RatProof( c,Mc.DoneProof)) - -type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list - -[@@@ocaml.warning "-37"] -type csdp_certificate = S of Sos_types.positivstellensatz option | F of string -(* Used to read the result of the execution of csdpcert *) - -type provername = string * int option - -(** - * The caching mechanism. - *) - -open Micromega_plugin.Persistent_cache - -module Cache = PHashtable(struct - type t = (provername * micromega_polys) - let equal = Pervasives.(=) - let hash = Hashtbl.hash -end) - -let csdp_cache = ".csdp.cache" - -(** - * Build the command to call csdpcert, and launch it. This in turn will call - * the sos driver to the csdp executable. - * Throw CsdpNotFound if Coq isn't aware of any csdp executable. - *) - -let require_csdp = - if System.is_in_system_path "csdp" - then lazy () - else lazy (raise CsdpNotFound) - -let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivstellensatz option = - fun provername poly -> - - Lazy.force require_csdp; - - let cmdname = - List.fold_left Filename.concat (Envars.coqlib ()) - ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in - - match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with - | F str -> failwith str - | S res -> res - -(** - * Check the cache before calling the prover. - *) - -let xcall_csdpcert = - Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb) - -(** - * Prover callback functions. - *) - -let call_csdpcert prover pb = xcall_csdpcert (prover,pb) - -let rec z_to_q_pol e = - match e with - | Mc.Pc z -> Mc.Pc {Mc.qnum = z ; Mc.qden = Mc.XH} - | Mc.Pinj(p,pol) -> Mc.Pinj(p,z_to_q_pol pol) - | Mc.PX(pol1,p,pol2) -> Mc.PX(z_to_q_pol pol1, p, z_to_q_pol pol2) - -let call_csdpcert_q provername poly = - match call_csdpcert provername poly with - | None -> None - | Some cert -> - let cert = Certificate.q_cert_of_pos cert in - if Mc.qWeakChecker poly cert - then Some cert - else ((print_string "buggy certificate") ;None) - -let call_csdpcert_z provername poly = - let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in - match call_csdpcert provername l with - | None -> None - | Some cert -> - let cert = Certificate.z_cert_of_pos cert in - if Mc.zWeakChecker poly cert - then Some cert - else ((print_string "buggy certificate" ; flush stdout) ;None) - -let xhyps_of_cone base acc prf = - let rec xtract e acc = - match e with - | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> acc - | Mc.PsatzIn n -> let n = (CoqToCaml.nat n) in - if n >= base - then ISet.add (n-base) acc - else acc - | Mc.PsatzMulC(_,c) -> xtract c acc - | Mc.PsatzAdd(e1,e2) | Mc.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in - - xtract prf acc - -let hyps_of_cone prf = xhyps_of_cone 0 ISet.empty prf - -let compact_cone prf f = - let np n = CamlToCoq.nat (f (CoqToCaml.nat n)) in - - let rec xinterp prf = - match prf with - | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> prf - | Mc.PsatzIn n -> Mc.PsatzIn (np n) - | Mc.PsatzMulC(e,c) -> Mc.PsatzMulC(e,xinterp c) - | Mc.PsatzAdd(e1,e2) -> Mc.PsatzAdd(xinterp e1,xinterp e2) - | Mc.PsatzMulE(e1,e2) -> Mc.PsatzMulE(xinterp e1,xinterp e2) in - - xinterp prf - -let hyps_of_pt pt = - - let rec xhyps base pt acc = - match pt with - | Mc.DoneProof -> acc - | Mc.RatProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) - | Mc.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) - | Mc.EnumProof(c1,c2,l) -> - let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in - List.fold_left (fun s x -> xhyps (base + 1) x s) s l in - - xhyps 0 pt ISet.empty - -let hyps_of_pt pt = - let res = hyps_of_pt pt in - if debug - then (Printf.fprintf stdout "\nhyps_of_pt : %a -> " pp_proof_term pt ; ISet.iter (fun i -> Printf.printf "%i " i) res); - res - -let compact_pt pt f = - let translate ofset x = - if x < ofset then x - else (f (x-ofset) + ofset) in - - let rec compact_pt ofset pt = - match pt with - | Mc.DoneProof -> Mc.DoneProof - | Mc.RatProof(c,pt) -> Mc.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) - | Mc.CutProof(c,pt) -> Mc.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) - | Mc.EnumProof(c1,c2,l) -> Mc.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)), - Mc.map (fun x -> compact_pt (ofset+1) x) l) in - compact_pt 0 pt - -(** - * Definition of provers. - * Instantiates the type ('a,'prf) prover defined above. - *) - -let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l) - -module CacheZ = PHashtable(struct - type prover_option = bool * int - - type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) - -module CacheQ = PHashtable(struct - type t = int * ((Mc.q Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) - -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) -let memo_nlia = CacheZ.memo ".nia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) -let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) - - - -let linear_prover_Q = { - name = "linear prover"; - get_option = get_lra_option ; - prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - - -let linear_prover_R = { - name = "linear prover"; - get_option = get_lra_option ; - prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let nlinear_prover_R = { - name = "nra"; - get_option = get_lra_option; - prover = memo_nra ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let non_linear_prover_Q str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let non_linear_prover_R str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone; - pp_prf = pp_psatz pp_q; - pp_f = fun o x -> pp_pol pp_q o (fst x) -} - -let non_linear_prover_Z str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -let linear_Z = { - name = "lia"; - get_option = get_lia_option; - prover = memo_zlinear_prover ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -let nlinear_Z = { - name = "nlia"; - get_option = get_lia_option; - prover = memo_nlia ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -(** - * Functions instantiating micromega_gen with the appropriate theories and - * solvers - *) - -let lra_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ linear_prover_Q ] - -let psatz_Q i = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] - -let lra_R = - micromega_genr [ linear_prover_R ] - -let psatz_R i = - micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] - - -let psatz_Z i = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] - -let sos_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ non_linear_prover_Z "pure_sos" None ] - -let sos_Q = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ non_linear_prover_Q "pure_sos" None ] - - -let sos_R = - micromega_genr [ non_linear_prover_R "pure_sos" None ] - - -let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ linear_Z ] - -let xnlia = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr - [ nlinear_Z ] - -let nra = - micromega_genr [ nlinear_prover_R ] - -let nqa = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr - [ nlinear_prover_R ] - - - -(* Local Variables: *) -(* coding: utf-8 *) -(* End: *) diff --git a/src/versions/standard/g_smtcoq_standard.mlg b/src/versions/standard/g_smtcoq_standard.mlg index 8e273db..443d558 100644 --- a/src/versions/standard/g_smtcoq_standard.mlg +++ b/src/versions/standard/g_smtcoq_standard.mlg @@ -80,17 +80,41 @@ TACTIC EXTEND Tactic_zchaff | [ "zchaff_bool_no_check" ] -> { Zchaff.tactic_no_check () } END -{ let lemmas_list = ref [] } +{ + +let lemmas_list = Summary.ref ~name:"Selected lemmas" [] + +let cache_lemmas (_, lems) = + lemmas_list := lems + +let declare_lemmas : Structures.constr_expr list -> Libobject.obj = + let open Libobject in + declare_object + { + (default_object "LEMMAS") with + cache_function = cache_lemmas; + load_function = (fun _ -> cache_lemmas); + } + +let add_lemmas lems = + Lib.add_anonymous_leaf (declare_lemmas (lems @ !lemmas_list)) + +let clear_lemmas () = + Lib.add_anonymous_leaf (declare_lemmas []) + +let get_lemmas () = !lemmas_list + +} VERNAC COMMAND EXTEND Add_lemma CLASSIFIED AS SIDEFF -| [ "Add_lemmas" constr_list(lems) ] -> { lemmas_list := lems @ !lemmas_list } -| [ "Clear_lemmas" ] -> { lemmas_list := [] } +| [ "Add_lemmas" constr_list(lems) ] -> { add_lemmas lems } +| [ "Clear_lemmas" ] -> { clear_lemmas () } END TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> { Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list } -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> { Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list } +| [ "verit_bool_base" constr_list(lpl) ] -> { Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) } +| [ "verit_bool_no_check_base" constr_list(lpl) ] -> { Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) } END TACTIC EXTEND Tactic_cvc4 diff --git a/src/versions/standard/mutils_full.ml b/src/versions/standard/mutils_full.ml deleted file mode 100644 index efa2e4d..0000000 --- a/src/versions/standard/mutils_full.ml +++ /dev/null @@ -1,358 +0,0 @@ -(*** This file is taken from Coq-8.9.0 to solve a compilation issue due - to a wrong order in dependencies. - See https://github.com/coq/coq/issues/9768 . ***) - - -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(* *) -(* Micromega: A reflexive tactic using the Positivstellensatz *) -(* *) -(* ** Utility functions ** *) -(* *) -(* - Modules CoqToCaml, CamlToCoq *) -(* - Modules Cmp, Tag, TagSet *) -(* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) -(* *) -(************************************************************************) - -module Micromega = Micromega_plugin.Micromega - -let rec pp_list f o l = - match l with - | [] -> () - | e::l -> f o e ; output_string o ";" ; pp_list f o l - - -let finally f rst = - try - let res = f () in - rst () ; res - with reraise -> - (try rst () - with any -> raise reraise - ); raise reraise - -let rec try_any l x = - match l with - | [] -> None - | (f,s)::l -> match f x with - | None -> try_any l x - | x -> x - -let all_sym_pairs f l = - let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in - - let rec xpairs acc l = - match l with - | [] -> acc - | e::l -> xpairs (pair_with acc e l) l in - xpairs [] l - -let all_pairs f l = - let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in - - let rec xpairs acc l = - match l with - | [] -> acc - | e::lx -> xpairs (pair_with acc e l) lx in - xpairs [] l - -let rec is_sublist f l1 l2 = - match l1 ,l2 with - | [] ,_ -> true - | e::l1', [] -> false - | e::l1' , e'::l2' -> - if f e e' then is_sublist f l1' l2' - else is_sublist f l1 l2' - -let extract pred l = - List.fold_left (fun (fd,sys) e -> - match fd with - | None -> - begin - match pred e with - | None -> fd, e::sys - | Some v -> Some(v,e) , sys - end - | _ -> (fd, e::sys) - ) (None,[]) l - -open Num -open Big_int - -let ppcm x y = - let g = gcd_big_int x y in - let x' = div_big_int x g in - let y' = div_big_int y g in - mult_big_int g (mult_big_int x' y') - -let denominator = function - | Int _ | Big_int _ -> unit_big_int - | Ratio r -> Ratio.denominator_ratio r - -let numerator = function - | Ratio r -> Ratio.numerator_ratio r - | Int i -> Big_int.big_int_of_int i - | Big_int i -> i - -let rec ppcm_list c l = - match l with - | [] -> c - | e::l -> ppcm_list (ppcm c (denominator e)) l - -let rec rec_gcd_list c l = - match l with - | [] -> c - | e::l -> rec_gcd_list (gcd_big_int c (numerator e)) l - -let gcd_list l = - let res = rec_gcd_list zero_big_int l in - if Int.equal (compare_big_int res zero_big_int) 0 - then unit_big_int else res - -let rats_to_ints l = - let c = ppcm_list unit_big_int l in - List.map (fun x -> (div_big_int (mult_big_int (numerator x) c) - (denominator x))) l - -(* assoc_pos j [a0...an] = [j,a0....an,j+n],j+n+1 *) -(** - * MODULE: Coq to Caml data-structure mappings - *) - -module CoqToCaml = -struct - open Micromega - - let rec nat = function - | O -> 0 - | S n -> (nat n) + 1 - - - let rec positive p = - match p with - | XH -> 1 - | XI p -> 1+ 2*(positive p) - | XO p -> 2*(positive p) - - let n nt = - match nt with - | N0 -> 0 - | Npos p -> positive p - - let rec index i = (* Swap left-right ? *) - match i with - | XH -> 1 - | XI i -> 1+(2*(index i)) - | XO i -> 2*(index i) - - open Big_int - - let rec positive_big_int p = - match p with - | XH -> unit_big_int - | XI p -> add_int_big_int 1 (mult_int_big_int 2 (positive_big_int p)) - | XO p -> (mult_int_big_int 2 (positive_big_int p)) - - let z_big_int x = - match x with - | Z0 -> zero_big_int - | Zpos p -> (positive_big_int p) - | Zneg p -> minus_big_int (positive_big_int p) - - let q_to_num {qnum = x ; qden = y} = - Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y))) - -end - - -(** - * MODULE: Caml to Coq data-structure mappings - *) - -module CamlToCoq = -struct - open Micromega - - let rec nat = function - | 0 -> O - | n -> S (nat (n-1)) - - - let rec positive n = - if Int.equal n 1 then XH - else if Int.equal (n land 1) 1 then XI (positive (n lsr 1)) - else XO (positive (n lsr 1)) - - let n nt = - if nt < 0 - then assert false - else if Int.equal nt 0 then N0 - else Npos (positive nt) - - let rec index n = - if Int.equal n 1 then XH - else if Int.equal (n land 1) 1 then XI (index (n lsr 1)) - else XO (index (n lsr 1)) - - - let z x = - match compare x 0 with - | 0 -> Z0 - | 1 -> Zpos (positive x) - | _ -> (* this should be -1 *) - Zneg (positive (-x)) - - open Big_int - - let positive_big_int n = - let two = big_int_of_int 2 in - let rec _pos n = - if eq_big_int n unit_big_int then XH - else - let (q,m) = quomod_big_int n two in - if eq_big_int unit_big_int m - then XI (_pos q) - else XO (_pos q) in - _pos n - - let bigint x = - match sign_big_int x with - | 0 -> Z0 - | 1 -> Zpos (positive_big_int x) - | _ -> Zneg (positive_big_int (minus_big_int x)) - - let q n = - {Micromega.qnum = bigint (numerator n) ; - Micromega.qden = positive_big_int (denominator n)} - -end - -(** - * MODULE: Comparisons on lists: by evaluating the elements in a single list, - * between two lists given an ordering, and using a hash computation - *) - -module Cmp = -struct - - let rec compare_lexical l = - match l with - | [] -> 0 (* Equal *) - | f::l -> - let cmp = f () in - if Int.equal cmp 0 then compare_lexical l else cmp - - let rec compare_list cmp l1 l2 = - match l1 , l2 with - | [] , [] -> 0 - | [] , _ -> -1 - | _ , [] -> 1 - | e1::l1 , e2::l2 -> - let c = cmp e1 e2 in - if Int.equal c 0 then compare_list cmp l1 l2 else c - -end - -(** - * MODULE: Labels for atoms in propositional formulas. - * Tags are used to identify unused atoms in CNFs, and propagate them back to - * the original formula. The translation back to Coq then ignores these - * superfluous items, which speeds the translation up a bit. - *) - -module type Tag = -sig - - type t - - val from : int -> t - val next : t -> t - val pp : out_channel -> t -> unit - val compare : t -> t -> int - -end - -module Tag : Tag = -struct - - type t = int - - let from i = i - let next i = i + 1 - let pp o i = output_string o (string_of_int i) - let compare : int -> int -> int = Int.compare - -end - -(** - * MODULE: Ordered sets of tags. - *) - -module TagSet = Set.Make(Tag) - -(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *) - -let rec waitpid_non_intr pid = - try snd (Unix.waitpid [] pid) - with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid - -(** - * Forking routine, plumbing the appropriate pipes where needed. - *) - -let command exe_path args vl = - (* creating pipes for stdin, stdout, stderr *) - let (stdin_read,stdin_write) = Unix.pipe () - and (stdout_read,stdout_write) = Unix.pipe () - and (stderr_read,stderr_write) = Unix.pipe () in - - (* Create the process *) - let pid = Unix.create_process exe_path args stdin_read stdout_write stderr_write in - - (* Write the data on the stdin of the created process *) - let outch = Unix.out_channel_of_descr stdin_write in - output_value outch vl ; - flush outch ; - - (* Wait for its completion *) - let status = waitpid_non_intr pid in - - finally - (* Recover the result *) - (fun () -> - match status with - | Unix.WEXITED 0 -> - let inch = Unix.in_channel_of_descr stdout_read in - begin - try Marshal.from_channel inch - with any -> - failwith - (Printf.sprintf "command \"%s\" exited %s" exe_path - (Printexc.to_string any)) - end - | Unix.WEXITED i -> - failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) - | Unix.WSIGNALED i -> - failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) - | Unix.WSTOPPED i -> - failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) - (* Cleanup *) - (fun () -> - List.iter (fun x -> try Unix.close x with any -> ()) - [stdin_read; stdin_write; - stdout_read; stdout_write; - stderr_read; stderr_write]) - -(* Local Variables: *) -(* coding: utf-8 *) -(* End: *) diff --git a/src/versions/standard/mutils_full.mli b/src/versions/standard/mutils_full.mli deleted file mode 100644 index d506485..0000000 --- a/src/versions/standard/mutils_full.mli +++ /dev/null @@ -1,77 +0,0 @@ -(*** This file is taken from Coq-8.9.0 to solve a compilation issue due - to a wrong order in dependencies. - See https://github.com/coq/coq/issues/9768 . ***) - - -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -module Micromega = Micromega_plugin.Micromega - -val numerator : Num.num -> Big_int.big_int -val denominator : Num.num -> Big_int.big_int - -module Cmp : sig - - val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int - val compare_lexical : (unit -> int) list -> int - -end - -module Tag : sig - - type t - - val pp : out_channel -> t -> unit - val next : t -> t - val from : int -> t - -end - -module TagSet : CSig.SetS with type elt = Tag.t - -val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit - -module CamlToCoq : sig - - val positive : int -> Micromega.positive - val bigint : Big_int.big_int -> Micromega.z - val n : int -> Micromega.n - val nat : int -> Micromega.nat - val q : Num.num -> Micromega.q - val index : int -> Micromega.positive - val z : int -> Micromega.z - val positive_big_int : Big_int.big_int -> Micromega.positive - -end - -module CoqToCaml : sig - - val z_big_int : Micromega.z -> Big_int.big_int - val q_to_num : Micromega.q -> Num.num - val positive : Micromega.positive -> int - val n : Micromega.n -> int - val nat : Micromega.nat -> int - val index : Micromega.positive -> int - -end - -val rats_to_ints : Num.num list -> Big_int.big_int list - -val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list -val all_sym_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list -val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option -val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool - -val gcd_list : Num.num list -> Big_int.big_int - -val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list - -val command : string -> string array -> 'a -> 'b diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack index 81ac24b..f210db1 100644 --- a/src/versions/standard/smtcoq_plugin_standard.mlpack +++ b/src/versions/standard/smtcoq_plugin_standard.mlpack @@ -1,5 +1,3 @@ -Mutils_full -Coq_micromega_full Structures SmtMisc diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index d7e7f96..3b112cf 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -41,9 +41,10 @@ let destRel = Constr.destRel let lift = Vars.lift let mkApp = Constr.mkApp let decompose_app = Constr.decompose_app -let mkLambda = Constr.mkLambda -let mkProd = Constr.mkProd -let mkLetIn = Constr.mkLetIn +let mkLambda (n, t, c) = Constr.mkLambda (Context.make_annot n Sorts.Relevant, t, c) +let mkProd (n, t, c) = Constr.mkProd (Context.make_annot n Sorts.Relevant, t, c) +let mkLetIn (n, c1, t, c2) = Constr.mkLetIn (Context.make_annot n Sorts.Relevant, c1, t, c2) +let mkArrow a b = Term.mkArrow a Sorts.Relevant b let pr_constr_env env = Printer.pr_constr_env env Evd.empty let pr_constr = pr_constr_env Environ.empty_env @@ -58,7 +59,7 @@ let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entr const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *) - const_entry_universes = Evd.const_univ_entry ~poly:false evd; + const_entry_universes = Evd.univ_entry ~poly:false evd; const_entry_opaque = false; const_entry_inline_code = false } @@ -71,20 +72,20 @@ let mkTConst c noc ty = const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some ty; - const_entry_universes = Evd.const_univ_entry ~poly:false evd; + const_entry_universes = Evd.univ_entry ~poly:false evd; const_entry_opaque = false; const_entry_inline_code = false } (* TODO : Set -> Type *) let declare_new_type t = - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in + let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in Constr.mkVar t let declare_new_variable v constr_t = let env = Global.env () in let evd = Evd.from_env env in let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in + let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in Constr.mkVar v let declare_constant n c = @@ -103,8 +104,11 @@ let econstr_of_constr = EConstr.of_constr (* Modules *) -let gen_constant_in_modules s m n = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n +let gen_constant_in_modules s m n = + (* UnivGen.constr_of_monomorphic_global will crash on universe polymorphic constants *) + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) +let init_modules = Coqlib.init_modules (* Int63 *) @@ -166,13 +170,14 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Mutils_full +module Micromega_plugin_Mutils = Micromega_plugin.Mutils module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega_full +module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega +module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache let micromega_coq_proofTerm = (* Cannot contain evars *) - lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin_Coq_micromega.M.coq_proofTerm))) + lazy (gen_constant_in_modules "ZMicromega" [["Coq"; "micromega";"ZMicromega"]] "ZArithProof") let micromega_dump_proof_term p = (* Cannot contain evars *) @@ -188,7 +193,7 @@ let assert_before n c = Tactics.assert_before n (EConstr.of_constr c) let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c) let mk_tactic tac = - Proofview.Goal.nf_enter (fun gl -> + Proofview.Goal.enter (fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in @@ -222,7 +227,8 @@ let constrextern_extern_constr c = Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c) let get_rel_dec_name = function - | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> n + | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> + Context.binder_name n let retyping_get_type_of env sigma c = (* Cannot contain evars since it comes from a Constr.t *) diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index cde4f4f..950135c 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -38,6 +38,7 @@ val decompose_app : constr -> constr * constr list val mkLambda : name * types * constr -> constr val mkProd : name * types * types -> types val mkLetIn : name * constr * types * constr -> constr +val mkArrow : types -> types -> constr val pr_constr_env : Environ.env -> constr -> Pp.t val pr_constr : constr -> Pp.t @@ -60,6 +61,7 @@ val econstr_of_constr : constr -> econstr (* Modules *) val gen_constant : string list list -> string -> constr lazy_t +val init_modules : string list list (* Int63 *) @@ -88,9 +90,10 @@ val mkTrace : (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Mutils_full +module Micromega_plugin_Mutils = Micromega_plugin.Mutils module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega_full +module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega +module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache val micromega_coq_proofTerm : constr lazy_t val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 71b28a8..225a90b 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -222,7 +222,7 @@ let theorems interp name fdimacs ftrace = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in - let vtype = Term.mkArrow (Lazy.force cint) (Lazy.force cbool) in + let vtype = Structures.mkArrow (Lazy.force cint) (Lazy.force cbool) in let theorem_type = Structures.mkProd (Structures.mkName "v", vtype, theorem_concl) in let theorem_proof_cast = diff --git a/unit-tests/Makefile b/unit-tests/Makefile index 0d4bdc1..4820887 100644 --- a/unit-tests/Makefile +++ b/unit-tests/Makefile @@ -7,6 +7,7 @@ OBJ=$(ZCHAFFLOG) $(VERITLOG) COQLIBS?= -R ../src SMTCoq OPT?= COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) +VIOFLAG?=-quick COQC?=$(COQBIN)coqc @@ -39,5 +40,17 @@ logs: $(OBJ) $(COQC) $(COQDEBUG) $(COQFLAGS) $* -clean: - rm -rf *~ $(ZCHAFFLOG) $(VERITLOG) *.vo *.glob +%.vio: %.v logs + $(COQC) $(VIOFLAG) $(COQDEBUG) $(COQFLAGS) $* + + +parallel: Tests_zchaff_tactics.vio Tests_verit_tactics.vio Tests_lfsc_tactics.vio + coqtop -schedule-vio-checking 3 Tests_zchaff_tactics Tests_verit_tactics Tests_lfsc_tactics + + +clean: cleanvo + rm -rf *~ $(ZCHAFFLOG) $(VERITLOG) + + +cleanvo: + rm -rf *~ *.vo *.glob *.vio diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index ee9df76..2268cb9 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -29,7 +29,7 @@ Local Open Scope bv_scope. Goal forall (a b c: bitvector 4), (c = (bv_and a b)) -> ((bv_and (bv_and c a) b) = c). - Proof. + Proof using. smt. Qed. @@ -38,19 +38,19 @@ Local Open Scope bv_scope. bv2 = #b|1|0|0|0| /\ bv3 = #b|1|1|0|0| -> bv_ultP bv1 bv2 /\ bv_ultP bv2 bv3. - Proof. + Proof using. smt. Qed. Goal forall (a: bitvector 32), a = a. - Proof. + Proof using. smt. Qed. Goal forall (bv1 bv2: bitvector 4), bv1 = bv2 <-> bv2 = bv1. - Proof. + Proof using. smt. Qed. @@ -64,7 +64,7 @@ Section Arrays. Goal forall (a:farray Z Z) i j, i = j -> a[i] = a[j]. - Proof. + Proof using. smt. Qed. @@ -74,7 +74,7 @@ Section Arrays. (f: Z -> Z), (a[x <- v] = b) /\ a[y <- w] = b -> (f x) = (f y) \/ (g a) = (g b). - Proof. + Proof using. smt. Qed. @@ -85,7 +85,7 @@ Section Arrays. (* d = b[0%Z <- 4][1%Z <- 4] -> *) (* a = d[1%Z <- b[1%Z]] -> *) (* a = c. *) - (* Proof. *) + (* Proof using. *) (* smt. *) (* Qed. *) @@ -93,7 +93,7 @@ Section Arrays. (* Goal forall (a b: farray Z Z) i, (select (store (store (store a i 3%Z) 1%Z (select (store b i 4) i)) 2%Z 2%Z) 1%Z) = 4. - Proof. + Proof using. smt. rewrite read_over_other_write; try easy. rewrite read_over_same_write; try easy; try apply Z_compdec. @@ -111,7 +111,7 @@ Section EUF. (x y: Z) (f: Z -> Z), y = x -> (f x) = (f y). - Proof. + Proof using. smt. Qed. @@ -119,7 +119,7 @@ Section EUF. (x y: Z) (f: Z -> Z), (f x) = (f y) -> (f y) = (f x). - Proof. + Proof using. smt. Qed. @@ -128,7 +128,7 @@ Section EUF. (x y: Z) (f: Z -> Z), x + 1 = (y + 1) -> (f y) = (f x). - Proof. + Proof using. smt. Qed. @@ -137,7 +137,7 @@ Section EUF. (x y: Z) (f: Z -> Z), x = (y + 1) -> (f y) = (f (x - 1)). - Proof. + Proof using. smt. Qed. @@ -145,7 +145,7 @@ Section EUF. (x y: Z) (f: Z -> Z), x = (y + 1) -> (f (y + 1)) = (f x). - Proof. + Proof using. smt. Qed. @@ -156,44 +156,44 @@ Section LIA. Goal forall (a b: Z), a = b <-> b = a. - Proof. + Proof using. smt. Qed. Goal forall (x y: Z), (x >= y) -> (y < x) \/ (x = y). - Proof. + Proof using. smt. Qed. Goal forall (f : Z -> Z) (a:Z), ((f a) > 1) -> ((f a) + 1) >= 2 \/((f a) = 30) . - Proof. + Proof using. smt. Qed. Goal forall x: Z, (x = 0%Z) -> (8 >= 0). - Proof. + Proof using. smt. Qed. Goal forall x: Z, ~ (x < 0%Z) -> (8 >= 0). - Proof. + Proof using. smt. Qed. Goal forall (a b: Z), a < b -> a < (b + 1). - Proof. + Proof using. smt. Qed. Goal forall (a b: Z), (a < b) -> (a + 2) < (b + 3). - Proof. + Proof using. smt. Qed. Goal forall a b, a < b -> a < (b + 10). - Proof. + Proof using. smt. Qed. @@ -208,141 +208,152 @@ Section PR. (* Simple connectors *) Goal forall (a:bool), a || negb a. +Proof using. smt. Qed. Goal forall a, negb (a || negb a) = false. +Proof using. smt. Qed. Goal forall a, (a && negb a) = false. +Proof using. smt. Qed. Goal forall a, negb (a && negb a). +Proof using. smt. Qed. Goal forall a, a --> a. +Proof using. smt. Qed. Goal forall a, negb (a --> a) = false. +Proof using. smt. Qed. Goal forall a , (xorb a a) || negb (xorb a a). +Proof using. smt. Qed. Goal forall a, (a||negb a) || negb (a||negb a). +Proof using. smt. Qed. (* Polarities *) Goal forall a b, andb (orb (negb (negb a)) b) (negb (orb a b)) = false. -Proof. +Proof using. smt. Qed. Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false. -Proof. +Proof using. smt. Qed. (* Multiple negations *) Goal forall a, orb a (negb (negb (negb a))) = true. -Proof. +Proof using. smt. Qed. Goal forall a b c, (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. -Proof. +Proof using. smt. Qed. Goal true. +Proof using. smt. Qed. Goal negb false. +Proof using. smt. Qed. Goal forall a, Bool.eqb a a. -Proof. +Proof using. smt. Qed. Goal forall (a:bool), a = a. +Proof using. smt. Qed. Goal (false || true) && false = false. -Proof. +Proof using. smt. Qed. Goal negb true = false. -Proof. +Proof using. smt. Qed. Goal false = false. -Proof. +Proof using. smt. Qed. Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)). -Proof. +Proof using. smt. Qed. Goal forall x y, Bool.eqb (x --> y) ((x && y) || (negb x)). -Proof. +Proof using. smt. Qed. Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)). -Proof. +Proof using. smt. Qed. Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false. -Proof. +Proof using. smt. Qed. Goal forall a, ((a || a) && (negb a)) = false. -Proof. +Proof using. smt. Qed. Goal forall a, (negb (a || (negb a))) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c, (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. -Proof. +Proof using. smt. Qed. @@ -353,19 +364,19 @@ Goal forall i j k, let b := j == k in let c := k == i in (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false. -Proof. +Proof using. smt. Qed. @@ -458,35 +469,35 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44) && (orb (orb (orb x15 x25) x35) x45)) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c f p, ((Z.eqb a c) && (Z.eqb b c) && ((negb (Z.eqb (f a) (f b))) || ((p a) && (negb (p b))))) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false. -Proof. +Proof using. smt. Qed. Goal forall x y z f, ((Z.eqb x y) && (Z.eqb y z) && (negb (Z.eqb (f x) (f z)))) = false. -Proof. +Proof using. smt. Qed. Goal forall x y z f, ((negb (Z.eqb (f x) (f y))) && (Z.eqb y z) && (Z.eqb (f x) (f (f z))) && (Z.eqb x y)) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c d e f, ((Z.eqb a b) && (Z.eqb b c) && (Z.eqb c d) && (Z.eqb c e) && (Z.eqb e f) && (negb (Z.eqb a f))) = false. -Proof. +Proof using. smt. Qed. @@ -494,54 +505,54 @@ Qed. Goal forall x y z, ((x <=? 3) && ((y <=? 7) || (z <=? 9))) --> ((x + y <=? 10) || (x + z <=? 12)) = true. -Proof. +Proof using. smt. Qed. Goal forall x, (Z.eqb (x - 3) 7) --> (x >=? 10) = true. -Proof. +Proof using. smt. Qed. Goal forall x y, (x >? y) --> (y + 1 <=? x) = true. -Proof. +Proof using. smt. Qed. Goal forall x y, Bool.eqb (x <? y) (x <=? y - 1) = true. -Proof. +Proof using. smt. Qed. Goal forall x y, ((x + y <=? - (3)) && (y >=? 0) || (x <=? - (3))) && (x >=? 0) = false. - Proof. + Proof using. smt. Qed. Goal forall x, (andb ((x - 3) <=? 7) (7 <=? (x - 3))) --> (x >=? 10) = true. -Proof. +Proof using. smt. Qed. Goal forall x, (Z.eqb (x - 3) 7) --> (10 <=? x) = true. -Proof. +Proof using. smt. Qed. (* More general examples *) Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false. -Proof. +Proof using. smt. Qed. Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), (negb (Z.eqb (f a) b)) || (negb (P (f a))) || (P b). -Proof. +Proof using. smt. Qed. @@ -551,7 +562,7 @@ Goal forall b1 b2 x1 x2, (ifb b2 (Z.eqb (2*x1+1) (2*x2+1)) (Z.eqb (2*x1+1) (2*x2))) (ifb b2 (Z.eqb (2*x1) (2*x2+1)) (Z.eqb (2*x1) (2*x2)))) --> ((b1 --> b2) && (b2 --> b1) && (Z.eqb x1 x2)). -Proof. +Proof using. smt. Qed. @@ -560,14 +571,14 @@ Qed. Goal forall b, let a := b in a && (negb a) = false. -Proof. +Proof using. smt. Qed. Goal forall b, let a := b in a || (negb a) = true. -Proof. +Proof using. smt. Qed. @@ -575,14 +586,14 @@ Qed. Goal forall i j, let a := i == j in a && (negb a) = false. -Proof. +Proof using. smt. Qed. Goal forall i j, let a := i == j in a || (negb a) = true. -Proof. +Proof using. smt. Qed. @@ -590,19 +601,19 @@ Qed. (* Congruence in which some premises are REFL *) Goal forall (f:Z -> Z -> Z) x y z, (Z.eqb x y) --> (Z.eqb (f z x) (f z y)). -Proof. +Proof using. smt. Qed. Goal forall (f:Z -> Z -> Z) x y z, (x = y) -> (f z x) = (f z y). -Proof. +Proof using. smt. Qed. Goal forall (P:Z -> Z -> bool) x y z, (Z.eqb x y) --> ((P z x) --> (P z y)). -Proof. +Proof using. smt. Qed. @@ -625,7 +636,7 @@ Section A_BV_EUF_LIA_PR. (* d = b[bv1 <- 4][bv2 <- 4] -> *) (* a = d[bv2 <- b[bv2]] -> *) (* a = c. *) - (* Proof. *) + (* Proof using. *) (* smt. *) (* Qed. *) @@ -638,7 +649,7 @@ Section A_BV_EUF_LIA_PR. (* d = b[bv1 <- 4][bv2 <- 4] /\ *) (* a = d[bv2 <- b[bv2]] -> *) (* a = c. *) - (* Proof. *) + (* Proof using. *) (* smt. *) (* Qed. *) @@ -652,7 +663,7 @@ Section A_BV_EUF_LIA_PR. r = s /\ h r = v /\ h s = y -> v < x + 1 /\ v > x - 1 -> f (h r) = f (h s) \/ g a = g b. - Proof. + Proof using. smt. (** "cvc4. verit." also solves the goal *) Qed. @@ -666,7 +677,7 @@ Section A_BV_EUF_LIA_PR. a[z <- w] = b /\ a[t <- v] = b -> r = s -> v < x + 10 /\ v > x - 5 -> ~ (g a = g b) \/ f (h r) = f (h s). - Proof. + Proof using. smt. (** "cvc4. verit." also solves the goal *) Qed. @@ -677,7 +688,7 @@ Section A_BV_EUF_LIA_PR. b[bv_add y x <- v] = a /\ b = a[bv_add x y <- v] -> a = b. - Proof. + Proof using. smt. (* CVC4 preprocessing hole on BV *) replace (bv_add x y) with (bv_add y x) @@ -686,12 +697,12 @@ Section A_BV_EUF_LIA_PR. Qed. Goal forall (a:farray Z Z), a = a. - Proof. + Proof using. smt. Qed. Goal forall (a b: farray Z Z), a = b <-> b = a. - Proof. + Proof using. smt. Qed. @@ -714,15 +725,15 @@ Section group. Lemma inverse' : forall a : Z, (op a (inv a) =? e). - Proof. smt. Qed. + Proof using associative identity inverse. smt. Qed. Lemma identity' : forall a : Z, (op a e =? a). - Proof. smt inverse'. Qed. + Proof using associative identity inverse. smt inverse'. Qed. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'; smt pe'. Qed. + Proof using associative identity inverse. intros pe'; smt pe'. Qed. Clear_lemmas. End group. diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 6ed1d67..896c1bf 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -23,14 +23,14 @@ Open Scope Z_scope. Lemma check_univ (x1: bool): (x1 && (negb x1)) = false. -Proof. +Proof using. verit. Qed. Lemma fun_const2 : forall f (g : Z -> Z -> bool), (forall x, g (f x) 2) -> g (f 3) 2. -Proof. +Proof using. intros f g Hf. verit Hf. Qed. @@ -38,51 +38,62 @@ Qed. (* Simple connectives *) Goal forall (a:bool), a || negb a. +Proof using. verit. Qed. Goal forall a, negb (a || negb a) = false. +Proof using. verit. Qed. Goal forall a, (a && negb a) = false. +Proof using. verit. Qed. Goal forall a, negb (a && negb a). +Proof using. verit. Qed. Goal forall a, implb a a. +Proof using. verit. Qed. Goal forall a, negb (implb a a) = false. +Proof using. verit. Qed. Goal forall a , (xorb a a) || negb (xorb a a). +Proof using. verit. Qed. Goal forall a, (a||negb a) || negb (a||negb a). +Proof using. verit. Qed. Goal true. +Proof using. verit. Qed. Goal negb false. +Proof using. verit. Qed. Goal forall a, Bool.eqb a a. -Proof. +Proof using. verit. Qed. Goal forall (a:bool), a = a. +Proof using. verit. Qed. @@ -90,43 +101,43 @@ Qed. (* Other connectives *) Goal (false || true) && false = false. -Proof. +Proof using. verit. Qed. Goal negb true = false. -Proof. +Proof using. verit. Qed. Goal false = false. -Proof. +Proof using. verit. Qed. Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)). -Proof. +Proof using. verit. Qed. Goal forall x y, Bool.eqb (negb (xorb x y)) ((x && y) || ((negb x) && (negb y))). -Proof. +Proof using. verit. Qed. Goal forall x y, Bool.eqb (implb x y) ((x && y) || (negb x)). -Proof. +Proof using. verit. Qed. Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)). -Proof. +Proof using. verit. Qed. @@ -134,7 +145,7 @@ Qed. (* Multiple negations *) Goal forall a, orb a (negb (negb (negb a))) = true. -Proof. +Proof using. verit. Qed. @@ -142,13 +153,13 @@ Qed. (* Polarities *) Goal forall a b, andb (orb a b) (negb (orb a b)) = false. -Proof. +Proof using. verit. Qed. Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false. -Proof. +Proof using. verit. Qed. @@ -157,7 +168,7 @@ Qed. (* ((a ∧ b) ∨ (b ∧ c)) ∧ ¬b = ⊥ *) Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false. -Proof. +Proof using. verit. Qed. @@ -166,7 +177,7 @@ Qed. (* (a ∨ a) ∧ ¬a = ⊥ *) Goal forall a, ((a || a) && (negb a)) = false. -Proof. +Proof using. verit. Qed. @@ -175,7 +186,7 @@ Qed. (* ¬(a ∨ ¬a) = ⊥ *) Goal forall a, (negb (a || (negb a))) = false. -Proof. +Proof using. verit. Qed. @@ -185,7 +196,7 @@ Qed. Goal forall a b c, (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. -Proof. +Proof using. verit. Qed. @@ -197,7 +208,7 @@ Goal forall i j k, let b := j == k in let c := k == i in (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. -Proof. +Proof using. verit. Qed. @@ -206,7 +217,7 @@ Qed. (* (a ∧ b) ∧ (c ∨ d) ∧ ¬(c ∨ (a ∧ b ∧ d)) = ⊥ *) Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false. -Proof. +Proof using. verit. Qed. @@ -215,7 +226,7 @@ Qed. (* a ∧ b ∧ c ∧ (¬a ∨ ¬b ∨ d) ∧ (¬d ∨ ¬c) = ⊥ *) Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false. -Proof. +Proof using. verit. Qed. @@ -309,7 +320,7 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44) && (orb (orb (orb x15 x25) x35) x45)) = false. -Proof. +Proof using. verit. Qed. @@ -317,7 +328,7 @@ Qed. (* uf1.smt *) Goal forall a b c f p, ( (a =? c) && (b =? c) && ((negb (f a =?f b)) || ((p a) && (negb (p b))))) = false. -Proof. +Proof using. verit. Qed. @@ -325,7 +336,7 @@ Qed. (* uf2.smt *) Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false. -Proof. +Proof using. verit. Qed. @@ -333,7 +344,7 @@ Qed. (* uf3.smt *) Goal forall x y z f, ((x =? y) && (y =? z) && (negb (f x =? f z))) = false. -Proof. +Proof using. verit. Qed. @@ -341,7 +352,7 @@ Qed. (* uf4.smt *) Goal forall x y z f, ((negb (f x =? f y)) && (y =? z) && (f x =? f (f z)) && (x =? y)) = false. -Proof. +Proof using. verit. Qed. @@ -349,7 +360,7 @@ Qed. (* uf5.smt *) Goal forall a b c d e f, ((a =? b) && (b =? c) && (c =? d) && (c =? e) && (e =? f) && (negb (a =? f))) = false. -Proof. +Proof using. verit. Qed. @@ -358,28 +369,28 @@ Qed. Goal forall x y z, implb ((x <=? 3) && ((y <=? 7) || (z <=? 9))) ((x + y <=? 10) || (x + z <=? 12)) = true. -Proof. +Proof using. verit. Qed. (* lia2.smt *) Goal forall x, implb (x - 3 =? 7) (x >=? 10) = true. -Proof. +Proof using. verit. Qed. (* lia3.smt *) Goal forall x y, implb (x >? y) (y + 1 <=? x) = true. -Proof. +Proof using. verit. Qed. (* lia4.smt *) Goal forall x y, Bool.eqb (x <? y) (x <=? y - 1) = true. -Proof. +Proof using. verit. Qed. @@ -387,21 +398,21 @@ Qed. Goal forall x y, ((x + y <=? - (3)) && (y >=? 0) || (x <=? - (3))) && (x >=? 0) = false. -Proof. +Proof using. verit. Qed. (* lia6.smt *) Goal forall x, implb (andb ((x - 3) <=? 7) (7 <=? (x - 3))) (x >=? 10) = true. -Proof. +Proof using. verit. Qed. (* lia7.smt *) Goal forall x, implb (x - 3 =? 7) (10 <=? x) = true. -Proof. +Proof using. verit. Qed. @@ -409,7 +420,7 @@ Qed. Lemma irrelf_ltb a b c: (Z.ltb a b) && (Z.ltb b c) && (Z.ltb c a) = false. -Proof. +Proof using. verit. Qed. @@ -419,20 +430,20 @@ Lemma comp f g (x1 x2 x3 : Z) : (Z.eqb x1 (f (g x3))) true) true. -Proof. verit. Qed. +Proof using. verit. Qed. (* More general examples *) Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false. -Proof. +Proof using. verit. Qed. Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), (negb (f a =? b)) || (negb (P (f a))) || (P b). -Proof. +Proof using. verit. Qed. @@ -443,7 +454,7 @@ Goal forall b1 b2 x1 x2, (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). -Proof. +Proof using. verit. Qed. @@ -453,21 +464,21 @@ Qed. Goal forall b, let a := b in a && (negb a) = false. -Proof. +Proof using. verit. Qed. Goal forall b, let a := b in a || (negb a) = true. -Proof. +Proof using. verit. Qed. (* Does not work since the [is_true] coercion includes [let in] Goal forall b, let a := b in a || (negb a). -Proof. +Proof using. verit. Qed. *) @@ -477,27 +488,27 @@ Qed. Goal forall i j, let a := i == j in a && (negb a) = false. -Proof. +Proof using. verit. Qed. Goal forall i j, let a := i == j in a || (negb a) = true. -Proof. +Proof using. verit. Qed. (* TODO: fails with native-coq: "compilation error" Goal forall (i j:int), (i == j) && (negb (i == j)) = false. -Proof. +Proof using. verit. exact int63_compdec. Qed. Goal forall i j, (i == j) || (negb (i == j)). -Proof. +Proof using. verit. exact int63_compdec. Qed. @@ -508,13 +519,13 @@ Qed. Goal forall (f:Z -> Z -> Z) x y z, implb (x =? y) (f z x =? f z y). -Proof. +Proof using. verit. Qed. Goal forall (P:Z -> Z -> bool) x y z, implb (x =? y) (implb (P z x) (P z y)). -Proof. +Proof using. verit. Qed. @@ -524,80 +535,80 @@ Qed. Lemma taut1 : forall f, f 2 =? 0 -> f 2 =? 0. -Proof. intros f p. verit p. Qed. +Proof using. intros f p. verit p. Qed. Lemma taut2 : forall f, 0 =? f 2 -> 0 =?f 2. -Proof. intros f p. verit p. Qed. +Proof using. intros f p. verit p. Qed. Lemma taut3 : forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0. -Proof. intros f p1 p2. verit p1 p2. Qed. +Proof using. intros f p1 p2. verit p1 p2. Qed. Lemma taut4 : forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0. -Proof. intros f p1 p2. verit p1 p2. Qed. +Proof using. intros f p1 p2. verit p1 p2. Qed. Lemma test_eq_sym a b : implb (a =? b) (b =? a). -Proof. verit. Qed. +Proof using. verit. Qed. Lemma taut5 : forall f, 0 =? f 2 -> f 2 =? 0. -Proof. intros f p. verit p. Qed. +Proof using. intros f p. verit p. Qed. Lemma fun_const_Z : forall f , (forall x, f x =? 2) -> f 3 =? 2. -Proof. intros f Hf. verit Hf. Qed. +Proof using. intros f Hf. verit Hf. Qed. Lemma lid (A : bool) : A -> A. -Proof. intro a. verit a. Qed. +Proof using. intro a. verit a. Qed. Lemma lpartial_id A : (xorb A A) -> (xorb A A). -Proof. intro xa. verit xa. Qed. +Proof using. intro xa. verit xa. Qed. Lemma llia1 X Y Z: (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) -> (X + Y <=? 10) || (X + Z <=? 12). -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma llia2 X: X - 3 =? 7 -> X >=? 10. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma llia3 X Y: X >? Y -> Y + 1 <=? X. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma llia6 X: andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma even_odd b1 b2 x1 x2: (ifb b1 (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) -> ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma lcongr1 (a b : Z) (P : Z -> bool) f: (f a =? b) -> (P (f a)) -> P b. -Proof. intros eqfab pfa. verit eqfab pfa. Qed. +Proof using. intros eqfab pfa. verit eqfab pfa. Qed. Lemma lcongr2 (f:Z -> Z -> Z) x y z: x =? y -> f z x =? f z y. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma lcongr3 (P:Z -> Z -> bool) x y z: x =? y -> P z x -> P z y. -Proof. intros eqxy pzx. verit eqxy pzx. Qed. +Proof using. intros eqxy pzx. verit eqxy pzx. Qed. Lemma test20 : forall x, (forall a, a <? x) -> 0 <=? x = false. -Proof. intros x H. verit H. Qed. +Proof using. intros x H. verit H. Qed. Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x). -Proof. intros x H. verit H. Qed. +Proof using. intros x H. verit H. Qed. Lemma un_menteur (a b c d : Z) dit: dit a =? c -> @@ -606,13 +617,13 @@ Lemma un_menteur (a b c d : Z) dit: (a =? c) || (a =? d) -> (b =? c) || (b =? d) -> a =? d. -Proof. intros H1 H2 H3 H4 H5. verit H1 H2 H3 H4 H5. Qed. +Proof using. intros H1 H2 H3 H4 H5. verit H1 H2 H3 H4 H5. Qed. Lemma const_fun_is_eq_val_0 : forall f : Z -> Z, (forall a b, f a =? f b) -> forall x, f x =? f 0. -Proof. intros f Hf. verit Hf. Qed. +Proof using. intros f Hf. verit Hf. Qed. (* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to the environment. If you did so in a section then, at the end of the section, @@ -624,7 +635,7 @@ Section S. Hypothesis th : forall x, Z.eqb (f x) 3. Add_lemmas th. Goal forall x, Z.eqb ((f x) + 1) 4. - Proof. verit. Qed. + Proof using th. verit. Qed. Clear_lemmas. End S. @@ -635,7 +646,7 @@ Section fins_sat6. Add_lemmas andab orcd. Lemma sat6 : orb c (andb a (andb b d)). - Proof. verit. Qed. + Proof using andab orcd. verit. Qed. Clear_lemmas. End fins_sat6. @@ -649,7 +660,7 @@ Section fins_lemma_multiple. Add_lemmas g_k_linear f'_equal_k. Lemma apply_lemma_multiple : forall x y, g (x + 1) =? g x + f' y. - Proof. verit. Qed. + Proof using g_k_linear f'_equal_k. verit. Qed. Clear_lemmas. End fins_lemma_multiple. @@ -661,11 +672,11 @@ Section fins_find_apply_lemma. Add_lemmas u_is_constant. Lemma apply_lemma : forall x, u x =? u 2. - Proof. verit. Qed. + Proof using u_is_constant. verit. Qed. Lemma find_inst : implb (u 2 =? 5) (u 3 =? 5). - Proof. verit. Qed. + Proof using u_is_constant. verit. Qed. Clear_lemmas. End fins_find_apply_lemma. @@ -678,7 +689,7 @@ Section mult3. Add_lemmas mult3_0 mult3_Sn. Lemma mult3_4_12 : mult3 4 =? 12. - Proof. verit. Qed. (* slow to verify with standard coq *) + Proof using mult3_0 mult3_Sn. verit. Qed. (* slow to verify with standard coq *) Clear_lemmas. End mult3. @@ -691,7 +702,7 @@ End mult3. (* Hypothesis mult_Sx : forall x y, mult (x+1) y =? mult x y + y. *) (* Lemma mult_1_x : forall x, mult 1 x =? x. *) -(* Proof. verit mult_0 mult_Sx. *) +(* Proof using. verit mult_0 mult_Sx. *) (* Qed. *) (* End mult. *) @@ -704,7 +715,7 @@ Section implicit_transform. Lemma implicit_transform : f a2. - Proof. verit. Qed. + Proof using f_const f_a1. verit. Qed. Clear_lemmas. End implicit_transform. @@ -724,23 +735,23 @@ Section list. Lemma in_cons1 : inlist 1 (1::2::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons2 : inlist 12 (2::4::12::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons3 : inlist 1 (5::1::(0-1)::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons4 : inlist 22 ((- (1))::22::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons5 : inlist 1 ((- 1)::1::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. (* Lemma in_cons_false1 : *) (* inlist 1 (2::3::nil). *) @@ -764,15 +775,15 @@ Section list. Lemma in_app1 : inlist 1 (1::2::nil ++ nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed. Lemma in_app2 : inlist 1 (nil ++ 2::1::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed. Lemma in_app3 : inlist 1 (1::3::nil ++ 2::1::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed. (* Lemma in_app_false1 : *) (* inlist 1 (nil ++ 2::3::nil). *) @@ -802,7 +813,7 @@ Section list. Lemma coqhammer_example l1 l2 x y1 y2 y3: implb (orb (inlist x l1) (orb (inlist x l2) (orb (x =? y1) (inlist x (y2 ::y3::nil))))) (inlist x (y1::(l1 ++ (y2 :: (l2 ++ (y3 :: nil)))))). - Proof. verit_no_check. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app in_nil in_inv inlist_app_comm_cons. verit_no_check. Qed. Clear_lemmas. End list. @@ -823,59 +834,59 @@ Section group. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'. verit pe'. Qed. + Proof using associative identity inverse. intros pe'. verit pe'. Qed. Lemma simplification_right x1 x2 y: op x1 y =? op x2 y -> x1 =? x2. - Proof. intro H. verit H. Qed. + Proof using associative identity inverse. intro H. verit H. Qed. Lemma simplification_left x1 x2 y: op y x1 =? op y x2 -> x1 =? x2. - Proof. intro H. verit H. Qed. + Proof using associative identity inverse. intro H. verit H. Qed. Clear_lemmas. End group. Section Linear1. - Parameter f : Z -> Z. - Axiom f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0). + Variable f : Z -> Z. + Hypothesis f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0). (* Cuts are not automatically proved when one equality is switched *) Lemma f_1 : f 1 =? 1. - Proof. + Proof using f_spec. verit_bool f_spec; replace (0 =? f 0) with (f 0 =? 0) by apply Z.eqb_sym; auto. Qed. End Linear1. Section Linear2. - Parameter g : Z -> Z. + Variable g : Z -> Z. - Axiom g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2). + Hypothesis g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2). (* The call to veriT does not terminate *) (* Lemma apply_lemma_infinite : *) (* forall x y, Z.eqb (g (x + y)) ((g x) + y * 2). *) -(* Proof. verit g_2_linear. *) +(* Proof using. verit g_2_linear. *) End Linear2. Section Input_switched1. - Parameter m : Z -> Z. + Variable m : Z -> Z. - Axiom m_0 : m 0 =? 5. + Hypothesis m_0 : m 0 =? 5. (* veriT switches the input lemma in this case *) Lemma cinq_m_0 : m 0 =? 5. - Proof. verit m_0. Qed. + Proof using m_0. verit m_0. Qed. End Input_switched1. Section Input_switched2. - Parameter h : Z -> Z -> Z. + Variable h : Z -> Z -> Z. - Axiom h_Sm_n : forall x y, h (x+1) y =? h x y. + Hypothesis h_Sm_n : forall x y, h (x+1) y =? h x y. (* veriT switches the input lemma in this case *) Lemma h_1_0 : h 1 0 =? h 0 0. - Proof. verit h_Sm_n. Qed. + Proof using h_Sm_n. verit h_Sm_n. Qed. End Input_switched2. @@ -887,7 +898,7 @@ Goal forall (f : positive -> positive) (x y : positive), implb ((x + 3) =? y) ((f (x + 3)) <=? (f y)) = true. -Proof. +Proof using. pos_convert. verit. Qed. @@ -896,7 +907,7 @@ Goal forall (f : positive -> positive) (x y : positive), implb ((x + 3) =? y) ((3 <? y) && ((f (x + 3)) <=? (f y))) = true. -Proof. +Proof using. pos_convert. verit. Qed. @@ -909,7 +920,7 @@ Goal forall (f : N -> N) (x y : N), implb ((x + 3) =? y) ((f (x + 3)) <=? (f y)) = true. -Proof. +Proof using. N_convert. verit. Qed. @@ -918,7 +929,7 @@ Goal forall (f : N -> N) (x y : N), implb ((x + 3) =? y) ((2 <? y) && ((f (x + 3)) <=? (f y))) = true. -Proof. +Proof using. N_convert. verit. Qed. @@ -932,7 +943,7 @@ Goal forall (f : nat -> nat) (x y : nat), implb (Nat.eqb (x + 3) y) ((f (x + 3)) <=? (f y)) = true. -Proof. +Proof using. nat_convert. verit. Qed. @@ -941,7 +952,7 @@ Goal forall (f : nat -> nat) (x y : nat), implb (Nat.eqb (x + 3) y) ((2 <? y) && ((f (x + 3)) <=? (f y))) = true. -Proof. +Proof using. nat_convert. verit. Qed. @@ -954,6 +965,7 @@ Goal forall f : positive -> nat -> N, forall (x : positive) (y : nat), (implb (Nat.eqb y 7) (implb (f 3%positive 7%nat =? 12)%N (f x y =? 12)%N)) = true. +Proof using. pos_convert. nat_convert. N_convert. @@ -964,3 +976,21 @@ Qed. (* The tactic simpl does too much here : *) (* Goal forall x, 3 + x = x + 3. *) (* nat_convert. *) + + +(* Issue 10 + https://github.com/smtcoq/smtcoq/issues/10 +*) + +Goal forall (x : positive), Zpos x <=? Zpos x. +Proof using. + intros. + verit. +Qed. + + +Goal forall (x : positive) (a : Z), (Z.eqb a a) || negb (Zpos x <? Zpos x). +Proof using. + intros. + verit. +Qed. diff --git a/unit-tests/Tests_zchaff_tactics.v b/unit-tests/Tests_zchaff_tactics.v index c6ed4e3..cf86bc1 100644 --- a/unit-tests/Tests_zchaff_tactics.v +++ b/unit-tests/Tests_zchaff_tactics.v @@ -23,7 +23,7 @@ Local Open Scope int63_scope. Lemma check_univ (x1: bool): (x1 && (negb x1)) = false. -Proof. +Proof using. zchaff. Qed. @@ -31,55 +31,67 @@ Qed. (* zChaff tactic *) Goal forall a, a || negb a. +Proof using. zchaff. Qed. Goal forall a, negb (a || negb a) = false. +Proof using. zchaff. Qed. Goal forall a, negb (negb (a || negb a)). +Proof using. zchaff. Qed. Goal forall a, (a && negb a) = false. +Proof using. zchaff. Qed. Goal forall a, negb (a && negb a). +Proof using. zchaff. Qed. Goal forall a, implb a a. +Proof using. zchaff. Qed. Goal forall a, negb (implb a a) = false. +Proof using. zchaff. Qed. Goal forall a , (xorb a a) || negb (xorb a a). +Proof using. zchaff. Qed. Goal forall a, (a||negb a) || negb (a||negb a). +Proof using. zchaff. Qed. Goal true. +Proof using. zchaff. Qed. Goal negb false. +Proof using. zchaff. Qed. Goal forall a, Bool.eqb a a. -Proof. +Proof using. zchaff. Qed. Goal forall (a:bool), a = a. +Proof using. zchaff. Qed. @@ -88,7 +100,7 @@ Qed. (* ((a ∧ b) ∨ (b ∧ c)) ∧ ¬b = ⊥ *) Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false. -Proof. +Proof using. zchaff. Qed. @@ -97,7 +109,7 @@ Qed. (* (a ∨ a) ∧ ¬a = ⊥ *) Goal forall a, ((a || a) && (negb a)) = false. -Proof. +Proof using. zchaff. Qed. @@ -106,7 +118,7 @@ Qed. (* ¬(a ∨ ¬a) = ⊥ *) Goal forall a, (negb (a || (negb a))) = false. -Proof. +Proof using. zchaff. Qed. @@ -116,7 +128,7 @@ Qed. Goal forall a b c, (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. -Proof. +Proof using. zchaff. Qed. @@ -125,7 +137,7 @@ Qed. Goal forall i j k, ((i == j) || (j == k) || (k == i)) && ((negb (i == j)) || (negb (j == k)) || (negb (k == i))) && ((negb (i == j)) || (j == k)) && ((negb (j == k)) || (k == i)) && ((negb (k == i)) || (i == j)) = false. -Proof. +Proof using. zchaff. Qed. @@ -134,7 +146,7 @@ Goal forall i j k, let b := j == k in let c := k == i in (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. -Proof. +Proof using. zchaff. Qed. @@ -143,7 +155,7 @@ Qed. (* (a ∧ b) ∧ (c ∨ d) ∧ ¬(c ∨ (a ∧ b ∧ d)) = ⊥ *) Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false. -Proof. +Proof using. zchaff. Qed. @@ -152,7 +164,7 @@ Qed. (* a ∧ b ∧ c ∧ (¬a ∨ ¬b ∨ d) ∧ (¬d ∨ ¬c) = ⊥ *) Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false. -Proof. +Proof using. zchaff. Qed. @@ -160,37 +172,37 @@ Qed. (* Other connectives *) Goal (false || true) && false = false. -Proof. +Proof using. zchaff. Qed. Goal negb true = false. -Proof. +Proof using. zchaff. Qed. Goal false = false. -Proof. +Proof using. zchaff. Qed. Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)). -Proof. +Proof using. zchaff. Qed. Goal forall x y, Bool.eqb (implb x y) ((x && y) || (negb x)). -Proof. +Proof using. zchaff. Qed. Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)). -Proof. +Proof using. zchaff. Qed. @@ -198,7 +210,7 @@ Qed. (* Multiple negations *) Goal forall a, orb a (negb (negb (negb a))) = true. -Proof. +Proof using. zchaff. Qed. @@ -206,13 +218,13 @@ Qed. (* Polarities *) Goal forall a b, andb (orb a b) (negb (orb a b)) = false. -Proof. +Proof using. zchaff. Qed. Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false. -Proof. +Proof using. zchaff. Qed. @@ -307,7 +319,7 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44) && (orb (orb (orb x15 x25) x35) x45)) = false. -Proof. +Proof using. zchaff. Qed. @@ -316,12 +328,12 @@ Qed. (* Goal forall x, x && (negb x). -Proof. +Proof using. zchaff. Abort. Goal forall x y, (implb (implb x y) (implb y x)). -Proof. +Proof using. zchaff. Abort. @@ -391,7 +403,7 @@ Goal forall x11 x12 x13 x14 x21 x22 x23 x24 x31 x32 x33 x34 x41 x42 x43 x44, ( (orb (orb (orb x12 x22) x32) x42) && (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44)) = false. -Proof. +Proof using. zchaff. Abort. *) |