From 75dff01782c3afdaea91841f69c734eb6ab9baf8 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 4 Feb 2022 11:56:09 +0100 Subject: Use trakt --- src/Conversion_tactics.v | 460 ------------------------------------------- src/PropToBool.v | 362 ---------------------------------- src/SMTCoq.v | 4 +- src/Tactics.v | 204 ++++++++----------- src/_CoqProject | 8 +- src/preproc/Conversion.v | 401 +++++++++++++++++++++++++++++++++++++ src/preproc/Database_trakt.v | 224 +++++++++++++++++++++ 7 files changed, 712 insertions(+), 951 deletions(-) delete mode 100644 src/Conversion_tactics.v delete mode 100644 src/PropToBool.v create mode 100644 src/preproc/Conversion.v create mode 100644 src/preproc/Database_trakt.v diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v deleted file mode 100644 index 0483db0..0000000 --- a/src/Conversion_tactics.v +++ /dev/null @@ -1,460 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -(* This file provides: - - a generic way to inject, via tactics, types of natural numbers into - the type Z, which is the type known by SMT solvers and, thus, by - SMTCoq - - an instanciation for the types nat, positive and N. -*) - - - -Require Import ZArith. - -(* This module represents the structure to be injected into Z *) -Module Type convert_type. - -(* The type to be injected *) -Parameter T : Type. - -(* Mapping both ways *) -Parameter Z2T : Z -> T. -Parameter T2Z : T -> Z. -(* T2Z is an injection *) -Axiom T2Z_id : forall x : T, Z2T (T2Z x) = x. - -(* A property about elements of Z coming from elements of T. - For instance, for nat, all elements are non-negative: (0 <=? z)%Z *) -Parameter inT : Z -> bool. -(* The image of the injection satisfies this property *) -Axiom T2Z_pres : forall x : T, inT (T2Z x) = true. -(* It is always possible to define inT as Z.eqb z (T2Z (Z2T z))>. - In this case, the proof of the axiom is simply: - . *) - -(* We ask this injection to be a morphism for all the following symbols *) - -(* Addition *) -Parameter add : T -> T -> T. -Axiom t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). - -(* Multiplication *) -Parameter mul : T -> T -> T. -Axiom t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). - -(* <= *) -Parameter leb : T -> T -> bool. -Axiom t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. - -(* < *) -Parameter ltb : T -> T -> bool. -Axiom t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. - -(* = *) -Parameter eqb : T -> T -> bool. -Axiom t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. -End convert_type. - -(* This fonctor builds a conversion tactic from a module of the signature above *) -Module convert (M : convert_type). - -Import M. - -(* SMTCoq uses Booleans *) -Lemma implb_impl : forall a b : bool, (implb a b = true -> a = true -> b = true). -Proof. -intros a b H. -destruct a; destruct b; try reflexivity; discriminate. -Qed. - -(* Get the head symbol of an application *) -Ltac get_head x := lazymatch x with ?x _ => get_head x | _ => x end. - -(* [inverse_tactic tactic] succceds when [tactic] fails, and the other way round *) -Ltac inverse_tactic tactic := try (tactic; fail 1). - -(* [constr_neq t u] fails if and only if [t] and [u] are convertible *) -Ltac constr_neq t u := inverse_tactic ltac:(constr_eq t u). - -(* [is_not_constructor U sym] fails if and only if [sym] is a constructor of [U] *) -Ltac is_not_constructor U sym := -let H := fresh in -assert (U -> True) as H by - (let x := fresh in - let y := fresh in - intro x; - pose x as y; - destruct x; - let C := eval unfold y in y in - let c := get_head C in - constr_neq sym c; - exact I); clear H. - -(* [is_constructor U sym] succeeds if and only if [sym] is a constructor of [U] *) -Ltac is_constructor U sym := inverse_tactic ltac:(is_not_constructor U sym). - -(* Replaces the sub-terms [x] of type [T] which are not under a known - symbol by Z2T (T2Z x) *) -Ltac converting := - (* The heart of the tactic *) - repeat - match goal with - (* We capture each subèterm [x] together with its context, i.e. the goal is C[x] *) - | |- context C[?x] => - (* If [x] has type [T] *) - let U := type of x in - lazymatch eval fold T in U with - | T => - lazymatch x with - (* If x is of the shape Z2T (T2Z _) we stop since [x] is already in the expected shape *) - | Z2T (T2Z _) => fail - | _ => - (* We generate a fresh variable of type T *) - let var := fresh in - pose proof x as var; - (* Otherwise, we analyze the formula obtained by replacing [x] by the fresh variable in the goal *) - lazymatch context C[var] with - | context [?h var] => - let h := get_head h in - lazymatch h with - (* [x] is already in the expected shape *) - | T2Z => fail - (* Not necessary to rewrite under symbols commuting with T2Z *) - | add => fail | mul => fail | ltb => fail | leb => fail | eqb => fail - (* Do not rewrite inside a constant *) - | Zpos => fail | Zneg => fail - | _ => - (* Idem: if the context contains a constructor of [T], and - [x] starts with a constructor of [T], we are inside a - constant *) - let hx := get_head x in - try (is_constructor T h; is_constructor T hx; fail 1); - (* Otherwise, we rewrite *) - let old_goal := context C[x] in - let new_goal := context C[Z2T (T2Z x)] in - replace old_goal with new_goal by (rewrite (T2Z_id x); reflexivity) end - end; - (* We clear the fresh variable *) - clear var - end - end - end. - -Ltac rewriting := - repeat (try rewrite <- t2z_leb_morph; - try rewrite <- t2z_ltb_morph; - try rewrite <- t2z_eqb_morph; - try rewrite <- t2z_add_morph; - try rewrite <- t2z_mul_morph). - - -(* expand_type [Tn;...T2;;T1] T = T1->T2->...->Tn->T *) -Fixpoint expand_type l T : Type := - match l with - | nil => T - | cons h l => expand_type l (h -> T) - end. -(* get_args (f t1 t2 ... tn) = [(Tn,tn);...;(T2,t2);(T1,t1)] *) -Ltac get_args X := - lazymatch X with - | ?x ?y => let x_args := get_args x in let T := type of y in constr:(cons (existT (fun z => z) T y) x_args) - | _ => constr:(@nil (sigT (fun x => x))) - end. -(* get_args_types [(Tn,tn);...;(T2,t2);(T1,t1)] = [Tn;...;T2;T1] *) -Fixpoint get_args_types (l : list (sigT (fun x => x))) : list Type := - match l with - | nil => nil - | cons (@existT _ _ T _) l => cons T (get_args_types l) - end. -(* apply_args [(Tn,tn);...;(T2,t2);(T1,t1)] T (f : T1->T2->...->Tn->T) = f t1 t2 ... tn *) -Ltac apply_args f args := - lazymatch args with - | nil => constr:(f) - | cons ?arg ?args => match arg with existT _ _ ?arg => let f := apply_args f args in constr:(f arg) end - end. - -(* expand_fun [Tn;...;T2;T1] T U (f : T1->T2->...->Tn->T) (g : T->U) = fun x1 x2 ... xn => g (f x1 x2 ... xn) *) -Fixpoint expand_fun (l : list Type) (T : Type) (U : Type) : expand_type l T -> (T -> U) -> expand_type l U := - match l with - | nil => fun f g => g f - | cons h l' => fun f g => expand_fun l' (h -> T) (h -> U) f (fun a x => g (a x)) - end. -(* expand (f (t1:T1) (t2:T2) ... (tn:Tn) : T) (g : T->U) = fun x1 x2 ... xn => g (f x1 x2 ... xn) *) -Ltac expand X g := - (* Let argsX = [(Tn,tn);...;(T2,t2);(T1,t1)] *) - let argsX := get_args X in - (* Let argsXtypes = [Tn;...;T2;T1] *) - let argsXtypes := constr:(get_args_types argsX) in - (* Let typeX = T *) - let typeX := type of X in - (* Let h = f *) - let h := get_head X in - (* Let typeg = U *) - let typeg := match type of g with _ -> ?U => U end in - (* We return expand_fun [Tn;...;T2;T1] T Z f T2Z = fun x1 x2 ... xn => g (f x1 x2 ... xn) *) - constr:(expand_fun argsXtypes typeX typeg h g). - -(* Replaces function symbols with return type in T, and variables in T, - by their counterparts in Z, adding the positivity hypotheses *) -Ltac renaming := - repeat - match goal with - (* If there is a term of the shape (T2Z (f t1 ... tn)) *) - | |- context [T2Z ?X] => - (* Get the head symbol *) - let f := get_head X in - (* Nothing to do if it is a constructor *) - is_not_constructor T f; - (* Otherwise, let fe = fun x1 ... xn => T2Z (f x1 ... xn) *) - let fe := expand X T2Z in - let fe := eval cbv in fe in - (* Pose fe_id := fun x1 ... xn => T2Z (f x1 ... xn) *) - let fe_id := fresh in pose (fe_id := fe); - repeat - match goal with - (* For each term of the shape (T2Z (f' t'1 ... t'n)) *) - | |- context [T2Z ?X'] => - (* Get the head symbol *) - let f' := get_head X' in - (* If f' = f *) - constr_eq f f'; - (* Add the hypothesis inT (T2Z X') *) - generalize (T2Z_pres X'); apply implb_impl; - (* Let args = [t'1;...;t'n] *) - let args := get_args X' in - (* Let Y = fe_id t'1 ... t'n *) - let Y := apply_args fe_id args in - (* Replace [T2Z (f' t'1 ... t'n)] by [Y] *) - change (T2Z X') with Y - end; - (* Abstract over [fe_id := fun x1 ... xn => T2Z (f x1 ... xn)] *) - generalize fe_id; - (* Erase the old f and the temporary fe_id *) - clear f fe_id; - (* Introduce the new f with the same name *) - let f := fresh f in - intro f - end. - -(* expand_fun' [Tn;...;T2;T1] T U (f : T1->T2->...->Tn->T) (a : T->U) = fun x1 x2 ... xn => a (f x1 x2 ... xn) *) -Fixpoint expand_fun' (l : list Type) : forall T U : Type, expand_type l T -> (T -> U) -> expand_type l U := - match l as l return forall T U, expand_type l T -> (T ->U) -> expand_type l U with - | nil => fun T U f a => a f - | cons T' l => fun T U f a => expand_fun' l (T' -> T) (T' -> U) f (fun g xn => a (g xn)) - end. -(* expand' (f (t1:T1) (t2:T2) ... (tn:Tn) : T) (g : U->Tn) = fun x1 x2 ... xn => f x1 x2 ... (g xn) *) -Ltac expand' X g := - (* Let argsX = [(Tn,tn);...;(T2,t2);(T1,t1)] *) - let argsX := get_args X in - (* Let argsXtypes = [Tn;...;T2;T1] *) - let argsXtypes := constr:(get_args_types argsX) in - let argsXtypes := eval cbv in argsXtypes in - (* Let Tn = Tn *) - let Tn := match argsXtypes with cons ?T _ => T end in - (* Let argsXtypes = [Tn-1;...;T2;T1] *) - let argsXtypes := match argsXtypes with cons _ ?args => args end in - (* Let typeX = T *) - let typeX := type of X in - (* Let h = f *) - let h := get_head X in - (* Let typeg = U *) - let typeg := match type of g with ?U -> _ => U end in - (* Return expand_fun' [Tn-1;...;T2;T1] (Tn->T) (Z->T) f (fun b x => b (g x))) = fun x1 x2 ... xn => f x1 x2 ... (g xn) *) - constr:(expand_fun' argsXtypes (Tn -> typeX) (typeg -> typeX) h (fun b x => b (g x))). - -(* Replaces function symbols with parameters in T, with their - counterparts with parameters in Z *) -Ltac renaming' := - repeat - match goal with - (* If there is a term of the shape (f t1 ... (Z2T tn)) *) - | |- context [?X (Z2T ?Y)] => - (* Get the head symbol *) - let f := get_head X in - (* Nothing to do if it is a constructor *) - is_not_constructor T f; - (* Otherwise, let fe = fun x1 ... xn => f x1 ... (Z2T xn) *) - let fe := expand' (X (Z2T Y)) Z2T in - let fe := eval simpl in fe in - repeat - match goal with - (* For each term of the shape (f' t'1 ... (Z2T t'n)) *) - | |- context [?X' (Z2T ?Y')] => - (* Get the head symbol *) - let f' := get_head X' in - (* If f' = f *) - constr_eq f f'; - (* Let args = [t'1;...;t'(n-1)] *) - let args := get_args X' in - (* Let Z = (fun x1 ... xn => f x1 ... (Z2T xn)) t'1 ... t'(n-1) *) - let Z := apply_args fe args in - (* Replace (f' t'1 ... (Z2T t'n)) with (Z t'n) *) - change (X' (Z2T Y')) with (Z Y') - end; - (* Abstract over (fun x1 ... xn => (f x1 ... (Z2T xn)) *) - generalize fe; - (* Erase the old f *) - clear f; - (* Introduce the new f with the same name *) - let f := fresh f in - intro f - end. - -(* The whole tactic *) -Ltac convert := -fold T add mul ltb leb eqb; -intros; -converting; -rewriting; -renaming; -renaming'; -let T2Z_unfolded := eval red in T2Z in change T2Z with T2Z_unfolded; -let inT_unfolded := eval red in inT in change inT with inT_unfolded; -simpl. - -End convert. - -(* Instanciation for the type [positive] *) -Module pos_convert_type <: convert_type. - -Definition T : Type := positive. - -Definition Z2T : Z -> T := fun z => - match z with - | 0%Z => 1%positive - | Zpos p => p - | Zneg _ => 1%positive - end. - -Definition T2Z : T -> Z := Zpos. -Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. reflexivity. Qed. - -Definition inT : Z -> bool := fun z => Z.ltb 0 z. -Lemma T2Z_pres : forall x, inT (T2Z x) = true. reflexivity. Qed. - -Definition add : T -> T -> T := Pos.add. -Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). -Proof. reflexivity. Qed. - -Definition mul : T -> T -> T := Pos.mul. -Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). -Proof. reflexivity. Qed. - -Definition leb : T -> T -> bool := Pos.leb. -Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. -Proof. reflexivity. Qed. - -Definition ltb : T -> T -> bool := Pos.ltb. -Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. -Proof. reflexivity. Qed. - -Definition eqb : T -> T -> bool := Pos.eqb. -Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. -Proof. reflexivity. Qed. -End pos_convert_type. - -Module pos_convert_mod := convert pos_convert_type. - -Ltac pos_convert := pos_convert_mod.convert. - - -(* Instanciation for the type [N] *) -Module N_convert_type <: convert_type. - -Definition T : Type := N. - -Definition Z2T : Z -> T := Z.to_N. - -Definition T2Z : T -> Z := Z.of_N. -Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. exact N2Z.id. Qed. - -Definition inT : Z -> bool := fun z => Z.leb 0 z. -Lemma T2Z_pres : forall x, inT (T2Z x) = true. intro; unfold inT; rewrite Z.leb_le; apply N2Z.is_nonneg. Qed. - -Definition add : T -> T -> T := N.add. -Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). -Proof. intros x y; destruct x, y; reflexivity. Qed. - -Definition mul : T -> T -> T := N.mul. -Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). -Proof. intros x y; destruct x, y; reflexivity. Qed. - -Definition leb : T -> T -> bool := N.leb. -Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. -Proof. intros x y; destruct x, y; reflexivity. Qed. - -Definition ltb : T -> T -> bool := N.ltb. -Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. -Proof. intros x y; destruct x, y; reflexivity. Qed. - -Definition eqb : T -> T -> bool := N.eqb. -Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. -Proof. intros x y; destruct x, y; reflexivity. Qed. - -End N_convert_type. - -Module N_convert_mod := convert N_convert_type. - -Ltac N_convert := N_convert_mod.convert. - -(* Instanciation for the type [nat] *) -Require Import NPeano. -Module nat_convert_type <: convert_type. - -Definition T : Type := nat. - -Definition Z2T : Z -> T := Z.to_nat. - -Definition T2Z : T -> Z := Z.of_nat. -Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. exact Nat2Z.id. Qed. - -Definition inT : Z -> bool := fun z => Z.leb 0 z. -Lemma T2Z_pres : forall x, inT (T2Z x) = true. intro; unfold inT; rewrite Z.leb_le; apply Nat2Z.is_nonneg. Qed. - -Definition add : T -> T -> T := Nat.add. -Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). -Proof. symmetry. apply Nat2Z.inj_add. Qed. - -Definition mul : T -> T -> T := Nat.mul. -Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). -Proof. symmetry. apply Nat2Z.inj_mul. Qed. - -Definition leb : T -> T -> bool := Nat.leb. -Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. -Proof. - intros x y; unfold leb. - case_eq (Nat.leb x y); [| rewrite <- 2 Bool.not_true_iff_false]; - rewrite <- Zle_is_le_bool; rewrite Nat.leb_le; rewrite Nat2Z.inj_le; auto. -Qed. - -Definition ltb : T -> T -> bool := Nat.ltb. -Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. -Proof. - intros x y; unfold ltb. - case_eq (Nat.ltb x y); [| rewrite <- 2 Bool.not_true_iff_false]; - rewrite <- Zlt_is_lt_bool; rewrite Nat.ltb_lt; rewrite Nat2Z.inj_lt; auto. -Qed. - -Definition eqb : T -> T -> bool := Nat.eqb. -Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. -Proof. - intros x y; unfold eqb. - case_eq (Nat.eqb x y); [| rewrite <- 2 Bool.not_true_iff_false]; - rewrite Z.eqb_eq; rewrite Nat.eqb_eq; rewrite Nat2Z.inj_iff; auto. -Qed. - -End nat_convert_type. - -Module nat_convert_mod := convert nat_convert_type. - -Ltac nat_convert := nat_convert_mod.convert. diff --git a/src/PropToBool.v b/src/PropToBool.v deleted file mode 100644 index 31f8b2d..0000000 --- a/src/PropToBool.v +++ /dev/null @@ -1,362 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -Require Import - Bool ZArith BVList Logic BVList FArray - SMT_classes SMT_classes_instances ReflectFacts. -Import BVList.BITVECTOR_LIST. - - -Lemma geb_ge (n m : Z) : (n >=? m)%Z = true <-> (n >= m)%Z. -Proof. - now rewrite Z.geb_le, Z.ge_le_iff. -Qed. - -Ltac prop2bool := - repeat - match goal with - | [ |- forall _ : ?t, _ ] => - lazymatch type of t with - | Prop => - match t with - | forall _ : _, _ => intro - | _ => fail - end - | _ => intro - end - - | [ |- context[ bv_ultP _ _ ] ] => rewrite <- bv_ult_B2P - | [ |- context[ bv_sltP _ _ ] ] => rewrite <- bv_slt_B2P - | [ |- context[ Z.lt _ _ ] ] => rewrite <- Z.ltb_lt - | [ |- context[ Z.gt _ _ ] ] => rewrite Zgt_is_gt_bool - | [ |- context[ Z.le _ _ ] ] => rewrite <- Z.leb_le - | [ |- context[ Z.ge _ _ ] ] => rewrite <- geb_ge - | [ |- context[ Z.eq _ _ ] ] => rewrite <- Z.eqb_eq - - | [ |- context[ @Logic.eq ?t ?x ?y ] ] => - lazymatch t with - | bitvector _ => rewrite <- bv_eq_reflect - | farray _ _ => rewrite <- equal_iff_eq - | Z => rewrite <- Z.eqb_eq - | bool => - lazymatch y with - | true => fail - | _ => rewrite <- (eqb_true_iff x y) - end - | _ => - lazymatch goal with - | [ p: (CompDec t) |- _ ] => - rewrite (@compdec_eq_eqb _ p) - | _ => - let p := fresh "p" in - assert (p:CompDec t); - [ try (exact _) (* Use the typeclass machinery *) - | rewrite (@compdec_eq_eqb _ p) - ] - end - end - - | [ |- context[?G0 = true \/ ?G1 = true ] ] => - rewrite (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1)); - [ | apply orP] - - | [ |- context[?G0 = true -> ?G1 = true ] ] => - rewrite (@reflect_iff (G0 = true -> G1 = true) (implb G0 G1)); - [ | apply implyP] - - | [ |- context[?G0 = true /\ ?G1 = true ] ] => - rewrite (@reflect_iff (G0 = true /\ G1 = true) (andb G0 G1)); - [ | apply andP] - - | [ |- context[?G0 = true <-> ?G1 = true ] ] => - rewrite (@reflect_iff (G0 = true <-> G1 = true) (Bool.eqb G0 G1)); - [ | apply iffP] - - | [ |- context[ ~ ?G = true ] ] => - rewrite (@reflect_iff (~ G = true) (negb G)); - [ | apply negP] - - | [ |- context[ is_true ?G ] ] => - unfold is_true - - | [ |- context[ True ] ] => rewrite <- TrueB - - | [ |- context[ False ] ] => rewrite <- FalseB - end. - - -Ltac bool2prop_true := - repeat - match goal with - | [ |- forall _ : ?t, _ ] => - lazymatch type of t with - | Prop => fail - | _ => intro - end - - | [ |- context[ bv_ult _ _ = true ] ] => rewrite bv_ult_B2P - | [ |- context[ bv_slt _ _ = true ] ] => rewrite bv_slt_B2P - | [ |- context[ Z.ltb _ _ = true ] ] => rewrite Z.ltb_lt - | [ |- context[ Z.gtb _ _ ] ] => rewrite <- Zgt_is_gt_bool - | [ |- context[ Z.leb _ _ = true ] ] => rewrite Z.leb_le - | [ |- context[ Z.geb _ _ ] ] => rewrite geb_ge - | [ |- context[ Z.eqb _ _ = true ] ] => rewrite Z.eqb_eq - - | [ |- context[ Bool.eqb _ _ = true ] ] => rewrite eqb_true_iff - - | [ |- context[ eqb_of_compdec ?p _ _ = true ] ] => rewrite <- (@compdec_eq_eqb _ p) - - | [ |- context[ ?G0 || ?G1 = true ] ] => - rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1)); - [ | apply orP] - - | [ |- context[ implb ?G0 ?G1 = true ] ] => - rewrite <- (@reflect_iff (G0 = true -> G1 = true) (implb G0 G1)); - [ | apply implyP] - - | [ |- context[?G0 && ?G1 = true ] ] => - rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (andb G0 G1)); - [ | apply andP] - - | [ |- context[Bool.eqb ?G0 ?G1 = true ] ] => - rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (Bool.eqb G0 G1)); - [ | apply iffP] - - | [ |- context[ negb ?G = true ] ] => - rewrite <- (@reflect_iff (~ G = true) (negb G)); - [ | apply negP] - - | [ |- context[ true = true ] ] => rewrite TrueB - - | [ |- context[ false = true ] ] => rewrite FalseB - end. - -Ltac bool2prop := unfold is_true; bool2prop_true. - - -Ltac prop2bool_hyp H := - let TH := type of H in - - (* Add a CompDec hypothesis if needed *) - let prop2bool_t := fresh "prop2bool_t" in epose (prop2bool_t := ?[prop2bool_t_evar] : Type); - let prop2bool_comp := fresh "prop2bool_comp" in epose (prop2bool_comp := ?[prop2bool_comp_evar] : bool); - let H' := fresh in - assert (H':False -> TH); - [ let HFalse := fresh "HFalse" in intro HFalse; - repeat match goal with - | [ |- forall _ : ?t, _ ] => - lazymatch type of t with - | Prop => fail - | _ => intro - end - | [ |- context[@Logic.eq ?A _ _] ] => instantiate (prop2bool_t_evar := A); instantiate (prop2bool_comp_evar := true) - | _ => instantiate (prop2bool_t_evar := nat); instantiate (prop2bool_comp_evar := false) - end; - destruct HFalse - | ]; - clear H'; - match (eval compute in prop2bool_comp) with - | true => - let A := eval cbv in prop2bool_t in - match goal with - | [ _ : CompDec A |- _ ] => idtac - | _ => - let Hcompdec := fresh "Hcompdec" in - assert (Hcompdec: CompDec A); - [ try (exact _) | ] - end - | false => idtac - end; - clear prop2bool_t; clear prop2bool_comp; - - (* Compute the bool version of the lemma *) - [ .. | - let prop2bool_Hbool := fresh "prop2bool_Hbool" in epose (prop2bool_Hbool := ?[prop2bool_Hbool_evar] : Prop); - assert (H':False -> TH); - [ let HFalse := fresh "HFalse" in intro HFalse; - let rec tac_rec := - match goal with - | [ |- forall _ : ?t, _ ] => - lazymatch type of t with - | Prop => fail - | _ => - let H := fresh in - intro H; tac_rec; revert H - end - | _ => prop2bool - end in - tac_rec; - match goal with - | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g - end; - destruct HFalse - | ]; - clear H'; - - (* Assert and prove the bool version of the lemma *) - assert (H':prop2bool_Hbool); subst prop2bool_Hbool; - [ bool2prop; apply H | ]; - - (* Replace the Prop version with the bool version *) - try clear H; let H := fresh H in assert (H:=H'); clear H' - ]. - - -Ltac remove_compdec_hyp H := - let TH := type of H in - match TH with - | forall p : CompDec ?A, _ => - match goal with - | [ p' : CompDec A |- _ ] => - let H1 := fresh in - assert (H1 := H p'); clear H; assert (H := H1); clear H1; - remove_compdec_hyp H - | _ => - let c := fresh "c" in - assert (c : CompDec A); - [ try (exact _) - | let H1 := fresh in - assert (H1 := H c); clear H; assert (H := H1); clear H1; - remove_compdec_hyp H ] - end - | _ => idtac - end. - - -Ltac prop2bool_hyps Hs := - lazymatch Hs with - | (?Hs1, ?Hs2) => prop2bool_hyps Hs1; [ .. | prop2bool_hyps Hs2] - | ?H => remove_compdec_hyp H; try prop2bool_hyp H - end. - - - -Section Test. - Variable A : Type. - - Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = (length l1 + length l2)%nat. - Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z. - Hypothesis uninterpreted_type : forall (a:A), a = a. - Hypothesis bool_eq : forall (b:bool), negb (negb b) = b. - - Goal True. - Proof. - prop2bool_hyp basic. - prop2bool_hyp no_eq. - prop2bool_hyp uninterpreted_type. - admit. - prop2bool_hyp bool_eq. - prop2bool_hyp plus_n_O. - Abort. - - Goal True. - Proof. - prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, bool_eq, plus_O_n). - admit. - Abort. -End Test. - -Section Group. - - Variable G : Type. - Variable HG : CompDec G. - Variable op : G -> G -> G. - Variable inv : G -> G. - Variable e : G. - - Hypothesis associative : - forall a b c : G, op a (op b c) = op (op a b) c. - Hypothesis identity : - forall a : G, (op e a = a) /\ (op a e = a). - Hypothesis inverse : - forall a : G, (op a (inv a) = e) /\ (op (inv a) a = e). - - Variable e' : G. - Hypothesis other_id : forall e' z, op e' z = z. - - Goal True. - Proof. - prop2bool_hyp associative. - prop2bool_hyp identity. - prop2bool_hyp inverse. - prop2bool_hyp other_id. - exact I. - Qed. - - Goal True. - Proof. - prop2bool_hyps (associative, identity, inverse, other_id). - exact I. - Qed. - -End Group. - - -Section MultipleCompDec. - - Variables A B : Type. - Hypothesis multiple : forall (a1 a2:A) (b1 b2:B), a1 = a2 -> b1 = b2. - - Goal True. - Proof. - Fail prop2bool_hyp multiple. - Abort. - -End MultipleCompDec. - - -(* We can assume that we deal only with monomorphic hypotheses, since - polymorphism will be removed before *) -Section Poly. - Hypothesis basic : forall (A:Type) (l1 l2:list A), - length (l1++l2) = (length l1 + length l2)%nat. - Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a. - - Goal True. - Proof. - prop2bool_hyp basic. - Fail prop2bool_hyp uninterpreted_type. - Abort. - -End Poly. - - - - - -Infix "--->" := implb (at level 60, right associativity) : bool_scope. -Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope. - - - -(* Does not fail since 8.10 *) - -Goal True. - evar (t:Type). - assert (H:True). - - instantiate (t:=nat). exact I. - - exact I. -Qed. - -Goal True. - evar (t:option Set). - assert (H:True). - - instantiate (t:=Some nat). exact I. - - exact I. -Qed. - -Goal True. - evar (t:option Type). - assert (H:True). - - Fail instantiate (t:=Some nat). exact I. - - exact I. -Abort. diff --git a/src/SMTCoq.v b/src/SMTCoq.v index 694f2ed..f3904ae 100644 --- a/src/SMTCoq.v +++ b/src/SMTCoq.v @@ -10,9 +10,9 @@ (**************************************************************************) -Require Export PropToBool. Require Export Int63 List. Require Export SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances. Require Export Tactics. -Require Export Conversion_tactics. Export Atom Form Sat_Checker Cnf_Checker Euf_Checker. +From Trakt Require Export Trakt. +Require Export Database_trakt. diff --git a/src/Tactics.v b/src/Tactics.v index 5be62cc..685cfdb 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -10,148 +10,104 @@ (**************************************************************************) -Require Import PropToBool. +From Trakt Require Import Trakt. +Require Import Conversion. Require Import Int63 List PArray Bool ZArith. Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst. Declare ML Module "smtcoq_plugin". -(** Collect all the hypotheses from the context *) - -Ltac get_hyps_acc acc := - match goal with - | [ H : ?P |- _ ] => - let T := type of P in - lazymatch T with - | Prop => - lazymatch P with - | id _ => fail - | _ => - let _ := match goal with _ => change P with (id P) in H end in - match acc with - | Some ?t => get_hyps_acc (Some (H, t)) - | None => get_hyps_acc (Some H) - end - end - | _ => fail - end - | _ => acc - end. - -Ltac eliminate_id := - repeat match goal with - | [ H : ?P |- _ ] => - lazymatch P with - | id ?Q => change P with Q in H - | _ => fail - end - end. - -Ltac get_hyps := - let Hs := get_hyps_acc (@None nat) in - let _ := match goal with _ => eliminate_id end in - Hs. - - -(* Section Test. *) -(* Variable A : Type. *) -(* Hypothesis H1 : forall a:A, a = a. *) -(* Variable n : Z. *) -(* Hypothesis H2 : n = 17%Z. *) - -(* Goal True. *) -(* Proof. *) -(* let Hs := get_hyps in idtac Hs. *) -(* Abort. *) -(* End Test. *) - - -(** Tactics in bool *) +Ltac zchaff := trakt Z bool; Tactics.zchaff_bool. +Ltac zchaff_no_check := trakt Z bool; Tactics.zchaff_bool_no_check. Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; try (exact _). Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; try (exact _). -Tactic Notation "verit_bool" constr(h) := - let Hs := get_hyps in - match Hs with - | Some ?Hs => verit_bool_base_auto (Some (h, Hs)) - | None => verit_bool_base_auto (Some h) - end; - vauto. -Tactic Notation "verit_bool" := - let Hs := get_hyps in - verit_bool_base_auto Hs; vauto. - -Tactic Notation "verit_bool_no_check" constr(h) := - let Hs := get_hyps in - match Hs with - | Some ?Hs => verit_bool_no_check_base_auto (Some (h, Hs)) - | None => verit_bool_no_check_base_auto (Some h) - end; - vauto. -Tactic Notation "verit_bool_no_check" := - let Hs := get_hyps in - fun Hs => verit_bool_no_check_base_auto Hs; vauto. - - -(** Tactics in Prop **) - -Ltac zchaff := prop2bool; zchaff_bool; bool2prop. -Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop. - -Tactic Notation "verit" constr(h) := - prop2bool; - [ .. | prop2bool_hyps h; - [ .. | let Hs := get_hyps in - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_base_auto (Some (h, Hs)) ] - | None => verit_bool_base_auto (Some h) - end; vauto - ] +Tactic Notation "verit" constr(global) := + intros; + unfold is_true in *; + let Hsglob := pose_hyps global (@None unit) in + let local := get_hyps_option in + let Hs := + lazymatch local with + | Some ?local' => pose_hyps local' Hsglob + | None => constr:(Hsglob) + end + in + preprocess1 Hs; + [ .. | + let Hs' := intros_names in + preprocess2 Hs'; + verit_bool_base_auto Hs'; + QInst.vauto ]. + Tactic Notation "verit" := - prop2bool; - [ .. | let Hs := get_hyps in - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_base_auto (Some Hs) ] - | None => verit_bool_base_auto (@None nat) - end; vauto + intros; + unfold is_true in *; + let local := get_hyps_option in + let Hs := + lazymatch local with + | Some ?local' => pose_hyps local' (@None unit) + | None => constr:(@None unit) + end + in + preprocess1 Hs; + [ .. | + let Hs' := intros_names in + preprocess2 Hs'; + verit_bool_base_auto Hs'; + QInst.vauto ]. -Tactic Notation "verit_no_check" constr(h) := - prop2bool; - [ .. | prop2bool_hyps h; - [ .. | let Hs := get_hyps in - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ] - | None => verit_bool_no_check_base_auto (Some h) - end; vauto - ] + +Tactic Notation "verit_no_check" constr(global) := + intros; + unfold is_true in *; + let Hsglob := pose_hyps global (@None unit) in + let local := get_hyps_option in + let Hs := + lazymatch local with + | Some ?local' => pose_hyps local' Hsglob + | None => constr:(Hsglob) + end + in + preprocess1 Hs; + [ .. | + let Hs' := intros_names in + preprocess2 Hs'; + verit_bool_no_check_base_auto Hs'; + QInst.vauto ]. + Tactic Notation "verit_no_check" := - prop2bool; - [ .. | let Hs := get_hyps in - match Hs with - | Some ?Hs => - prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base_auto (Some Hs) ] - | None => verit_bool_no_check_base_auto (@None nat) - end; vauto + intros; + unfold is_true in *; + let local := get_hyps_option in + let Hs := + lazymatch local with + | Some ?local' => pose_hyps local' (@None unit) + | None => constr:(@None unit) + end + in + preprocess1 Hs; + [ .. | + let Hs' := intros_names in + preprocess2 Hs'; + verit_bool_no_check_base_auto Hs'; + QInst.vauto ]. -Ltac cvc4 := prop2bool; [ .. | cvc4_bool; bool2prop ]. -Ltac cvc4_no_check := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ]. +Ltac cvc4 := trakt Z bool; [ .. | cvc4_bool ]. +Ltac cvc4_no_check := trakt Z bool; [ .. | cvc4_bool_no_check ]. + +Tactic Notation "smt" constr(h) := intros; try verit h; cvc4; try verit h. +Tactic Notation "smt" := intros; try verit ; cvc4; try verit. +Tactic Notation "smt_no_check" constr(h) := + intros; try verit_no_check h; cvc4_no_check; try verit_no_check h. +Tactic Notation "smt_no_check" := + intros; try verit_no_check ; cvc4_no_check; try verit_no_check. -Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try verit h; cvc4_bool; try verit h; bool2prop ]). -Tactic Notation "smt" := (prop2bool; [ .. | try verit ; cvc4_bool; try verit ; bool2prop ]). -Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try verit_no_check h; cvc4_bool_no_check; try verit_no_check h; bool2prop]). -Tactic Notation "smt_no_check" := (prop2bool; [ .. | try verit_no_check ; cvc4_bool_no_check; try verit_no_check ; bool2prop]). diff --git a/src/_CoqProject b/src/_CoqProject index 9ac5799..21bd41b 100644 --- a/src/_CoqProject +++ b/src/_CoqProject @@ -8,7 +8,7 @@ ######################################################################## ## To generate the Makefile: ## -## coq_makefile -f Make -o Makefile ## +## coq_makefile -f _CoqProject -o Makefile ## ## sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile ## ## WARNING: DO NOT FORGET THE SECOND LINE (see PR#62) ## ######################################################################## @@ -26,6 +26,7 @@ -I lia -I smtlib2 -I trace +-I preproc -I verit -I zchaff -I PArray @@ -134,11 +135,12 @@ spl/Syntactic.v spl/Arithmetic.v spl/Operators.v -Conversion_tactics.v +preproc/Database_trakt.v +preproc/Conversion.v + Misc.v SMTCoq.v ReflectFacts.v -PropToBool.v QInst.v Tactics.v SMT_terms.v diff --git a/src/preproc/Conversion.v b/src/preproc/Conversion.v new file mode 100644 index 0000000..635a47a --- /dev/null +++ b/src/preproc/Conversion.v @@ -0,0 +1,401 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2021 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +From Trakt Require Import Trakt. +Require Import Database_trakt. +Require Import ZArith. + +Require SMT_classes BVList FArray. + + +(* Conversion tactic *) + +Infix "--->" := implb (at level 60, right associativity) : bool_scope. +Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope. + + +(* Get all hypotheses of type Prop *) + +Ltac get_hyps_option := + match goal with + | H : ?P |- _ => + let _ := match goal with _ => revert H end in + let acc := get_hyps_option in + let _ := match goal with _ => intro H end in + let S := type of P in + lazymatch S with + | Prop => + lazymatch acc with + | Some ?acc' => constr:(Some (acc',H)) + | None => constr:(Some H) + end + | _ => constr:(acc) + end + | _ => constr:(@None unit) + end. + + +(* Assert global and local hypotheses (local: to avoid problems with Section variables) *) + +Ltac pose_hyps Hs acc := + lazymatch Hs with + | (?Hs1, ?Hs2) => + let acc1 := pose_hyps Hs1 acc in + let acc2 := pose_hyps Hs2 acc1 in + constr:(acc2) + | ?H' => + let H := fresh "H" in + let _ := match goal with _ => assert (H := H') end in + lazymatch acc with + | Some ?acc' => constr:(Some (acc', H)) + | None => constr:(Some H) + end + end. + +(* Goal True. *) +(* let Hs := pose_hyps ((@List.nil_cons positive 5%positive nil), (@List.nil_cons N 42%N nil), List.nil_cons) (@None unit) in *) +(* idtac Hs. *) +(* Abort. *) + + +(* Get all the hypotheses and the goal *) + +Ltac get_context b := + match goal with + | H : ?P |- _ => + let _ := match goal with _ => revert H end in + let acc := get_context b in + let _ := match goal with _ => intro H end in + constr:((acc,P)) + | _ => constr:(b) + end. + +Ltac get_context_concl := + match goal with + | |- ?g => get_context g + end. + +(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *) +(* 3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *) +(* 17%positive = 42%positive. *) +(* Proof. *) +(* intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *) +(* let h := get_context_concl in idtac h. *) +(* Abort. *) + + +(* List of interpreted types *) + +Ltac is_interpreted_type T := + lazymatch T with + | BVList.BITVECTOR_LIST.bitvector _ => constr:(true) + | FArray.farray _ _ => constr:(true) + | Z => constr:(true) | nat => constr:(true) | positive => constr:(true) + | bool => constr:(true) + | _ => constr:(false) + end. + + +(* Add CompDec for types over which an equality appears in the goal or + in a local hypothesis *) + +Ltac add_compdecs_term u := + match u with + | context C [@Logic.eq ?t _ _] => + let u' := context C [True] in + lazymatch is_interpreted_type t with + | true => + (* For interpreted types, we need a specific Boolean equality *) + add_compdecs_term u' + | false => + (* For uninterpreted types, we use CompDec *) + match goal with + (* If it is already in the local context, do nothing *) + | _ : SMT_classes.CompDec t |- _ => add_compdecs_term u' + (* Otherwise, add it in the local context *) + | _ => + let p := fresh "p" in + assert (p:SMT_classes.CompDec t); + [ try (exact _) (* Use the typeclass machinery *) + | add_compdecs_term u' ] + end + end + | _ => idtac + end. + +Ltac add_compdecs_terms t := + match t with + | (?t', ?H) => + add_compdecs_term H; + add_compdecs_terms t' + | ?g => add_compdecs_term g + end. + +(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *) +(* 3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *) +(* 17%positive = 42%positive /\ (5,6) = (6,7). *) +(* Proof. *) +(* intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *) +(* let h := get_context_concl in add_compdecs_terms h. *) +(* Show 3. *) +(* Abort. *) + + +Ltac add_compdecs := + let h := get_context_concl in + add_compdecs_terms h. + +(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *) +(* 3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *) +(* 17%positive = 42%positive /\ (5,6) = (6,7). *) +(* Proof. *) +(* intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *) +(* add_compdecs. *) +(* Show 3. *) +(* Abort. *) + + +(* Collect CompDec in local hypotheses *) + +Ltac collect_compdecs := + match goal with + | H : SMT_classes.CompDec ?T |- _ => + let _ := match goal with _ => change (id (SMT_classes.CompDec T)) in H end in + let acc := collect_compdecs in + let _ := match goal with _ => change (SMT_classes.CompDec T) in H end in + let res := + lazymatch is_interpreted_type T with + | true => constr:(acc) + | false => constr:((acc, H)) + end + in + constr:(res) + | _ => constr:(unit) + end. + +(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *) +(* 3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *) +(* 17%positive = 42%positive /\ (5,6) = (6,7). *) +(* Proof. *) +(* intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *) +(* add_compdecs. *) +(* Focus 3. *) +(* let cs := collect_compdecs in idtac cs. *) +(* Abort. *) + + +(* Generate CompDec rels for trakt *) + +Ltac generate_rels compdecs := + lazymatch compdecs with + | (?compdecs', ?HA) => + let ty := type of HA in + lazymatch ty with + | SMT_classes.CompDec ?A => + let rel := constr:((@eq A, @SMT_classes.eqb_of_compdec A HA, @SMT_classes.compdec_eq_eqb A HA)) in + let acc := generate_rels compdecs' in + lazymatch acc with + | None => constr:(Some rel) + | Some ?res => constr:(Some (res, rel)) + end + end + | _ => constr:(@None unit) + end. + +(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *) +(* 3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *) +(* 17%positive = 42%positive /\ (5,6) = (6,7). *) +(* Proof. *) +(* intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *) +(* add_compdecs. *) +(* Focus 3. *) +(* let cs := collect_compdecs in *) +(* let rels := generate_rels cs in *) +(* idtac rels. *) +(* Abort. *) + + +(* Use trakt *) + +Ltac trakt_rels rels := + lazymatch rels with + | Some ?rels' => trakt Z bool with rel rels' + | None => trakt Z bool + end. + +Ltac revert_and_trakt Hs rels := + lazymatch Hs with + | (?Hs, ?H) => + revert H; + revert_and_trakt Hs rels + (* intro H *) + | ?H => + revert H; + trakt_rels rels + (* intro H *) + end. + + +Definition sep := True. + +Ltac get_hyps_upto_sep := + lazymatch goal with + | H' : ?P |- _ => + lazymatch P with + | sep => constr:(@None unit) + | _ => + let T := type of P in + lazymatch T with + | Prop => + let _ := match goal with _ => revert H' end in + let acc := get_hyps_upto_sep in + let _ := match goal with _ => intro H' end in + lazymatch acc with + | Some ?acc' => constr:(Some (acc', H')) + | None => constr:(Some H') + end + | _ => + let _ := match goal with _ => revert H' end in + let acc := get_hyps_upto_sep in + let _ := match goal with _ => intro H' end in + acc + end + end + end. + + +(* Goal False -> 1 = 1 -> unit -> false = true -> True. *) +(* Proof. *) +(* intros H1 H2. *) +(* assert (H : sep) by exact I. *) +(* intros H3 H4. *) +(* let Hs := get_hyps_upto_sep in idtac Hs. *) +(* Abort. *) + + +Ltac intros_names := + let H := fresh in + let _ := match goal with _ => assert (H : sep) by exact I; intros end in + let Hs := get_hyps_upto_sep in + let _ := match goal with _ => clear H end in + Hs. + + +(* Goal False -> 1 = 1 -> unit -> false = true -> True. *) +(* Proof. *) +(* intros H1 H2. *) +(* let Hs := intros_names in idtac Hs. *) +(* Abort. *) + + +Ltac post_trakt Hs := + lazymatch Hs with + | (?Hs1, ?Hs2) => + post_trakt Hs1; + post_trakt Hs2 + | ?H => try (revert H; trakt_reorder_quantifiers; trakt_boolify_arrows; intro H) + end. + +Ltac trakt1 rels Hs := + lazymatch Hs with + | Some ?Hs => revert_and_trakt Hs rels + | None => trakt_rels rels + end. + + +(* Section Test. *) +(* Variables (A:Type) (HA:SMT_classes.CompDec A). *) + +(* Goal forall (a1 a2:A), a1 = a2. *) +(* Proof. *) +(* intros a1 a2. *) +(* trakt Z bool with rel (@eq A, @SMT_classes.eqb_of_compdec A HA, @SMT_classes.compdec_eq_eqb A HA). *) +(* Abort. *) +(* End Test. *) + +(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *) +(* 3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *) +(* 17%positive = 42%positive /\ (5,6) = (6,7). *) +(* Proof. *) +(* intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros H. *) +(* add_compdecs. *) +(* Focus 3. *) +(* (* Set Printing All. *) *) +(* let cs := collect_compdecs in *) +(* let rels := generate_rels cs in *) +(* trakt1 rels (Some H). *) +(* Abort. *) + + +(* Remove quantifications on CompDecs in hypotheses *) + +Ltac remove_compdec_hyp H := + let TH := type of H in + match TH with + | forall p : SMT_classes.CompDec ?A, _ => + match goal with + | [ p' : SMT_classes.CompDec A |- _ ] => + let H1 := fresh in + assert (H1 := H p'); clear H; assert (H := H1); clear H1; + remove_compdec_hyp H + | _ => + let c := fresh "c" in + assert (c : SMT_classes.CompDec A); + [ try (exact _) + | let H1 := fresh in + assert (H1 := H c); clear H; assert (H := H1); clear H1; + remove_compdec_hyp H ] + end + | _ => idtac + end. + +Ltac remove_compdec_hyps Hs := + lazymatch Hs with + | (?Hs1, ?Hs2) => + remove_compdec_hyps Hs1; + remove_compdec_hyps Hs2 + | ?H => remove_compdec_hyp H + end. + +Ltac remove_compdec_hyps_option Hs := + lazymatch Hs with + | Some ?Hs => remove_compdec_hyps Hs + | None => idtac + end. + + +(* Perform all the preprocessing *) + +Ltac preprocess1 Hs := + add_compdecs; + [ .. | + remove_compdec_hyps_option Hs; + let cpds := collect_compdecs in + let rels := generate_rels cpds in + trakt1 rels Hs]. + + +(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *) +(* 3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *) +(* 17%positive = 42%positive /\ (5,6) = (6,7) (* /\ 0%N = 0%N *). *) +(* Proof. *) +(* intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *) +(* assert (H1 := @List.nil_cons positive 5%positive nil). *) +(* preprocess1 (Some (H1, H)). *) +(* Show 3. *) +(* Abort. *) + +Ltac preprocess2 Hs' := + lazymatch Hs' with + | Some ?Hs' => post_trakt Hs' + | None => idtac + end. diff --git a/src/preproc/Database_trakt.v b/src/preproc/Database_trakt.v new file mode 100644 index 0000000..8f3ac34 --- /dev/null +++ b/src/preproc/Database_trakt.v @@ -0,0 +1,224 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2021 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +From Trakt Require Import Trakt. + + +(* Boolean equality *) + +Lemma eqbool_Booleqb_embedding: forall n m : bool, n = m <-> (Bool.eqb n m) = true. +Proof. intros n m. now rewrite Bool.eqb_true_iff. Qed. +Trakt Add Relation (@eq bool) (Bool.eqb) (eqbool_Booleqb_embedding). + + +(* Boolean relations for Z *) + +From Coq Require Import ZArith. + + +Lemma eqZ_Zeqb_embedding: forall n m : Z, n = m <-> (Z.eqb n m) = true. +Proof. intros n m. now rewrite Z.eqb_eq. Qed. +Trakt Add Relation (@eq Z) (Z.eqb) (eqZ_Zeqb_embedding). + +Lemma ltZ_Zltb_embedding: forall n m : Z, (n < m)%Z <-> (Z.ltb n m) = true. +Proof. intros n m. now rewrite Z.ltb_lt. Qed. +Trakt Add Relation (@Z.lt) (Z.ltb) (ltZ_Zltb_embedding). + +Lemma leZ_Zleb_embedding: forall n m : Z, (n <= m)%Z <-> (Z.leb n m) = true. +Proof. intros n m. now rewrite Z.leb_le. Qed. +Trakt Add Relation (@Z.le) (Z.leb) (leZ_Zleb_embedding). + +Lemma gtZ_Zgtb_embedding: forall n m : Z, (n > m)%Z <-> (Z.gtb n m) = true. +Proof. intros n m. rewrite Z.gtb_lt. now apply Z.gt_lt_iff. Qed. +Trakt Add Relation (@Z.gt) (Z.gtb) (gtZ_Zgtb_embedding). + +Lemma geZ_Zgeb_embedding: forall n m : Z, (n >= m)%Z <-> (Z.geb n m) = true. +Proof. intros n m. rewrite Z.geb_le. now apply Z.ge_le_iff. Qed. +Trakt Add Relation (@Z.ge) (Z.geb) (geZ_Zgeb_embedding). + +Goal forall (x y : Z), ((x < y)%Z \/ x = y \/ (x > y)%Z) /\ ((x <= y)%Z \/ (x >= y)%Z). +Proof. + trakt Z bool. +Abort. + + +(* Embedding for nat *) + +Section Relations_nat. + + (* Embedding *) + Lemma nat_Z_FBInverseProof : forall (n : nat), n = Z.to_nat (Z.of_nat n). + Proof. intro n; symmetry; apply Nat2Z.id. Qed. + + Lemma nat_Z_BFPartialInverseProof_bool : forall (z : Z), (0 <=? z)%Z = true -> + Z.of_nat (Z.to_nat z) = z. + Proof. intros Z H; apply Z2Nat.id; apply Zle_is_le_bool; assumption. Qed. + + Lemma nat_Z_ConditionProof_bool : forall (n : nat), (0 <=? Z.of_nat n)%Z = true. + Proof. intros n. rewrite <- Zle_is_le_bool. apply Zle_0_nat. Qed. + + (* Addition *) + Lemma Natadd_Zadd_embedding_equality : forall (n m : nat), + Z.of_nat (n + m)%nat = ((Z.of_nat n) + (Z.of_nat m))%Z. + Proof. apply Nat2Z.inj_add. Qed. + + Lemma Natsub_Zsub_embedding_equality : forall (n m : nat), + Z.of_nat (n - m)%nat = (if Z.leb (Z.of_nat n) (Z.of_nat m) then 0%Z else (Z.of_nat n) - (Z.of_nat m))%Z. + Proof. intros n m. destruct (Z.of_nat n <=? Z.of_nat m)%Z eqn:E. + - apply Zle_is_le_bool in E. apply Nat2Z.inj_le in E. rewrite <- Nat.sub_0_le in E. + rewrite E. reflexivity. + - apply Nat2Z.inj_sub. rewrite Z.leb_nle in E. apply Znot_le_gt in E. apply + Z.gt_lt in E. apply Z.lt_le_incl in E. rewrite Nat2Z.inj_le. assumption. Qed. + + (* Multiplication *) + Lemma Natmul_Zmul_embedding_equality : forall (n m : nat), + Z.of_nat (n * m)%nat = ((Z.of_nat n) * (Z.of_nat m))%Z. + Proof. apply Nat2Z.inj_mul. Qed. + + (* Successor *) + Lemma S_Zadd1_embedding_equality : forall (n : nat), Z.of_nat (S n) = Z.add 1%Z (Z.of_nat n). + Proof. intros n. + rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. reflexivity. Qed. + + (* Zero *) + Lemma zero_nat_Z_embedding_equality : Z.of_nat O = 0%Z. + Proof. reflexivity. Qed. + + (* Equality *) + Lemma eq_Zeqb_embedding : forall (n m : nat), + n = m <-> (Z.eqb (Z.of_nat n) (Z.of_nat m)) = true. + Proof. intros ; split. + - intros H. apply inj_eq in H. rewrite <- Z.eqb_eq in H. assumption. + - intros H. rewrite Z.eqb_eq in H. rewrite <- Nat2Z.inj_iff. + assumption. Qed. + + Lemma Nateqb_Zeqb_embedding_equality : forall (n m : nat), + Nat.eqb n m = (Z.eqb (Z.of_nat n) (Z.of_nat m)). + Proof. + intros n m. destruct (n =? m) eqn:E. + rewrite Nat.eqb_eq in E. rewrite eq_Zeqb_embedding in E. symmetry. assumption. + apply beq_nat_false in E. rewrite eq_Zeqb_embedding in E. destruct (Z.of_nat n =? Z.of_nat m)%Z. + now elim E. reflexivity. Qed. + + (* Less or equal *) + Lemma le_Zleb_embedding : forall (n m : nat), + n <= m <-> (Z.leb (Z.of_nat n) (Z.of_nat m)) = true. + Proof. intros n m. split. + - intros H. apply Zle_imp_le_bool. + apply Nat2Z.inj_le. assumption. + - intros H. apply Zle_is_le_bool in H. apply Nat2Z.inj_le in H. assumption. Qed. + + Lemma Natleb_Zleb_embedding_equality : forall (n m : nat), + n <=? m = (Z.leb (Z.of_nat n) (Z.of_nat m)). + Proof. + intros n m. + destruct (n <=? m) eqn:E. + - symmetry. apply leb_complete in E. apply Nat2Z.inj_le in E. +apply Zle_is_le_bool. assumption. + - apply leb_iff_conv in E. symmetry. apply Z.leb_gt. apply inj_lt in E. assumption. + Qed. + + (* Less than *) + Lemma lt_Zltb_embedding : forall (n m : nat), + n < m <-> (Z.ltb (Z.of_nat n) (Z.of_nat m)) = true. + Proof. intros n m. rewrite Nat2Z.inj_lt. apply Zlt_is_lt_bool. Qed. + + + Lemma Natltb_Zltb_embedding_equality : forall (n m : nat), + n = m <-> (Z.geb (Z.of_nat n) (Z.of_nat m)) = true. + Proof. intros n m. split. + - intro H. apply geZ_Zgeb_embedding. apply Nat2Z.inj_ge. assumption. + - intro H. apply geZ_Zgeb_embedding in H. apply Nat2Z.inj_ge. assumption. + Qed. + + (* Greater than *) + Lemma gt_Zgtb_embedding : forall (n m : nat), + n > m <-> (Z.gtb (Z.of_nat n) (Z.of_nat m)) = true. + Proof. intros n m. split. + - intro H. apply Zgt_is_gt_bool. apply Nat2Z.inj_gt. assumption. + - intro H. apply Zgt_is_gt_bool in H. apply Nat2Z.inj_gt. assumption. + Qed. + +End Relations_nat. + +Trakt Add Embedding + (nat) (Z) (Z.of_nat) (Z.to_nat) (nat_Z_FBInverseProof) (nat_Z_BFPartialInverseProof_bool) + (nat_Z_ConditionProof_bool). + +Trakt Add Symbol (Init.Nat.add) (Z.add) (Natadd_Zadd_embedding_equality). +Trakt Add Symbol (Init.Nat.mul) (Z.mul) (Natmul_Zmul_embedding_equality). +Trakt Add Symbol (S) (Z.add 1%Z) (S_Zadd1_embedding_equality). +Trakt Add Symbol (O) (0%Z) (zero_nat_Z_embedding_equality). +Trakt Add Symbol (Nat.eqb) (Z.eqb) (Nateqb_Zeqb_embedding_equality). +Trakt Add Symbol (Nat.leb) (Z.leb) (Natleb_Zleb_embedding_equality). +Trakt Add Symbol (Nat.ltb) (Z.ltb) (Natltb_Zltb_embedding_equality). + +Trakt Add Relation (@eq nat) (Z.eqb) (eq_Zeqb_embedding). +Trakt Add Relation (le) (Z.leb) (le_Zleb_embedding). +Trakt Add Relation (lt) (Z.ltb) (lt_Zltb_embedding). +Trakt Add Relation (ge) (Z.geb) (ge_Zgeb_embedding). +Trakt Add Relation (gt) (Z.gtb) (gt_Zgtb_embedding). + +(* Goal 3%nat = 3%nat. *) +(* Proof. trakt Z bool. Abort. *) + +(* Goal Nat.eqb 3%nat 3%nat = true. *) +(* Proof. trakt Z bool. Abort. *) + +(* Goal (3+4)%nat = 7%nat. *) +(* Proof. trakt Z bool. Abort. *) + +(* Goal forall (x y:nat), x <= x + y. *) +(* Proof. trakt Z bool. Abort. *) + + +(* Embedding for N (to be completed) *) + +Section Relations_N. + + Lemma N_Z_FBInverseProof : forall (n : N), n = Z.to_N (Z.of_N n). + Proof. intros n ; symmetry ; apply N2Z.id. Qed. + + Lemma N_Z_BFPartialInverseProof_bool : forall (z : Z), (0 <=? z)%Z = true -> + Z.of_N (Z.to_N z) = z. + Proof. intros z H. induction z. + - reflexivity. + - reflexivity. + - assert (H1 : forall p : positive, (Z.neg p < 0)%Z) by apply Pos2Z.neg_is_neg. + specialize (H1 p). apply Zle_bool_imp_le in H. apply Zle_not_lt in H. + unfold not in H1. apply H in H1. elim H1. Qed. + + Lemma N_Z_ConditionProof_bool : forall (n : N), (0 <=? Z.of_N n)%Z = true. + Proof. intros n. apply Zle_imp_le_bool. apply N2Z.is_nonneg. Qed. + +End Relations_N. + +Trakt Add Embedding + (N) (Z) (Z.of_N) (Z.to_N) (N_Z_FBInverseProof) (N_Z_BFPartialInverseProof_bool) + (N_Z_ConditionProof_bool). + + +(* This is about Z, but it fails if we put it upper in the file...?? *) + +(* Lemma Zneg_Zopp_embedding_equality : forall (x : positive), Zneg x = Z.opp (Zpos x). +Admitted. +Trakt Add Symbol (Zneg) (Z.opp) (Zneg_Zopp_embedding_equality). *) -- cgit