diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-01 13:33:41 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-01 13:33:41 +0100 |
| commit | 8ab748064ddeec8400859e210bf9963826cba631 (patch) | |
| tree | 25eef87f75dbac861d99c781a653b5595c6755ff | |
| parent | 9e28c50232e56e35437afb468c6d273abcf5eab5 (diff) | |
Imported Upstream version 0.2.1upstream/0.2.1
| -rw-r--r-- | AAC.v | 478 | ||||
| -rw-r--r-- | AAC_coq.ml | 374 | ||||
| -rw-r--r-- | AAC_coq.mli | 42 | ||||
| -rw-r--r-- | AAC_helper.ml | 16 | ||||
| -rw-r--r-- | AAC_matcher.ml | 720 | ||||
| -rw-r--r-- | AAC_matcher.mli | 34 | ||||
| -rw-r--r-- | AAC_print.ml | 72 | ||||
| -rw-r--r-- | AAC_print.mli | 4 | ||||
| -rw-r--r-- | AAC_rewrite.ml | 315 | ||||
| -rw-r--r-- | AAC_search_monad.ml | 28 | ||||
| -rw-r--r-- | AAC_search_monad.mli | 2 | ||||
| -rw-r--r-- | AAC_theory.ml | 742 | ||||
| -rw-r--r-- | AAC_theory.mli | 60 | ||||
| -rw-r--r-- | Caveats.v | 64 | ||||
| -rw-r--r-- | Instances.v | 78 | ||||
| -rw-r--r-- | Tutorial.v | 126 |
16 files changed, 1577 insertions, 1578 deletions
@@ -16,17 +16,17 @@ equality of reified terms: first normalise reified terms, then compare them. This allows us to close transitivity steps automatically, in the [aac_rewrite] tactic. - + We restrict ourselves to the case where all symbols operate on a single fixed type. In particular, this means that we cannot handle - situations like + situations like [H: forall x y, nat_of_pos (pos_of_nat (x) + y) + x = ....] where one occurrence of [+] operates on nat while the other one operates on positive. *) -Require Import Arith NArith. +Require Import Arith NArith. Require Import List. Require Import FMapPositive FMapFacts. Require Import RelationClasses Equality. @@ -41,7 +41,7 @@ Local Open Scope signature_scope. Section sigma. Definition sigma := PositiveMap.t. Definition sigma_get A (null : A) (map : sigma A) (n : positive) : A := - match PositiveMap.find n map with + match PositiveMap.find n map with | None => null | Some x => x end. @@ -52,9 +52,9 @@ End sigma. (** * Classes for properties of operators *) -Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) := +Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) := law_assoc : forall x y z, R (dot x (dot y z)) (dot (dot x y) z). -Class Commutative (X:Type) (R: relation X) (plus: X -> X -> X) := +Class Commutative (X:Type) (R: relation X) (plus: X -> X -> X) := law_comm: forall x y, R (plus x y) (plus y x). Class Unit (X:Type) (R:relation X) (op : X -> X -> X) (unit:X) := { law_neutral_left: forall x, R (op unit x) x; @@ -72,16 +72,16 @@ Class AAC_lift X (R: relation X) (E : relation X) := { (** simple instances, when we have a subrelation, or an equivalence *) -Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E} +Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E} {HR: @Transitive X R} {HER: subrelation E R}: AAC_lift R E | 3. -Proof. +Proof. constructor; trivial. - intros ? ? H ? ? H'. split; intro G. - rewrite <- H, G. apply HER, H'. - rewrite H, G. apply HER. symmetry. apply H'. + intros ? ? H ? ? H'. split; intro G. + rewrite <- H, G. apply HER, H'. + rewrite H, G. apply HER. symmetry. apply H'. Qed. -Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E} +Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E} {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4. @@ -92,35 +92,35 @@ Module Internal. Section copy. - Context {X} {R} {HR: @Equivalence X R} {plus} + Context {X} {R} {HR: @Equivalence X R} {plus} (op: Associative R plus) (op': Commutative R plus) (po: Proper (R ==> R ==> R) plus). (* copy n x = x+...+x (n times) *) - Fixpoint copy' n x := match n with + Fixpoint copy' n x := match n with | xH => x | xI n => let xn := copy' n x in plus (plus xn xn) x - | xO n => let xn := copy' n x in (plus xn xn) + | xO n => let xn := copy' n x in (plus xn xn) end. Definition copy n x := Prect (fun _ => X) x (fun _ xn => plus x xn) n. - + Lemma copy_plus : forall n m x, R (copy (n+m) x) (plus (copy n x) (copy m x)). Proof. unfold copy. induction n using Pind; intros m x. - rewrite Prect_base. rewrite <- Pplus_one_succ_l. rewrite Prect_succ. reflexivity. - rewrite Pplus_succ_permute_l. rewrite 2Prect_succ. rewrite IHn. apply op. + rewrite Prect_base. rewrite <- Pplus_one_succ_l. rewrite Prect_succ. reflexivity. + rewrite Pplus_succ_permute_l. rewrite 2Prect_succ. rewrite IHn. apply op. Qed. - Lemma copy_xH : forall x, R (copy 1 x) x. + Lemma copy_xH : forall x, R (copy 1 x) x. Proof. intros; unfold copy; rewrite Prect_base. reflexivity. Qed. - Lemma copy_Psucc : forall n x, R (copy (Psucc n) x) (plus x (copy n x)). + Lemma copy_Psucc : forall n x, R (copy (Psucc n) x) (plus x (copy n x)). Proof. intros; unfold copy; rewrite Prect_succ. reflexivity. Qed. Global Instance copy_compat n: Proper (R ==> R) (copy n). Proof. unfold copy. induction n using Pind; intros x y H. - rewrite 2Prect_base. assumption. - rewrite 2Prect_succ. apply po; auto. + rewrite 2Prect_base. assumption. + rewrite 2Prect_succ. apply po; auto. Qed. End copy. @@ -133,7 +133,7 @@ End copy. Local Notation idx := positive. Fixpoint eq_idx_bool i j := - match i,j with + match i,j with | xH, xH => true | xO i, xO j => eq_idx_bool i j | xI i, xI j => eq_idx_bool i j @@ -141,7 +141,7 @@ Fixpoint eq_idx_bool i j := end. Fixpoint idx_compare i j := - match i,j with + match i,j with | xH, xH => Eq | xH, _ => Lt | _, xH => Gt @@ -163,7 +163,7 @@ Proof. induction i; destruct j; simpl; try (constructor; congruence). case (IHi j); constructor; congruence. case (IHi j); constructor; congruence. -Qed. +Qed. (** weak specification predicate for comparison functions: only the 'Eq' case is specified *) Inductive compare_weak_spec A: A -> A -> comparison -> Prop := @@ -185,20 +185,20 @@ Section dep. Variable U: Type. Variable T: U -> Type. - Lemma cast_eq: (forall u v: U, {u=v}+{u<>v}) -> + Lemma cast_eq: (forall u v: U, {u=v}+{u<>v}) -> forall A (H: A=A) (u: T A), cast T H u = u. - Proof. intros. rewrite <- Eqdep_dec.eq_rect_eq_dec; trivial. Qed. + Proof. intros. rewrite <- Eqdep_dec.eq_rect_eq_dec; trivial. Qed. Variable f: forall A B, T A -> T B -> comparison. Definition reflect_eqdep := forall A u B v (H: A=B), @f A B u v = Eq -> cast T H u = v. (* these lemmas have to remain transparent to get structural recursion in the lemma [tcompare_weak_spec] below *) - Lemma reflect_eqdep_eq: reflect_eqdep -> + Lemma reflect_eqdep_eq: reflect_eqdep -> forall A u v, @f A A u v = Eq -> u = v. - Proof. intros H A u v He. apply (H _ _ _ _ eq_refl He). Defined. + Proof. intros H A u v He. apply (H _ _ _ _ eq_refl He). Defined. - Lemma reflect_eqdep_weak_spec: reflect_eqdep -> + Lemma reflect_eqdep_weak_spec: reflect_eqdep -> forall A u v, compare_weak_spec u v (@f A A u v). Proof. intros. case_eq (f u v); try constructor. @@ -210,20 +210,20 @@ End dep. (** * Utilities about (non-empty) lists and multisets *) -Inductive nelist (A : Type) : Type := +Inductive nelist (A : Type) : Type := | nil : A -> nelist A | cons : A -> nelist A -> nelist A. Local Notation "x :: y" := (cons x y). -Fixpoint nelist_map (A B: Type) (f: A -> B) l := - match l with +Fixpoint nelist_map (A B: Type) (f: A -> B) l := + match l with | nil x => nil ( f x) | cons x l => cons ( f x) (nelist_map f l) end. -Fixpoint appne A l l' : nelist A := - match l with +Fixpoint appne A l l' : nelist A := + match l with nil x => cons x l' | cons t q => cons t (appne A q l') end. @@ -234,7 +234,7 @@ Local Notation "x ++ y" := (appne x y). Definition mset A := nelist (A*positive). (** lexicographic composition of comparisons (this is a notation to keep it lazy) *) -Local Notation lex e f := (match e with Eq => f | _ => e end). +Local Notation lex e f := (match e with Eq => f | _ => e end). Section lists. @@ -244,27 +244,27 @@ Section lists. Section c. Variables A B: Type. Variable compare: A -> B -> comparison. - Fixpoint list_compare h k := + Fixpoint list_compare h k := match h,k with | nil x, nil y => compare x y | nil x, _ => Lt | _, nil x => Gt | u::h, v::k => lex (compare u v) (list_compare h k) - end. + end. End c. Definition mset_compare A B compare: mset A -> mset B -> comparison := - list_compare (fun un vm => - let '(u,n) := un in - let '(v,m) := vm in + list_compare (fun un vm => + let '(u,n) := un in + let '(v,m) := vm in lex (compare u v) (pos_compare n m)). Section list_compare_weak_spec. Variable A: Type. Variable compare: A -> A -> comparison. Hypothesis Hcompare: forall u v, compare_weak_spec u v (compare u v). - (* this lemma has to remain transparent to get structural recursion + (* this lemma has to remain transparent to get structural recursion in the lemma [tcompare_weak_spec] below *) - Lemma list_compare_weak_spec: forall h k, + Lemma list_compare_weak_spec: forall h k, compare_weak_spec h k (list_compare compare h k). Proof. induction h as [|u h IHh]; destruct k as [|v k]; simpl; try constructor. @@ -279,9 +279,9 @@ Section lists. Variable A: Type. Variable compare: A -> A -> comparison. Hypothesis Hcompare: forall u v, compare_weak_spec u v (compare u v). - (* this lemma has to remain transparent to get structural recursion + (* this lemma has to remain transparent to get structural recursion in the lemma [tcompare_weak_spec] below *) - Lemma mset_compare_weak_spec: forall h k, + Lemma mset_compare_weak_spec: forall h k, compare_weak_spec h k (mset_compare compare h k). Proof. apply list_compare_weak_spec. @@ -296,10 +296,10 @@ Section lists. Section m. Variable A: Type. Variable compare: A -> A -> comparison. - Definition insert n1 h1 := + Definition insert n1 h1 := let fix insert_aux l2 := match l2 with - | nil (h2,n2) => + | nil (h2,n2) => match compare h1 h2 with | Eq => nil (h1,Pplus n1 n2) | Lt => (h1,n1):: nil (h2,n2) @@ -313,14 +313,14 @@ Section lists. end end in insert_aux. - + Fixpoint merge_msets l1 := match l1 with | nil (h1,n1) => fun l2 => insert n1 h1 l2 | (h1,n1)::t1 => let fix merge_aux l2 := match l2 with - | nil (h2,n2) => + | nil (h2,n2) => match compare h1 h2 with | Eq => (h1,Pplus n1 n2) :: t1 | Lt => (h1,n1):: merge_msets t1 l2 @@ -359,7 +359,7 @@ Section lists. Variable ret : A -> B. Variable bind : A -> B -> B. Fixpoint fold_map' (l : nelist A) : B := - match l with + match l with | nil x => ret x | u::l => bind u (fold_map' l) end. @@ -374,7 +374,7 @@ End lists. Module Sym. Section t. Context {X} {R : relation X} . - + (** type of an arity *) Fixpoint type_of (n: nat) := match n with @@ -383,14 +383,14 @@ Module Sym. end. (** relation to be preserved at an arity *) - Fixpoint rel_of n : relation (type_of n) := + Fixpoint rel_of n : relation (type_of n) := match n with | O => R | S n => respectful R (rel_of n) end. - - (** a symbol package contains an arity, - a value of the corresponding type, + + (** a symbol package contains an arity, + a value of the corresponding type, and a proof that the value is a proper morphism *) Record pack : Type := mkPack { ar : nat; @@ -400,11 +400,11 @@ Module Sym. (** helper to build default values, when filling reification environments *) Definition null: pack := mkPack 1 (fun x => x) (fun _ _ H => H). - + End t. End Sym. - + (** ** binary operations *) Module Bin. @@ -431,11 +431,11 @@ Section s. (* We use environments to store the various operators and the morphisms.*) - - Variable e_sym: idx -> @Sym.pack X R. + + Variable e_sym: idx -> @Sym.pack X R. Variable e_bin: idx -> @Bin.pack X R. - + (** packaging units (depends on e_bin) *) Record unit_of u := mk_unit_for { @@ -445,10 +445,10 @@ Section s. Record unit_pack := mk_unit_pack { u_value:> X; - u_desc: list (unit_of u_value) + u_desc: list (unit_of u_value) }. Variable e_unit: positive -> unit_pack. - + Hint Resolve e_bin e_unit: typeclass_instances. (** ** Almost normalised syntax @@ -457,14 +457,14 @@ Section s. - products do not contain products - there are no unary sums or products - lists and msets are lexicographically sorted according to the order we define below - - [vT n] denotes the set of term vectors of size [n] (the mutual dependency could be removed), + + [vT n] denotes the set of term vectors of size [n] (the mutual dependency could be removed), Note that [T] and [vT] depend on the [e_sym] environment (which contains, among other things, the arity of symbols) *) - Inductive T: Type := + Inductive T: Type := | sum: idx -> mset T -> T | prd: idx -> nelist T -> T | sym: forall i, vT (Sym.ar (e_sym i)) -> T @@ -476,7 +476,7 @@ Section s. (** lexicographic rpo over the normalised syntax *) Fixpoint compare (u v: T) := - match u,v with + match u,v with | sum i l, sum j vs => lex (idx_compare i j) (mset_compare compare l vs) | prd i l, prd j vs => lex (idx_compare i j) (list_compare compare l vs) | sym i l, sym j vs => lex (idx_compare i j) (vcompare l vs) @@ -496,13 +496,13 @@ Section s. | _, vnil => Gt | vcons _ u us, vcons _ v vs => lex (compare u v) (vcompare us vs) end. - + (** ** Evaluation from syntax to the abstract domain *) Fixpoint eval u: X := - match u with + match u with | sum i l => let o := Bin.value (e_bin i) in fold_map (fun un => let '(u,n):=un in @copy _ o n (eval u)) o l | prd i l => fold_map eval (Bin.value (e_bin i)) l @@ -537,11 +537,11 @@ Section s. apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst. constructor. induction us; destruct vs; simpl; intros H Huv; try discriminate. - apply cast_eq, eq_nat_dec. + apply cast_eq, eq_nat_dec. injection H; intro Hn. - revert Huv; case (tcompare_weak_spec t t0); intros; try discriminate. + revert Huv; case (tcompare_weak_spec t t0); intros; try discriminate. symmetry in Hn. subst. (* symmetry required *) - rewrite <- (IHus _ _ eq_refl Huv). + rewrite <- (IHus _ _ eq_refl Huv). apply cast_eq, eq_nat_dec. Qed. @@ -549,37 +549,37 @@ Section s. Proof. induction l; simpl; repeat intro. assumption. - apply IHl, H. reflexivity. + apply IHl, H. reflexivity. Qed. - + (* is [i] a unit for [j] ? *) - Definition is_unit_of j i := + Definition is_unit_of j i := List.existsb (fun p => eq_idx_bool j (uf_idx p)) (u_desc (e_unit i)). (* is [i] commutative ? *) - Definition is_commutative i := + Definition is_commutative i := match Bin.comm (e_bin i) with Some _ => true | None => false end. (** ** Normalisation *) Inductive discr {A} : Type := - | Is_op : A -> discr - | Is_unit : idx -> discr + | Is_op : A -> discr + | Is_unit : idx -> discr | Is_nothing : discr . - + (* This is called sum in the std lib *) - Inductive m {A} {B} := + Inductive m {A} {B} := | left : A -> m | right : B -> m. Definition comp A B (merge : B -> B -> B) (l : B) (l' : @m A B) : @m A B := - match l' with + match l' with | left _ => right l | right l' => right (merge l l') end. - + (** auxiliary functions, to clean up sums *) Section sums. @@ -587,33 +587,33 @@ Section s. Variable is_unit : idx -> bool. Definition sum' (u: mset T): T := - match u with + match u with | nil (u,xH) => u | _ => sum i u end. Definition is_sum (u: T) : @discr (mset T) := - match u with + match u with | sum j l => if eq_idx_bool j i then Is_op l else Is_nothing - | unit j => if is_unit j then Is_unit j else Is_nothing + | unit j => if is_unit j then Is_unit j else Is_nothing | u => Is_nothing end. Definition copy_mset n (l: mset T): mset T := - match n with + match n with | xH => l | _ => nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l end. - + Definition return_sum u n := - match is_sum u with + match is_sum u with | Is_nothing => right (nil (u,n)) - | Is_op l' => right (copy_mset n l') + | Is_op l' => right (copy_mset n l') | Is_unit j => left j end. - - Definition add_to_sum u n (l : @m idx (mset T)) := - match is_sum u with + + Definition add_to_sum u n (l : @m idx (mset T)) := + match is_sum u with | Is_nothing => comp (merge_msets compare) (nil (u,n)) l | Is_op l' => comp (merge_msets compare) (copy_mset n l') l | Is_unit _ => l @@ -621,13 +621,13 @@ Section s. Definition norm_msets_ norm (l: mset T) := - fold_map' + fold_map' (fun un => let '(u,n) := un in return_sum (norm u) n) (fun un l => let '(u,n) := un in add_to_sum (norm u) n l) l. End sums. - + (** similar functions for products *) Section prds. @@ -635,35 +635,35 @@ Section s. Variable i : idx. Variable is_unit : idx -> bool. Definition prd' (u: nelist T): T := - match u with + match u with | nil u => u | _ => prd i u end. Definition is_prd (u: T) : @discr (nelist T) := - match u with + match u with | prd j l => if eq_idx_bool j i then Is_op l else Is_nothing - | unit j => if is_unit j then Is_unit j else Is_nothing + | unit j => if is_unit j then Is_unit j else Is_nothing | u => Is_nothing end. - - + + Definition return_prd u := - match is_prd u with + match is_prd u with | Is_nothing => right (nil (u)) - | Is_op l' => right (l') + | Is_op l' => right (l') | Is_unit j => left j end. - - Definition add_to_prd u (l : @m idx (nelist T)) := - match is_prd u with + + Definition add_to_prd u (l : @m idx (nelist T)) := + match is_prd u with | Is_nothing => comp (@appne T) (nil (u)) l | Is_op l' => comp (@appne T) (l') l | Is_unit _ => l end. Definition norm_lists_ norm (l : nelist T) := - fold_map' + fold_map' (fun u => return_prd (norm u)) (fun u l => add_to_prd (norm u) l) l. @@ -671,32 +671,32 @@ Section s. End prds. - Definition run_list x := match x with + Definition run_list x := match x with | left n => nil (unit n) | right l => l end. - + Definition norm_lists norm i l := let is_unit := is_unit_of i in run_list (norm_lists_ i is_unit norm l). - Definition run_msets x := match x with + Definition run_msets x := match x with | left n => nil (unit n, xH) | right l => l end. - + Definition norm_msets norm i l := let is_unit := is_unit_of i in - run_msets (norm_msets_ i is_unit norm l). - + run_msets (norm_msets_ i is_unit norm l). + Fixpoint norm u {struct u}:= - match u with + match u with | sum i l => if is_commutative i then sum' i (norm_msets norm i l) else u - | prd i l => prd' i (norm_lists norm i l) + | prd i l => prd' i (norm_lists norm i l) | sym i l => sym i (vnorm l) | unit i => unit i end - with vnorm i (l: vT i): vT i := + with vnorm i (l: vT i): vT i := match l with | vnil => vnil | vcons _ u l => vcons (norm u) (vnorm l) @@ -713,7 +713,7 @@ Section s. revert H' ; case (eq_idx_spec); [intros H' _ ; subst| intros _ H'; discriminate]. simpl. destruct x. simpl. auto. Qed. - + Instance Binvalue_Commutative i (H : is_commutative i = true) : Commutative R (@Bin.value _ _ (e_bin i) ). Proof. unfold is_commutative in H. @@ -725,7 +725,7 @@ Section s. Proof. destruct ((e_bin i)); auto. Qed. - + Instance Binvalue_Proper i : Proper (R ==> R ==> R) (@Bin.value _ _ (e_bin i) ). Proof. destruct ((e_bin i)); auto. @@ -744,43 +744,43 @@ Section s. | is_sum_spec_op : forall j l, j = i -> is_sum_spec_ind (sum j l) (Is_op l) | is_sum_spec_unit : forall j, is_unit j = true -> is_sum_spec_ind (unit j) (Is_unit j) | is_sum_spec_nothing : forall u, is_sum_spec_ind u (Is_nothing). - + Lemma is_sum_spec u : is_sum_spec_ind u (is_sum i is_unit u). Proof. unfold is_sum; case u; intros; try constructor. - case_eq (eq_idx_bool p i); intros; subst; try constructor; auto. + case_eq (eq_idx_bool p i); intros; subst; try constructor; auto. revert H. case eq_idx_spec; try discriminate. auto. case_eq (is_unit p); intros; try constructor. auto. Qed. Instance assoc : @Associative X R (Bin.value (e_bin i)). - Proof. + Proof. destruct (e_bin i). simpl. assumption. Qed. Instance proper : Proper (R ==> R ==> R)(Bin.value (e_bin i)). - Proof. + Proof. destruct (e_bin i). simpl. assumption. Qed. Hypothesis comm : @Commutative X R (Bin.value (e_bin i)). Lemma sum'_sum : forall (l: mset T), eval (sum' i l) ==eval (sum i l) . - Proof. - intros [[a n] | [a n] l]; destruct n; simpl; reflexivity. + Proof. + intros [[a n] | [a n] l]; destruct n; simpl; reflexivity. Qed. - Lemma eval_sum_nil x: + Lemma eval_sum_nil x: eval (sum i (nil (x,xH))) == (eval x). - Proof. rewrite <- sum'_sum. reflexivity. Qed. - + Proof. rewrite <- sum'_sum. reflexivity. Qed. + Lemma eval_sum_cons : forall n a (l: mset T), (eval (sum i ((a,n)::l))) == (@Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval a)) (eval (sum i l))). Proof. intros n a [[? ? ]|[b m] l]; simpl; reflexivity. Qed. - - Inductive compat_sum_unit : @m idx (mset T) -> Prop := - | csu_left : forall x, is_unit x = true-> compat_sum_unit (left x) - | csu_right : forall m, compat_sum_unit (right m) + + Inductive compat_sum_unit : @m idx (mset T) -> Prop := + | csu_left : forall x, is_unit x = true-> compat_sum_unit (left x) + | csu_right : forall m, compat_sum_unit (right m) . Lemma compat_sum_unit_return x n : compat_sum_unit (return_sum i is_unit x n). @@ -788,159 +788,159 @@ Section s. unfold return_sum. case is_sum_spec; intros; try constructor; auto. Qed. - - Lemma compat_sum_unit_add : forall x n h, + + Lemma compat_sum_unit_add : forall x n h, compat_sum_unit h -> - compat_sum_unit + compat_sum_unit (add_to_sum i (is_unit_of i) x n h). Proof. unfold add_to_sum;intros; inversion H; case_eq (is_sum i (is_unit_of i) x); - intros; simpl; try constructor || eauto. apply H0. + intros; simpl; try constructor || eauto. apply H0. Qed. (* Hint Resolve copy_plus. : this lags because of the inference of the implicit arguments *) Hint Extern 5 (copy (?n + ?m) (eval ?a) == Bin.value (copy ?n (eval ?a)) (copy ?m (eval ?a))) => apply copy_plus. - Hint Extern 5 (?x == ?x) => reflexivity. - Hint Extern 5 ( Bin.value ?x ?y == Bin.value ?y ?x) => apply Bin.comm. - + Hint Extern 5 (?x == ?x) => reflexivity. + Hint Extern 5 ( Bin.value ?x ?y == Bin.value ?y ?x) => apply Bin.comm. + Lemma eval_merge_bin : forall (h k: mset T), eval (sum i (merge_msets compare h k)) == @Bin.value _ _ (e_bin i) (eval (sum i h)) (eval (sum i k)). Proof. - induction h as [[a n]|[a n] h IHh]; intro k. - simpl. - induction k as [[b m]|[b m] k IHk]; simpl. - destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. apply copy_plus; auto. - + induction h as [[a n]|[a n] h IHh]; intro k. + simpl. + induction k as [[b m]|[b m] k IHk]; simpl. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. apply copy_plus; auto. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. - rewrite copy_plus,law_assoc; auto. + rewrite copy_plus,law_assoc; auto. rewrite IHk; clear IHk. rewrite 2 law_assoc. apply proper. apply law_comm. reflexivity. - - induction k as [[b m]|[b m] k IHk]; simpl; simpl in IHh. + + induction k as [[b m]|[b m] k IHk]; simpl; simpl in IHh. destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. - rewrite (law_comm _ (copy m (eval a))), law_assoc, <- copy_plus, Pplus_comm; auto. - rewrite <- law_assoc, IHh. reflexivity. + rewrite (law_comm _ (copy m (eval a))), law_assoc, <- copy_plus, Pplus_comm; auto. + rewrite <- law_assoc, IHh. reflexivity. rewrite law_comm. reflexivity. - + simpl in IHk. destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. - rewrite IHh; clear IHh. rewrite 2 law_assoc. rewrite (law_comm _ (copy m (eval a))). rewrite law_assoc, <- copy_plus, Pplus_comm; auto. - rewrite IHh; clear IHh. simpl. rewrite law_assoc. reflexivity. - rewrite 2 (law_comm (copy m (eval b))). rewrite law_assoc. apply proper; [ | reflexivity]. - rewrite <- IHk. reflexivity. + rewrite IHh; clear IHh. rewrite 2 law_assoc. rewrite (law_comm _ (copy m (eval a))). rewrite law_assoc, <- copy_plus, Pplus_comm; auto. + rewrite IHh; clear IHh. simpl. rewrite law_assoc. reflexivity. + rewrite 2 (law_comm (copy m (eval b))). rewrite law_assoc. apply proper; [ | reflexivity]. + rewrite <- IHk. reflexivity. Qed. - + Lemma copy_mset' n (l: mset T): copy_mset n l = nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l. Proof. unfold copy_mset. destruct n; try reflexivity. - + simpl. induction l as [|[a l] IHl]; simpl; try congruence. destruct a. reflexivity. Qed. - - + + Lemma copy_mset_succ n (l: mset T): eval (sum i (copy_mset (Psucc n) l)) == @Bin.value _ _ (e_bin i) (eval (sum i l)) (eval (sum i (copy_mset n l))). Proof. rewrite 2 copy_mset'. - + induction l as [[a m]|[a m] l IHl]. simpl eval. rewrite <- copy_plus; auto. rewrite Pmult_Sn_m. reflexivity. - - simpl nelist_map. rewrite ! eval_sum_cons. rewrite IHl. clear IHl. - rewrite Pmult_Sn_m. rewrite copy_plus; auto. rewrite <- !law_assoc. + + simpl nelist_map. rewrite ! eval_sum_cons. rewrite IHl. clear IHl. + rewrite Pmult_Sn_m. rewrite copy_plus; auto. rewrite <- !law_assoc. apply Binvalue_Proper; try reflexivity. rewrite law_comm . rewrite <- !law_assoc. apply proper; try reflexivity. - apply law_comm. + apply law_comm. Qed. Lemma copy_mset_copy : forall n (m : mset T), eval (sum i (copy_mset n m)) == @copy _ (@Bin.value _ _ (e_bin i)) n (eval (sum i m)). Proof. induction n using Pind; intros. - + unfold copy_mset. rewrite copy_xH. reflexivity. rewrite copy_mset_succ. rewrite copy_Psucc. rewrite IHn. reflexivity. Qed. - + Instance compat_sum_unit_Unit : forall p, compat_sum_unit (left p) -> @Unit X R (Bin.value (e_bin i)) (eval (unit p)). Proof. intros. inversion H. subst. auto. Qed. - - Lemma copy_n_unit : forall j n, is_unit j = true -> + + Lemma copy_n_unit : forall j n, is_unit j = true -> eval (unit j) == @copy _ (Bin.value (e_bin i)) n (eval (unit j)). Proof. intros. - induction n using Prect. + induction n using Prect. rewrite copy_xH. reflexivity. rewrite copy_Psucc. rewrite <- IHn. apply is_unit_sum_Unit in H. rewrite law_neutral_left. reflexivity. Qed. - - Lemma z0 l r (H : compat_sum_unit r): + + Lemma z0 l r (H : compat_sum_unit r): eval (sum i (run_msets (comp (merge_msets compare) l r))) == eval (sum i ((merge_msets compare) (l) (run_msets r))). Proof. unfold comp. unfold run_msets. - case_eq r; intros; subst. + case_eq r; intros; subst. rewrite eval_merge_bin; auto. - rewrite eval_sum_nil. - apply compat_sum_unit_Unit in H. rewrite law_neutral_right. reflexivity. + rewrite eval_sum_nil. + apply compat_sum_unit_Unit in H. rewrite law_neutral_right. reflexivity. reflexivity. Qed. - Lemma z1 : forall n x, - eval (sum i (run_msets (return_sum i (is_unit) x n ))) + Lemma z1 : forall n x, + eval (sum i (run_msets (return_sum i (is_unit) x n ))) == @copy _ (@Bin.value _ _ (e_bin i)) n (eval x). Proof. intros. unfold return_sum. unfold run_msets. case (is_sum_spec); intros; subst. rewrite copy_mset_copy. - reflexivity. - - rewrite eval_sum_nil. apply copy_n_unit. auto. + reflexivity. + + rewrite eval_sum_nil. apply copy_n_unit. auto. reflexivity. Qed. Lemma z2 : forall u n x, compat_sum_unit x -> - eval (sum i ( run_msets - (add_to_sum i (is_unit) u n x))) - == + eval (sum i ( run_msets + (add_to_sum i (is_unit) u n x))) + == @Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval u)) (eval (sum i (run_msets x))). Proof. intros u n x Hix . - unfold add_to_sum. + unfold add_to_sum. case is_sum_spec; intros; subst. - - rewrite z0 by auto. rewrite eval_merge_bin. rewrite copy_mset_copy. reflexivity. + + rewrite z0 by auto. rewrite eval_merge_bin. rewrite copy_mset_copy. reflexivity. rewrite <- copy_n_unit by assumption. apply is_unit_sum_Unit in H. rewrite law_neutral_left. reflexivity. - - - rewrite z0 by auto. rewrite eval_merge_bin. reflexivity. + + + rewrite z0 by auto. rewrite eval_merge_bin. reflexivity. Qed. End sum_correctness. - Lemma eval_norm_msets i norm + Lemma eval_norm_msets i norm (Comm : Commutative R (Bin.value (e_bin i))) (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (sum i (norm_msets norm i h)) == eval (sum i h). Proof. unfold norm_msets. - assert (H : + assert (H : forall h : mset T, eval (sum i (run_msets (norm_msets_ i (is_unit_of i) norm h))) == eval (sum i h) /\ compat_sum_unit (is_unit_of i) (norm_msets_ i (is_unit_of i) norm h)). - + induction h as [[a n] | [a n] h [IHh IHh']]; simpl norm_msets_; split. rewrite z1 by auto. rewrite Hnorm . reflexivity. auto. apply compat_sum_unit_return. - - rewrite z2 by auto. rewrite IHh. - rewrite eval_sum_cons. rewrite Hnorm. reflexivity. apply compat_sum_unit_add, IHh'. - + + rewrite z2 by auto. rewrite IHh. + rewrite eval_sum_cons. rewrite Hnorm. reflexivity. apply compat_sum_unit_add, IHh'. + apply H. Defined. - + (** auxiliary lemmas about products *) Section prd_correctness. @@ -949,59 +949,59 @@ Section s. Hypothesis is_unit_prd_Unit : forall j, is_unit j = true-> @Unit X R (Bin.value (e_bin i)) (eval (unit j)). Inductive is_prd_spec_ind : T -> @discr (nelist T) -> Prop := - | is_prd_spec_op : + | is_prd_spec_op : forall j l, j = i -> is_prd_spec_ind (prd j l) (Is_op l) - | is_prd_spec_unit : + | is_prd_spec_unit : forall j, is_unit j = true -> is_prd_spec_ind (unit j) (Is_unit j) - | is_prd_spec_nothing : + | is_prd_spec_nothing : forall u, is_prd_spec_ind u (Is_nothing). - + Lemma is_prd_spec u : is_prd_spec_ind u (is_prd i is_unit u). Proof. unfold is_prd; case u; intros; try constructor. case (eq_idx_spec); intros; subst; try constructor; auto. - case_eq (is_unit p); intros; try constructor; auto. + case_eq (is_unit p); intros; try constructor; auto. Qed. Lemma prd'_prd : forall (l: nelist T), eval (prd' i l) == eval (prd i l). - Proof. - intros [?|? [|? ?]]; simpl; reflexivity. + Proof. + intros [?|? [|? ?]]; simpl; reflexivity. Qed. - - - Lemma eval_prd_nil x: eval (prd i (nil x)) == eval x. + + + Lemma eval_prd_nil x: eval (prd i (nil x)) == eval x. Proof. rewrite <- prd'_prd. simpl. reflexivity. Qed. Lemma eval_prd_cons a : forall (l: nelist T), eval (prd i (a::l)) == @Bin.value _ _ (e_bin i) (eval a) (eval (prd i l)). Proof. intros [|b l]; simpl; reflexivity. - Qed. + Qed. Lemma eval_prd_app : forall (h k: nelist T), eval (prd i (h++k)) == @Bin.value _ _ (e_bin i) (eval (prd i h)) (eval (prd i k)). Proof. induction h; intro k. simpl; try reflexivity. simpl appne. rewrite 2 eval_prd_cons, IHh, law_assoc. reflexivity. - Qed. + Qed. - Inductive compat_prd_unit : @m idx (nelist T) -> Prop := - | cpu_left : forall x, is_unit x = true -> compat_prd_unit (left x) - | cpu_right : forall m, compat_prd_unit (right m) + Inductive compat_prd_unit : @m idx (nelist T) -> Prop := + | cpu_left : forall x, is_unit x = true -> compat_prd_unit (left x) + | cpu_right : forall m, compat_prd_unit (right m) . - - Lemma compat_prd_unit_return x: compat_prd_unit (return_prd i is_unit x). - Proof. - unfold return_prd. + + Lemma compat_prd_unit_return x: compat_prd_unit (return_prd i is_unit x). + Proof. + unfold return_prd. case (is_prd_spec); intros; try constructor; auto. Qed. - Lemma compat_prd_unit_add : forall x h, + Lemma compat_prd_unit_add : forall x h, compat_prd_unit h -> - compat_prd_unit - (add_to_prd i is_unit x - h). - Proof. - intros. + compat_prd_unit + (add_to_prd i is_unit x + h). + Proof. + intros. unfold add_to_prd. unfold comp. case (is_prd_spec); intros; try constructor; auto. @@ -1009,15 +1009,15 @@ Section s. unfold comp; case h; try constructor. Qed. - + Instance compat_prd_Unit : forall p, compat_prd_unit (left p) -> @Unit X R (Bin.value (e_bin i)) (eval (unit p)). Proof. - intros. + intros. inversion H; subst. apply is_unit_prd_Unit. assumption. Qed. - Lemma z0' : forall l (r: @m idx (nelist T)), compat_prd_unit r -> + Lemma z0' : forall l (r: @m idx (nelist T)), compat_prd_unit r -> eval (prd i (run_list (comp (@appne T) l r))) == eval (prd i ((appne (l) (run_list r)))). Proof. intros. @@ -1027,24 +1027,24 @@ Section s. apply compat_prd_Unit in H. rewrite law_neutral_right. reflexivity. reflexivity. Qed. - + Lemma z1' a : eval (prd i (run_list (return_prd i is_unit a))) == eval (prd i (nil a)). Proof. intros. unfold return_prd. unfold run_list. case (is_prd_spec); intros; subst; reflexivity. Qed. - Lemma z2' : forall u x, compat_prd_unit x -> - eval (prd i ( run_list + Lemma z2' : forall u x, compat_prd_unit x -> + eval (prd i ( run_list (add_to_prd i is_unit u x))) == @Bin.value _ _ (e_bin i) (eval u) (eval (prd i (run_list x))). - Proof. + Proof. intros u x Hix. - unfold add_to_prd. + unfold add_to_prd. case (is_prd_spec); intros; subst. rewrite z0' by auto. rewrite eval_prd_app. reflexivity. apply is_unit_prd_Unit in H. rewrite law_neutral_left. reflexivity. - rewrite z0' by auto. rewrite eval_prd_app. reflexivity. + rewrite z0' by auto. rewrite eval_prd_app. reflexivity. Qed. - + End prd_correctness. @@ -1057,24 +1057,24 @@ Section s. eval (prd i (run_list (norm_lists_ i (is_unit_of i) norm h))) == eval (prd i h) /\ compat_prd_unit (is_unit_of i) (norm_lists_ i (is_unit_of i) norm h)). + - induction h as [a | a h [IHh IHh']]; simpl norm_lists_; split. rewrite z1'. simpl. apply Hnorm. - - apply compat_prd_unit_return. - - rewrite z2'. rewrite IHh. rewrite eval_prd_cons. rewrite Hnorm. reflexivity. apply is_unit_of_Unit. + + apply compat_prd_unit_return. + + rewrite z2'. rewrite IHh. rewrite eval_prd_cons. rewrite Hnorm. reflexivity. apply is_unit_of_Unit. auto. - apply compat_prd_unit_add. auto. + apply compat_prd_unit_add. auto. apply H. Defined. (** correctness of the normalisation function *) Theorem eval_norm: forall u, eval (norm u) == eval u - with eval_norm_aux: forall i (l: vT i) (f: Sym.type_of i), + with eval_norm_aux: forall i (l: vT i) (f: Sym.type_of i), Proper (@Sym.rel_of X R i) f -> eval_aux (vnorm l) f == eval_aux l f. Proof. induction u as [ p m | p l | ? | ?]; simpl norm. @@ -1099,15 +1099,15 @@ Section s. Lemma normalise : forall (u v: T), eval (norm u) == eval (norm v) -> eval u == eval v. Proof. intros u v. rewrite 2 eval_norm. trivial. Qed. - + Lemma compare_reflect_eq: forall u v, compare u v = Eq -> eval u == eval v. Proof. intros u v. case (tcompare_weak_spec u v); intros; try congruence. reflexivity. Qed. Lemma decide: forall (u v: T), compare (norm u) (norm v) = Eq -> eval u == eval v. Proof. intros u v H. apply normalise. apply compare_reflect_eq. apply H. Qed. - Lemma lift_normalise {S} {H : AAC_lift S R}: - forall (u v: T), (let x := norm u in let y := norm v in + Lemma lift_normalise {S} {H : AAC_lift S R}: + forall (u v: T), (let x := norm u in let y := norm v in S (eval x) (eval y)) -> S (eval u) (eval v). Proof. destruct H. intros u v; simpl; rewrite 2 eval_norm. trivial. Qed. @@ -1123,13 +1123,13 @@ Section t. Lemma lift_transitivity_left (y x z : X): E x y -> R y z -> R x z. Proof. destruct H as [Hequiv Hproper]; intros G;rewrite G. trivial. Qed. - + Lemma lift_transitivity_right (y x z : X): E y z -> R x y -> R x z. Proof. destruct H as [Hequiv Hproper]; intros G. rewrite G. trivial. Qed. - Lemma lift_reflexivity {HR :Reflexive R}: forall x y, E x y -> R x y. + Lemma lift_reflexivity {HR :Reflexive R}: forall x y, E x y -> R x y. Proof. destruct H. intros ? ? G. rewrite G. reflexivity. Qed. End t. - + Declare ML Module "aac_tactics". @@ -14,7 +14,7 @@ open Names open Coqlib (* The contrib name is used to locate errors when loading constrs *) -let contrib_name = "aac_tactics" +let contrib_name = "aac_tactics" (* Getting constrs (primitive Coq terms) from existing Coq libraries. *) @@ -25,93 +25,93 @@ let init_constant dir s = find_constant contrib_name dir s (* A clause specifying that the [let] should not try to fold anything in the goal *) -let nowhere = - { Tacexpr.onhyps = Some []; - Tacexpr.concl_occs = Rawterm.no_occurrences_expr +let nowhere = + { Tacexpr.onhyps = Some []; + Tacexpr.concl_occs = Rawterm.no_occurrences_expr } -let cps_mk_letin +let cps_mk_letin (name:string) (c: constr) - (k : constr -> Proof_type.tactic) + (k : constr -> Proof_type.tactic) : Proof_type.tactic = - fun goal -> + fun goal -> let name = (Names.id_of_string name) in - let name = Tactics.fresh_id [] name goal in - let letin = (Tactics.letin_tac None (Name name) c None nowhere) in + let name = Tactics.fresh_id [] name goal in + let letin = (Tactics.letin_tac None (Name name) c None nowhere) in Tacticals.tclTHEN letin (k (mkVar name)) goal (** {2 General functions} *) -type goal_sigma = Proof_type.goal Tacmach.sigma +type goal_sigma = Proof_type.goal Tacmach.sigma let goal_update (goal : goal_sigma) evar_map : goal_sigma= - let it = Tacmach.sig_it goal in - Tacmach.re_sig it evar_map + let it = Tacmach.sig_it goal in + Tacmach.re_sig it evar_map let fresh_evar goal ty : constr * goal_sigma = - let env = Tacmach.pf_env goal in - let evar_map = Tacmach.project goal in - let (em,x) = Evarutil.new_evar evar_map env ty in + let env = Tacmach.pf_env goal in + let evar_map = Tacmach.project goal in + let (em,x) = Evarutil.new_evar evar_map env ty in x,( goal_update goal em) - + let resolve_one_typeclass goal ty : constr*goal_sigma= - let env = Tacmach.pf_env goal in - let evar_map = Tacmach.project goal in - let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in + let env = Tacmach.pf_env goal in + let evar_map = Tacmach.project goal in + let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in c, (goal_update goal em) let general_error = "Cannot resolve a typeclass : please report" -let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic = fun t k goal -> - Tacmach.pf_apply - (fun env em -> let em ,c = - try Typeclasses.resolve_one_typeclass env em t - with Not_found -> - begin match error with +let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic = fun t k goal -> + Tacmach.pf_apply + (fun env em -> let em ,c = + try Typeclasses.resolve_one_typeclass env em t + with Not_found -> + begin match error with | None -> Util.anomaly "Cannot resolve a typeclass : please report" | Some x -> Util.error x end - in + in Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal ) goal -let nf_evar goal c : Term.constr= - let evar_map = Tacmach.project goal in +let nf_evar goal c : Term.constr= + let evar_map = Tacmach.project goal in Evarutil.nf_evar evar_map c -let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma = - let env = Tacmach.pf_env gl in - let evar_map = Tacmach.project gl in - let (em,x) = Evarutil.new_evar evar_map env x in +let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma = + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let (em,x) = Evarutil.new_evar evar_map env x in x,(goal_update gl em) - -let evar_binary (gl: goal_sigma) (x : constr) = - let env = Tacmach.pf_env gl in - let evar_map = Tacmach.project gl in - let ty = mkArrow x (mkArrow x x) in - let (em,x) = Evarutil.new_evar evar_map env ty in + +let evar_binary (gl: goal_sigma) (x : constr) = + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let ty = mkArrow x (mkArrow x x) in + let (em,x) = Evarutil.new_evar evar_map env ty in x,( goal_update gl em) -let evar_relation (gl: goal_sigma) (x: constr) = - let env = Tacmach.pf_env gl in - let evar_map = Tacmach.project gl in - let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in - let (em,r) = Evarutil.new_evar evar_map env ty in +let evar_relation (gl: goal_sigma) (x: constr) = + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in + let (em,r) = Evarutil.new_evar evar_map env ty in r,( goal_update gl em) -let cps_evar_relation (x: constr) k = fun goal -> - Tacmach.pf_apply - (fun env em -> - let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in +let cps_evar_relation (x: constr) k = fun goal -> + Tacmach.pf_apply + (fun env em -> + let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in let (em,r) = Evarutil.new_evar em env ty in Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal ) goal (* decomp_term : constr -> (constr, types) kind_of_term *) let decomp_term c = kind_of_term (strip_outer_cast c) - + let lapp c v = mkApp (Lazy.force c, v) (** {2 Bindings with Coq' Standard Library} *) @@ -119,7 +119,7 @@ module Std = struct (* Here we package the module to be able to use List, later *) module Pair = struct - + let path = ["Coq"; "Init"; "Datatypes"] let typ = lazy (init_constant path "prod") let pair = lazy (init_constant path "pair") @@ -132,7 +132,7 @@ module Bool = struct let typ = lazy (init_constant path "bool") let ctrue = lazy (init_constant path "true") let cfalse = lazy (init_constant path "false") - let of_bool b = + let of_bool b = if b then Lazy.force ctrue else Lazy.force cfalse end @@ -157,13 +157,13 @@ module Option = struct let none = lazy (init_constant path "None") let some t x = mkApp (Lazy.force some, [| t ; x|]) let none t = mkApp (Lazy.force none, [| t |]) - let of_option t x = match x with + let of_option t x = match x with | Some x -> some t x | None -> none t -end +end module Pos = struct - + let path = ["Coq" ; "NArith"; "BinPos"] let typ = lazy (init_constant path "positive") let xI = lazy (init_constant path "xI") @@ -172,14 +172,14 @@ module Pos = struct (* A coq positive from an int *) let of_int n = - let rec aux n = - begin match n with + let rec aux n = + begin match n with | n when n < 1 -> assert false - | 1 -> Lazy.force xH - | n -> mkApp + | 1 -> Lazy.force xH + | n -> mkApp ( - (if n mod 2 = 0 - then Lazy.force xO + (if n mod 2 = 0 + then Lazy.force xO else Lazy.force xI ), [| aux (n/2)|] ) @@ -187,7 +187,7 @@ module Pos = struct in aux n end - + module Nat = struct let path = ["Coq" ; "Init"; "Datatypes"] let typ = lazy (init_constant path "nat") @@ -195,11 +195,11 @@ module Nat = struct let _O = lazy (init_constant path "O") (* A coq nat from an int *) let of_int n = - let rec aux n = - begin match n with + let rec aux n = + begin match n with | n when n < 0 -> assert false | 0 -> Lazy.force _O - | n -> mkApp + | n -> mkApp ( (Lazy.force _S ), [| aux (n-1)|] @@ -208,24 +208,24 @@ module Nat = struct in aux n end - + (** Lists from the standard library*) module List = struct let path = ["Coq"; "Lists"; "List"] let typ = lazy (init_constant path "list") let nil = lazy (init_constant path "nil") let cons = lazy (init_constant path "cons") - let cons ty h t = + let cons ty h t = mkApp (Lazy.force cons, [| ty; h ; t |]) - let nil ty = - (mkApp (Lazy.force nil, [| ty |])) - let rec of_list ty = function + let nil ty = + (mkApp (Lazy.force nil, [| ty |])) + let rec of_list ty = function | [] -> nil ty | t::q -> cons ty t (of_list ty q) let type_of_list ty = mkApp (Lazy.force typ, [|ty|]) end - + (** Morphisms *) module Classes = struct @@ -263,7 +263,7 @@ module Relation = struct let make ty r = {carrier = ty; r = r } let split t = t.carrier, t.r end - + module Transitive = struct type t = { @@ -272,19 +272,19 @@ module Transitive = struct transitive : constr; } let make ty leq transitive = {carrier = ty; leq = leq; transitive = transitive} - let infer goal ty leq = - let ask = Classes.mk_transitive ty leq in - let transitive , goal = resolve_one_typeclass goal ask in - make ty leq transitive, goal + let infer goal ty leq = + let ask = Classes.mk_transitive ty leq in + let transitive , goal = resolve_one_typeclass goal ask in + make ty leq transitive, goal let from_relation goal rlt = infer goal (rlt.Relation.carrier) (rlt.Relation.r) let cps_from_relation rlt k = - let ty =rlt.Relation.carrier in - let r = rlt.Relation.r in - let ask = Classes.mk_transitive ty r in - cps_resolve_one_typeclass ask + let ty =rlt.Relation.carrier in + let r = rlt.Relation.r in + let ask = Classes.mk_transitive ty r in + cps_resolve_one_typeclass ask (fun trans -> k (make ty r trans) ) - let to_relation t = + let to_relation t = {Relation.carrier = t.carrier; Relation.r = t.leq} end @@ -297,55 +297,55 @@ module Equivalence = struct equivalence : constr; } let make ty eq equivalence = {carrier = ty; eq = eq; equivalence = equivalence} - let infer goal ty eq = - let ask = Classes.mk_equivalence ty eq in - let equivalence , goal = resolve_one_typeclass goal ask in - make ty eq equivalence, goal + let infer goal ty eq = + let ask = Classes.mk_equivalence ty eq in + let equivalence , goal = resolve_one_typeclass goal ask in + make ty eq equivalence, goal let from_relation goal rlt = infer goal (rlt.Relation.carrier) (rlt.Relation.r) let cps_from_relation rlt k = - let ty =rlt.Relation.carrier in - let r = rlt.Relation.r in - let ask = Classes.mk_equivalence ty r in + let ty =rlt.Relation.carrier in + let r = rlt.Relation.r in + let ask = Classes.mk_equivalence ty r in cps_resolve_one_typeclass ask (fun equiv -> k (make ty r equiv) ) - let to_relation t = + let to_relation t = {Relation.carrier = t.carrier; Relation.r = t.eq} let split t = t.carrier, t.eq, t.equivalence end -end +end (**[ match_as_equation goal eqt] see [eqt] as an equation. An optionnal rel_context can be provided to ensure taht the term remains typable*) -let match_as_equation ?(context = Term.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option = - let env = Tacmach.pf_env goal in - let env = Environ.push_rel_context context env in - let evar_map = Tacmach.project goal in +let match_as_equation ?(context = Term.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option = + let env = Tacmach.pf_env goal in + let env = Environ.push_rel_context context env in + let evar_map = Tacmach.project goal in begin - match decomp_term equation with + match decomp_term equation with | App(c,ca) when Array.length ca >= 2 -> - let n = Array.length ca in - let left = ca.(n-2) in + let n = Array.length ca in + let left = ca.(n-2) in let right = ca.(n-1) in - let r = (mkApp (c, Array.sub ca 0 (n - 2))) in - let carrier = Typing.type_of env evar_map left in + let r = (mkApp (c, Array.sub ca 0 (n - 2))) in + let carrier = Typing.type_of env evar_map left in let rlt =Std.Relation.make carrier r - in + in Some (left, right, rlt ) | _ -> None - end + end (** {1 Tacticals} *) let tclTIME msg tac = fun gl -> - let u = Sys.time () in - let r = tac gl in - let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in + let u = Sys.time () in + let r = tac gl in + let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in r let tclDEBUG msg tac = fun gl -> - let _ = Pp.msgnl (Pp.str msg) in + let _ = Pp.msgnl (Pp.str msg) in tac gl let tclPRINT tac = fun gl -> @@ -356,24 +356,24 @@ let tclPRINT tac = fun gl -> (** {1 Error related mechanisms} *) (* functions to handle the failures of our tactic. Some should be reported [anomaly], some are on behalf of the user [user_error]*) -let anomaly msg = +let anomaly msg = Util.anomaly ("[aac_tactics] " ^ msg) -let user_error msg = +let user_error msg = Util.error ("[aac_tactics] " ^ msg) let warning msg = Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) - + (** {1 Rewriting tactics used in aac_rewrite} *) module Rewrite = struct (** Some informations about the hypothesis, with an (informal) - invariant: + invariant: - [typeof hyp = hyptype] - [hyptype = forall context, body] - [body = rel left right] - + *) type hypinfo = @@ -389,24 +389,24 @@ type hypinfo = } let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proof_type.tactic = fun goal -> - let ctype = Tacmach.pf_type_of goal c in - let (rel_context, body_type) = Term.decompose_prod_assum ctype in + let ctype = Tacmach.pf_type_of goal c in + let (rel_context, body_type) = Term.decompose_prod_assum ctype in let rec check f e = match decomp_term e with - | Term.Rel i -> - let name, constr_option, types = Term.lookup_rel i rel_context + | Term.Rel i -> + let name, constr_option, types = Term.lookup_rel i rel_context in f types | _ -> Term.fold_constr (fun acc x -> acc && check f x) true e - in - begin match check_type with + in + begin match check_type with | None -> () - | Some f -> - if not (check f body_type) + | Some f -> + if not (check f body_type) then user_error "Unable to deal with higher-order or heterogeneous patterns"; end; - begin + begin match match_as_equation ~context:rel_context goal body_type with - | None -> + | None -> user_error "The hypothesis is not an applied relation" | Some (hleft,hright,hrlt) -> k { @@ -417,11 +417,11 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proo context = rel_context; rel = hrlt ; left =hleft; - right = hright; + right = hright; } goal end - + (* The problem : Given a term to rewrite of type [H :forall xn ... x1, t], we have to instanciate the subset of [xi] of type @@ -438,75 +438,75 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proo (* Fresh evars for everyone (should be the good way to do this recompose in Coq v8.4) *) -let recompose_prod +let recompose_prod (context : Term.rel_context) - (subst : (int * Term.constr) list) + (subst : (int * Term.constr) list) env em : Evd.evar_map * Term.constr list = (* the last index of rel relevant for the rewriting *) - let min_n = List.fold_left - (fun acc (x,_) -> min acc x) - (List.length context) subst in - let rec aux context acc em n = - let _ = Printf.printf "%i\n%!" n in - match context with + let min_n = List.fold_left + (fun acc (x,_) -> min acc x) + (List.length context) subst in + let rec aux context acc em n = + let _ = Printf.printf "%i\n%!" n in + match context with | [] -> env, em, acc - | ((name,c,ty) as t)::q -> + | ((name,c,ty) as t)::q -> let env, em, acc = aux q acc em (n+1) in - if n >= min_n + if n >= min_n then - let em,x = - try em, List.assoc n subst - with | Not_found -> - Evarutil.new_evar em env (Term.substl acc ty) - in + let em,x = + try em, List.assoc n subst + with | Not_found -> + Evarutil.new_evar em env (Term.substl acc ty) + in (Environ.push_rel t env), em,x::acc else env,em,acc in - let _,em,acc = aux context [] em 1 in - em, acc + let _,em,acc = aux context [] em 1 in + em, acc (* no fresh evars : instead, use a lambda abstraction around an application to handle non-instanciated variables. *) - -let recompose_prod' + +let recompose_prod' (context : Term.rel_context) (subst : (int *Term.constr) list) c = - let rec popn pop n l = - if n <= 0 then l - else match l with + let rec popn pop n l = + if n <= 0 then l + else match l with | [] -> [] | t::q -> pop t :: (popn pop (n-1) q) - in - let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in + in + let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in let rec aux sign n next app ctxt = - match sign with - | [] -> List.rev app, List.rev ctxt + match sign with + | [] -> List.rev app, List.rev ctxt | decl::sign -> - try let term = (List.assoc n subst) in + try let term = (List.assoc n subst) in aux sign (n+1) next (term::app) (None :: ctxt) with - | Not_found -> - let term = Term.mkRel next in + | Not_found -> + let term = Term.mkRel next in aux sign (n+1) (next+1) (term::app) (Some decl :: ctxt) - in - let app,ctxt = aux context 1 1 [] [] in + in + let app,ctxt = aux context 1 1 [] [] in (* substitutes in the context *) let rec update ctxt app = - match ctxt,app with + match ctxt,app with | [],_ -> [] | _,[] -> [] | None :: sign, _ :: app -> None :: update sign (List.map (Termops.pop) app) - | Some decl :: sign, _ :: app -> - Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) - in - let ctxt = update ctxt app in + | Some decl :: sign, _ :: app -> + Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) + in + let ctxt = update ctxt app in (* updates the rel accordingly, taking some care not to go to far beyond: it is important not to lift indexes homogeneously, we have to update *) @@ -519,68 +519,68 @@ let recompose_prod' update sign (decl :: res) (n+1) in let ctxt = update ctxt [] 0 in - let c = Term.applistc c (List.rev app) in - let c = Term.it_mkLambda_or_LetIn c (ctxt) in + let c = Term.applistc c (List.rev app) in + let c = Term.it_mkLambda_or_LetIn c (ctxt) in c (* Version de Matthieu -let subst_rel_context k cstr ctx = +let subst_rel_context k cstr ctx = let (_, ctx') = List.fold_left (fun (k, ctx') (id, b, t) -> (succ k, (id, Option.map (Term.substnl [cstr] k) b, Term.substnl [cstr] k t) :: ctx')) (k, []) ctx in List.rev ctx' -let recompose_prod' context subst c = +let recompose_prod' context subst c = let len = List.length context in - let rec aux sign n next app ctxt = - match sign with - | [] -> List.rev app, List.rev ctxt + let rec aux sign n next app ctxt = + match sign with + | [] -> List.rev app, List.rev ctxt | decl::sign -> - try let term = (List.assoc n subst) in - aux (subst_rel_context 0 term sign) (pred n) (succ next) - (term::List.map (Term.lift (-1)) app) ctxt - with Not_found -> - let term = Term.mkRel (len - next) in - aux sign (pred n) (succ next) (term::app) (decl :: ctxt) + try let term = (List.assoc n subst) in + aux (subst_rel_context 0 term sign) (pred n) (succ next) + (term::List.map (Term.lift (-1)) app) ctxt + with Not_found -> + let term = Term.mkRel (len - next) in + aux sign (pred n) (succ next) (term::app) (decl :: ctxt) in - let app,ctxt = aux (List.rev context) len 0 [] [] in + let app,ctxt = aux (List.rev context) len 0 [] [] in Term.it_mkLambda_or_LetIn (Term.applistc c(app)) (List.rev ctxt) *) -let build - (h : hypinfo) +let build + (h : hypinfo) (subst : (int *Term.constr) list) - (k :Term.constr -> Proof_type.tactic) + (k :Term.constr -> Proof_type.tactic) : Proof_type.tactic = fun goal -> - let c = recompose_prod' h.context subst h.hyp in + let c = recompose_prod' h.context subst h.hyp in Tacticals.tclTHENLIST [k c] goal -let build_with_evar - (h : hypinfo) +let build_with_evar + (h : hypinfo) (subst : (int *Term.constr) list) - (k :Term.constr -> Proof_type.tactic) - : Proof_type.tactic + (k :Term.constr -> Proof_type.tactic) + : Proof_type.tactic = fun goal -> - Tacmach.pf_apply - (fun env em -> + Tacmach.pf_apply + (fun env em -> let evar_map, acc = recompose_prod h.context subst env em in let c = Term.applistc h.hyp (List.rev acc) in Tacticals.tclTHENLIST [Refiner.tclEVARS evar_map; k c] goal - ) goal + ) goal -let rewrite ?(abort=false)hypinfo subst k = - build hypinfo subst - (fun rew -> +let rewrite ?(abort=false)hypinfo subst k = + build hypinfo subst + (fun rew -> let tac = if not abort then Equality.general_rewrite_bindings - hypinfo.l2r - Termops.all_occurrences + hypinfo.l2r + Termops.all_occurrences false (rew,Rawterm.NoBindings) true - else + else Tacticals.tclIDTAC in k tac ) diff --git a/AAC_coq.mli b/AAC_coq.mli index 116ff4c..a0f2ce0 100644 --- a/AAC_coq.mli +++ b/AAC_coq.mli @@ -10,7 +10,7 @@ and we import several definitions from Coq's standard library. This general purpose library could be reused by other plugins. - + Some salient points: - we use Caml's module system to mimic Coq's one, and avoid cluttering the namespace; @@ -27,18 +27,18 @@ val init_constant : string list -> string -> Term.constr (** {2 General purpose functions} *) -type goal_sigma = Proof_type.goal Tacmach.sigma +type goal_sigma = Proof_type.goal Tacmach.sigma val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma -val cps_resolve_one_typeclass: ?error:string -> Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val cps_resolve_one_typeclass: ?error:string -> Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic val nf_evar : goal_sigma -> Term.constr -> Term.constr val fresh_evar :goal_sigma -> Term.types -> Term.constr* goal_sigma val evar_unit :goal_sigma ->Term.constr -> Term.constr* goal_sigma -val evar_binary: goal_sigma -> Term.constr -> Term.constr* goal_sigma -val evar_relation: goal_sigma -> Term.constr -> Term.constr* goal_sigma -val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val evar_binary: goal_sigma -> Term.constr -> Term.constr* goal_sigma +val evar_relation: goal_sigma -> Term.constr -> Term.constr* goal_sigma +val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic (** [cps_mk_letin name v] binds the constr [v] using a letin tactic *) -val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term @@ -51,7 +51,7 @@ module List: sig (** [of_list ty l] *) val of_list:Term.constr ->Term.constr list ->Term.constr - + (** [type_of_list ty] *) val type_of_list:Term.constr ->Term.constr end @@ -77,7 +77,7 @@ module Comparison : sig val gt : Term.constr lazy_t end -module Leibniz : sig +module Leibniz : sig val eq_refl : Term.types -> Term.constr -> Term.constr end @@ -85,7 +85,7 @@ module Option : sig val some : Term.constr -> Term.constr -> Term.constr val none : Term.constr -> Term.constr val of_option : Term.constr -> Term.constr option -> Term.constr -end +end (** Coq positive numbers (pos) *) module Pos: @@ -108,14 +108,14 @@ sig val mk_equivalence: Term.constr -> Term.constr -> Term.constr val mk_reflexive: Term.constr -> Term.constr -> Term.constr val mk_transitive: Term.constr -> Term.constr -> Term.constr -end +end module Relation : sig type t = {carrier : Term.constr; r : Term.constr;} - val make : Term.constr -> Term.constr -> t + val make : Term.constr -> Term.constr -> t val split : t -> Term.constr * Term.constr end - + module Transitive : sig type t = { @@ -125,7 +125,7 @@ module Transitive : sig } val make : Term.constr -> Term.constr -> Term.constr -> t val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma - val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic val to_relation : t -> Relation.t end @@ -135,11 +135,11 @@ module Equivalence : sig { carrier : Term.constr; eq : Term.constr; - equivalence : Term.constr; - } + equivalence : Term.constr; + } val make : Term.constr -> Term.constr -> Term.constr -> t val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma - val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic val to_relation : t -> Relation.t val split : t -> Term.constr * Term.constr * Term.constr @@ -171,7 +171,7 @@ val warning : string -> unit (** {2 Rewriting tactics used in aac_rewrite} *) -module Rewrite : sig +module Rewrite : sig (** The rewriting tactics used in aac_rewrite, build as handlers of the usual [setoid_rewrite]*) @@ -179,11 +179,11 @@ module Rewrite : sig (** {2 Datatypes} *) (** We keep some informations about the hypothesis, with an (informal) - invariant: + invariant: - [typeof hyp = typ] - [typ = forall context, body] - [body = rel left right] - + *) type hypinfo = { @@ -202,7 +202,7 @@ type hypinfo = function can be provided to check the type of every free variable of the body of the hypothesis. *) val get_hypinfo :Term.constr -> l2r:bool -> ?check_type:(Term.types -> bool) -> (hypinfo -> Proof_type.tactic) -> Proof_type.tactic - + (** {2 Rewriting with bindings} The problem : Given a term to rewrite of type [H :forall xn ... x1, diff --git a/AAC_helper.ml b/AAC_helper.ml index 15372f2..637def1 100644 --- a/AAC_helper.ml +++ b/AAC_helper.ml @@ -14,28 +14,28 @@ end module Debug (X : CONTROL) = struct open X - let debug x = - if debug then + let debug x = + if debug then Printf.printf "%s\n%!" x let time f x fmt = - if time then + if time then let t = Sys.time () in let r = f x in Printf.printf fmt (Sys.time () -. t); r - else f x + else f x - let pr_constr msg constr = - if printing then + let pr_constr msg constr = + if printing then ( Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg)); Pp.msgnl (Printer.pr_constr constr); ) - let debug_exception msg e = + let debug_exception msg e = debug (msg ^ (Printexc.to_string e)) - + end diff --git a/AAC_matcher.ml b/AAC_matcher.ml index a427cf8..47ab840 100644 --- a/AAC_matcher.ml +++ b/AAC_matcher.ml @@ -8,7 +8,7 @@ (** This module defines our matching functions, modulo associativity and commutativity (AAC). - + The basic idea is to find a substitution [env] such that the pattern [p] instantiated by [env] is equal to [t] modulo AAC. @@ -31,10 +31,10 @@ *) -module Control = -struct +module Control = +struct let debug = false - let time = false + let time = false let printing = false end @@ -44,21 +44,21 @@ open Debug type symbol = int type var = int type units = (symbol * symbol) list (* from AC/A symbols to the unit *) -type ext_units = +type ext_units = { - unit_for : units; + unit_for : units; is_ac : (symbol * bool) list } -let print_units units= +let print_units units= List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; Printf.printf "\n%!" exception NoUnit -let get_unit units op = - try List.assoc op units - with +let get_unit units op = + try List.assoc op units + with | Not_found -> raise NoUnit let is_unit units op unit = List.mem (op,unit) units @@ -67,21 +67,21 @@ let is_unit units op unit = List.mem (op,unit) units open AAC_search_monad type 'a mset = ('a * int) list -let linear p = +let linear p = let rec ncons t l = function | 0 -> l | n -> t::ncons t l (n-1) in - let rec aux = function + let rec aux = function [ ] -> [] - | (t,n)::q -> let q = aux q in + | (t,n)::q -> let q = aux q in ncons t q n in aux p - + -(** The module {!Terms} defines two different types for expressions. - +(** The module {!Terms} defines two different types for expressions. + - a public type {!Terms.t} that represent abstract syntax trees of expressions with binary associative (and commutative) operators @@ -93,7 +93,7 @@ let linear p = *) -module Terms : sig +module Terms : sig (** {1 Abstract syntax tree of terms} @@ -111,7 +111,7 @@ module Terms : sig val size: t -> int (** {1 Terms in normal form} - + A term in normal form is the canonical representative of the equivalence class of all the terms that are equal modulo Associativity and Commutativity. Outside the {!AAC_matcher} module, @@ -120,27 +120,27 @@ module Terms : sig type nf_term = private - | TAC of symbol * nf_term mset + | TAC of symbol * nf_term mset | TA of symbol * nf_term list | TSym of symbol * nf_term list | TUnit of symbol | TVar of var - + (** {2 Constructors: we ensure that the terms are always normalised - + braibant - Fri 27 Aug 2010, 15:11 Moreover, we assure that we will not build empty sums or empty products, leaving this task to the caller function. - } + } *) - val mk_TAC : units -> symbol -> nf_term mset -> nf_term - val mk_TA : units -> symbol -> nf_term list -> nf_term + val mk_TAC : units -> symbol -> nf_term mset -> nf_term + val mk_TA : units -> symbol -> nf_term list -> nf_term val mk_TSym : symbol -> nf_term list -> nf_term val mk_TVar : var -> nf_term val mk_TUnit : symbol -> nf_term - + (** {2 Comparisons} *) val nf_term_compare : nf_term -> nf_term -> int val nf_equal : nf_term -> nf_term -> bool @@ -149,7 +149,7 @@ module Terms : sig val sprint_nf_term : nf_term -> string (** {2 Conversion functions} *) - val term_of_t : units -> t -> nf_term + val term_of_t : units -> t -> nf_term val t_of_term : nf_term -> t (* we could return the units here *) end = struct @@ -161,53 +161,53 @@ end | Var of var | Unit of symbol - let rec size = function - | Dot (_,x,y) + let rec size = function + | Dot (_,x,y) | Plus (_,x,y) -> size x+ size y + 1 | Sym (_,v)-> Array.fold_left (fun acc x -> size x + acc) 1 v | _ -> 1 - type nf_term = - | TAC of symbol * nf_term mset + type nf_term = + | TAC of symbol * nf_term mset | TA of symbol * nf_term list | TSym of symbol * nf_term list - | TUnit of symbol + | TUnit of symbol | TVar of var - + (** {2 Constructors: we ensure that the terms are always normalised} *) (** {3 Pre constructors : These constructors ensure that sums and products are not degenerated (no trailing units)} *) - let mk_TAC' units (s : symbol) l = match l with + let mk_TAC' units (s : symbol) l = match l with | [] -> TUnit (get_unit units s ) | [_,0] -> assert false - | [t,1] -> t - | _ -> TAC (s,l) - let mk_TA' units (s : symbol) l = match l with + | [t,1] -> t + | _ -> TAC (s,l) + let mk_TA' units (s : symbol) l = match l with | [] -> TUnit (get_unit units s ) - | [t] -> t + | [t] -> t | _ -> TA (s,l) - + (** {2 Comparison} *) let nf_term_compare = Pervasives.compare - let nf_equal a b = + let nf_equal a b = a = b (** [merge_ac comp l1 l2] merges two lists of terms with coefficients into one. Terms that are equal modulo the comparison function [comp] will see their arities added. *) - + (* This function could be improved by the use of sorted msets *) let merge_ac (compare : 'a -> 'a -> int) (l : 'a mset) (l' : 'a mset) : 'a mset = - let rec aux l l'= - match l,l' with + let rec aux l l'= + match l,l' with | [], _ -> l' | _, [] -> l | (t,tar)::q, (t',tar')::q' -> @@ -215,7 +215,7 @@ end | 0 -> ( t,tar+tar'):: aux q q' | -1 -> (t, tar):: aux q l' | _ -> (t', tar'):: aux l q' - end + end in aux l l' (** [merge_map f l] uses the combinator [f] to combine the head of the @@ -231,46 +231,46 @@ end merge_ac nf_term_compare l l' let extract_A units s t = - match t with + match t with | TA (s',l) when s' = s -> l - | TUnit u when is_unit units s u -> [] + | TUnit u when is_unit units s u -> [] | _ -> [t] - let extract_AC units s (t,ar) : nf_term mset = - match t with + let extract_AC units s (t,ar) : nf_term mset = + match t with | TAC (s',l) when s' = s -> List.map (fun (x,y) -> (x,y*ar)) l - | TUnit u when is_unit units s u -> [] + | TUnit u when is_unit units s u -> [] | _ -> [t,ar] (** {3 Constructors of {!nf_term}}*) - let mk_TAC units (s : symbol) (l : (nf_term *int) list) = - mk_TAC' units s - (merge_map (fun u l -> merge (extract_AC units s u) l) l) - let mk_TA units s l = + let mk_TAC units (s : symbol) (l : (nf_term *int) list) = + mk_TAC' units s + (merge_map (fun u l -> merge (extract_AC units s u) l) l) + let mk_TA units s l = mk_TA' units s - (merge_map (fun u l -> (extract_A units s u) @ l) l) - let mk_TSym s l = TSym (s,l) + (merge_map (fun u l -> (extract_A units s u) @ l) l) + let mk_TSym s l = TSym (s,l) let mk_TVar v = TVar v let mk_TUnit s = TUnit s (** {2 Printing function} *) - let print_binary_list (single : 'a -> string) - (unit : string) + let print_binary_list (single : 'a -> string) + (unit : string) (binary : string -> string -> string) (l : 'a list) = let rec aux l = - match l with + match l with [] -> unit | [t] -> single t | t::q -> - let r = aux q in + let r = aux q in Printf.sprintf "%s" (binary (single t) r) - in + in aux l let print_symbol s = - match s with + match s with | s, None -> Printf.sprintf "%i" s | s , Some u -> Printf.sprintf "%i(unit %i)" s u @@ -287,31 +287,31 @@ end ) let print_symbol single s l = - match l with + match l with [] -> Printf.sprintf "%i" s - | _ -> - Printf.sprintf "%i(%s)" + | _ -> + Printf.sprintf "%i(%s)" s (print_binary_list single "" (fun x y -> x ^ "," ^ y) l) let print_ac single s l = - Printf.sprintf "[%s:AC]{%s}" + Printf.sprintf "[%s:AC]{%s}" (string_of_int s ) - (sprint_ac + (sprint_ac single l ) let print_a single s l = - Printf.sprintf "[%s:A]{%s}" + Printf.sprintf "[%s:A]{%s}" (string_of_int s) - (print_binary_list single "1" (fun x y -> x ^ " , " ^ y) l) + (print_binary_list single "1" (fun x y -> x ^ " , " ^ y) l) let rec sprint_nf_term = function - | TSym (s,l) -> print_symbol sprint_nf_term s l + | TSym (s,l) -> print_symbol sprint_nf_term s l | TAC (s,l) -> print_ac sprint_nf_term s l - | TA (s,l) -> print_a sprint_nf_term s l + | TA (s,l) -> print_a sprint_nf_term s l | TVar v -> Printf.sprintf "x%i" v | TUnit s -> Printf.sprintf "unit%i" s @@ -322,51 +322,51 @@ end (* rebuilds a tree out of a list, under the assumption that the list is not empty *) let rec binary_of_list f comb l = - let l = List.rev l in - let rec aux = function + let l = List.rev l in + let rec aux = function | [] -> assert false | [t] -> f t | t::q -> comb (aux q) (f t) - in + in aux l - let term_of_t units : t -> nf_term = + let term_of_t units : t -> nf_term = let rec term_of_t = function - | Dot (s,l,r) -> - let l = term_of_t l in - let r = term_of_t r in + | Dot (s,l,r) -> + let l = term_of_t l in + let r = term_of_t r in mk_TA units s [l;r] - | Plus (s,l,r) -> - let l = term_of_t l in - let r = term_of_t r in + | Plus (s,l,r) -> + let l = term_of_t l in + let r = term_of_t r in mk_TAC units s [l,1;r,1] - | Unit x -> + | Unit x -> mk_TUnit x - | Sym (s,t) -> - let t = Array.to_list t in - let t = List.map term_of_t t in + | Sym (s,t) -> + let t = Array.to_list t in + let t = List.map term_of_t t in mk_TSym s t - | Var i -> + | Var i -> mk_TVar ( i) in term_of_t - let rec t_of_term : nf_term -> t = function + let rec t_of_term : nf_term -> t = function | TAC (s,l) -> - (binary_of_list + (binary_of_list t_of_term (fun l r -> Plus ( s,l,r)) - (linear l) + (linear l) ) | TA (s,l) -> - (binary_of_list - t_of_term + (binary_of_list + t_of_term (fun l r -> Dot ( s,l,r)) l ) - | TSym (s,l) -> - let v = Array.of_list l in - let v = Array.map (t_of_term) v in + | TSym (s,l) -> + let v = Array.of_list l in + let v = Array.map (t_of_term) v in Sym ( s,v) | TVar x -> Var x | TUnit s -> Unit s @@ -379,16 +379,16 @@ end (** Terms environments defined as association lists from variables to terms in normal form {! Terms.nf_term} *) module Subst : sig - type t + type t val find : t -> var -> Terms.nf_term option val add : t -> var -> Terms.nf_term -> t - val empty : t + val empty : t val instantiate : t -> Terms.t -> Terms.t val sprint : t -> string val to_list : t -> (var*Terms.t) list end - = + = struct open Terms @@ -402,32 +402,32 @@ end let empty = [] let sprint (l : t) = - match l with + match l with | [] -> Printf.sprintf "Empty environment\n" - | _ -> - let s = List.fold_left - (fun acc (x,y) -> - Printf.sprintf "%sX%i -> %s\n" - acc - x + | _ -> + let s = List.fold_left + (fun acc (x,y) -> + Printf.sprintf "%sX%i -> %s\n" + acc + x (sprint_nf_term y) - ) + ) "" - (List.rev l) in + (List.rev l) in Printf.sprintf "%s\n%!" s (** [instantiate] is an homomorphism except for the variables*) let instantiate (t: t) (x:Terms.t) : Terms.t = - let rec aux = function + let rec aux = function | Unit _ as x -> x | Sym (s,t) -> Sym (s,Array.map aux t) | Plus (s,l,r) -> Plus (s, aux l, aux r) | Dot (s,l,r) -> Dot (s, aux l, aux r) - | Var i -> + | Var i -> begin match find t i with - | None -> Util.error "aac_tactics: instantiate failure" + | None -> Util.error "aac_tactics: instantiate failure" | Some x -> t_of_term x end in aux x @@ -445,39 +445,39 @@ end the units, we package them in a module. This functor will then be applied to a module containing the units, in the exported functions. *) - module M (X : sig - val units : units - val is_ac : (symbol * bool) list + module M (X : sig + val units : units + val is_ac : (symbol * bool) list val strict : bool (* variables cannot be instantiated with units *) end) = struct - - open X + + open X - let nullifiable p = - let nullable = not strict in - let has_unit s = + let nullifiable p = + let nullable = not strict in + let has_unit s = try let _ = get_unit units s in true - with NoUnit -> false - in - let rec aux = function - | TA (s,l) -> has_unit s && List.for_all (aux) l + with NoUnit -> false + in + let rec aux = function + | TA (s,l) -> has_unit s && List.for_all (aux) l | TAC (s,l) -> has_unit s && List.for_all (fun (x,n) -> aux x) l | TSym _ -> false | TVar _ -> nullable | TUnit _ -> true in aux p - - let print_units ()= + + let print_units ()= List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; Printf.printf "\n%!" - + let mk_TAC s l = mk_TAC units s l let mk_TA s l = mk_TA units s l - let mk_TAC' s l = + let mk_TAC' s l = try return( mk_TAC s l) with _ -> fail () - let mk_TA' s l = - try return( mk_TA s l) + let mk_TA' s l = + try return( mk_TA s l) with _ -> fail () (** First, we need to be able to perform non-deterministic choice of @@ -486,27 +486,27 @@ end *) let a_nondet_split_raw t : ('a list * 'a list) m = let rec aux l l' = - match l' with - | [] -> + match l' with + | [] -> return ( l,[]) - | t::q -> + | t::q -> return ( l,l' ) - >>| aux (l @ [t]) q - in - aux [] t + >>| aux (l @ [t]) q + in + aux [] t (** Same as the previous [a_nondet_split], but split the list in 3 parts *) let a_nondet_middle t : ('a list * 'a list * 'a list) m = a_nondet_split_raw t >> - (fun (left, right) -> - a_nondet_split_raw left >> + (fun (left, right) -> + a_nondet_split_raw left >> (fun (left, middle) -> return (left, middle, right)) ) (** Non deterministic splits of ac lists *) let dispatch f n = - let rec aux k = + let rec aux k = if k = 0 then return (f n 0) else return (f (n-k) k) >>| aux (k-1) in @@ -518,78 +518,78 @@ end let ac_nondet_split_raw (l : 'a mset) : ('a mset * 'a mset) m = let rec aux = function | [] -> return ([],[]) - | (t,tar)::q -> + | (t,tar)::q -> aux q - >> + >> (fun (left,right) -> - dispatch (fun arl arr -> - add_with_arith t arl left, + dispatch (fun arl arr -> + add_with_arith t arl left, add_with_arith t arr right ) tar ) in aux l - + let a_nondet_split current t : (nf_term * nf_term list) m= a_nondet_split_raw t >> - (fun (l,r) -> - if strict && (l=[]) - then fail() + (fun (l,r) -> + if strict && (l=[]) + then fail() else - mk_TA' current l >> + mk_TA' current l >> fun t -> return (t, r) ) - + let ac_nondet_split current t : (nf_term * nf_term mset) m= ac_nondet_split_raw t >> - (fun (l,r) -> - if strict && (l=[]) - then fail() + (fun (l,r) -> + if strict && (l=[]) + then fail() else - mk_TAC' current l >> + mk_TAC' current l >> fun t -> return (t, r) ) - + (** Try to affect the variable [x] to each left factor of [t]*) let var_a_nondet_split env current x t = a_nondet_split current t >> - (fun (t,res) -> + (fun (t,res) -> return ((Subst.add env x t), res) ) (** Try to affect variable [x] to _each_ subset of t. *) let var_ac_nondet_split (current: symbol) env (x : var) (t : nf_term mset) : (Subst.t * (nf_term mset)) m = - ac_nondet_split current t + ac_nondet_split current t >> - (fun (t,res) -> + (fun (t,res) -> return ((Subst.add env x t), res) ) (** See the term t as a given AC symbol. Unwrap the first constructor if necessary *) - let get_AC (s : symbol) (t : nf_term) : (nf_term *int) list = - match t with - | TAC (s',l) when s' = s -> l + let get_AC (s : symbol) (t : nf_term) : (nf_term *int) list = + match t with + | TAC (s',l) when s' = s -> l | TUnit u when is_unit units s u -> [] | _ -> [t,1] (** See the term t as a given A symbol. Unwrap the first constructor if necessary *) - let get_A (s : symbol) (t : nf_term) : nf_term list = - match t with - | TA (s',l) when s' = s -> l + let get_A (s : symbol) (t : nf_term) : nf_term list = + match t with + | TA (s',l) when s' = s -> l | TUnit u when is_unit units s u -> [] | _ -> [t] (** See the term [t] as an symbol [s]. Fail if it is not such symbol. *) - let get_Sym s t = - match t with + let get_Sym s t = + match t with | TSym (s',l) when s' = s -> return l | _ -> fail () @@ -600,22 +600,22 @@ end (** We remove the left factor v in a term list. This function runs linearly with respect to the size of the first pattern symbol *) - let left_factor current (v : nf_term) (t : nf_term list) = - let rec aux a b = - match a,b with + let left_factor current (v : nf_term) (t : nf_term list) = + let rec aux a b = + match a,b with | t::q , t' :: q' when nf_equal t t' -> aux q q' | [], q -> return q | _, _ -> fail () - in - match v with + in + match v with | TA (s,l) when s = current -> aux l t | TUnit u when is_unit units current u -> return t | _ -> - begin match t with + begin match t with | [] -> fail () - | t::q -> - if nf_equal v t - then return q + | t::q -> + if nf_equal v t + then return q else fail () end @@ -634,17 +634,17 @@ end let pick_sym (s : symbol) (t : nf_term mset ) = let rec aux front back = - match back with + match back with | [] -> fail () - | (t,tar)::q -> - begin match t with + | (t,tar)::q -> + begin match t with | TSym (s',v') when s = s' -> let back = if tar > 1 then (t,tar -1) ::q else q in - return (v' , List.rev_append front back ) + return (v' , List.rev_append front back ) >>| aux ((t,tar)::front) q | _ -> aux ((t,tar)::front) q end @@ -659,7 +659,7 @@ end with | NoUnit -> false let is_same_AC s t : nf_term mset option= - match t with + match t with TAC (s',l) when s = s' -> Some l | _ -> None @@ -667,11 +667,11 @@ end symbol *) let single_AC_factor (s : symbol) (v : nf_term) v_ar (t : nf_term mset) : (nf_term mset) m = let rec aux front back = - match back with + match back with | [] -> fail () - | (t,tar)::q -> - begin - if nf_equal v t + | (t,tar)::q -> + begin + if nf_equal v t then match () with | _ when tar < v_ar -> fail () @@ -681,7 +681,7 @@ end aux ((t,tar) :: front) q end in - if is_unit_AC s v + if is_unit_AC s v then return t else @@ -691,13 +691,13 @@ end the same symbol, we remove every elements, one at a time (and we do care of the arities) *) let factor_AC (s : symbol) (v: nf_term) (t : nf_term mset) : ( nf_term mset ) m = - match is_same_AC s v with - | None -> single_AC_factor s v 1 t + match is_same_AC s v with + | None -> single_AC_factor s v 1 t | Some l -> (* We are trying to remove an AC factor *) - List.fold_left (fun acc (v,v_ar) -> + List.fold_left (fun acc (v,v_ar) -> acc >> (single_AC_factor s v v_ar) - ) + ) (return t) l @@ -715,12 +715,12 @@ end it is the duty of the user to reverse the front if needed *) -let tri_fold f (l : 'a list) (acc : 'b)= match l with +let tri_fold f (l : 'a list) (acc : 'b)= match l with [] -> acc | _ -> - let _,_,acc = List.fold_left (fun acc (t : 'a) -> - let l,r,acc = acc in - let r = List.tl r in + let _,_,acc = List.fold_left (fun acc (t : 'a) -> + let l,r,acc = acc in + let r = List.tl r in t::l,r,f acc l t r ) ([], l,acc) l in acc @@ -743,61 +743,61 @@ module Positions = struct let ac (l: 'a mset) : ('a mset * 'a )m = - let rec aux = function + let rec aux = function | [] -> assert false | [t,1] -> return ([],t) | [t,tar] -> return ([t,tar -1],t) - | (t,tar) as h :: q -> - (aux q >> (fun (c,x) -> return (h :: c,x))) + | (t,tar) as h :: q -> + (aux q >> (fun (c,x) -> return (h :: c,x))) >>| (if tar > 1 then return ((t,tar-1) :: q,t) else return (q,t)) - in - aux l + in + aux l let ac' current (l: 'a mset) : ('a mset * 'a )m = - ac_nondet_split_raw l >> + ac_nondet_split_raw l >> (fun (l,r) -> if l = [] || r = [] then fail () else - mk_TAC' current r >> + mk_TAC' current r >> fun t -> return (l, t) ) - + let a (l : 'a list) : ('a list * 'a * 'a list) m = let rec aux left right : ('a list * 'a * 'a list) m = - match right with + match right with | [] -> assert false | [t] -> return (left,t,[]) - | t::q -> + | t::q -> aux (left@[t]) q >>| return (left,t,q) in aux [] l end -let build_ac (current : symbol) (context : nf_term mset) (p : t) : t m= - if context = [] - then return p - else +let build_ac (current : symbol) (context : nf_term mset) (p : t) : t m= + if context = [] + then return p + else mk_TAC' current context >> fun t -> return (Plus (current,t_of_term t,p)) -let build_a (current : symbol) - (left : nf_term list) (right : nf_term list) (p : t) : t m= +let build_a (current : symbol) + (left : nf_term list) (right : nf_term list) (p : t) : t m= let right_pat p = - if right = [] - then return p + if right = [] + then return p else - mk_TA' current right >> + mk_TA' current right >> fun t -> return (Dot (current,p,t_of_term t)) in let left_pat p= - if left = [] - then return p + if left = [] + then return p else - mk_TA' current left >> + mk_TA' current left >> fun t -> return (Dot (current,t_of_term t,p)) - in + in right_pat p >> left_pat >> (fun p -> return p) @@ -809,49 +809,49 @@ let conts (unit : symbol) (l : symbol list) p : t m = / \ / \ / \ 1 p p 1 p 1 *) - let ac,a = List.partition (fun s -> List.assoc s is_ac) l in - let acc = fail () in - let acc = List.fold_left - (fun acc s -> + let ac,a = List.partition (fun s -> List.assoc s is_ac) l in + let acc = fail () in + let acc = List.fold_left + (fun acc s -> acc >>| return (Plus (s,p,Unit unit)) - ) acc ac in - let acc = - List.fold_left - (fun acc s -> + ) acc ac in + let acc = + List.fold_left + (fun acc s -> acc >>| return (Dot (s,p,Unit unit)) >>| return (Dot (s,Unit unit,p)) ) acc a in acc - -(** + +(** - Return the same thing as subterm : + Return the same thing as subterm : - The size of the context - The context - A collection of substitutions (here == return Subst.empty) *) let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m = - let symbols = List.fold_left - (fun acc (ac,u) -> if u = unit then ac :: acc else acc ) [] units - in + let symbols = List.fold_left + (fun acc (ac,u) -> if u = unit then ac :: acc else acc ) [] units + in (* make a unit appear at each strict sub-position of the term*) let rec positions (t : nf_term) : t m = match t with (* with a final unit at the end *) | TAC (s,l) -> - let symbols' = List.filter (fun x -> x <> s) symbols in + let symbols' = List.filter (fun x -> x <> s) symbols in ( ac_nondet_split_raw l >> (fun (l,r) -> if l = [] || r = [] then fail () else ( - match r with - | [p,1] -> - positions p >>| conts unit symbols' p - | _ -> - mk_TAC' s r >> conts unit symbols' + match r with + | [p,1] -> + positions p >>| conts unit symbols' p + | _ -> + mk_TAC' s r >> conts unit symbols' ) >> build_ac s l )) - | TA (s,l) -> - let symbols' = List.filter (fun x -> x <> s) symbols in + | TA (s,l) -> + let symbols' = List.filter (fun x -> x <> s) symbols in ( (* first the other symbols, and then the more simple case of this aprticular symbol *) @@ -861,20 +861,20 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m = if (l = [] && r = []) then fail () else - ( - match m with - | [p] -> - positions p >>| conts unit symbols' p - | _ -> - mk_TA' s m >> conts unit symbols' + ( + match m with + | [p] -> + positions p >>| conts unit symbols' p + | _ -> + mk_TA' s m >> conts unit symbols' ) >> build_a s l r )) >>| ( if List.mem s symbols then - begin match l with + begin match l with | [a] -> assert false | [a;b] -> build_a s [a] [b] (Unit unit) - | _ -> + | _ -> (* on ne construit que les elements interieurs, d'ou la disymetrie *) (Positions.a l >> @@ -884,14 +884,14 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m = end else fail () ) - - | TSym (s,l) -> - tri_fold (fun acc l t r -> + + | TSym (s,l) -> + tri_fold (fun acc l t r -> ((positions t) >> (fun (p) -> - let l = List.map t_of_term l in - let r = List.map t_of_term r in - return (Sym (s, Array.of_list (List.rev_append l (p::r)))) )) + let l = List.map t_of_term l in + let r = List.map t_of_term r in + return (Sym (s, Array.of_list (List.rev_append l (p::r)))) )) >>| ( conts unit symbols t >> @@ -899,23 +899,23 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m = let l = List.map t_of_term l in let r = List.map t_of_term r in return (Sym (s, Array.of_list (List.rev_append l (p::r)))) ) - ) + ) >>| acc ) l (fail()) - | TVar x -> assert false + | TVar x -> assert false | TUnit x when x = unit -> return (Unit unit) | TUnit x as t -> conts unit symbols t - in - (positions t - >>| - (match t with + in + (positions t + >>| + (match t with | TSym _ -> conts unit symbols t | TAC (s,l) -> conts unit symbols t | TA (s,l) -> conts unit symbols t | _ -> fail()) ) >> fun (p) -> return (Terms.size p,p,return Subst.empty) - + @@ -923,10 +923,10 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m = (* Matching *) (************) - + (** {!matching} is the generic matching judgement. Each time a - non-deterministic split is made, we have to come back to this one. + non-deterministic split is made, we have to come back to this one. {!matchingSym} is used to match two applications that have the same (free) head-symbol. @@ -942,42 +942,42 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m = *) -let matching = - let rec matching env (p : nf_term) (t: nf_term) : Subst.t AAC_search_monad.m= - match p with - | TAC (s,l) -> - let l = linear l in - matchingAC env s l (get_AC s t) +let matching = + let rec matching env (p : nf_term) (t: nf_term) : Subst.t AAC_search_monad.m= + match p with + | TAC (s,l) -> + let l = linear l in + matchingAC env s l (get_AC s t) | TA (s,l) -> - matchingA env s l (get_A s t) - | TSym (s,l) -> - (get_Sym s t) + matchingA env s l (get_A s t) + | TSym (s,l) -> + (get_Sym s t) >> (fun t -> matchingSym env l t) - | TVar x -> - begin match Subst.find env x with + | TVar x -> + begin match Subst.find env x with | None -> return (Subst.add env x t) | Some v -> if nf_equal v t then return env else fail () end - | TUnit s -> + | TUnit s -> if nf_equal p t then return env else fail () and - matchingAC (env : Subst.t) (current : symbol) (l : nf_term list) (t : (nf_term *int) list) = - match l with - | TSym (s,v):: q -> - pick_sym s t - >> (fun (v',t') -> - matchingSym env v v' + matchingAC (env : Subst.t) (current : symbol) (l : nf_term list) (t : (nf_term *int) list) = + match l with + | TSym (s,v):: q -> + pick_sym s t + >> (fun (v',t') -> + matchingSym env v v' >> (fun env -> matchingAC env current q t')) - | TAC (s,v)::q when s = current -> + | TAC (s,v)::q when s = current -> assert false | TVar x:: q -> (* This is an optimization *) - begin match Subst.find env x with - | None -> - (var_ac_nondet_split current env x t) + begin match Subst.find env x with + | None -> + (var_ac_nondet_split current env x t) >> (fun (env,residual) -> matchingAC env current q residual) - | Some v -> - (factor_AC current v t) + | Some v -> + (factor_AC current v t) >> (fun residual -> matchingAC env current q residual) end | TUnit s as v :: q -> (* this is an optimization *) @@ -985,7 +985,7 @@ let matching = (fun residual -> matchingAC env current q residual) | h :: q ->(* PAC =/= curent or PA or unit for this symbol*) (ac_nondet_split current t) - >> + >> (fun (t,right) -> matching env h t >> @@ -993,54 +993,54 @@ let matching = fun env -> matchingAC env current q right ) - ) - | [] -> if t = [] then return env else fail () + ) + | [] -> if t = [] then return env else fail () and matchingA (env : Subst.t) (current : symbol) (l : nf_term list) (t : nf_term list) = - match l with + match l with | TSym (s,v) :: l -> - begin match t with - | TSym (s',v') :: r when s = s' -> - (matchingSym env v v') + begin match t with + | TSym (s',v') :: r when s = s' -> + (matchingSym env v v') >> (fun env -> matchingA env current l r) | _ -> fail () end | TA (s,v) :: l when s = current -> assert false | TVar x :: l -> - begin match Subst.find env x with - | None -> - debug (Printf.sprintf "var %i (%s)" x + begin match Subst.find env x with + | None -> + debug (Printf.sprintf "var %i (%s)" x (let b = Buffer.create 21 in List.iter (fun t -> Buffer.add_string b ( Terms.sprint_nf_term t)) t; Buffer.contents b )); - var_a_nondet_split env current x t - >> (fun (env,residual)-> debug (Printf.sprintf "pl %i %i" x(List.length residual)); matchingA env current l residual) - | Some v -> - (left_factor current v t) + var_a_nondet_split env current x t + >> (fun (env,residual)-> debug (Printf.sprintf "pl %i %i" x(List.length residual)); matchingA env current l residual) + | Some v -> + (left_factor current v t) >> (fun residual -> matchingA env current l residual) end | TUnit s as v :: q -> (* this is an optimization *) (left_factor current v t) >> (fun residual -> matchingA env current q residual) | h :: l -> - a_nondet_split current t - >> (fun (t,r) -> + a_nondet_split current t + >> (fun (t,r) -> matching env h t >> (fun env -> matchingA env current l r) ) | [] -> if t = [] then return env else fail () and matchingSym (env : Subst.t) (l : nf_term list) (t : nf_term list) = - List.fold_left2 + List.fold_left2 (fun acc p t -> acc >> (fun env -> matching env p t)) - (return env) - l + (return env) + l t - in - fun env l r -> - let _ = debug (Printf.sprintf "pattern :%s\nterm :%s\n%!" (Terms.sprint_nf_term l) (Terms.sprint_nf_term r)) in - let m = matching env l r in - let _ = debug (Printf.sprintf "count %i" (AAC_search_monad.count m)) in + in + fun env l r -> + let _ = debug (Printf.sprintf "pattern :%s\nterm :%s\n%!" (Terms.sprint_nf_term l) (Terms.sprint_nf_term r)) in + let m = matching env l r in + let _ = debug (Printf.sprintf "count %i" (AAC_search_monad.count m)) in m @@ -1060,11 +1060,11 @@ let matching = {!subterm_AC}, {!subterm_A} to find the matching subterm, making non-deterministic choices to split the term into a context and an intersting sub-term. Intuitively, the only case in which we have to - go in depth is when we are left with a sub-term that is atomic. + go in depth is when we are left with a sub-term that is atomic. Indeed, rewriting [H: b = c |- a+b+a = a+a+c], we do not want to find recursively the sub-terms of [a+b] and [b+a], since they will - overlap with the sub-terms of [a+b+a]. + overlap with the sub-terms of [a+b+a]. We rebuild the context on the fly, leaving the variables in the pattern uninstantiated. We do so in order to allow interaction @@ -1086,65 +1086,65 @@ let return_non_empty raw_p m = let subterm (raw_p:t) (raw_t:t): (int * t * Subst.t m) m= let _ = debug (String.make 40 '=') in - let p = term_of_t units raw_p in - let t = term_of_t units raw_t in - let _ = + let p = term_of_t units raw_p in + let t = term_of_t units raw_t in + let _ = if nullifiable p - then - Pp.msg_warning + then + Pp.msg_warning (Pp.str "[aac_tactics] This pattern might be nullifiable, some solutions can be missing"); in - let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in - let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in - let filter_right current right (p,m) = - if right = [] - then return (p,m) - else + let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in + let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in + let filter_right current right (p,m) = + if right = [] + then return (p,m) + else mk_TAC' current right >> fun t -> return (Plus (current,p,t_of_term t),m) in let filter_middle current left right (p,m) = let right_pat p = - if right = [] - then return p + if right = [] + then return p else - mk_TA' current right >> + mk_TA' current right >> fun t -> return (Dot (current,p,t_of_term t)) in let left_pat p= - if left = [] - then return p + if left = [] + then return p else - mk_TA' current left >> + mk_TA' current left >> fun t -> return (Dot (current,t_of_term t,p)) - in + in right_pat p >> left_pat >> (fun p -> return (p,m)) in let rec subterm (t:nf_term) : (t * Subst.t m) m= - match t with + match t with | TAC (s,l) -> ((ac_nondet_split_raw l) >> (fun (left,right) -> (subterm_AC s left) >> (filter_right s right) )) - | TA (s,l) -> - (a_nondet_middle l) >> + | TA (s,l) -> + (a_nondet_middle l) >> (fun (left, middle, right) -> (subterm_A s middle) >> (filter_middle s left right) ) - | TSym (s, l) -> - let init = - return_non_empty raw_p (matching Subst.empty p t) - in - tri_fold (fun acc l t r -> + | TSym (s, l) -> + let init = + return_non_empty raw_p (matching Subst.empty p t) + in + tri_fold (fun acc l t r -> ((subterm t) >> (fun (p,m) -> - let l = List.map t_of_term l in - let r = List.map t_of_term r in - let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in + let l = List.map t_of_term l in + let r = List.map t_of_term r in + let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in return (p,m) )) >>| acc ) l init @@ -1152,21 +1152,21 @@ let subterm (raw_p:t) (raw_t:t): (int * t * Subst.t m) m= | TUnit s -> fail () and subterm_AC s tl = - match tl with + match tl with [x,1] -> subterm x - | _ -> + | _ -> mk_TAC' s tl >> fun t -> return_non_empty raw_p (matching Subst.empty p t) and subterm_A s tl = - match tl with + match tl with [x] -> subterm x - | _ -> - mk_TA' s tl >> + | _ -> + mk_TA' s tl >> fun t -> return_non_empty raw_p (matching Subst.empty p t) - in - match p with - | TUnit x -> + in + match p with + | TUnit x -> unit_subterm t x | _ -> (subterm t >> fun (p,m) -> return (Terms.size p,p,m)) @@ -1175,32 +1175,32 @@ let subterm (raw_p:t) (raw_t:t): (int * t * Subst.t m) m= (* The functions we export, handlers for the previous ones. Some debug information also *) let subterm ?(strict = false) units raw t = - let module M = M (struct - let is_ac = units.is_ac - let units = units.unit_for + let module M = M (struct + let is_ac = units.is_ac + let units = units.unit_for let strict = strict - end) in + end) in let sols = time (M.subterm raw) t "%fs spent in subterm (including matching)\n" in - debug - (Printf.sprintf "%i possible solution(s)\n" - (AAC_search_monad.fold (fun (_,_,envm) acc -> count envm + acc) sols 0)); + debug + (Printf.sprintf "%i possible solution(s)\n" + (AAC_search_monad.fold (fun (_,_,envm) acc -> count envm + acc) sols 0)); sols -let matcher ?(strict = false) units p t = - let module M = M (struct - let is_ac = units.is_ac - let units = units.unit_for +let matcher ?(strict = false) units p t = + let module M = M (struct + let is_ac = units.is_ac + let units = units.unit_for let strict = false - end) in + end) in let units = units.unit_for in - let sols = time - (fun (p,t) -> - let p = (Terms.term_of_t units p) in - let t = (Terms.term_of_t units t) in - M.matching Subst.empty p t) (p,t) + let sols = time + (fun (p,t) -> + let p = (Terms.term_of_t units p) in + let t = (Terms.term_of_t units t) in + M.matching Subst.empty p t) (p,t) "%fs spent in the matcher\n" - in + in debug (Printf.sprintf "%i solutions\n" (count sols)); sols diff --git a/AAC_matcher.mli b/AAC_matcher.mli index 531a2cf..896a2a9 100644 --- a/AAC_matcher.mli +++ b/AAC_matcher.mli @@ -21,7 +21,7 @@ function {!matcher} is limited to top-level matching, that is, the subject must make a perfect match against the pattern ([x+x] does not match [a+a+b] ). - + We use a search monad {!AAC_search_monad} to perform non-deterministic choices in an almost transparent way. @@ -30,7 +30,7 @@ gives a solution to the aforementioned case ([x+x] against [a+b+a]). - On a slightly more involved level : + On a slightly more involved level : - it must be noted that we allow several AC/A operators to share the same units, but that a given AC/A operator can have at most one unit. @@ -42,7 +42,7 @@ of the term increase (by making neutral elements appear in a layered fashion). Hence, in this case, a warning is issued, and some solutions are omitted. - + *) (** {2 Utility functions} *) @@ -57,9 +57,9 @@ type var = int and that operations can share a unit). *) type units =(symbol * symbol) list (* from AC/A symbols to the unit *) -type ext_units = +type ext_units = { - unit_for : units; (* from AC/A symbols to the unit *) + unit_for : units; (* from AC/A symbols to the unit *) is_ac : (symbol * bool) list } @@ -73,7 +73,7 @@ val linear : 'a mset -> 'a list (** Representations of expressions - The module {!Terms} defines two different types for expressions. + The module {!Terms} defines two different types for expressions. - a public type {!Terms.t} that represents abstract syntax trees of expressions with binary associative and commutative operators - a private type {!Terms.nf_term}, corresponding to a canonical @@ -97,8 +97,8 @@ sig by the following value [Sym(0,[| Dot(1, Sym(2,[||]), Sym(3,[||])); Dot(4, Sym(2,[||]), Sym(5,[|Sym(3,[||])|])) |])] - where the implicit symbol environment associates - [f] to [0], [(^)] to [1], [a] to [2], [b] to [3], [( * )] to [4], and [g] to [5], + where the implicit symbol environment associates + [f] to [0], [(^)] to [1], [a] to [2], [b] to [3], [( * )] to [4], and [g] to [5], Accordingly, the following value, that contains "variables" [Sym(0,[| Dot(1, Var x, Unit (1); Dot(4, Var x, @@ -120,18 +120,18 @@ sig (** {2 Normalised terms (canonical representation) } - + A term in normal form is the canonical representative of the equivalence class of all the terms that are equal modulo AACU. This representation is only used internally; it is exported here for the sake of completeness *) - type nf_term + type nf_term (** {3 Comparisons} *) val nf_term_compare : nf_term -> nf_term -> int - val nf_equal : nf_term -> nf_term -> bool + val nf_equal : nf_term -> nf_term -> bool (** {3 Printing function} *) @@ -141,8 +141,8 @@ sig (** we have the following property: [a] and [b] are equal modulo AACU iif [nf_equal (term_of_t a) (term_of_t b) = true] *) - val term_of_t : units -> t -> nf_term - val t_of_term : nf_term -> t + val term_of_t : units -> t -> nf_term + val t_of_term : nf_term -> t end @@ -152,11 +152,11 @@ end The module {!Subst} contains infrastructure to deal with substitutions, i.e., functions from variables to terms. Only a restricted subsets of these functions need to be exported. - + As expected, a particular substitution can be used to instantiate a pattern. *) -module Subst : +module Subst : sig type t val sprint : t -> string @@ -179,11 +179,11 @@ val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t AAC_sea (** [subterm p t] computes a set of solutions to the given subterm-matching problem. - + Return a collection of possible solutions (each with the associated depth, the context, and the solutions of the matching problem). The context is actually a {!Terms.t} where the variables are yet to be instantiated by one of the associated substitutions *) -val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t AAC_search_monad.m) AAC_search_monad.m +val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t AAC_search_monad.m) AAC_search_monad.m diff --git a/AAC_print.ml b/AAC_print.ml index e9c4b48..512efa3 100644 --- a/AAC_print.ml +++ b/AAC_print.ml @@ -11,35 +11,35 @@ open Pp open AAC_matcher type named_env = (Names.name * Terms.t) list - + (** {pp_env} prints a substitution mapping names to terms, using the provided printer *) let pp_env pt : named_env -> Pp.std_ppcmds = fun env -> - List.fold_left + List.fold_left (fun acc (v,t) -> begin match v with | Names.Name s -> str (Printf.sprintf "%s: " (Names.string_of_id s)) | Names.Anonymous -> str ("_") end ++ pt t ++ str "; " ++ acc - ) + ) (str "") env - + (** {pp_envm} prints a collection of possible environments, and number them. This number must remain compatible with the parameters given to {!aac_rewrite} *) let pp_envm pt : named_env AAC_search_monad.m -> Pp.std_ppcmds = fun m -> - let _,s = - AAC_search_monad.fold - (fun env (n,acc) -> + let _,s = + AAC_search_monad.fold + (fun env (n,acc) -> n+1, h 0 (str (Printf.sprintf "%i:\t[" n) ++pp_env pt env ++ str "]") ++ fnl () :: acc - ) m (0,[]) - in + ) m (0,[]) + in List.fold_left (fun acc s -> s ++ acc) (str "") (s) - + let trivial_substitution envm = match AAC_search_monad.choose envm with | None -> true (* assert false *) @@ -49,16 +49,16 @@ let trivial_substitution envm = possibles substitutions, giving a number to each. This number must remain compatible with the parameters of {!aac_rewrite} *) let pp_all pt : (int * Terms.t * named_env AAC_search_monad.m) AAC_search_monad.m -> Pp.std_ppcmds = fun m -> - let _,s = AAC_search_monad.fold - (fun (size,context,envm) (n,acc) -> - let s = str (Printf.sprintf "occurence %i: transitivity through " n) in - let s = s ++ pt context ++ str "\n" in - let s = if trivial_substitution envm then s else + let _,s = AAC_search_monad.fold + (fun (size,context,envm) (n,acc) -> + let s = str (Printf.sprintf "occurence %i: transitivity through " n) in + let s = s ++ pt context ++ str "\n" in + let s = if trivial_substitution envm then s else s ++ str (Printf.sprintf "%i possible(s) substitution(s)" (AAC_search_monad.count envm) ) - ++ fnl () ++ pp_envm pt envm - in + ++ fnl () ++ pp_envm pt envm + in n+1, s::acc - ) m (0,[]) in + ) m (0,[]) in List.fold_left (fun acc s -> s ++ str "\n" ++ acc) (str "") (s) (** The main printing function. {!print} uses the debruijn_env the @@ -66,35 +66,35 @@ rename the variables, and rebuilds raw Coq terms (for the context, and the terms in the environment). In order to do so, it requires the information gathered by the {!AAC_theory.Trans} module.*) let print rlt ir m (context : Term.rel_context) goal = - if AAC_search_monad.count m = 0 + if AAC_search_monad.count m = 0 then ( Tacticals.tclFAIL 0 (Pp.str "No subterm modulo AC") goal ) else - let _ = Pp.msgnl (Pp.str "All solutions:") in - let m = AAC_search_monad.(>>) m - (fun (i,t,envm) -> + let _ = Pp.msgnl (Pp.str "All solutions:") in + let m = AAC_search_monad.(>>) m + (fun (i,t,envm) -> let envm = AAC_search_monad.(>>) envm ( fun env -> - let l = AAC_matcher.Subst.to_list env in - let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in - let l = - List.map (fun (v,t) -> - let (name,body,types) = Term.lookup_rel v context in + let l = AAC_matcher.Subst.to_list env in + let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in + let l = + List.map (fun (v,t) -> + let (name,body,types) = Term.lookup_rel v context in (name,t) - ) l - in + ) l + in AAC_search_monad.return l - ) + ) in AAC_search_monad.return (i,t,envm) ) in - let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in - let _ = Pp.msgnl - (pp_all + let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in + let _ = Pp.msgnl + (pp_all (fun t -> Printer.pr_constr (AAC_theory.Trans.raw_constr_of_t ir rlt context t) ) m - ) - in + ) + in Tacticals.tclIDTAC goal - + diff --git a/AAC_print.mli b/AAC_print.mli index 6cd41c5..bacd806 100644 --- a/AAC_print.mli +++ b/AAC_print.mli @@ -14,10 +14,10 @@ to rename the variables, and rebuilds raw Coq terms (for the given context, and the terms in the environment). In order to do so, it requires the information gathered by the {!AAC_theory.Trans} module.*) -val print : +val print : AAC_coq.Relation.t -> AAC_theory.Trans.ir -> (int * AAC_matcher.Terms.t * AAC_matcher.Subst.t AAC_search_monad.m) AAC_search_monad.m -> - Term.rel_context -> + Term.rel_context -> Proof_type.tactic diff --git a/AAC_rewrite.ml b/AAC_rewrite.ml index bdba9cb..be286f9 100644 --- a/AAC_rewrite.ml +++ b/AAC_rewrite.ml @@ -9,20 +9,20 @@ (** aac_rewrite -- rewriting modulo *) -module Control = struct +module Control = struct let debug = false let printing = false let time = false end -module Debug = AAC_helper.Debug (Control) +module Debug = AAC_helper.Debug (Control) open Debug let time_tac msg tac = if Control.time then AAC_coq.tclTIME msg tac else tac -let tac_or_exn tac exn msg = fun gl -> - try tac gl with e -> +let tac_or_exn tac exn msg = fun gl -> + try tac gl with e -> pr_constr "last goal" (Tacmach.pf_concl gl); exn msg e @@ -37,7 +37,7 @@ module M = AAC_matcher open Term open Names open Coqlib -open Proof_type +open Proof_type (** The various kind of relation we can encounter, as a hierarchy *) type rew_relation = @@ -46,12 +46,12 @@ type rew_relation = | Equivalence of AAC_coq.Equivalence.t (** {!promote try to go higher in the aforementionned hierarchy} *) -let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = - try AAC_coq.Equivalence.cps_from_relation rlt +let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = + try AAC_coq.Equivalence.cps_from_relation rlt (fun e -> k (Equivalence e)) with - | Not_found -> - begin + | Not_found -> + begin try AAC_coq.Transitive.cps_from_relation rlt (fun trans -> k (Transitive trans)) with @@ -61,13 +61,13 @@ let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = (* Various situations: - p == q |- left == right : rewrite <- -> - p <= q |- left <= right : rewrite -> + p == q |- left == right : rewrite <- -> + p <= q |- left <= right : rewrite -> p <= q |- left == right : failure p == q |- left <= right : rewrite <- -> - + Not handled - p <= q |- left >= right : failure + p <= q |- left >= right : failure *) (** aac_lift : the ideal type beyond AAC.v/AAC_lift @@ -78,15 +78,15 @@ let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = lift connects the two things *) type aac_lift = { - r : AAC_coq.Relation.t; + r : AAC_coq.Relation.t; e : AAC_coq.Equivalence.t; - lift : Term.constr + lift : Term.constr } - + type rewinfo = { hypinfo : AAC_coq.Rewrite.hypinfo; - + in_left : bool; (** are we rewriting in the left hand-sie of the goal *) pattern : constr; subject : constr; @@ -97,9 +97,9 @@ type rewinfo = } let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic = - AAC_coq.cps_evar_relation rlt.AAC_coq.Relation.carrier (fun e -> - let lift_ty = - mkApp (Lazy.force AAC_theory.Stubs.lift, + AAC_coq.cps_evar_relation rlt.AAC_coq.Relation.carrier (fun e -> + let lift_ty = + mkApp (Lazy.force AAC_theory.Stubs.lift, [| rlt.AAC_coq.Relation.carrier; rlt.AAC_coq.Relation.r; @@ -107,11 +107,11 @@ let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tac |] ) in AAC_coq.cps_resolve_one_typeclass ~error:"Cannot infer a lifting" - lift_ty (fun lift goal -> - let x = rlt.AAC_coq.Relation.carrier in - let r = rlt.AAC_coq.Relation.r in - let eq = (AAC_coq.nf_evar goal e) in - let equiv = AAC_coq.lapp AAC_theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in + lift_ty (fun lift goal -> + let x = rlt.AAC_coq.Relation.carrier in + let r = rlt.AAC_coq.Relation.r in + let eq = (AAC_coq.nf_evar goal e) in + let equiv = AAC_coq.lapp AAC_theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in let lift = { r = rlt; @@ -120,14 +120,14 @@ let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tac } in k ~lift:lift goal - )) - + )) + (** Builds a rewinfo, once and for all *) -let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic= +let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic= let l2r = hypinfo.AAC_coq.Rewrite.l2r in - infer_lifting rlt + infer_lifting rlt (fun ~lift -> - let eq = lift.e in + let eq = lift.e in k { hypinfo = hypinfo; in_left = in_left; @@ -137,10 +137,10 @@ let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) eqt = eq; lifting = lift; rlt = rlt - } + } ) - - + + (** {1 Tactics} *) @@ -148,34 +148,34 @@ let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) (** Build the reifiers, the reified terms, and the evaluation fonction *) let handle eqt zero envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) k = - let (x,r,_) = AAC_coq.Equivalence.split eqt in - AAC_theory.Trans.mk_reifier (AAC_coq.Equivalence.to_relation eqt) zero envs - (fun (maps, reifier) -> + let (x,r,_) = AAC_coq.Equivalence.split eqt in + AAC_theory.Trans.mk_reifier (AAC_coq.Equivalence.to_relation eqt) zero envs + (fun (maps, reifier) -> (* fold through a term and reify *) - let t = AAC_theory.Trans.reif_constr_of_t reifier t in + let t = AAC_theory.Trans.reif_constr_of_t reifier t in let t' = AAC_theory.Trans.reif_constr_of_t reifier t' in (* Some letins *) let eval = (mkApp (Lazy.force AAC_theory.Stubs.eval, [|x;r; maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units|])) in - + AAC_coq.cps_mk_letin "eval" eval (fun eval -> - AAC_coq.cps_mk_letin "left" t (fun t -> - AAC_coq.cps_mk_letin "right" t' (fun t' -> + AAC_coq.cps_mk_letin "left" t (fun t -> + AAC_coq.cps_mk_letin "right" t' (fun t' -> k maps eval t t')))) (** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that - is merely a proof of equality of two terms modulo AAC *) + is merely a proof of equality of two terms modulo AAC *) let by_aac_reflexivity zero eqt envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) : Proof_type.tactic = - handle eqt zero envs t t' + handle eqt zero envs t t' (fun maps eval t t' -> - let (x,r,e) = AAC_coq.Equivalence.split eqt in + let (x,r,e) = AAC_coq.Equivalence.split eqt in let decision_thm = AAC_coq.lapp AAC_theory.Stubs.decide_thm - [|x;r;e; - maps.AAC_theory.Trans.env_sym; + [|x;r;e; + maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units; t;t'; - |] + |] in (* This convert is required to deal with evars in a proper way *) @@ -193,20 +193,20 @@ let by_aac_reflexivity zero ) let by_aac_normalise zero lift ir t t' = - let eqt = lift.e in - let rlt = lift.r in - handle eqt zero ir t t' - (fun maps eval t t' -> - let (x,r,e) = AAC_coq.Equivalence.split eqt in + let eqt = lift.e in + let rlt = lift.r in + handle eqt zero ir t t' + (fun maps eval t t' -> + let (x,r,e) = AAC_coq.Equivalence.split eqt in let normalise_thm = AAC_coq.lapp AAC_theory.Stubs.lift_normalise_thm - [|x;r;e; - maps.AAC_theory.Trans.env_sym; + [|x;r;e; + maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units; rlt.AAC_coq.Relation.r; lift.lift; t;t'; - |] + |] in (* This convert is required to deal with evars in a proper way *) @@ -223,37 +223,36 @@ let by_aac_normalise zero lift ir t t' = (** A handler tactic, that reifies the goal, and infer the liftings, and then call its continuation *) -let aac_conclude - (k : Term.constr -> aac_lift -> AAC_theory.Trans.ir -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) = fun goal -> +let aac_conclude + (k : Term.constr -> aac_lift -> AAC_theory.Trans.ir -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) = fun goal -> - let (equation : Term.types) = Tacmach.pf_concl goal in - let envs = AAC_theory.Trans.empty_envs () in - let left, right,r = + let (equation : Term.types) = Tacmach.pf_concl goal in + let envs = AAC_theory.Trans.empty_envs () in + let left, right,r = match AAC_coq.match_as_equation goal equation with | None -> AAC_coq.user_error "The goal is not an applied relation" - | Some x -> x in - try infer_lifting r + | Some x -> x in + try infer_lifting r (fun ~lift goal -> - let eq = AAC_coq.Equivalence.to_relation lift.e in - let tleft,tright, goal = AAC_theory.Trans.t_of_constr goal eq envs (left,right) in - let goal, ir = AAC_theory.Trans.ir_of_envs goal eq envs in - let concl = Tacmach.pf_concl goal in - let _ = pr_constr "concl "concl in - let evar_map = Tacmach.project goal in + let eq = AAC_coq.Equivalence.to_relation lift.e in + let tleft,tright, goal = AAC_theory.Trans.t_of_constr goal eq envs (left,right) in + let goal, ir = AAC_theory.Trans.ir_of_envs goal eq envs in + let concl = Tacmach.pf_concl goal in + let _ = pr_constr "concl "concl in + let evar_map = Tacmach.project goal in Tacticals.tclTHEN (Refiner.tclEVARS evar_map) (k left lift ir tleft tright) - goal - )goal - with + goal + )goal + with | Not_found -> AAC_coq.user_error "No lifting from the goal's relation to an equivalence" -open Libnames +open Libnames open Tacinterp -open Q_coqast -let aac_normalise = fun goal -> - let ids = Tacmach.pf_ids_of_hyps goal in +let aac_normalise = fun goal -> + let ids = Tacmach.pf_ids_of_hyps goal in Tacticals.tclTHENLIST [ aac_conclude by_aac_normalise; @@ -271,17 +270,17 @@ let aac_normalise = fun goal -> Tactics.keep ids ] goal -let aac_reflexivity = fun goal -> - aac_conclude - (fun zero lift ir t t' -> - let x,r = AAC_coq.Relation.split (lift.r) in - let r_reflexive = (AAC_coq.Classes.mk_reflexive x r) in - AAC_coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive" +let aac_reflexivity = fun goal -> + aac_conclude + (fun zero lift ir t t' -> + let x,r = AAC_coq.Relation.split (lift.r) in + let r_reflexive = (AAC_coq.Classes.mk_reflexive x r) in + AAC_coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive" r_reflexive (fun reflexive -> - let lift_reflexivity = - mkApp (Lazy.force (AAC_theory.Stubs.lift_reflexivity), - [| + let lift_reflexivity = + mkApp (Lazy.force (AAC_theory.Stubs.lift_reflexivity), + [| x; r; lift.e.AAC_coq.Equivalence.eq; @@ -291,33 +290,33 @@ let aac_reflexivity = fun goal -> in Tacticals.tclTHEN (Tactics.apply lift_reflexivity) - (fun goal -> - let concl = Tacmach.pf_concl goal in - let _ = pr_constr "concl "concl in + (fun goal -> + let concl = Tacmach.pf_concl goal in + let _ = pr_constr "concl "concl in by_aac_reflexivity zero lift.e ir t t' goal) ) ) goal (** A sub-tactic to lift the rewriting using AAC_lift *) -let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq.Equivalence.t): tactic = +let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq.Equivalence.t): tactic = fun goal -> (* catch the equation and the two members*) - let concl = Tacmach.pf_concl goal in - let (left, right, _ ) = match AAC_coq.match_as_equation goal concl with + let concl = Tacmach.pf_concl goal in + let (left, right, _ ) = match AAC_coq.match_as_equation goal concl with | Some x -> x | None -> AAC_coq.user_error "The goal is not an equation" - in - let lift_transitivity = - let thm = - if in_left + in + let lift_transitivity = + let thm = + if in_left then Lazy.force AAC_theory.Stubs.lift_transitivity_left else Lazy.force AAC_theory.Stubs.lift_transitivity_right in - mkApp (thm, - [| - preorder.AAC_coq.Relation.carrier; + mkApp (thm, + [| + preorder.AAC_coq.Relation.carrier; preorder.AAC_coq.Relation.r; using_eq.AAC_coq.Equivalence.eq; lifting; @@ -326,7 +325,7 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq right; |]) in - Tacticals.tclTHENLIST + Tacticals.tclTHENLIST [ Tactics.apply lift_transitivity ] goal @@ -334,19 +333,19 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq (** The core tactic for aac_rewrite *) let core_aac_rewrite ?abort - rewinfo + rewinfo subst (by_aac_reflexivity : AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) - (tr : constr) t left : tactic = - pr_constr "transitivity through" tr; + (tr : constr) t left : tactic = + pr_constr "transitivity through" tr; let tran_tac = lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt in - AAC_coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> + AAC_coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> Tacticals.tclTHENSV (tac_or_exn (tran_tac) AAC_coq.anomaly "Unable to make the transitivity step") ( - if rewinfo.in_left + if rewinfo.in_left then [| by_aac_reflexivity left t ; rew |] else [| by_aac_reflexivity t left ; rew |] ) @@ -355,23 +354,23 @@ let core_aac_rewrite ?abort exception NoSolutions -(** Choose a substitution from a +(** Choose a substitution from a [(int * Terms.t * Env.env AAC_search_monad.m) AAC_search_monad.m ] *) (* WARNING: Beware, since the printing function can change the order of the printed monad, this function has to be updated accordingly *) let choose_subst subterm sol m= - try - let (depth,pat,envm) = match subterm with + try + let (depth,pat,envm) = match subterm with | None -> (* first solution *) - List.nth ( List.rev (AAC_search_monad.to_list m)) 0 - | Some x -> - List.nth ( List.rev (AAC_search_monad.to_list m)) x - in - let env = match sol with + List.nth ( List.rev (AAC_search_monad.to_list m)) 0 + | Some x -> + List.nth ( List.rev (AAC_search_monad.to_list m)) x + in + let env = match sol with None -> List.nth ( (AAC_search_monad.to_list envm)) 0 - | Some x -> List.nth ( (AAC_search_monad.to_list envm)) x - in + | Some x -> List.nth ( (AAC_search_monad.to_list envm)) x + in pat, env with | _ -> raise NoSolutions @@ -379,66 +378,66 @@ let choose_subst subterm sol m= (** rewrite the constr modulo AC from left to right in the left member of the goal *) let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ~occ_subterm ~occ_sol ?extra : Proof_type.tactic = fun goal -> - let envs = AAC_theory.Trans.empty_envs () in - let (concl : Term.types) = Tacmach.pf_concl goal in + let envs = AAC_theory.Trans.empty_envs () in + let (concl : Term.types) = Tacmach.pf_concl goal in let (_,_,rlt) as concl = match AAC_coq.match_as_equation goal concl with | None -> AAC_coq.user_error "The goal is not an applied relation" - | Some (left, right, rlt) -> left,right,rlt + | Some (left, right, rlt) -> left,right,rlt in - let check_type x = + let check_type x = Tacmach.pf_conv_x goal x rlt.AAC_coq.Relation.carrier in AAC_coq.Rewrite.get_hypinfo rew ~l2r ?check_type:(Some check_type) (fun hypinfo -> dispatch in_left concl hypinfo ( - fun rewinfo -> - let goal = - match extra with - | Some t -> AAC_theory.Trans.add_symbol goal rewinfo.morph_rlt envs t + fun rewinfo -> + let goal = + match extra with + | Some t -> AAC_theory.Trans.add_symbol goal rewinfo.morph_rlt envs t | None -> goal in - let pattern, subject, goal = - AAC_theory.Trans.t_of_constr goal rewinfo.morph_rlt envs - (rewinfo.pattern , rewinfo.subject) - in - let goal, ir = AAC_theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in - - let units = AAC_theory.Trans.ir_to_units ir in - let m = AAC_matcher.subterm ?strict units pattern subject in + let pattern, subject, goal = + AAC_theory.Trans.t_of_constr goal rewinfo.morph_rlt envs + (rewinfo.pattern , rewinfo.subject) + in + let goal, ir = AAC_theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in + + let units = AAC_theory.Trans.ir_to_units ir in + let m = AAC_matcher.subterm ?strict units pattern subject in (* We sort the monad in increasing size of contet *) - let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in - + let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in + if show - then - AAC_print.print rewinfo.morph_rlt ir m (hypinfo.AAC_coq.Rewrite.context) + then + AAC_print.print rewinfo.morph_rlt ir m (hypinfo.AAC_coq.Rewrite.context) else - try - let pat,subst = choose_subst occ_subterm occ_sol m in - let tr_step = AAC_matcher.Subst.instantiate subst pat in - let tr_step_raw = AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in + try + let pat,subst = choose_subst occ_subterm occ_sol m in + let tr_step = AAC_matcher.Subst.instantiate subst pat in + let tr_step_raw = AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in - let conv = (AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.AAC_coq.Rewrite.context)) in + let conv = (AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.AAC_coq.Rewrite.context)) in let subst = AAC_matcher.Subst.to_list subst in - let subst = List.map (fun (x,y) -> x, conv y) subst in - let by_aac_reflexivity = (by_aac_reflexivity rewinfo.subject rewinfo.eqt ir) in - core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject - - with - | NoSolutions -> - Tacticals.tclFAIL 0 - (Pp.str (if occ_subterm = None && occ_sol = None - then "No matching occurence modulo AC found" - else "No such solution")) - ) + let subst = List.map (fun (x,y) -> x, conv y) subst in + let by_aac_reflexivity = (by_aac_reflexivity rewinfo.subject rewinfo.eqt ir) in + core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject + + with + | NoSolutions -> + Tacticals.tclFAIL 0 + (Pp.str (if occ_subterm = None && occ_sol = None + then "No matching occurence modulo AC found" + else "No such solution")) + ) ) goal open Rewrite open Tacmach -open Tacticals +open Tacticals open Tacexpr open Tacinterp open Extraargs @@ -454,19 +453,19 @@ let get k l = try Some (List.assoc k l) with Not_found -> None let get_lhs l = try List.assoc "in_right" l; false with Not_found -> true -let aac_rewrite ~args = +let aac_rewrite ~args = aac_rewrite ~occ_subterm:(get "at" args) ~occ_sol:(get "subst" args) ~in_left:(get_lhs args) -let pr_aac_args _ _ _ l = - List.fold_left +let pr_aac_args _ _ _ l = + List.fold_left (fun acc -> function | ("in_right" as s,_) -> Pp.(++) (Pp.str s) acc | (k,i) -> Pp.(++) (Pp.(++) (Pp.str k) (Pp.int i)) acc ) (Pp.str "") l -ARGUMENT EXTEND aac_args -TYPED AS ((string * int) list ) +ARGUMENT EXTEND aac_args +TYPED AS ((string * int) list ) PRINTED BY pr_aac_args | [ "at" integer(n) aac_args(q) ] -> [ add "at" n q ] | [ "subst" integer(n) aac_args(q) ] -> [ add "subst" n q ] @@ -475,12 +474,12 @@ PRINTED BY pr_aac_args END let pr_constro _ _ _ = fun b -> - match b with + match b with | None -> Pp.str "" | Some o -> Pp.str "<constr>" ARGUMENT EXTEND constro -TYPED AS (constr option) +TYPED AS (constr option) PRINTED BY pr_constro | [ "[" constr(c) "]" ] -> [ Some c ] | [ ] -> [ None ] @@ -498,7 +497,7 @@ TACTIC EXTEND _aac_rewrite_ | [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl ] END - + TACTIC EXTEND _aac_pattern_ | [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl ] @@ -513,7 +512,7 @@ TACTIC EXTEND _aacu_rewrite_ | [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl ] END - + TACTIC EXTEND _aacu_pattern_ | [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl ] diff --git a/AAC_search_monad.ml b/AAC_search_monad.ml index f5ea243..b7aabbd 100644 --- a/AAC_search_monad.ml +++ b/AAC_search_monad.ml @@ -8,32 +8,32 @@ type 'a m = | F of 'a | N of 'a m list - + let fold (f : 'a -> 'b -> 'b) (m : 'a m) (acc : 'b) = let rec aux acc = function F x -> f x acc - | N l -> + | N l -> (List.fold_left (fun acc x -> - match x with + match x with | (N []) -> acc | x -> aux acc x ) acc l) in aux acc m - -let rec (>>) : 'a m -> ('a -> 'b m) -> 'b m = + +let rec (>>) : 'a m -> ('a -> 'b m) -> 'b m = fun m f -> - match m with - | F x -> f x - | N l -> + match m with + | F x -> f x + | N l -> N (List.fold_left (fun acc x -> - match x with + match x with | (N []) -> acc | x -> (x >> f)::acc ) [] l) -let (>>|) (m : 'a m) (n :'a m) : 'a m = match (m,n) with +let (>>|) (m : 'a m) (n :'a m) : 'a m = match (m,n) with | N [],_ -> n | _,N [] -> m | F x, N l -> N (F x::l) @@ -41,11 +41,11 @@ let (>>|) (m : 'a m) (n :'a m) : 'a m = match (m,n) with | x,y -> N [x;y] let return : 'a -> 'a m = fun x -> F x -let fail : unit -> 'a m = fun () -> N [] +let fail : unit -> 'a m = fun () -> N [] let sprint f m = fold (fun x acc -> Printf.sprintf "%s\n%s" acc (f x)) m "" -let rec count = function +let rec count = function | F _ -> 1 | N l -> List.fold_left (fun acc x -> acc+count x) 0 l @@ -53,13 +53,13 @@ let opt_comb f x y = match x with None -> f y | _ -> x let rec choose = function | F x -> Some x - | N l -> List.fold_left (fun acc x -> + | N l -> List.fold_left (fun acc x -> opt_comb choose acc x ) None l let is_empty = fun x -> choose x = None let to_list m = (fold (fun x acc -> x::acc) m []) - + let sort f m = N (List.map (fun x -> F x) (List.sort f (to_list m))) diff --git a/AAC_search_monad.mli b/AAC_search_monad.mli index 048fa2c..093f9d9 100644 --- a/AAC_search_monad.mli +++ b/AAC_search_monad.mli @@ -14,7 +14,7 @@ *) (** A data type that represent a collection of ['a] *) -type 'a m +type 'a m (** {2 Monadic operations} *) diff --git a/AAC_theory.ml b/AAC_theory.ml index 3c26f1e..55b9e21 100644 --- a/AAC_theory.ml +++ b/AAC_theory.ml @@ -6,7 +6,7 @@ (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) -(** Constr from the theory of this particular development +(** Constr from the theory of this particular development The inner-working of this module is highly correlated with the particular structure of {b AAC.v}, therefore, it should @@ -26,15 +26,15 @@ open Debug (** {1 HMap : Specialized Hashtables based on constr} *) -module Hashed_constr = -struct - type t = constr - let equal = (=) +module Hashed_constr = +struct + type t = constr + let equal = (=) let hash = Hashtbl.hash end (* TODO module HMap = Hashtbl, du coup ? *) -module HMap = Hashtbl.Make Hashed_constr +module HMap = Hashtbl.Make(Hashed_constr) let ac_theory_path = ["AAC_tactics"; "AAC"] @@ -42,79 +42,79 @@ module Stubs = struct let path = ac_theory_path@["Internal"] (** The constants from the inductive type *) - let _Tty = lazy (AAC_coq.init_constant path "T") - let vTty = lazy (AAC_coq.init_constant path "vT") - - let rsum = lazy (AAC_coq.init_constant path "sum") - let rprd = lazy (AAC_coq.init_constant path "prd") - let rsym = lazy (AAC_coq.init_constant path "sym") - let runit = lazy (AAC_coq.init_constant path "unit") - - let vnil = lazy (AAC_coq.init_constant path "vnil") - let vcons = lazy (AAC_coq.init_constant path "vcons") + let _Tty = lazy (AAC_coq.init_constant path "T") + let vTty = lazy (AAC_coq.init_constant path "vT") + + let rsum = lazy (AAC_coq.init_constant path "sum") + let rprd = lazy (AAC_coq.init_constant path "prd") + let rsym = lazy (AAC_coq.init_constant path "sym") + let runit = lazy (AAC_coq.init_constant path "unit") + + let vnil = lazy (AAC_coq.init_constant path "vnil") + let vcons = lazy (AAC_coq.init_constant path "vcons") let eval = lazy (AAC_coq.init_constant path "eval") let decide_thm = lazy (AAC_coq.init_constant path "decide") let lift_normalise_thm = lazy (AAC_coq.init_constant path "lift_normalise") - let lift = + let lift = lazy (AAC_coq.init_constant ac_theory_path "AAC_lift") - let lift_proj_equivalence= + let lift_proj_equivalence= lazy (AAC_coq.init_constant ac_theory_path "aac_lift_equivalence") let lift_transitivity_left = lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_left") - let lift_transitivity_right = + let lift_transitivity_right = lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_right") - let lift_reflexivity = + let lift_reflexivity = lazy(AAC_coq.init_constant ac_theory_path "lift_reflexivity") end -module Classes = struct +module Classes = struct module Associative = struct - let path = ac_theory_path + let path = ac_theory_path let typ = lazy (AAC_coq.init_constant path "Associative") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = + let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; rlt.AAC_coq.Relation.r; value |] ) let infer goal rlt value = let ty = ty rlt value in - AAC_coq.resolve_one_typeclass goal ty + AAC_coq.resolve_one_typeclass goal ty end - + module Commutative = struct - let path = ac_theory_path + let path = ac_theory_path let typ = lazy (AAC_coq.init_constant path "Commutative") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = + let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; rlt.AAC_coq.Relation.r; value |] ) end - + module Proper = struct - let path = ac_theory_path @ ["Internal";"Sym"] - let typeof = lazy (AAC_coq.init_constant path "type_of") - let relof = lazy (AAC_coq.init_constant path "rel_of") + let path = ac_theory_path @ ["Internal";"Sym"] + let typeof = lazy (AAC_coq.init_constant path "type_of") + let relof = lazy (AAC_coq.init_constant path "rel_of") let mk_typeof : AAC_coq.Relation.t -> int -> constr = fun rlt n -> let x = rlt.AAC_coq.Relation.carrier in - mkApp (Lazy.force typeof, [| x ; AAC_coq.Nat.of_int n |]) + mkApp (Lazy.force typeof, [| x ; AAC_coq.Nat.of_int n |]) let mk_relof : AAC_coq.Relation.t -> int -> constr = fun rlt n -> - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force relof, [| x;r ; AAC_coq.Nat.of_int n |]) + let (x,r) = AAC_coq.Relation.split rlt in + mkApp (Lazy.force relof, [| x;r ; AAC_coq.Nat.of_int n |]) - let ty rlt op ar = - let typeof = mk_typeof rlt ar in - let relof = mk_relof rlt ar in - AAC_coq.Classes.mk_morphism typeof relof op + let ty rlt op ar = + let typeof = mk_typeof rlt ar in + let relof = mk_relof rlt ar in + AAC_coq.Classes.mk_morphism typeof relof op let infer goal rlt op ar = let ty = ty rlt op ar in AAC_coq.resolve_one_typeclass goal ty end - + module Unit = struct let path = ac_theory_path let typ = lazy (AAC_coq.init_constant path "Unit") @@ -125,7 +125,7 @@ module Classes = struct unit |] ) end - + end (* Non empty lists *) @@ -134,11 +134,11 @@ module NEList = struct let typ = lazy (AAC_coq.init_constant path "list") let nil = lazy (AAC_coq.init_constant path "nil") let cons = lazy (AAC_coq.init_constant path "cons") - let cons ty h t = + let cons ty h t = mkApp (Lazy.force cons, [| ty; h ; t |]) - let nil ty x = - (mkApp (Lazy.force nil, [| ty ; x|])) - let rec of_list ty = function + let nil ty x = + (mkApp (Lazy.force nil, [| ty ; x|])) + let rec of_list ty = function | [] -> invalid_arg "NELIST" | [x] -> nil ty x | t::q -> cons ty t (of_list ty q) @@ -148,16 +148,16 @@ module NEList = struct end (** a [mset] is a ('a * pos) list *) -let mk_mset ty (l : (constr * int) list) = - let pos = Lazy.force AAC_coq.Pos.typ in +let mk_mset ty (l : (constr * int) list) = + let pos = Lazy.force AAC_coq.Pos.typ in let pair (x : constr) (ar : int) = AAC_coq.Pair.of_pair ty pos (x, AAC_coq.Pos.of_int ar) in - let pair_ty = AAC_coq.lapp AAC_coq.Pair.typ [| ty ; pos|] in - let rec aux = function + let pair_ty = AAC_coq.lapp AAC_coq.Pair.typ [| ty ; pos|] in + let rec aux = function | [ ] -> assert false | [x,ar] -> NEList.nil pair_ty (pair x ar) - | (t,ar)::q -> NEList.cons pair_ty (pair t ar) (aux q) + | (t,ar)::q -> NEList.cons pair_ty (pair t ar) (aux q) in aux l @@ -166,31 +166,31 @@ module Sigma = struct let sigma_empty = lazy (AAC_coq.init_constant ac_theory_path "sigma_empty") let sigma_add = lazy (AAC_coq.init_constant ac_theory_path "sigma_add") let sigma_get = lazy (AAC_coq.init_constant ac_theory_path "sigma_get") - - let add ty n x map = + + let add ty n x map = mkApp (Lazy.force sigma_add,[|ty; n; x ; map|]) let empty ty = mkApp (Lazy.force sigma_empty,[|ty |]) - let typ ty = + let typ ty = mkApp (Lazy.force sigma, [|ty|]) - let to_fun ty null map = + let to_fun ty null map = mkApp (Lazy.force sigma_get, [|ty;null;map|]) let of_list ty null l = - match l with - | (_,t)::q -> + match l with + | (_,t)::q -> let map = - List.fold_left - (fun acc (i,t) -> + List.fold_left + (fun acc (i,t) -> assert (i > 0); - add ty (AAC_coq.Pos.of_int i) ( t) acc) + add ty (AAC_coq.Pos.of_int i) ( t) acc) (empty ty) q - in to_fun ty (t) map + in to_fun ty (t) map | [] -> debug "of_list empty" ; to_fun ty (null) (empty ty) - - + + end @@ -201,16 +201,16 @@ module Sym = struct let mkPack = lazy (AAC_coq.init_constant path "mkPack") let value = lazy (AAC_coq.init_constant path "value") let null = lazy (AAC_coq.init_constant path "null") - let mk_pack (rlt: AAC_coq.Relation.t) s = + let mk_pack (rlt: AAC_coq.Relation.t) s = let (x,r) = AAC_coq.Relation.split rlt in mkApp (Lazy.force mkPack, [|x;r; s.ar;s.value;s.morph|]) let null rlt = - let x = rlt.AAC_coq.Relation.carrier in - let r = rlt.AAC_coq.Relation.r in + let x = rlt.AAC_coq.Relation.carrier in + let r = rlt.AAC_coq.Relation.r in mkApp (Lazy.force null, [| x;r;|]) let mk_ty : AAC_coq.Relation.t -> constr = fun rlt -> - let (x,r) = AAC_coq.Relation.split rlt in + let (x,r) = AAC_coq.Relation.split rlt in mkApp (Lazy.force typ, [| x; r|] ) end @@ -224,29 +224,29 @@ module Bin =struct let path = ac_theory_path @ ["Internal";"Bin"] let typ = lazy (AAC_coq.init_constant path "pack") let mkPack = lazy (AAC_coq.init_constant path "mk_pack") - + let mk_pack: AAC_coq.Relation.t -> pack -> Term.constr = fun (rlt) s -> let (x,r) = AAC_coq.Relation.split rlt in - let comm_ty = Classes.Commutative.ty rlt s.value in - mkApp (Lazy.force mkPack , [| x ; r; - s.value; - s.compat ; - s.assoc; + let comm_ty = Classes.Commutative.ty rlt s.value in + mkApp (Lazy.force mkPack , [| x ; r; + s.value; + s.compat ; + s.assoc; AAC_coq.Option.of_option comm_ty s.comm |]) let mk_ty : AAC_coq.Relation.t -> constr = fun rlt -> - let (x,r) = AAC_coq.Relation.split rlt in + let (x,r) = AAC_coq.Relation.split rlt in mkApp (Lazy.force typ, [| x; r|] ) end - + module Unit = struct let path = ac_theory_path @ ["Internal"] let unit_of_ty = lazy (AAC_coq.init_constant path "unit_of") let unit_pack_ty = lazy (AAC_coq.init_constant path "unit_pack") let mk_unit_of = lazy (AAC_coq.init_constant path "mk_unit_for") let mk_unit_pack = lazy (AAC_coq.init_constant path "mk_unit_pack") - - type unit_of = + + type unit_of = { uf_u : Term.constr; (* u *) uf_idx : Term.constr; @@ -258,16 +258,16 @@ module Unit = struct u_desc : (unit_of) list (* unit_of u_value *) } - let ty_unit_of rlt e_bin u = + let ty_unit_of rlt e_bin u = let (x,r) = AAC_coq.Relation.split rlt in - mkApp ( Lazy.force unit_of_ty, [| x; r; e_bin; u |]) + mkApp ( Lazy.force unit_of_ty, [| x; r; e_bin; u |]) - let ty_unit_pack rlt e_bin = + let ty_unit_pack rlt e_bin = let (x,r) = AAC_coq.Relation.split rlt in mkApp (Lazy.force unit_pack_ty, [| x; r; e_bin |]) - + let mk_unit_of rlt e_bin u unit_of = - let (x,r) = AAC_coq.Relation.split rlt in + let (x,r) = AAC_coq.Relation.split rlt in mkApp (Lazy.force mk_unit_of , [| x; r; e_bin ; @@ -275,15 +275,15 @@ module Unit = struct unit_of.uf_idx; unit_of.uf_desc |]) - + let mk_pack rlt e_bin pack : Term.constr = let (x,r) = AAC_coq.Relation.split rlt in - let ty = ty_unit_of rlt e_bin pack.u_value in - let mk_unit_of = mk_unit_of rlt e_bin pack.u_value in + let ty = ty_unit_of rlt e_bin pack.u_value in + let mk_unit_of = mk_unit_of rlt e_bin pack.u_value in let u_desc =AAC_coq.List.of_list ( ty ) (List.map mk_unit_of pack.u_desc) in - mkApp (Lazy.force mk_unit_pack, [|x;r; - e_bin ; - pack.u_value; + mkApp (Lazy.force mk_unit_pack, [|x;r; + e_bin ; + pack.u_value; u_desc |]) @@ -294,25 +294,25 @@ module Unit = struct end -let anomaly msg = +let anomaly msg = Util.anomaly ("aac_tactics: " ^ msg) -let user_error msg = +let user_error msg = Util.error ("aac_tactics: " ^ msg) module Trans = struct - + (** {1 From Coq to Abstract Syntax Trees (AST)} - + This module provides facilities to interpret a Coq term with arbitrary operators as an abstract syntax tree. Considering an - application, we try to infer instances of our classes. - + application, we try to infer instances of our classes. + We consider that [A] operators are coarser than [AC] operators, which in turn are coarser than raw morphisms. That means that [List.append], of type [(A : Type) -> list A -> list A -> list A] can be understood as an [A] operator. - + During this reification, we gather some informations that will be used to rebuild Coq terms from AST ( type {!envs}) @@ -322,7 +322,7 @@ module Trans = struct (* 'a * (unit, op_unit) option *) type 'a with_unit = 'a * (Unit.unit_of) option - type pack = + type pack = (* used to infer the AC/A structure in the first pass {!Gather} *) | Bin of Bin.pack with_unit (* will only be used in the second pass : {!Parse}*) @@ -330,44 +330,44 @@ module Trans = struct | Unit of constr (* to avoid confusion in bloom *) (** discr is a map from {!Term.constr} to {!pack}. - + [None] means that it is not possible to instantiate this partial application to an interesting class. [Some x] means that we found something in the past. This means in particular that a single [constr] cannot be two things at the same time. - + The field [bloom] allows to give a unique number to each class we found. *) - type envs = + type envs = { discr : (pack option) HMap.t ; - bloom : (pack, int ) Hashtbl.t; + bloom : (pack, int ) Hashtbl.t; bloom_back : (int, pack ) Hashtbl.t; bloom_next : int ref; } - let empty_envs () = + let empty_envs () = { discr = HMap.create 17; - bloom = Hashtbl.create 17; - bloom_back = Hashtbl.create 17; + bloom = Hashtbl.create 17; + bloom_back = Hashtbl.create 17; bloom_next = ref 1; } - + - let add_bloom envs pack = - if Hashtbl.mem envs.bloom pack + let add_bloom envs pack = + if Hashtbl.mem envs.bloom pack then () else - let x = ! (envs.bloom_next) in + let x = ! (envs.bloom_next) in Hashtbl.add envs.bloom pack x; Hashtbl.add envs.bloom_back x pack; incr (envs.bloom_next) - let find_bloom envs pack = + let find_bloom envs pack = try Hashtbl.find envs.bloom pack with Not_found -> assert false @@ -380,88 +380,88 @@ module Trans = struct staging process allows us to prefer AC/A operators over raw morphisms. Moreover, for each AC/A operators, we need to try to infer units. Otherwise, we do not have [x * y * x <= a * a] since 1 - does not occur. - + does not occur. + But, do we also need to check whether constants are units. Otherwise, we do not have the ability to rewrite [0 = a + a] in [a = ...]*) - module Gather : sig + module Gather : sig val gather : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma end - = struct + = struct let memoize envs t pack : unit = begin - HMap.add envs.discr t (Some pack); + HMap.add envs.discr t (Some pack); add_bloom envs pack; - match pack with + match pack with | Bin (_, None) | Sym _ -> () | Bin (_, Some (unit_of)) -> let unit = unit_of.Unit.uf_u in - HMap.add envs.discr unit (Some (Unit unit)); + HMap.add envs.discr unit (Some (Unit unit)); add_bloom envs (Unit unit); | Unit _ -> assert false end - let get_unit (rlt : AAC_coq.Relation.t) op goal : + let get_unit (rlt : AAC_coq.Relation.t) op goal : (AAC_coq.goal_sigma * constr * constr ) option= - let x = (rlt.AAC_coq.Relation.carrier) in - let unit, goal = AAC_coq.evar_unit goal x in + let x = (rlt.AAC_coq.Relation.carrier) in + let unit, goal = AAC_coq.evar_unit goal x in let ty =Classes.Unit.ty rlt op unit in - let result = - try + let result = + try let t,goal = AAC_coq.resolve_one_typeclass goal ty in Some (goal,t,unit) with Not_found -> None in - match result with + match result with | None -> None - | Some (goal,s,unit) -> - let unit = AAC_coq.nf_evar goal unit in + | Some (goal,s,unit) -> + let unit = AAC_coq.nf_evar goal unit in Some (goal, unit, s) (** gives back the class and the operator *) let is_bin (rlt: AAC_coq.Relation.t) (op: constr) ( goal: AAC_coq.goal_sigma) - : (AAC_coq.goal_sigma * Bin.pack) option = - let assoc_ty = Classes.Associative.ty rlt op in - let comm_ty = Classes.Commutative.ty rlt op in + : (AAC_coq.goal_sigma * Bin.pack) option = + let assoc_ty = Classes.Associative.ty rlt op in + let comm_ty = Classes.Commutative.ty rlt op in let proper_ty = Classes.Proper.ty rlt op 2 in - try + try let proper , goal = AAC_coq.resolve_one_typeclass goal proper_ty in let assoc, goal = AAC_coq.resolve_one_typeclass goal assoc_ty in let comm , goal = - try - let comm, goal = AAC_coq.resolve_one_typeclass goal comm_ty in - Some comm, goal - with Not_found -> + try + let comm, goal = AAC_coq.resolve_one_typeclass goal comm_ty in + Some comm, goal + with Not_found -> None, goal - in - let bin = - {Bin.value = op; + in + let bin = + {Bin.value = op; Bin.compat = proper; - Bin.assoc = assoc; - Bin.comm = comm } - in + Bin.assoc = assoc; + Bin.comm = comm } + in Some (goal,bin) with |Not_found -> None - + let is_bin (rlt : AAC_coq.Relation.t) (op : constr) (goal : AAC_coq.goal_sigma)= match is_bin rlt op goal with | None -> None - | Some (goal, bin_pack) -> - match get_unit rlt op goal with + | Some (goal, bin_pack) -> + match get_unit rlt op goal with | None -> Some (goal, Bin (bin_pack, None)) - | Some (gl, unit,s) -> - let unit_of = + | Some (gl, unit,s) -> + let unit_of = { Unit.uf_u = unit; (* TRICK : this term is not well-typed by itself, but it is okay the way we use it in the other functions *) - Unit.uf_idx = op; + Unit.uf_idx = op; Unit.uf_desc = s; } in Some (gl,Bin (bin_pack, Some (unit_of))) @@ -470,66 +470,66 @@ module Trans = struct (** {is_morphism} try to infer the kind of operator we are dealing with *) let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option = - let typeof = Classes.Proper.mk_typeof rlt ar in - let relof = Classes.Proper.mk_relof rlt ar in + let typeof = Classes.Proper.mk_typeof rlt ar in + let relof = Classes.Proper.mk_relof rlt ar in let m = AAC_coq.Classes.mk_morphism typeof relof papp in - try + try let m,goal = AAC_coq.resolve_one_typeclass goal m in - let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in - Some (goal, Sym pack) - with + let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in + Some (goal, Sym pack) + with | Not_found -> None - - - (* [crop_app f [| a_0 ; ... ; a_n |]] - returns Some (f a_0 ... a_(n-2), [|a_(n-1); a_n |] ) + + + (* [crop_app f [| a_0 ; ... ; a_n |]] + returns Some (f a_0 ... a_(n-2), [|a_(n-1); a_n |] ) *) - let crop_app t ca : (constr * constr array) option= - let n = Array.length ca in - if n <= 1 + let crop_app t ca : (constr * constr array) option= + let n = Array.length ca in + if n <= 1 then None - else + else let papp = Term.mkApp (t, Array.sub ca 0 (n-2) ) in let args = Array.sub ca (n-2) 2 in Some (papp, args ) - + let fold goal (rlt : AAC_coq.Relation.t) envs t ca cont = let fold_morphism t ca = - let nb_params = Array.length ca in - let rec aux n = + let nb_params = Array.length ca in + let rec aux n = assert (n < nb_params && 0 < nb_params ); - let papp = Term.mkApp (t, Array.sub ca 0 n) in - match is_morphism goal rlt papp (nb_params - n) with - | None -> + let papp = Term.mkApp (t, Array.sub ca 0 n) in + match is_morphism goal rlt papp (nb_params - n) with + | None -> (* here we have to memoize the failures *) HMap.add envs.discr papp None; if n < nb_params - 1 then aux (n+1) else goal | Some (goal, pack) -> let args = Array.sub ca (n) (nb_params -n)in - let goal = Array.fold_left cont goal args in + let goal = Array.fold_left cont goal args in memoize envs papp pack; goal - in + in if nb_params = 0 then goal else aux 0 in - let is_aac t = is_bin rlt t in - match crop_app t ca with - | None -> - fold_morphism t ca - | Some (papp, args) -> - begin match is_aac papp goal with + let is_aac t = is_bin rlt t in + match crop_app t ca with + | None -> + fold_morphism t ca + | Some (papp, args) -> + begin match is_aac papp goal with | None -> fold_morphism t ca - | Some (goal, pack) -> + | Some (goal, pack) -> memoize envs papp pack; - Array.fold_left cont goal args + Array.fold_left cont goal args end (* update in place the envs of known stuff, using memoization. We have to memoize failures, here. *) let gather goal (rlt : AAC_coq.Relation.t ) envs t : AAC_coq.goal_sigma = - let rec aux goal x = - match AAC_coq.decomp_term x with - | App (t,ca) -> + let rec aux goal x = + match AAC_coq.decomp_term x with + | App (t,ca) -> fold goal rlt envs t ca (aux ) | _ -> goal in @@ -539,12 +539,12 @@ module Trans = struct (** We build a term out of a constr, updating in place the environment if needed (the only kind of such updates are the constants). *) - module Parse : - sig + module Parse : + sig val t_of_constr : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma end = struct - + (** [discriminates goal envs rlt t ca] infer : - its {! pack } (is it an AC operator, or an A operator, or a @@ -563,28 +563,28 @@ module Trans = struct that a constant is a morphism. But not an eva. *) let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option = - let typeof = Classes.Proper.mk_typeof rlt ar in - let relof = Classes.Proper.mk_relof rlt ar in + let typeof = Classes.Proper.mk_typeof rlt ar in + let relof = Classes.Proper.mk_relof rlt ar in let m = AAC_coq.Classes.mk_morphism typeof relof papp in - try + try let m,goal = AAC_coq.resolve_one_typeclass goal m in - let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in - Some (goal, Sym pack) - with + let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in + Some (goal, Sym pack) + with | e -> None exception NotReflexive - let discriminate goal envs (rlt : AAC_coq.Relation.t) t ca : AAC_coq.goal_sigma * pack * constr * constr array = + let discriminate goal envs (rlt : AAC_coq.Relation.t) t ca : AAC_coq.goal_sigma * pack * constr * constr array = let nb_params = Array.length ca in - let rec fold goal ar :AAC_coq.goal_sigma * pack * constr * constr array = + let rec fold goal ar :AAC_coq.goal_sigma * pack * constr * constr array = begin assert (0 <= ar && ar <= nb_params); - let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in + let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in begin - try - begin match HMap.find envs.discr p_app with - | None -> - fold goal (ar-1) + try + begin match HMap.find envs.discr p_app with + | None -> + fold goal (ar-1) | Some pack -> (goal, pack, p_app, Array.sub ca (nb_params -ar ) ar) end @@ -593,15 +593,15 @@ module Trans = struct memoize (is_morphism goal rlt p_app ar) p_app ar end end - and memoize (x) p_app ar = + and memoize (x) p_app ar = assert (0 <= ar && ar <= nb_params); match x with - | Some (goal, pack) -> + | Some (goal, pack) -> HMap.add envs.discr p_app (Some pack); add_bloom envs pack; (goal, pack, p_app, Array.sub ca (nb_params-ar) ar) - | None -> - + | None -> + if ar = 0 then raise NotReflexive; begin (* to memoise the failures *) @@ -611,22 +611,22 @@ module Trans = struct fold goal (ar-1) end in - try match HMap.find envs.discr (mkApp (t,ca))with + try match HMap.find envs.discr (mkApp (t,ca))with | None -> fold goal (nb_params) | Some pack -> goal, pack, (mkApp (t,ca)), [| |] with Not_found -> fold goal (nb_params) - + let discriminate goal envs rlt x = - try - match AAC_coq.decomp_term x with - | App (t,ca) -> + try + match AAC_coq.decomp_term x with + | App (t,ca) -> discriminate goal envs rlt t ca | _ -> discriminate goal envs rlt x [| |] - with + with | NotReflexive -> user_error "The relation to which the goal was lifted is not Reflexive" (* TODO: is it the only source of invalid use that fall into this catch_all ? *) - | e -> + | e -> user_error "Cannot handle this kind of hypotheses (variables occuring under a function symbol which is not a proper morphism)." (** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree @@ -634,51 +634,51 @@ module Trans = struct known stuff [envs], and eventually creates fresh evars. Therefore, we give back the goal updated accordingly *) let t_of_constr goal (rlt: AAC_coq.Relation.t ) envs : constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma = - let r_goal = ref (goal) in - let rec aux x = - match AAC_coq.decomp_term x with + let r_goal = ref (goal) in + let rec aux x = + match AAC_coq.decomp_term x with | Rel i -> AAC_matcher.Terms.Var i - | _ -> - let goal, pack , p_app, ca = discriminate (!r_goal) envs rlt x in + | _ -> + let goal, pack , p_app, ca = discriminate (!r_goal) envs rlt x in r_goal := goal; let k = find_bloom envs pack - in - match pack with + in + match pack with | Bin (pack,_) -> - begin match pack.Bin.comm with + begin match pack.Bin.comm with | Some _ -> assert (Array.length ca = 2); AAC_matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1)) - | None -> + | None -> assert (Array.length ca = 2); AAC_matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1)) end - | Unit _ -> + | Unit _ -> assert (Array.length ca = 0); AAC_matcher.Terms.Unit ( k) | Sym _ -> AAC_matcher.Terms.Sym ( k, Array.map aux ca) - in + in ( - fun x -> let r = aux x in r, !r_goal - ) - + fun x -> let r = aux x in r, !r_goal + ) + end (* Parse *) let add_symbol goal rlt envs l = - let goal = Gather.gather goal rlt envs (Term.mkApp (l, [| Term.mkRel 0;Term.mkRel 0|])) in - goal - + let goal = Gather.gather goal rlt envs (Term.mkApp (l, [| Term.mkRel 0;Term.mkRel 0|])) in + goal + (* [t_of_constr] buils a the abstract syntax tree of a constr, updating in place the environment. Doing so, we infer all the morphisms and the AC/A operators. It is mandatory to do so both for the pattern and the term, since AC symbols can occur in one and not the other *) - let t_of_constr goal rlt envs (l,r) = - let goal = Gather.gather goal rlt envs l in - let goal = Gather.gather goal rlt envs r in - let l,goal = Parse.t_of_constr goal rlt envs l in - let r, goal = Parse.t_of_constr goal rlt envs r in + let t_of_constr goal rlt envs (l,r) = + let goal = Gather.gather goal rlt envs l in + let goal = Gather.gather goal rlt envs r in + let l,goal = Parse.t_of_constr goal rlt envs l in + let r, goal = Parse.t_of_constr goal rlt envs r in l, r, goal (* An intermediate representation of the environment, with association lists for AC/A operators, and also the raw [packer] information *) @@ -688,65 +688,65 @@ module Trans = struct packer : (int, pack) Hashtbl.t; (* = bloom_back *) bin : (int * Bin.pack) list ; units : (int * Unit.pack) list; - sym : (int * Term.constr) list ; + sym : (int * Term.constr) list ; matcher_units : AAC_matcher.ext_units } let ir_to_units ir = ir.matcher_units - + let ir_of_envs goal (rlt : AAC_coq.Relation.t) envs = - let add x y l = (x,y)::l in - let nil = [] in + let add x y l = (x,y)::l in + let nil = [] in let sym , (bin : (int * Bin.pack with_unit) list), (units : (int * constr) list) = - Hashtbl.fold - (fun int pack (sym,bin,units) -> - match pack with - | Bin s -> + Hashtbl.fold + (fun int pack (sym,bin,units) -> + match pack with + | Bin s -> sym, add (int) s bin, units | Sym s -> add (int) s sym, bin, units | Unit s -> sym, bin, add int s units - ) - envs.bloom_back + ) + envs.bloom_back (nil,nil,nil) in let matcher_units = let unit_for , is_ac = - List.fold_left - (fun ((unit_for,is_ac) as acc) (n,(bp,wu)) -> - match wu with + List.fold_left + (fun ((unit_for,is_ac) as acc) (n,(bp,wu)) -> + match wu with | None -> acc - | Some (unit_of) -> - let unit_n = Hashtbl.find envs.bloom + | Some (unit_of) -> + let unit_n = Hashtbl.find envs.bloom (Unit unit_of.Unit.uf_u) in - ( n, unit_n)::unit_for, + ( n, unit_n)::unit_for, (n, bp.Bin.comm <> None )::is_ac - + ) ([],[]) bin in {AAC_matcher.unit_for = unit_for; AAC_matcher.is_ac = is_ac} in - let units : (int * Unit.pack) list = - List.fold_left - (fun acc (n,u) -> + let units : (int * Unit.pack) list = + List.fold_left + (fun acc (n,u) -> (* first, gather all bins with this unit *) - let all_bin = + let all_bin = List.fold_left - ( fun acc (nop,(bp,wu)) -> - match wu with + ( fun acc (nop,(bp,wu)) -> + match wu with | None -> acc - | Some unit_of -> + | Some unit_of -> if unit_of.Unit.uf_u = u - then - {unit_of with + then + {unit_of with Unit.uf_idx = (AAC_coq.Pos.of_int nop)} :: acc - else + else acc ) [] bin @@ -754,11 +754,11 @@ module Trans = struct (n,{ Unit.u_value = u; Unit.u_desc = all_bin - })::acc + })::acc ) [] units - in + in goal, { packer = envs.bloom_back; bin = (List.map (fun (n,(s,_)) -> n, s) bin); @@ -767,10 +767,10 @@ module Trans = struct matcher_units = matcher_units } - + (** {1 From AST back to Coq } - + The next functions allow one to map OCaml abstract syntax trees to Coq terms *) @@ -780,75 +780,75 @@ module Trans = struct representation, without products on top, and maybe escaping free debruijn indices (in the case of a pattern for example). *) let raw_constr_of_t_debruijn ir (t : AAC_matcher.Terms.t) : Term.constr * int list = - let add_set,get = - let r = ref [] in - let rec add x = function + let add_set,get = + let r = ref [] in + let rec add x = function [ ] -> [x] | t::q when t = x -> t::q - | t::q -> t:: (add x q) - in + | t::q -> t:: (add x q) + in (fun x -> r := add x !r),(fun () -> !r) in (* Here, we rely on the invariant that the maps are well formed: it is meanigless to fail to find a symbol in the maps, or to find the wrong kind of pack in the maps *) let rec aux t = - match t with + match t with | AAC_matcher.Terms.Plus (s,l,r) -> - begin match Hashtbl.find ir.packer s with - | Bin (s,_) -> + begin match Hashtbl.find ir.packer s with + | Bin (s,_) -> mkApp (s.Bin.value , [|(aux l);(aux r)|]) | _ -> Printf.printf "erreur:%i\n%!"s; assert false end | AAC_matcher.Terms.Dot (s,l,r) -> - begin match Hashtbl.find ir.packer s with - | Bin (s,_) -> + begin match Hashtbl.find ir.packer s with + | Bin (s,_) -> mkApp (s.Bin.value, [|(aux l);(aux r)|]) | _ -> assert false end | AAC_matcher.Terms.Sym (s,t) -> - begin match Hashtbl.find ir.packer s with - | Sym s -> + begin match Hashtbl.find ir.packer s with + | Sym s -> mkApp (s.Sym.value, Array.map aux t) | _ -> assert false end | AAC_matcher.Terms.Unit x -> - begin match Hashtbl.find ir.packer x with + begin match Hashtbl.find ir.packer x with | Unit s -> s | _ -> assert false end | AAC_matcher.Terms.Var i -> add_set i; mkRel (i) - in - let t = aux t in + in + let t = aux t in t , get ( ) (** [raw_constr_of_t] rebuilds a term in the raw representation *) - let raw_constr_of_t ir rlt (context:rel_context) t = + let raw_constr_of_t ir rlt (context:rel_context) t = (** cap rebuilds the products in front of the constr *) let rec cap c = function [] -> c - | t::q -> - let i = Term.lookup_rel t context in + | t::q -> + let i = Term.lookup_rel t context in cap (mkProd_or_LetIn i c) q in - let t,indices = raw_constr_of_t_debruijn ir t in + let t,indices = raw_constr_of_t_debruijn ir t in cap t (List.sort (Pervasives.compare) indices) - + (** {2 Building reified terms} *) (* Some informations to be able to build the maps *) - type reif_params = + type reif_params = { bin_null : Bin.pack; (* the default A operator *) - sym_null : constr; - unit_null : Unit.pack; + sym_null : constr; + unit_null : Unit.pack; sym_ty : constr; (* the type, as it appears in e_sym *) bin_ty : constr } - + (** A record containing the environments that will be needed by the decision procedure, as a Coq constr. Contains the functions from the symbols (as ints) to indexes (as constr) *) @@ -858,8 +858,8 @@ module Trans = struct env_bin : Term.constr; env_units : Term.constr; (* the [idx -> X:constr] *) } - - + + type sigma_maps = { sym_to_pos : int -> Term.constr; bin_to_pos : int -> Term.constr; @@ -873,15 +873,15 @@ module Trans = struct (* Note : this function can fail if the user is using the wrong relation, like proving a = b, while the classes are defined with another relation (==) *) - let build_reif_params goal (rlt : AAC_coq.Relation.t) (zero) : - reif_params * AAC_coq.goal_sigma = + let build_reif_params goal (rlt : AAC_coq.Relation.t) (zero) : + reif_params * AAC_coq.goal_sigma = let carrier = rlt.AAC_coq.Relation.carrier in - let bin_null = + let bin_null = try - let op,goal = AAC_coq.evar_binary goal carrier in - let assoc,goal = Classes.Associative.infer goal rlt op in - let compat,goal = Classes.Proper.infer goal rlt op 2 in - let op = AAC_coq.nf_evar goal op in + let op,goal = AAC_coq.evar_binary goal carrier in + let assoc,goal = Classes.Associative.infer goal rlt op in + let compat,goal = Classes.Proper.infer goal rlt op 2 in + let op = AAC_coq.nf_evar goal op in { Bin.value = op; Bin.compat = compat; @@ -889,94 +889,94 @@ module Trans = struct Bin.comm = None } with Not_found -> user_error "Cannot infer a default A operator (required at least to be Proper and Associative)" - in + in let zero, goal = try - let evar_op,goal = AAC_coq.evar_binary goal carrier in - let evar_unit, goal = AAC_coq.evar_unit goal carrier in - let query = Classes.Unit.ty rlt evar_op evar_unit in - let _, goal = AAC_coq.resolve_one_typeclass goal query in + let evar_op,goal = AAC_coq.evar_binary goal carrier in + let evar_unit, goal = AAC_coq.evar_unit goal carrier in + let query = Classes.Unit.ty rlt evar_op evar_unit in + let _, goal = AAC_coq.resolve_one_typeclass goal query in AAC_coq.nf_evar goal evar_unit, goal with _ -> zero, goal in - let sym_null = Sym.null rlt in - let unit_null = Unit.default zero in - let record = + let sym_null = Sym.null rlt in + let unit_null = Unit.default zero in + let record = { - bin_null = bin_null; - sym_null = sym_null; + bin_null = bin_null; + sym_null = sym_null; unit_null = unit_null; sym_ty = Sym.mk_ty rlt ; - bin_ty = Bin.mk_ty rlt + bin_ty = Bin.mk_ty rlt } - in + in record, goal (* We want to lift down the indexes of symbols. *) let renumber (l: (int * 'a) list ) = - let _, l = List.fold_left (fun (next,acc) (glob,x) -> + let _, l = List.fold_left (fun (next,acc) (glob,x) -> (next+1, (next,glob,x)::acc) ) (1,[]) l - in - let rec to_global loc = function + in + let rec to_global loc = function | [] -> assert false | (local, global,x)::q when local = loc -> global | _::q -> to_global loc q - in - let rec to_local glob = function + in + let rec to_local glob = function | [] -> assert false | (local, global,x)::q when global = glob -> local | _::q -> to_local glob q - in - let locals = List.map (fun (local,global,x) -> local,x) l in + in + let locals = List.map (fun (local,global,x) -> local,x) l in locals, (fun x -> to_local x l) , (fun x -> to_global x l) (** [build_sigma_maps] given a envs and some reif_params, we are able to build the sigmas *) - let build_sigma_maps (rlt : AAC_coq.Relation.t) zero ir (k : sigmas * sigma_maps -> Proof_type.tactic ) : Proof_type.tactic = fun goal -> - let rp,goal = build_reif_params goal rlt zero in - let renumbered_sym, to_local, to_global = renumber ir.sym in - let env_sym = Sigma.of_list - rp.sym_ty - (rp.sym_null) - renumbered_sym + let build_sigma_maps (rlt : AAC_coq.Relation.t) zero ir (k : sigmas * sigma_maps -> Proof_type.tactic ) : Proof_type.tactic = fun goal -> + let rp,goal = build_reif_params goal rlt zero in + let renumbered_sym, to_local, to_global = renumber ir.sym in + let env_sym = Sigma.of_list + rp.sym_ty + (rp.sym_null) + renumbered_sym in - AAC_coq.cps_mk_letin "env_sym" env_sym - (fun env_sym -> + AAC_coq.cps_mk_letin "env_sym" env_sym + (fun env_sym -> let bin = (List.map ( fun (n,s) -> n, Bin.mk_pack rlt s) ir.bin) in - let env_bin = - Sigma.of_list - rp.bin_ty - (Bin.mk_pack rlt rp.bin_null) - bin + let env_bin = + Sigma.of_list + rp.bin_ty + (Bin.mk_pack rlt rp.bin_null) + bin in - AAC_coq.cps_mk_letin "env_bin" env_bin - (fun env_bin -> - let units = (List.map (fun (n,s) -> n, Unit.mk_pack rlt env_bin s)ir.units) in + AAC_coq.cps_mk_letin "env_bin" env_bin + (fun env_bin -> + let units = (List.map (fun (n,s) -> n, Unit.mk_pack rlt env_bin s)ir.units) in let env_units = - Sigma.of_list + Sigma.of_list (Unit.ty_unit_pack rlt env_bin) (Unit.mk_pack rlt env_bin rp.unit_null ) units in - AAC_coq.cps_mk_letin "env_units" env_units - (fun env_units -> - let sigmas = + AAC_coq.cps_mk_letin "env_units" env_units + (fun env_units -> + let sigmas = { env_sym = env_sym ; env_bin = env_bin ; env_units = env_units; - } in - let f = List.map (fun (x,_) -> (x,AAC_coq.Pos.of_int x)) in + } in + let f = List.map (fun (x,_) -> (x,AAC_coq.Pos.of_int x)) in let sigma_maps = - { + { sym_to_pos = (let sym = f renumbered_sym in fun x -> (List.assoc (to_local x) sym)); bin_to_pos = (let bin = f bin in fun x -> (List.assoc x bin)); units_to_pos = (let units = f units in fun x -> (List.assoc x units)); } - in + in k (sigmas, sigma_maps ) - ) + ) ) ) goal @@ -986,37 +986,37 @@ module Trans = struct rsum: constr -> constr -> constr -> constr; rprd: constr -> constr -> constr -> constr; rsym: constr -> constr array -> constr; - runit : constr -> constr + runit : constr -> constr } (* donne moi une tactique, je rajoute ma part. Potentiellement, il est possible d'utiliser la notation 'do' a la Haskell: http://www.cas.mcmaster.ca/~carette/pa_monad/ *) - let (>>) : 'a * Proof_type.tactic -> ('a -> 'b * Proof_type.tactic) -> 'b * Proof_type.tactic = + let (>>) : 'a * Proof_type.tactic -> ('a -> 'b * Proof_type.tactic) -> 'b * Proof_type.tactic = fun (x,t) f -> - let b,t' = f x in + let b,t' = f x in b, Tacticals.tclTHEN t t' - + let return x = x, Tacticals.tclIDTAC - + let mk_vect vnil vcons v = - let ar = Array.length v in - let rec aux = function + let ar = Array.length v in + let rec aux = function | 0 -> vnil - | n -> let n = n-1 in - mkApp( vcons, - [| + | n -> let n = n-1 in + mkApp( vcons, + [| (AAC_coq.Nat.of_int n); v.(ar - 1 - n); (aux (n)) |] ) in aux ar - + (* TODO: use a do notation *) let mk_reif_builders (rlt: AAC_coq.Relation.t) (env_sym:constr) (k: reif_builders -> Proof_type.tactic) = - let x = (rlt.AAC_coq.Relation.carrier) in - let r = (rlt.AAC_coq.Relation.r) in + let x = (rlt.AAC_coq.Relation.carrier) in + let r = (rlt.AAC_coq.Relation.r) in let x_r_env = [|x;r;env_sym|] in let tty = mkApp (Lazy.force Stubs._Tty, x_r_env) in @@ -1025,29 +1025,29 @@ module Trans = struct let rsym = mkApp (Lazy.force Stubs.rsym, x_r_env) in let vnil = mkApp (Lazy.force Stubs.vnil, x_r_env) in let vcons = mkApp (Lazy.force Stubs.vcons, x_r_env) in - AAC_coq.cps_mk_letin "tty" tty - (fun tty -> - AAC_coq.cps_mk_letin "rsum" rsum - (fun rsum -> - AAC_coq.cps_mk_letin "rprd" rprd - (fun rprd -> - AAC_coq.cps_mk_letin "rsym" rsym + AAC_coq.cps_mk_letin "tty" tty + (fun tty -> + AAC_coq.cps_mk_letin "rsum" rsum + (fun rsum -> + AAC_coq.cps_mk_letin "rprd" rprd + (fun rprd -> + AAC_coq.cps_mk_letin "rsym" rsym (fun rsym -> AAC_coq.cps_mk_letin "vnil" vnil (fun vnil -> - AAC_coq.cps_mk_letin "vcons" vcons + AAC_coq.cps_mk_letin "vcons" vcons (fun vcons -> let r ={ - rsum = + rsum = begin fun idx l r -> mkApp (rsum, [| idx ; mk_mset tty [l,1 ; r,1]|]) end; - rprd = + rprd = begin fun idx l r -> let lst = NEList.of_list tty [l;r] in - mkApp (rprd, [| idx; lst|]) + mkApp (rprd, [| idx; lst|]) end; - rsym = + rsym = begin fun idx v -> let vect = mk_vect vnil vcons v in mkApp (rsym, [| idx; vect|]) @@ -1055,20 +1055,20 @@ module Trans = struct runit = fun idx -> (* could benefit of a letin *) mkApp (Lazy.force Stubs.runit , [|x;r;env_sym;idx; |]) } - in k r + in k r )))))) - + type reifier = sigma_maps * reif_builders + - - let mk_reifier rlt zero envs (k : sigmas *reifier -> Proof_type.tactic) = - build_sigma_maps rlt zero envs + let mk_reifier rlt zero envs (k : sigmas *reifier -> Proof_type.tactic) = + build_sigma_maps rlt zero envs (fun (s,sm) -> - mk_reif_builders rlt s.env_sym + mk_reif_builders rlt s.env_sym (fun rb ->k (s,(sm,rb)) ) - + ) (** [reif_constr_of_t reifier t] rebuilds the term [t] in the @@ -1078,17 +1078,17 @@ module Trans = struct let rec aux = function | AAC_matcher.Terms.Plus (s,l,r) -> let idx = sm.bin_to_pos s in - rb.rsum idx (aux l) (aux r) + rb.rsum idx (aux l) (aux r) | AAC_matcher.Terms.Dot (s,l,r) -> - let idx = sm.bin_to_pos s in - rb.rprd idx (aux l) (aux r) + let idx = sm.bin_to_pos s in + rb.rprd idx (aux l) (aux r) | AAC_matcher.Terms.Sym (s,t) -> - let idx = sm.sym_to_pos s in + let idx = sm.sym_to_pos s in rb.rsym idx (Array.map aux t) | AAC_matcher.Terms.Unit s -> - let idx = sm.units_to_pos s in - rb.runit idx - | AAC_matcher.Terms.Var i -> + let idx = sm.units_to_pos s in + rb.runit idx + | AAC_matcher.Terms.Var i -> anomaly "call to reif_constr_of_t on a term with variables." in aux t end diff --git a/AAC_theory.mli b/AAC_theory.mli index 128e88b..2f57446 100644 --- a/AAC_theory.mli +++ b/AAC_theory.mli @@ -7,8 +7,8 @@ (***************************************************************************) (** Bindings for Coq constants that are specific to the plugin; - reification and translation functions. - + reification and translation functions. + Note: this module is highly correlated with the definitions of {i AAC.v}. @@ -35,7 +35,7 @@ module Sigma: sig (** [add ty n x map] adds the value [x] of type [ty] with key [n] in [map] *) val add: Term.constr ->Term.constr ->Term.constr ->Term.constr ->Term.constr - + (** [empty ty] create an empty map of type [ty] *) val empty: Term.constr ->Term.constr @@ -58,10 +58,10 @@ sig (** [mk_pack rlt (ar,value,morph)] *) val mk_pack: AAC_coq.Relation.t -> pack -> Term.constr - + (** [null] builds a dummy (identity) symbol, given an {!AAC_coq.Relation.t} *) val null: AAC_coq.Relation.t -> Term.constr - + end @@ -76,27 +76,27 @@ module Stubs : sig (** The evaluation fonction, used to convert a reified coq term to a raw coq term *) val eval: Term.constr lazy_t - - (** The main lemma of our theory, that is + + (** The main lemma of our theory, that is [compare (norm u) (norm v) = Eq -> eval u == eval v] *) - val decide_thm:Term.constr lazy_t + val decide_thm:Term.constr lazy_t val lift_normalise_thm : Term.constr lazy_t end (** {2 Building reified terms} - + We define a bundle of functions to build reified versions of the terms (those that will be given to the reflexive decision procedure). In particular, each field takes as first argument the index of the symbol rather than the symbol itself. *) - + (** Tranlations between Coq and OCaml *) module Trans : sig (** This module provides facilities to interpret a term with arbitrary operators as an instance of an abstract syntax tree - {!AAC_matcher.Terms.t}. + {!AAC_matcher.Terms.t}. For each Coq application [f x_1 ... x_n], this amounts to deciding whether one of the partial applications [f x_1 @@ -105,25 +105,25 @@ module Trans : sig whether the whole term is the unit for some A or AC operator. We use typeclass resolution to test each of these possibilities. - Note that there are ambiguous terms: + Note that there are ambiguous terms: - a term like [f x y] might yield a unary morphism ([f x]) and a binary one ([f]); we select the latter one (unless [f] is A or AC, in which case we declare it accordingly); - - a term like [S O] can be considered as a morphism ([S]) - applied to a unit for [(+)], or as a unit for [( * )]; we - chose to give priority to units, so that the latter - interpretation is selected in this case; - - an element might be the unit for several operations + - a term like [S O] can be considered as a morphism ([S]) + applied to a unit for [(+)], or as a unit for [( * )]; we + chose to give priority to units, so that the latter + interpretation is selected in this case; + - an element might be the unit for several operations *) - + (** To achieve this reification, one need to record informations about the collected operators (symbols, binary operators, units). We use the following imperative internal data-structure to this end. *) - - type envs + + type envs val empty_envs : unit -> envs - + (** {2 Reification: from Coq terms to AST {!AAC_matcher.Terms.t} } *) @@ -135,15 +135,15 @@ module Trans : sig environment [envs]. Moreover, we need to create fresh evars; this is why we give back the [goal], accordingly updated. *) - + val t_of_constr : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> (Term.constr * Term.constr) -> AAC_matcher.Terms.t * AAC_matcher.Terms.t * AAC_coq.goal_sigma (** [add_symbol] adds a given binary symbol to the environment of known stuff. *) - val add_symbol : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma + val add_symbol : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma (** {2 Reconstruction: from AST back to Coq terms } - + The next functions allow one to map OCaml abstract syntax trees to Coq terms. We need two functions to rebuild different kind of terms: first, raw terms, like the one encountered by @@ -155,7 +155,7 @@ module Trans : sig val ir_to_units : ir -> AAC_matcher.ext_units (** {2 Building raw, natural, terms} *) - + (** [raw_constr_of_t] rebuilds a term in the raw representation, and reconstruct the named products on top of it. In particular, this allow us to print the context put around the left (or right) @@ -163,7 +163,7 @@ module Trans : sig val raw_constr_of_t : ir -> AAC_coq.Relation.t -> (Term.rel_context) ->AAC_matcher.Terms.t -> Term.constr (** {2 Building reified terms} *) - + (** The reification environments, as Coq constrs *) type sigmas = { @@ -171,18 +171,18 @@ module Trans : sig env_bin : Term.constr; env_units : Term.constr; (* the [idx -> X:constr] *) } - - + + (** We need to reify two terms (left and right members of a goal) that share the same reification envirnoment. Therefore, we need to add letins to the proof context in order to ensure some - sharing in the proof terms we produce. + sharing in the proof terms we produce. Moreover, in order to have as much sharing as possible, we also add letins for various partial applications that are used throughout the terms. - + To achieve this, we decompose the reconstruction function into two steps: first, we build the reification environment and then reify each term successively.*) @@ -35,8 +35,8 @@ Require Instances. Section parameters. - Context {X} {R} {E: @Equivalence X R} - {plus} {plus_A: Associative R plus} {plus_C: Commutative R plus} + Context {X} {R} {E: @Equivalence X R} + {plus} {plus_A: Associative R plus} {plus_C: Commutative R plus} {plus_Proper: Proper (R ==> R ==> R) plus} {zero} {Zero: Unit R plus zero}. @@ -55,9 +55,9 @@ Section parameters. Fail aac_rewrite Hf. (** [aac_rewrite] does not instantiate [n] automatically *) aac_rewrite (Hf k). (** of course, this argument can be given explicitly *) aac_reflexivity. - Qed. + Qed. - (** for the same reason, we cannot handle higher-order parameters (here, [g])*) + (** for the same reason, we cannot handle higher-order parameters (here, [g])*) Hypothesis H : forall g x y, g x + g y == g (x + y). Variable g : X -> X. Hypothesis Hg : Proper (R ==> R) g. @@ -70,16 +70,16 @@ Section parameters. End parameters. -(** *** 2. Exogeneous morphisms +(** *** 2. Exogeneous morphisms We do not handle `exogeneous' morphisms: morphisms that move from type [T] to some other type [T']. *) Section morphism. - Require Import NArith Minus. + Require Import NArith Minus. Open Scope nat_scope. - (** Typically, although [N_of_nat] is a proper morphism from + (** Typically, although [N_of_nat] is a proper morphism from [@eq nat] to [@eq N], we cannot rewrite under [N_of_nat] *) Goal forall a b: nat, N_of_nat (a+b-(b+a)) = 0%N. intros. @@ -111,39 +111,39 @@ Section morphism. Fail aac_rewrite minus_diag. split; aac_rewrite minus_diag; reflexivity. Qed. - + End morphism. (** *** 3. Treatment of variance with inequations. We do not take variance into account when we compute the set of - solutions to a matching problem modulo AC. As a consequence, + solutions to a matching problem modulo AC. As a consequence, [aac_instances] may propose solutions for which [aac_rewrite] will fail, due to the lack of adequate morphisms *) -Section ineq. +Section ineq. Require Import ZArith. Import Instances.Z. Open Scope Z_scope. Instance Zplus_incr: Proper (Zle ==> Zle ==> Zle) Zplus. - Proof. intros ? ? H ? ? H'. apply Zplus_le_compat; assumption. Qed. + Proof. intros ? ? H ? ? H'. apply Zplus_le_compat; assumption. Qed. Hypothesis H: forall x, x+x <= x. Goal forall a b c, c + - (a + a) + b + b <= c. intros. (** this fails because the first solution is not valid ([Zopp] is not increasing), *) Fail aac_rewrite H. - aac_instances H. - (** on the contrary, the second solution is valid: *) - aac_rewrite H at 1. + aac_instances H. + (** on the contrary, the second solution is valid: *) + aac_rewrite H at 1. (** Currently, we cannot filter out such invalid solutions in an easy way; this should be fixed in the future *) Abort. -End ineq. +End ineq. @@ -166,23 +166,23 @@ Section Peano. Abort. Goal 1*1 = 1. - (** fails since 1 is seen as a unit, not the application of the + (** fails since 1 is seen as a unit, not the application of the morphism [S] to the constant [O] *) - Fail aacu_rewrite H. + Fail aacu_rewrite H. Abort. Hypothesis H': forall x, x+1 = 1+x. Goal forall a, a+S(0+0) = 1+a. (** ok (no multiplication around), [x] is instantiated with [a]*) - intro. aac_rewrite H'. + intro. aac_rewrite H'. Abort. Goal forall a, a*a+S(0+0) = 1+a*a. (** fails: although [S(0+0)] is understood as the application of - the morphism [S] to the constant [O], it is not recognised + the morphism [S] to the constant [O], it is not recognised as the unit [S O] of multiplication *) - intro. Fail aac_rewrite H'. + intro. Fail aac_rewrite H'. Abort. (** More generally, similar counter-intuitive behaviours can appear @@ -223,7 +223,7 @@ End evars. (** *** 3. Distinction between [aac_rewrite] and [aacu_rewrite] *) Section U. - Context {X} {R} {E: @Equivalence X R} + Context {X} {R} {E: @Equivalence X R} {dot} {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot} {one} {One: Unit R dot one}. @@ -257,14 +257,14 @@ End U. (** *** 4. Rewriting units *) Section V. - Context {X} {R} {E: @Equivalence X R} + Context {X} {R} {E: @Equivalence X R} {dot} {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot} {one} {One: Unit R dot one}. Infix "==" := R (at level 70). Infix "*" := dot. Notation "1" := one. - + (** [aac_rewrite] uses the symbols appearing in the goal and the hypothesis to infer the AC and A operations. In the following example, [dot] appears neither in the left-hand-side of the goal, @@ -289,7 +289,7 @@ Section W. Hypothesis H: 0 = c. Goal b*(a+a) <= b*(c+a+a+1). - + (** [aac_rewrite] finds a pattern modulo AC that matches a given hypothesis, and then makes a call to [setoid_rewrite]. This [setoid_rewrite] can unfortunately make several rewrites (in a @@ -299,8 +299,8 @@ Section W. (** To this end, we provide a companion tactic to [aac_rewrite] and [aacu_rewrite], that makes the transitivity step, but not the - setoid_rewrite: - + setoid_rewrite: + This allows the user to select the relevant occurrences in which to rewrite. *) aac_pattern H at 2. setoid_rewrite H at 1. @@ -336,18 +336,18 @@ Goal a+b*c = c. Abort. (** **** If the pattern is a unit: - + The heuristic is to make the unit appear at each possible position in the term, e.g. transforming [a] into [1*a] and [a*1], but this process is not recursive (we will not transform [1*a]) into [(1+0*1)*a] *) Goal a+b+c = c. - - aac_instances H0 [mult]. + + aac_instances H0 [mult]. (** 1 solution, we miss solutions like [(a+b+c*(1+0*(1+[])))] and so on *) - - aac_instances H1 [mult]. + + aac_instances H1 [mult]. (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*) Abort. @@ -365,7 +365,7 @@ Goal a*a+b*a + c = c. (** There are three solutions using aacu_instances (but, here, there are infinitely many different solutions). We miss e.g. [a*a +b*a + (x*x + y*x)*c], which seems to be more peculiar. *) - aacu_instances <- H. + aacu_instances <- H. Abort. diff --git a/Instances.v b/Instances.v index 250ed90..bb309fe 100644 --- a/Instances.v +++ b/Instances.v @@ -22,23 +22,23 @@ Module Peano. Require Import Arith NArith Max. Instance aac_plus_Assoc : Associative eq plus := plus_assoc. Instance aac_plus_Comm : Commutative eq plus := plus_comm. - + Instance aac_mult_Comm : Commutative eq mult := mult_comm. Instance aac_mult_Assoc : Associative eq mult := mult_assoc. - + Instance aac_min_Comm : Commutative eq min := min_comm. Instance aac_min_Assoc : Associative eq min := min_assoc. Instance aac_max_Comm : Commutative eq max := max_comm. Instance aac_max_Assoc : Associative eq max := max_assoc. - - Instance aac_one : Unit eq mult 1 := Build_Unit eq mult 1 mult_1_l mult_1_r. + + Instance aac_one : Unit eq mult 1 := Build_Unit eq mult 1 mult_1_l mult_1_r. Instance aac_zero_plus : Unit eq plus O := Build_Unit eq plus (O) plus_0_l plus_0_r. - Instance aac_zero_max : Unit eq max O := Build_Unit eq max 0 max_0_l max_0_r. + Instance aac_zero_max : Unit eq max O := Build_Unit eq max 0 max_0_l max_0_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder le := Build_PreOrder _ _ le_refl le_trans. + Instance preorder_le : PreOrder le := Build_PreOrder _ _ le_refl le_trans. Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _. End Peano. @@ -49,21 +49,21 @@ Module Z. Open Scope Z_scope. Instance aac_Zplus_Assoc : Associative eq Zplus := Zplus_assoc. Instance aac_Zplus_Comm : Commutative eq Zplus := Zplus_comm. - + Instance aac_Zmult_Comm : Commutative eq Zmult := Zmult_comm. Instance aac_Zmult_Assoc : Associative eq Zmult := Zmult_assoc. - + Instance aac_Zmin_Comm : Commutative eq Zmin := Zmin_comm. Instance aac_Zmin_Assoc : Associative eq Zmin := Zmin_assoc. Instance aac_Zmax_Comm : Commutative eq Zmax := Zmax_comm. Instance aac_Zmax_Assoc : Associative eq Zmax := Zmax_assoc. - - Instance aac_one : Unit eq Zmult 1 := Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. + + Instance aac_one : Unit eq Zmult 1 := Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. Instance aac_zero_Zplus : Unit eq Zplus 0 := Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r. (* We also provide liftings from le to eq *) - Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ _ Zle_refl Zle_trans. + Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ _ Zle_refl Zle_trans. Instance lift_le_eq : AAC_lift Zle eq := Build_AAC_lift eq_equivalence _. End Z. @@ -86,21 +86,21 @@ Module N. Open Scope N_scope. Instance aac_Nplus_Assoc : Associative eq Nplus := Nplus_assoc. Instance aac_Nplus_Comm : Commutative eq Nplus := Nplus_comm. - + Instance aac_Nmult_Comm : Commutative eq Nmult := Nmult_comm. Instance aac_Nmult_Assoc : Associative eq Nmult := Nmult_assoc. - + Instance aac_Nmin_Comm : Commutative eq Nmin := N.min_comm. Instance aac_Nmin_Assoc : Associative eq Nmin := N.min_assoc. Instance aac_Nmax_Comm : Commutative eq Nmax := N.max_comm. Instance aac_Nmax_Assoc : Associative eq Nmax := N.max_assoc. - - Instance aac_one : Unit eq Nmult (1)%N := Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. + + Instance aac_one : Unit eq Nmult (1)%N := Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. Instance aac_zero : Unit eq Nplus (0)%N := Build_Unit eq Nplus (0)%N Nplus_0_l Nplus_0_r. - Instance aac_zero_max : Unit eq Nmax 0 := Build_Unit eq Nmax 0 N.max_0_l N.max_0_r. - - (* We also provide liftings from le to eq *) + Instance aac_zero_max : Unit eq Nmax 0 := Build_Unit eq Nmax 0 N.max_0_l N.max_0_r. + + (* We also provide liftings from le to eq *) Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.T.le_refl N.T.le_trans. Instance lift_le_eq : AAC_lift Nle eq := Build_AAC_lift eq_equivalence _. @@ -111,21 +111,21 @@ Module P. Open Scope positive_scope. Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc. Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm. - + Instance aac_Pmult_Comm : Commutative eq Pmult := Pmult_comm. Instance aac_Pmult_Assoc : Associative eq Pmult := Pmult_assoc. - + Instance aac_Pmin_Comm : Commutative eq Pmin := P.min_comm. Instance aac_Pmin_Assoc : Associative eq Pmin := P.min_assoc. Instance aac_Pmax_Comm : Commutative eq Pmax := P.max_comm. Instance aac_Pmax_Assoc : Associative eq Pmax := P.max_assoc. - - Instance aac_one : Unit eq Pmult 1 := Build_Unit eq Pmult 1 _ Pmult_1_r. + + Instance aac_one : Unit eq Pmult 1 := Build_Unit eq Pmult 1 _ Pmult_1_r. intros; reflexivity. Qed. (* TODO : add this lemma in the stdlib *) - Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 P.max_1_l P.max_1_r. + Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 P.max_1_l P.max_1_r. - (* We also provide liftings from le to eq *) + (* We also provide liftings from le to eq *) Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple P.T.le_refl P.T.le_trans. Instance lift_le_eq : AAC_lift Ple eq := Build_AAC_lift eq_equivalence _. End P. @@ -134,21 +134,21 @@ Module Q. Require Import QArith Qminmax. Instance aac_Qplus_Assoc : Associative Qeq Qplus := Qplus_assoc. Instance aac_Qplus_Comm : Commutative Qeq Qplus := Qplus_comm. - + Instance aac_Qmult_Comm : Commutative Qeq Qmult := Qmult_comm. Instance aac_Qmult_Assoc : Associative Qeq Qmult := Qmult_assoc. - + Instance aac_Qmin_Comm : Commutative Qeq Qmin := Q.min_comm. Instance aac_Qmin_Assoc : Associative Qeq Qmin := Q.min_assoc. Instance aac_Qmax_Comm : Commutative Qeq Qmax := Q.max_comm. Instance aac_Qmax_Assoc : Associative Qeq Qmax := Q.max_assoc. - - Instance aac_one : Unit Qeq Qmult 1 := Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. + + Instance aac_one : Unit Qeq Qmult 1 := Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. Instance aac_zero_Qplus : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r. - (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Q.T.le_refl Q.T.le_trans. + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Q.T.le_refl Q.T.le_trans. Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _. End Q. @@ -160,7 +160,7 @@ Module Prop_ops. Instance aac_and_Comm : Commutative iff and. Proof. unfold Commutative; tauto. Qed. Instance aac_True : Unit iff or False. Proof. constructor; firstorder. Qed. Instance aac_False : Unit iff and True. Proof. constructor; firstorder. Qed. - + Program Instance aac_not_compat : Proper (iff ==> iff) not. Solve All Obligations using firstorder. @@ -174,7 +174,7 @@ Module Bool. Instance aac_andb_Comm : Commutative eq andb. Proof. unfold Commutative; firstorder. Qed. Instance aac_true : Unit eq orb false. Proof. constructor; firstorder. Qed. Instance aac_false : Unit eq andb true. Proof. constructor; intros [|];firstorder. Qed. - + Instance negb_compat : Proper (eq ==> eq) negb. Proof. intros [|] [|]; auto. Qed. End Bool. @@ -191,9 +191,9 @@ Module Relations. Definition bot : relation T := fun _ _ => False. Definition top : relation T := fun _ _ => True. End defs. - + Instance eq_same_relation T : Equivalence (same_relation T). Proof. firstorder. Qed. - + Instance aac_union_Comm T : Commutative (same_relation T) (union T). Proof. unfold Commutative; compute; intuition. Qed. Instance aac_union_Assoc T : Associative (same_relation T) (union T). Proof. unfold Associative; compute; intuition. Qed. Instance aac_bot T : Unit (same_relation T) (union T) (bot T). Proof. constructor; compute; intuition. Qed. @@ -201,7 +201,7 @@ Module Relations. Instance aac_inter_Comm T : Commutative (same_relation T) (inter T). Proof. unfold Commutative; compute; intuition. Qed. Instance aac_inter_Assoc T : Associative (same_relation T) (inter T). Proof. unfold Associative; compute; intuition. Qed. Instance aac_top T : Unit (same_relation T) (inter T) (top T). Proof. constructor; compute; intuition. Qed. - + (* note that we use [eq] directly as a neutral element for composition *) Instance aac_compo T : Associative (same_relation T) (compo T). Proof. unfold Associative; compute; firstorder. Qed. Instance aac_eq T : Unit (same_relation T) (compo T) (eq). Proof. compute; firstorder subst; trivial. Qed. @@ -231,10 +231,10 @@ Module Relations. Instance clos_refl_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_refl_trans T). Proof. intros R S H; split; apply clos_refl_trans_incr, H. Qed. - Instance preorder_inclusion T : PreOrder (inclusion T). + Instance preorder_inclusion T : PreOrder (inclusion T). Proof. constructor; unfold Reflexive, Transitive, inclusion; intuition. Qed. - - Instance lift_inclusion_same_relation T: AAC_lift (inclusion T) (same_relation T) := + + Instance lift_inclusion_same_relation T: AAC_lift (inclusion T) (same_relation T) := Build_AAC_lift (eq_same_relation T) _. Proof. firstorder. Qed. @@ -249,7 +249,7 @@ Module All. Export Bool. Export Relations. End All. - + (* Here, we should not see any instance of our classes. Print HintDb typeclass_instances. *) @@ -6,7 +6,7 @@ (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) -(** * Tutorial for using the [aac_tactics] library. +(** * Tutorial for using the [aac_tactics] library. Depending on your installation, either modify the following two lines, or add them to your .coqrc files, replacing "." with the @@ -17,7 +17,7 @@ Add ML Path ".". Require Import AAC. Require Instances. -(** ** Introductory example +(** ** Introductory example Here is a first example with relative numbers ([Z]): one can rewrite an universally quantified hypothesis modulo the @@ -39,37 +39,37 @@ Section introduction. reflexivity. Qed. - (** Notes: + (** Notes: - the tactic handles arbitrary function symbols like [Zopp] (as long as they are proper morphisms w.r.t. the considered equivalence relation); - here, ring would have done the job. *) -End introduction. +End introduction. -(** ** Usage +(** ** Usage One can also work in an abstract context, with arbitrary associative and commutative operators. (Note that one can declare several operations of each kind.) *) Section base. - Context {X} {R} {E: Equivalence R} - {plus} - {dot} + Context {X} {R} {E: Equivalence R} + {plus} + {dot} {zero} {one} - {dot_A: @Associative X R dot } + {dot_A: @Associative X R dot } {plus_A: @Associative X R plus } {plus_C: @Commutative X R plus } {dot_Proper :Proper (R ==> R ==> R) dot} {plus_Proper :Proper (R ==> R ==> R) plus} {Zero : Unit R plus zero} {One : Unit R dot one} - . - + . + Notation "x == y" := (R x y) (at level 70). Notation "x * y" := (dot x y) (at level 40, left associativity). Notation "1" := (one). @@ -83,7 +83,7 @@ Section base. Section reminder. Hypothesis H : forall x, x * x == x. Variables a b c : X. - + Goal (a+b+c)*(c+a+b) == a+b+c. aac_rewrite H. aac_reflexivity. @@ -97,7 +97,7 @@ Section base. aac_reflexivity. Qed. End reminder. - + (** The tactic can deal with "proper" morphisms of arbitrary arity (here [f] and [g], or [Zopp] earlier): it rewrites under such morphisms ([g]), and, more importantly, it is able to reorder @@ -108,7 +108,7 @@ Section base. Hypothesis Hf : Proper (R ==> R ==> R) f. Variable g : X -> X. Hypothesis Hg : Proper (R ==> R) g. - + Variable a b: X. Hypothesis H : forall x y, x+f (b+y) x == y+x. Goal g ((f (a+b) a) + a) == g (a+a). @@ -117,7 +117,7 @@ Section base. Qed. End morphisms. - (** *** Selecting what and where to rewrite + (** *** Selecting what and where to rewrite There are sometimes several solutions to the matching problem. We now show how to interact with the tactic to select the desired @@ -127,7 +127,7 @@ Section base. Variable f : X -> X. Variable a : X. Hypothesis Hf : Proper (R ==> R) f. - Hypothesis H : forall x, x + x == x. + Hypothesis H : forall x, x + x == x. Goal f(a+a)+f(a+a) == f a. (** In case there are several possible solutions, one can print @@ -137,29 +137,29 @@ Section base. (** the default choice is the occurrence with the smallest possible context (number 0), but one can choose the desired one; *) - aac_rewrite H at 1. - (** now the goal is [f a + f a == f a], there is only one solution. *) + aac_rewrite H at 1. + (** now the goal is [f a + f a == f a], there is only one solution. *) aac_rewrite H. reflexivity. Qed. - + End occurrence. Section subst. Variables a b c d : X. Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b. Hypothesis H': forall x, x + x == x. - + Goal a*c*d*c*d*b == a*c*d*b. (** Here, there is only one possible occurrence, but several substitutions; *) aac_instances H. (** one can select them with the proper keyword. *) - aac_rewrite H subst 1. + aac_rewrite H subst 1. aac_rewrite H'. aac_reflexivity. Qed. End subst. - + (** As expected, one can use both keywords together to select the occurrence and the substitution. We also provide a keyword to specify that the rewrite should be done in the right-hand side of @@ -169,7 +169,7 @@ Section base. Variables a b c d : X. Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b. Hypothesis H': forall x, x + x == x. - + Goal a*c*d*c*d*b*b == a*(c*d*b)*b. aac_instances H. aac_rewrite H at 1 subst 1. @@ -179,10 +179,10 @@ Section base. aac_rewrite H at 0 subst 1 in_right. aac_reflexivity. Qed. - + End both. - (** *** Distinction between [aac_rewrite] and [aacu_rewrite]: + (** *** Distinction between [aac_rewrite] and [aacu_rewrite]: [aac_rewrite] rejects solutions in which variables are instantiated by units, while the companion tactic, [aacu_rewrite] allows such @@ -192,31 +192,31 @@ Section base. Variables a b c: X. Hypothesis H: forall x, a*x*a == x. Goal a*a == 1. - (** Here, [x] must be instantiated with [1], so that the [aac_*] + (** Here, [x] must be instantiated with [1], so that the [aac_*] tactics give no solutions; *) - try aac_instances H. - (** while we get solutions with the [aacu_*] tactics. *) + try aac_instances H. + (** while we get solutions with the [aacu_*] tactics. *) aacu_instances H. aacu_rewrite H. reflexivity. - Qed. - + Qed. + (** We introduced this distinction because it allows us to rule out dummy cases in common situations: *) Hypothesis H': forall x y z, x*y + x*z == x*(y+z). Goal a*b*c + a*c + a*b == a*(c+b*(1+c)). (** 6 solutions without units, *) - aac_instances H'. + aac_instances H'. aac_rewrite H' at 0. (** more than 52 with units. *) aacu_instances H'. Abort. - End dealing_with_units. + End dealing_with_units. End base. -(** *** Declaring instances +(** *** Declaring instances To use one's own operations: it suffices to declare them as instances of our classes. (Note that the following instances are @@ -224,15 +224,15 @@ End base. Section Peano. Require Import Arith. - + Instance aac_plus_Assoc : Associative eq plus := plus_assoc. Instance aac_plus_Comm : Commutative eq plus := plus_comm. - - Instance aac_one : Unit eq mult 1 := - Build_Unit eq mult 1 mult_1_l mult_1_r. - Instance aac_zero_plus : Unit eq plus O := + + Instance aac_one : Unit eq mult 1 := + Build_Unit eq mult 1 mult_1_l mult_1_r. + Instance aac_zero_plus : Unit eq plus O := Build_Unit eq plus (O) plus_0_l plus_0_r. - + (** Two (or more) operations may share the same units: in the following example, [0] is understood as the unit of [max] as well as @@ -241,26 +241,26 @@ Section Peano. Instance aac_max_Comm : Commutative eq Max.max := Max.max_comm. Instance aac_max_Assoc : Associative eq Max.max := Max.max_assoc. - Instance aac_zero_max : Unit eq Max.max O := - Build_Unit eq Max.max 0 Max.max_0_l Max.max_0_r. + Instance aac_zero_max : Unit eq Max.max O := + Build_Unit eq Max.max 0 Max.max_0_l Max.max_0_r. Variable a b c : nat. Goal Max.max (a + 0) 0 = a. aac_reflexivity. Qed. - + (** Furthermore, several operators can be mixed: *) Hypothesis H : forall x y z, Max.max (x + y) (x + z) = x+ Max.max y z. - - Goal Max.max (a + b) (c + (a * 1)) = Max.max c b + a. + + Goal Max.max (a + b) (c + (a * 1)) = Max.max c b + a. aac_instances H. aac_rewrite H. aac_reflexivity. - Qed. - Goal Max.max (a + b) (c + Max.max (a*1+0) 0) = a + Max.max b c. + Qed. + Goal Max.max (a + b) (c + Max.max (a*1+0) 0) = a + Max.max b c. aac_instances H. aac_rewrite H. aac_reflexivity. Qed. - + (** *** Working with inequations To be able to use the tactics, the goal must be a relation [R] @@ -272,28 +272,28 @@ Section Peano. (** One can rewrite equations in the left member of inequations, *) Goal (forall x, x + x = x) -> a + b + b + a <= a + b. - intro Hx. + intro Hx. aac_rewrite Hx. reflexivity. Qed. (** or in the right member of inequations, using the [in_right] keyword *) Goal (forall x, x + x = x) -> a + b <= a + b + b + a. - intro Hx. + intro Hx. aac_rewrite Hx in_right. reflexivity. Qed. - + (** Similarly, one can rewrite inequations in inequations, *) Goal (forall x, x + x <= x) -> a + b + b + a <= a + b. - intro Hx. + intro Hx. aac_rewrite Hx. reflexivity. - Qed. + Qed. (** possibly in the right-hand side. *) Goal (forall x, x <= x + x) -> a + b <= a + b + b + a. - intro Hx. + intro Hx. aac_rewrite <- Hx in_right. reflexivity. Qed. @@ -319,7 +319,7 @@ Section Peano. End Peano. -(** *** Normalising goals +(** *** Normalising goals We also provide a tactic to normalise terms modulo AC. This normalisation is the one we use internally. *) @@ -329,7 +329,7 @@ Section AAC_normalise. Import Instances.Z. Require Import ZArith. Open Scope Z_scope. - + Variable a b c d : Z. Goal a + (b + c*c*d) + a + 0 + d*1 = a. aac_normalise. @@ -349,16 +349,16 @@ Section Examples. (** *** Reverse triangle inequality *) - Lemma Zabs_triangle : forall x y, Zabs (x + y) <= Zabs x + Zabs y . - Proof Zabs_triangle. + Lemma Zabs_triangle : forall x y, Zabs (x + y) <= Zabs x + Zabs y . + Proof Zabs_triangle. Lemma Zplus_opp_r : forall x, x + -x = 0. - Proof Zplus_opp_r. + Proof Zplus_opp_r. (** The following morphisms are required to perform the required rewrites *) Instance Zminus_compat : Proper (Zge ==> Zle) Zopp. Proof. intros x y. omega. Qed. - + Instance Proper_Zplus : Proper (Zle ==> Zle ==> Zle) Zplus. Proof. firstorder. Qed. @@ -367,8 +367,8 @@ Section Examples. aac_instances <- (Zminus_diag b). aac_rewrite <- (Zminus_diag b) at 3. unfold Zminus. - aac_rewrite Zabs_triangle. - aac_rewrite Zplus_opp_r. + aac_rewrite Zabs_triangle. + aac_rewrite Zplus_opp_r. aac_reflexivity. Qed. @@ -380,8 +380,8 @@ Section Examples. Lemma Hbin1: forall x y, (x+y)^2 = x^2 + y^2 + 2⋅x*y. Proof. intros; ring. Qed. Lemma Hbin2: forall x y, x^2 + y^2 = (x+y)^2 + -(2⋅x*y). Proof. intros; ring. Qed. - Lemma Hopp : forall x, x + -x = 0. Proof Zplus_opp_r. - + Lemma Hopp : forall x, x + -x = 0. Proof Zplus_opp_r. + Variables a b c : Z. Hypothesis H : c^2 + 2⋅(a+1)*b = (a+1+b)^2. Goal a^2 + b^2 + 2⋅a + 1 = c^2. |