diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-11-29 23:30:48 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-11-29 23:30:48 +0100 |
| commit | 1aa8b6f6a876af22f538c869f022bc4ca5986b40 (patch) | |
| tree | 037f0286a86b2bcee9bfa08f00112005a71e0e18 | |
Imported Upstream version 0.1-r13244upstream/0.1-r13244
| -rw-r--r-- | AAC.v | 689 | ||||
| -rw-r--r-- | COPYING | 674 | ||||
| -rw-r--r-- | COPYING.LESSER | 165 | ||||
| -rw-r--r-- | Instances.v | 150 | ||||
| -rw-r--r-- | LICENSE | 13 | ||||
| -rw-r--r-- | README.txt | 65 | ||||
| -rw-r--r-- | Tests.v | 373 | ||||
| -rw-r--r-- | Tutorial.v | 321 | ||||
| -rw-r--r-- | aac_rewrite.ml | 308 | ||||
| -rw-r--r-- | aac_rewrite.mli | 59 | ||||
| -rw-r--r-- | coq.ml | 212 | ||||
| -rw-r--r-- | coq.mli | 117 | ||||
| -rw-r--r-- | files.txt | 7 | ||||
| -rw-r--r-- | magic.txt | 4 | ||||
| -rwxr-xr-x | make_makefile | 49 | ||||
| -rw-r--r-- | matcher.ml | 980 | ||||
| -rw-r--r-- | matcher.mli | 192 | ||||
| -rw-r--r-- | theory.ml | 708 | ||||
| -rw-r--r-- | theory.mli | 219 |
19 files changed, 5305 insertions, 0 deletions
@@ -0,0 +1,689 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** * Theory file for the aac_rewrite tactic + + We define several base classes to package associative and possibly + commutative operators, and define a data-type for reified (or + quoted) expressions (with morphisms). + + We then define a reflexive decision procedure to decide the + equality of reified terms: first normalize 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 + + [H: forall x y, nat_of_pos (pos_of_nat (x) + y) + x = ....] + + where one occurence of [+] operates on nat while the other one + operates on positive. *) + +Require Import Arith NArith. +Require Import List. +Require Import FMapPositive FMapFacts. +Require Import RelationClasses Equality. +Require Export Morphisms. + +Set Implicit Arguments. +Unset Automatic Introduction. +Open Scope signature_scope. + +(** * Environments for the reification process: we use positive maps to index elements *) + +Section sigma. + Definition sigma := PositiveMap.t. + Definition sigma_get A (null : A) (map : sigma A) (n : positive) : A := + match PositiveMap.find n map with + | None => null + | Some x => x + end. + Definition sigma_add := @PositiveMap.add. + Definition sigma_empty := @PositiveMap.empty. +End sigma. + +(** * Packaging structures *) + +(** ** Free symbols *) +Module Sym. + Section t. + Context {X} {R : relation X} . + + (** type of an arity *) + Fixpoint type_of (n: nat) := + match n with + | O => X + | S n => X -> type_of n + end. + + (** relation to be preserved at an arity *) + 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, + and a proof that the value is a proper morphism *) + Record pack : Type := mkPack { + ar : nat; + value : type_of ar; + morph : Proper (rel_of ar) value + }. + + (** helper to build default values, when filling reification environments *) + Program Definition null (H: Equivalence R) (x : X) := mkPack 0 x _. + + End t. + +End Sym. + +(** ** Associative commutative operations (commutative monoids) + + See #<a href="Instances.html">Instances.v</a># for concrete instances of these classes. + +*) + +Class Op_AC (X:Type) (R: relation X) (plus: X -> X -> X) (zero:X) := { + plus_compat:> Proper (R ==> R ==> R) plus; + plus_neutral_left: forall x, R (plus zero x) x; + plus_assoc: forall x y z, R (plus x (plus y z)) (plus (plus x y) z); + plus_com: forall x y, R (plus x y) (plus y x) +}. + +Module Sum. + Section t. + Context {X : Type} {R: relation X}. + Class pack : Type := mkPack { + plus : X -> X -> X; + zero : X; + opac :> @Op_AC X R plus zero + }. + End t. +End Sum. + + + +(** ** Associative operations (monoids) *) +Class Op_A (X:Type) (R:relation X) (dot: X -> X -> X) (one: X) := { + dot_compat:> Proper (R ==> R ==> R) dot; + dot_neutral_left: forall x, R (dot one x) x; + dot_neutral_right: forall x, R (dot x one) x; + dot_assoc: forall x y z, R (dot x (dot y z)) (dot (dot x y) z) +}. + + +Module Prd. + Section t. + Context {X : Type} {R: relation X}. + Class pack : Type := mkPack { + dot : X -> X -> X; + one : X; + opa :> @Op_A X R dot one + }. + End t. +End Prd. + + +(** an helper lemma to derive an A class out of an AC one (not + declared as an instance to avoid useless branches in typeclass + resolution) *) +Lemma AC_A {X} {R:relation X} {EQ: Equivalence R} {plus} {zero} (op: Op_AC R plus zero): Op_A R plus zero. +Proof. + split; try apply op. + intros. rewrite plus_com. apply op. +Qed. + + + +(** * Utilities for the evaluation function *) +Section copy. + + Context {X} {R: relation X} {HR : @Equivalence X R} {plus} {zero} {op: @Op_AC X R plus zero}. + + (* copy n x = x+...+x (n times) *) + 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 plus_assoc. + 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 plus_compat; auto. + Qed. + +End copy. + +(** * Utilities for positive numbers + which we use as: + - indices for morphisms and symbols + - multiplicity of terms in sums + *) +Notation idx := positive. + +Fixpoint eq_idx_bool i j := + 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 + | _, _ => false + end. + +Fixpoint idx_compare i j := + match i,j with + | xH, xH => Eq + | xH, _ => Lt + | _, xH => Gt + | xO i, xO j => idx_compare i j + | xI i, xI j => idx_compare i j + | xI _, xO _ => Gt + | xO _, xI _ => Lt + end. + +Notation pos_compare := idx_compare (only parsing). + +(** specification predicate for boolean binary functions *) +Inductive decide_spec {A} {B} (R : A -> B -> Prop) (x : A) (y : B) : bool -> Prop := +| decide_true : R x y -> decide_spec R x y true +| decide_false : ~(R x y) -> decide_spec R x y false. + +Lemma eq_idx_spec : forall i j, decide_spec (@eq _) i j (eq_idx_bool i j). +Proof. + induction i; destruct j; simpl; try (constructor; congruence). + case (IHi j); constructor; congruence. + case (IHi j); constructor; congruence. +Qed. + +(** weak specification predicate for comparison functions: only the 'Eq' case is specified *) +Inductive compare_weak_spec A: A -> A -> comparison -> Prop := +| pcws_eq: forall i, compare_weak_spec i i Eq +| pcws_lt: forall i j, compare_weak_spec i j Lt +| pcws_gt: forall i j, compare_weak_spec i j Gt. + +Lemma pos_compare_weak_spec: forall i j, compare_weak_spec i j (pos_compare i j). +Proof. induction i; destruct j; simpl; try constructor; case (IHi j); intros; constructor. Qed. + +Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j. +Proof. intros i j. case (pos_compare_weak_spec i j); intros; congruence. Qed. + + +(** * Dependent types utilities *) +Notation cast T H u := (eq_rect _ T u _ H). + +Section dep. + Variable U: Type. + Variable T: U -> Type. + + 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. + + 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 -> 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. + + 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. + intro H'. apply reflect_eqdep_eq in H'. subst. constructor. assumption. + Defined. +End dep. + + +(** * Utilities about lists and multisets *) + +(** finite multisets are represented with ordered lists with multiplicities *) +Definition mset A := list (A*positive). + +(** lexicographic composition of comparisons (this is a notation to keep it lazy) *) +Notation lex e f := (match e with Eq => f | _ => e end). + + +Section lists. + + (** comparison function *) + Section c. + Variables A B: Type. + Variable compare: A -> B -> comparison. + Fixpoint list_compare h k := + match h,k with + | nil, nil => Eq + | nil, _ => Lt + | _, nil => Gt + | u::h, v::k => lex (compare u v) (list_compare h k) + 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 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 + in the lemma [tcompare_weak_spec] below *) + 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. + case (Hcompare u v); try constructor. + case (IHh k); intros; constructor. + Defined. + End list_compare_weak_spec. + + Section mset_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 + in the lemma [tcompare_weak_spec] below *) + Lemma mset_compare_weak_spec: forall h k, compare_weak_spec h k (mset_compare compare h k). + Proof. + apply list_compare_weak_spec. + intros [u n] [v m]. + case (Hcompare u v); try constructor. + case (pos_compare_weak_spec n m); try constructor. + Defined. + End mset_compare_weak_spec. + + (** (sorted) merging functions *) + Section m. + Variable A: Type. + Variable compare: A -> A -> comparison. + + Fixpoint merge_msets l1 := + match l1 with + | nil => fun l2 => l2 + | (h1,n1)::t1 => + let fix merge_aux l2 := + match l2 with + | nil => l1 + | (h2,n2)::t2 => + match compare h1 h2 with + | Eq => (h1,Pplus n1 n2)::merge_msets t1 t2 + | Lt => (h1,n1)::merge_msets t1 l2 + | Gt => (h2,n2)::merge_aux t2 + end + end + in merge_aux + end. + + (** interpretation of a list with a constant and a binary operation *) + Variable B: Type. + Variable map: A -> B. + Variable b2: B -> B -> B. + Variable b0: B. + Fixpoint fold_map l := + match l with + | nil => b0 + | u::nil => map u + | u::l => b2 (map u) (fold_map l) + end. + + (** mapping and merging *) + Variable merge: A -> list B -> list B. + Fixpoint merge_map (l: list A): list B := + match l with + | nil => nil + | u::l => merge u (merge_map l) + end. + + End m. + +End lists. + + + +(** * Reification, normalisation, and decision *) +Section s. + Context {X} {R: relation X} {E: @Equivalence X R}. + Infix "==" := R (at level 80). + + (* We use environments to store the various operators and the + morphisms.*) + + Variable e_sym: idx -> @Sym.pack X R. + Variable e_prd: idx -> @Prd.pack X R. + Variable e_sum: idx -> @Sum.pack X R. + Hint Resolve e_sum e_prd: typeclass_instances. + + + (** ** Almost normalised syntax + a term in [T] is in normal form if: + - sums do not contain sums + - 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), + + Note that [T] and [vT] depend on the [e_sym] environment (which + contains, among other things, the arity of symbols) + *) + Inductive T: Type := + | sum: idx -> mset T -> T + | prd: idx -> list T -> T + | sym: forall i, vT (Sym.ar (e_sym i)) -> T + with vT: nat -> Type := + | vnil: vT O + | vcons: forall n, T -> vT n -> vT (S n). + + + (** lexicographic rpo over the normalised syntax *) + Fixpoint compare (u v: T) := + 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) + | sum _ _, _ => Lt + | _ , sum _ _ => Gt + | prd _ _, _ => Lt + | _ , prd _ _ => Gt + end + with vcompare i j (us: vT i) (vs: vT j) := + match us,vs with + | vnil, vnil => Eq + | vnil, _ => Lt + | _, vnil => Gt + | vcons _ u us, vcons _ v vs => lex (compare u v) (vcompare us vs) + end. + + + (** we need to show that compare reflects equality + (this is because we work with msets rather than lists with arities) + *) + + Lemma tcompare_weak_spec: forall (u v : T), compare_weak_spec u v (compare u v) + with vcompare_reflect_eqdep: forall i us j vs (H: i=j), vcompare us vs = Eq -> cast vT H us = vs. + Proof. + induction u. + destruct v; simpl; try constructor. + case (pos_compare_weak_spec p p0); intros; try constructor. + case (mset_compare_weak_spec compare tcompare_weak_spec m m0); intros; try constructor. + destruct v; simpl; try constructor. + case (pos_compare_weak_spec p p0); intros; try constructor. + case (list_compare_weak_spec compare tcompare_weak_spec l l0); intros; try constructor. + destruct v0; simpl; try constructor. + case_eq (idx_compare i i0); intro Hi; try constructor. + apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst. (* the [symmetry] is required ! *) + case_eq (vcompare v v0); intro Hv; try constructor. + rewrite <- (vcompare_reflect_eqdep _ _ _ _ eq_refl Hv). constructor. + + induction us; destruct vs; simpl; intros H Huv; try discriminate. + apply cast_eq, eq_nat_dec. + injection H; intro Hn. + revert Huv; case (tcompare_weak_spec t t0); intros; try discriminate. + symmetry in Hn. subst. (* symmetry required *) + rewrite <- (IHus _ _ eq_refl Huv). + apply cast_eq, eq_nat_dec. + Qed. + + (** ** Evaluation from syntax to the abstract domain *) + Fixpoint eval u: X := + match u with + | sum i l => fold_map (fun un => let '(u,n):=un in @copy _ (@Sum.plus _ _ (e_sum i)) n (eval u)) + (@Sum.plus _ _ (e_sum i)) (@Sum.zero _ _ (e_sum i)) l + | prd i l => fold_map eval + (@Prd.dot _ _ (e_prd i)) (@Prd.one _ _ (e_prd i)) l + | sym i v => @eval_aux _ v (Sym.value (e_sym i)) + end + with eval_aux i (v: vT i): Sym.type_of i -> X := + match v with + | vnil => fun f => f + | vcons _ u v => fun f => eval_aux v (f (eval u)) + end. + + + Instance eval_aux_compat i (l: vT i): Proper (@Sym.rel_of X R i ==> R) (eval_aux l). + Proof. + induction l; simpl; repeat intro. + assumption. + apply IHl, H. reflexivity. + Qed. + + + (** ** Normalisation *) + + (** auxiliary functions, to clean up sums and products *) + Definition sum' i (u: mset T): T := + match u with + | (u,xH)::nil => u + | _ => sum i u + end. + Definition is_sum i (u: T): option (mset T) := + match u with + | sum j l => if eq_idx_bool j i then Some l else None + | u => None + end. + Definition copy_mset n (l: mset T): mset T := + match n with + | xH => l + | _ => List.map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l + end. + Definition sum_to_mset i (u: T) n := + match is_sum i u with + | Some l' => copy_mset n l' + | None => (u,n)::nil + end. + + Definition prd' i (u: list T): T := + match u with + | u::nil => u + | _ => prd i u + end. + Definition is_prd i (u: T): option (list T) := + match u with + | prd j l => if eq_idx_bool j i then Some l else None + | u => None + end. + Definition prd_to_list i (u: T) := + match is_prd i u with + | Some l' => l' + | None => u::nil + end. + + + (** we deduce the normalisation function *) + Fixpoint norm u := + match u with + | sum i l => sum' i (merge_map (fun un l => let '(u,n):=un in + merge_msets compare (sum_to_mset i (norm u) n) l) l) + | prd i l => prd' i (merge_map (fun u l => prd_to_list i (norm u) ++ l) l) + | sym i l => sym i (vnorm l) + end + with vnorm i (l: vT i): vT i := + match l with + | vnil => vnil + | vcons _ u l => vcons (norm u) (vnorm l) + end. + + + (** ** Correctness *) + + (** auxiliary lemmas about sums *) + Lemma sum'_sum i (l: mset T): eval (sum' i l) ==eval (sum i l) . + Proof. + intros i [|? [|? ?]]. + reflexivity. + destruct p; destruct p; simpl; reflexivity. + destruct p; destruct p; simpl; reflexivity. + Qed. + + Lemma eval_sum_cons i n a (l: mset T): + (eval (sum i ((a,n)::l))) == (@Sum.plus _ _ (e_sum i) (@copy _ (@Sum.plus _ _ (e_sum i)) n (eval a)) (eval (sum i l))). + Proof. + intros i n a [|[b m] l]; simpl. + rewrite plus_com, plus_neutral_left. reflexivity. + reflexivity. + Qed. + + Lemma eval_sum_app i (h k: mset T): eval (sum i (h++k)) == @Sum.plus _ _ (e_sum i) (eval (sum i h)) (eval (sum i k)). + Proof. + induction h; intro k. + simpl. rewrite plus_neutral_left. reflexivity. + simpl app. destruct a. rewrite 2 eval_sum_cons, IHh, plus_assoc. reflexivity. + Qed. + + Lemma eval_merge_sum i (h k: mset T): + eval (sum i (merge_msets compare h k)) == @Sum.plus _ _ (e_sum i) (eval (sum i h)) (eval (sum i k)). + Proof. + induction h as [|[a n] h IHh]; intro k. + simpl. rewrite plus_neutral_left. reflexivity. + induction k as [|[b m] k IHk]. + simpl. setoid_rewrite plus_com. rewrite plus_neutral_left. reflexivity. + simpl merge_msets. rewrite eval_sum_cons. destruct (tcompare_weak_spec a b) as [a|a b|a b]. + rewrite 2eval_sum_cons. rewrite IHh. rewrite <- plus_assoc. setoid_rewrite plus_assoc at 3. + setoid_rewrite plus_com at 5. rewrite !plus_assoc. rewrite copy_plus. reflexivity. + + rewrite eval_sum_cons. rewrite IHh. apply plus_assoc. + + rewrite <- eval_sum_cons. setoid_rewrite eval_sum_cons at 3. + rewrite plus_com, <- plus_assoc. rewrite plus_com in IHk. rewrite <- IHk. + rewrite eval_sum_cons. apply plus_compat; reflexivity. + Qed. + + Inductive sum_spec: T -> option (mset T) -> Prop := + | ss_sum1: forall i l, sum_spec (sum i l) (Some l) + | ss_sum2: forall j i l, i<>j -> sum_spec (sum i l) None + | ss_prd: forall i l, sum_spec (prd i l) None + | ss_sym: forall i l, sum_spec (@sym i l) None. + Lemma is_sum_spec: forall i (a: T), sum_spec a (is_sum i a). + Proof. + intros i [j l|j l|j l]; simpl; try constructor. + case eq_idx_spec; intro. + subst. constructor. + econstructor. eassumption. + Qed. + + Lemma eval_is_sum: forall i (a: T) k, is_sum i a = Some k -> eval (sum i k) = eval a. + Proof. + intros i [j l|j l|j l] k; simpl is_sum; try (intro; discriminate). + case eq_idx_spec; intros ? H. + injection H. clear H. intros <-. congruence. + discriminate. + Qed. + + Lemma copy_mset' n (l: mset T): + copy_mset n l = List.map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l. + Proof. + intros. destruct n; try reflexivity. + simpl. induction l as [|[a l] IHl]; simpl; congruence. + Qed. + + + Lemma copy_mset_succ i n (l: mset T): + eval (sum i (copy_mset (Psucc n) l)) == @Sum.plus _ _ (e_sum i) (eval (sum i l)) (eval (sum i (copy_mset n l))). + Proof. + intros. rewrite 2copy_mset'. + induction l as [|[a m] l IHl]. + simpl eval at 2. rewrite plus_neutral_left. destruct n; reflexivity. + simpl map. rewrite ! eval_sum_cons. rewrite IHl. + rewrite Pmult_Sn_m. rewrite copy_plus. rewrite <- !plus_assoc. apply plus_compat; try reflexivity. + setoid_rewrite plus_com at 3. rewrite <- !plus_assoc. apply plus_compat; try reflexivity. apply plus_com. + Qed. + + Lemma eval_sum_to_mset: forall i n a, eval (sum i (sum_to_mset i a n)) == @copy _ (@Sum.plus _ _ (e_sum i)) n (eval a). + Proof. + intros. unfold sum_to_mset. + case_eq (is_sum i a). + intros k Hk. induction n using Pind. + simpl copy_mset. rewrite (eval_is_sum _ _ Hk). reflexivity. + rewrite copy_mset_succ. rewrite IHn. rewrite (eval_is_sum _ _ Hk). + unfold copy at 2. rewrite Prect_succ. reflexivity. + reflexivity. + Qed. + + + (** auxiliary lemmas about products *) + Lemma prd'_prd i (l: list T): eval (prd' i l) == eval (prd i l). + Proof. intros i [|? [|? ?]]; reflexivity. Qed. + + Lemma eval_prd_cons i a (l: list T): eval (prd i (a::l)) == @Prd.dot _ _ (e_prd i) (eval a) (eval (prd i l)). + Proof. + intros i a [|b l]; simpl. + rewrite dot_neutral_right. reflexivity. + reflexivity. + Qed. + + Lemma eval_prd_app i (h k: list T): eval (prd i (h++k)) == @Prd.dot _ _ (e_prd i) (eval (prd i h)) (eval (prd i k)). + Proof. + induction h; intro k. + simpl. rewrite dot_neutral_left. reflexivity. + simpl app. rewrite 2 eval_prd_cons, IHh, dot_assoc. reflexivity. + Qed. + + Lemma eval_is_prd: forall i (a: T) k, is_prd i a = Some k -> eval (prd i k) = eval a. + Proof. + intros i [j l|j l|j l] k; simpl is_prd; try (intro; discriminate). + case eq_idx_spec; intros ? H. + injection H. clear H. intros <-. subst. congruence. + discriminate. + Qed. + + Lemma eval_prd_to_list: forall i a, eval (prd i (prd_to_list i a)) = eval a. + Proof. + intros. unfold prd_to_list. + case_eq (is_prd i a). + intros k Hk. apply eval_is_prd. assumption. + reflexivity. + Qed. + + + (** 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), + Proper (@Sym.rel_of X R i) f -> eval_aux (vnorm l) f == eval_aux l f. + Proof. + induction u. + simpl norm. rewrite sum'_sum. induction m as [|[u n] m IHm]. + reflexivity. + simpl merge_map. rewrite eval_merge_sum. + rewrite eval_sum_to_mset, IHm, eval_norm. + rewrite eval_sum_cons. reflexivity. + + simpl norm. rewrite prd'_prd. induction l. + reflexivity. + simpl merge_map. + rewrite eval_prd_app. + rewrite eval_prd_to_list, IHl, eval_norm. + rewrite eval_prd_cons. reflexivity. + + simpl. apply eval_norm_aux, Sym.morph. + + + induction l; simpl; intros f Hf. + reflexivity. + rewrite eval_norm. apply IHl, Hf. reflexivity. + Qed. + + (** corollaries, for goal normalisation or decision *) + 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. + +End s. +Declare ML Module "aac_tactics". @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/> + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + <one line to give the program's name and a brief idea of what it does.> + Copyright (C) <year> <name of author> + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see <http://www.gnu.org/licenses/>. + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + <program> Copyright (C) <year> <name of author> + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +<http://www.gnu.org/licenses/>. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +<http://www.gnu.org/philosophy/why-not-lgpl.html>. diff --git a/COPYING.LESSER b/COPYING.LESSER new file mode 100644 index 0000000..cca7fc2 --- /dev/null +++ b/COPYING.LESSER @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/> + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. diff --git a/Instances.v b/Instances.v new file mode 100644 index 0000000..1a2e08f --- /dev/null +++ b/Instances.v @@ -0,0 +1,150 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Instances for aac_rewrite.*) + +(* At the moment, all the instances are exported even if they are packaged into modules. *) + +Require Export AAC. + +Module Peano. + Require Import Arith NArith Max. + Program Instance aac_plus : @Op_AC nat eq plus 0 := @Build_Op_AC nat (@eq nat) plus 0 _ plus_0_l plus_assoc plus_comm. + + + Program Instance aac_mult : Op_AC eq mult 1 := Build_Op_AC _ _ _ mult_assoc mult_comm. + (* We also declare a default associative operation: this is currently + required to fill reification environments *) + Definition default_a := AC_A aac_plus. Existing Instance default_a. +End Peano. + +Module Z. + Require Import ZArith. + Open Scope Z_scope. + Program Instance aac_plus : Op_AC eq Zplus 0 := Build_Op_AC _ _ _ Zplus_assoc Zplus_comm. + Program Instance aac_mult : Op_AC eq Zmult 1 := Build_Op_AC _ _ Zmult_1_l Zmult_assoc Zmult_comm. + Definition default_a := AC_A aac_plus. Existing Instance default_a. +End Z. + +Module Q. + Require Import QArith. + Program Instance aac_plus : Op_AC Qeq Qplus 0 := Build_Op_AC _ _ Qplus_0_l Qplus_assoc Qplus_comm. + Program Instance aac_mult : Op_AC Qeq Qmult 1 := Build_Op_AC _ _ Qmult_1_l Qmult_assoc Qmult_comm. + Definition default_a := AC_A aac_plus. Existing Instance default_a. +End Q. + +Module Prop_ops. + Program Instance aac_or : Op_AC iff or False. Solve All Obligations using tauto. + + Program Instance aac_and : Op_AC iff and True. Solve All Obligations using tauto. + + Definition default_a := AC_A aac_and. Existing Instance default_a. + + Program Instance aac_not_compat : Proper (iff ==> iff) not. + Solve All Obligations using firstorder. +End Prop_ops. + +Module Bool. + Program Instance aac_orb : Op_AC eq orb false. + Solve All Obligations using firstorder. + + Program Instance aac_andb : Op_AC eq andb true. + Solve All Obligations using firstorder. + + Definition default_a := AC_A aac_andb. Existing Instance default_a. + + Instance negb_compat : Proper (eq ==> eq) negb. + Proof. intros [|] [|]; auto. Qed. +End Bool. + +Module Relations. + Require Import Relations. + Section defs. + Variable T : Type. + Variables R S: relation T. + Definition inter : relation T := fun x y => R x y /\ S x y. + Definition compo : relation T := fun x y => exists z : T, R x z /\ S z y. + Definition negr : relation T := fun x y => ~ R x y. + (* union and converse are already defined in the standard library *) + + Definition bot : relation T := fun _ _ => False. + Definition top : relation T := fun _ _ => True. + End defs. + + Program Instance aac_union T : Op_AC (same_relation T) (union T) (bot T). + Solve All Obligations using compute; [tauto || intuition]. + + Program Instance aac_inter T : Op_AC (same_relation T) (inter T) (top T). + Solve All Obligations using compute; firstorder. + + (* note that we use [eq] directly as a neutral element for composition *) + Program Instance aac_compo T : Op_A (same_relation T) (compo T) eq. + Solve All Obligations using compute; firstorder. + Solve All Obligations using compute; firstorder subst; trivial. + + Instance negr_compat T : Proper (same_relation T ==> same_relation T) (negr T). + Proof. compute. firstorder. Qed. + + Instance transp_compat T : Proper (same_relation T ==> same_relation T) (transp T). + Proof. compute. firstorder. Qed. + + Instance clos_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_trans T). + Proof. + intros R S H x y Hxy. induction Hxy. + constructor 1. apply H. assumption. + econstructor 2; eauto 3. + Qed. + Instance clos_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_trans T). + Proof. intros R S H; split; apply clos_trans_incr, H. Qed. + + Instance clos_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T). + Proof. + intros R S H x y Hxy. induction Hxy. + constructor 1. apply H. assumption. + constructor 2. + econstructor 3; eauto 3. + Qed. + 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. + +End Relations. + +Module All. + Export Peano. + Export Z. + Export Prop_ops. + Export Bool. + Export Relations. +End All. + +(* A small test to ensure that everything can live together *) +(* Section test. + Import All. + Require Import ZArith. + Open Scope Z_scope. + Notation "x ^2" := (x*x) (at level 40). + Hypothesis H : forall x y, x^2 + y^2 + x*y + x* y = (x+y)^2. + Goal forall a b c, a*1*(a ^2)*a + c + (b+0)*1*b + a^2*b + a*b*a = (a^2+b)^2+c. + intros. + aac_rewrite H. + aac_rewrite <- H . + symmetry. + aac_rewrite <- H . + aac_reflexivity. + Qed. + Open Scope nat_scope. + Notation "x ^^2" := (x * x) (at level 40). + Hypothesis H' : forall (x y : nat), x^^2 + y^^2 + x*y + x* y = (x+y)^^2. + + Goal forall (a b c : nat), a*1*(a ^^2)*a + c + (b+0)*1*b + a^^2*b + a*b*a = (a^^2+b)^^2+c. + intros. aac_rewrite H'. aac_reflexivity. + Qed. +End test. + +*) + @@ -0,0 +1,13 @@ +The aac_tactics plugin library is free software: you can redistribute +it and/or modify it under the terms of the GNU Lesser General Public +License as published by the Free Software Foundation, either version 3 +of the License, or (at your option) any later version. + +This library is distributed in the hope that it will be useful, but +WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +Lesser General Public License for more details. + +You should have received a copy of the GNU Lesser General Public +License along with this library. If not, see +<http://www.gnu.org/licenses/>. diff --git a/README.txt b/README.txt new file mode 100644 index 0000000..ad3b5c9 --- /dev/null +++ b/README.txt @@ -0,0 +1,65 @@ + + aac_tactics + =========== + + Thomas Braibant & Damien Pous + +Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France + +Webpage of the project: http://sardes.inrialpes.fr/~braibant/aac_tactics/ + + +FOREWORD +======== + +This plugin provides tactics for rewriting universally quantified +equations, modulo associativity and commutativity of some operators. + +INSTALL +======= + +- run [./make_makefile] in the top-level directory to generate a Makefile +- run [make world] to build the plugin and the documentation + +This should work with Coq v8.3 `beta' : -r 13027, -r 13060 and hopefully the +following ones. + +To be able to import the plugin from anywhere, add the following to +your ~/.coqrc + +Add Rec LoadPath "path_to_aac_tactics". +Add ML Path "path_to_aac_tactics". + + +DOCUMENTATION +============= + +Please refer to Tutorial.v for a succint introduction on how to use +this plugin. + +To understand the inner-working of the tactic, please refer to the +.mli files as the main source of information on each .ml +file. Alternatively, [make world] generates ocamldoc/coqdoc +documentation in directories doc/ and html/, respectively. + +File Instances.v defines several instances for frequent use-cases of +this plugin, that should allow you to use it out-of-the-shelf. Namely, +we have instances for: + +- Peano naturals (Import Instances.Peano) +- Z binary numbers (Import Instances.Z) +- Rationnal numbers (Import Instances.Q) +- Prop (Import Instances.Prop_ops) +- Booleans (Import Instances.Bool) +- Relations (Import Instances.Relations) +- All of the above (Import Instances.All) + + +ACKNOWLEDGEMENTS +================ + +We are grateful to Evelyne Contejean, Hugo Herbelin, Assia Mahboubi +and Matthieu Sozeau for highly instructive discussions. + +This plugin took inspiration from the plugin tutorial "constructors", +distributed under the LGPL 2.1, copyrighted by Matthieu Sozeau @@ -0,0 +1,373 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +Require Import AAC. + +Section sanity. + + Context {X} {R} {E: Equivalence R} {plus} {zero} + {dot} {one} {A: @Op_A X R dot one} {AC: Op_AC R plus zero}. + + + Notation "x == y" := (R x y) (at level 70). + Notation "x * y" := (dot x y) (at level 40, left associativity). + Notation "1" := (one). + Notation "x + y" := (plus x y) (at level 50, left associativity). + Notation "0" := (zero). + + Section t0. + Hypothesis H : forall x, x+x == x. + Goal forall a b, a+b +a == a+b. + intros a b; aacu_rewrite H; aac_reflexivity. + Qed. + End t0. + + Section t1. + Variables a b : X. + + Variable P : X -> Prop. + Hypothesis H : forall x y, P y -> x+y+x == x. + Hypothesis Hb : P b. + Goal a+b +a == a. + aacu_rewrite H. + aac_reflexivity. + auto. + Qed. + End t1. + + Section t. + Variable f : X -> X. + Hypothesis Hf : Proper (R ==> R) f. + Hypothesis H : forall x, x+x == x. + Goal forall y, f(y+y) == f (y). + intros y. + aacu_instances H. + aacu_rewrite H. + aac_reflexivity. + Qed. + + Goal forall y z, f(y+z+z+y) == f (y+z). + intros y z. + aacu_instances H. + aacu_rewrite H. + aac_reflexivity. + Qed. + + Hypothesis H' : forall x, x*x == x. + Goal forall y z, f(y*z*y*z) == f (y*z). + intros y z. + aacu_instances H'. + aacu_rewrite H'. + aac_reflexivity. + Qed. + End t. + + Goal forall x y, (plus x y) == (plus y x). intros. + aac_reflexivity. + Qed. + + Goal forall x y, R (plus (dot x one) y) (plus y x). intros. + aac_reflexivity. + Qed. + + Goal (forall f y, f y + f y == y) -> forall a b g (Hg: Proper (R ==> R) g), g (a+b) + g b + g (b+a) == a + b + g b. + intros. + try aacu_rewrite H. + aacu_rewrite (H g). + Restart. + intros. + set (H' := H g). + aacu_rewrite H'. + aac_reflexivity. + Qed. + + Section t2. + Variables a b: X. + Variables g : X ->X. + Hypothesis Hg:Proper (R ==> R) g. + Hypothesis H: (forall y, (g y) + y == y). + Goal g (a+b) + b +a+a == a + b +a. + intros. + aacu_rewrite H. + aac_reflexivity. + Qed. + End t2. + Section t3. + Variables a b: X. + Variables g : X ->X. + Hypothesis Hg:Proper (R ==> R) g. + Hypothesis H: (forall f y, f y + y == y). + + Goal g (a+b) + b +a+a == a + b +a. + intros. + aacu_rewrite (H g). + aac_reflexivity. + Qed. +End t3. + +Section null. + Hypothesis dot_ann : forall x, 0 * x == 0. + Goal forall a, 0*a == 0. + intros a. aac_rewrite dot_ann. reflexivity. + Qed. +End null. + +End sanity. + +Section abs. + Context + {X} {E: Equivalence (@eq X)} + {plus} {zero} {AC: @Op_AC X eq plus zero} + {plus'} {zero'} {AC': @Op_AC X eq plus' zero'} + {dot} {one} {A: @Op_A X eq dot one} + {dot'} {one'} {A': @Op_A X eq dot' one'}. + + Notation "x * y" := (dot x y) (at level 40, left associativity). + Notation "x @ y" := (dot' x y) (at level 20, left associativity). + Notation "1" := (one). + Notation "1'" := (one'). + Notation "x + y" := (plus x y) (at level 50, left associativity). + Notation "x ^ y" := (plus' x y) (at level 30, right associativity). + Notation "0" := (zero). + Notation "0'" := (zero'). + + Variables a b c d e k: X. + Variables f g: X -> X. + Hypothesis Hf: Proper (eq ==> eq) f. + Hypothesis Hg: Proper (eq ==> eq) g. + + Variables h: X -> X -> X. + Hypothesis Hh: Proper (eq ==> eq ==> eq) h. + + Variables q: X -> X -> X -> X. + Hypothesis Hq: Proper (eq ==> eq ==> eq ==> eq) q. + + + + + Hypothesis dot_ann_left: forall x, 0*x = 0. + + Goal f (a*0*b*c*d) = k. + aac_rewrite dot_ann_left. + Restart. + aac_rewrite dot_ann_left subterm 1 subst 0. + Abort. + + + + + Hypothesis distr_dp: forall x y z, x*(y+z) = x*y+x*z. + Hypothesis distr_dp': forall x y z, x*y+x*z = x*(y+z). + + Hypothesis distr_pp: forall x y z, x^(y+z) = x^y+x^z. + Hypothesis distr_pp': forall x y z, x^y+x^z = x^(y+z). + + Hypothesis distr_dd: forall x y z, x@(y*z) = x@y * x@z. + Hypothesis distr_dd': forall x y z, x@y * x@z = x@(y*z). + + + Goal a*b*(c+d+e) = k. + aac_instances distr_dp. + aacu_instances distr_dp. + aac_rewrite distr_dp subterm 0 subst 4. + + aac_instances distr_dp'. + aac_rewrite distr_dp'. + Abort. + + Goal a@(b*c)@d@(e*e) = k. + aacu_instances distr_dd. + aac_instances distr_dd. + aac_rewrite distr_dd. + Abort. + + Goal a^(b+c)^d^(e+e) = k. + aacu_instances distr_dd. + aac_instances distr_dd. + aacu_instances distr_pp. + aac_instances distr_pp. + aac_rewrite distr_pp subterm 9. + Abort. + + + + + Hypothesis plus_idem: forall x, x+x = x. + Hypothesis plus_idem3: forall x, x+x+x = x. + Hypothesis dot_idem: forall x, x*x = x. + Hypothesis dot_idem3: forall x, x*x*x = x. + + Goal a*b*a*b = k. + aac_instances dot_idem. + aacu_instances dot_idem. + aac_rewrite dot_idem. + aac_instances distr_dp. (* TODO: no solution -> fail ? *) + aacu_instances distr_dp. + Abort. + + Goal a+a+a+a = k. + aac_instances plus_idem3. + aac_rewrite plus_idem3. + Abort. + + Goal a*a*a*a = k. + aac_instances dot_idem3. + aac_rewrite dot_idem3. + Abort. + + Goal a*a*a*a*a*a = k. + aac_instances dot_idem3. + aac_rewrite dot_idem3. + Abort. + + Goal f(a*a)*f(a*a) = k. + aac_instances dot_idem. + (* TODO: pas clair qu'on doive réécrire les deux petits + sous-termes quand on nous demande de n'en réécrire qu'un... + d'autant plus que le comportement est nécessairement + imprévisible (cf. les deux exemples en dessous) + ceci dit, je suis conscient que c'est relou à empêcher... *) + aac_rewrite dot_idem subterm 1. + Abort. + + Goal f(a*a*b)*f(a*a*b) = k. + aac_instances dot_idem. + aac_rewrite dot_idem subterm 2. (* une seule instance réécrite *) + Abort. + + Goal f(b*a*a)*f(b*a*a) = k. + aac_instances dot_idem. + aac_rewrite dot_idem subterm 2. (* deux instances réécrites *) + Abort. + + Goal h (a*a) (a*b*c*d*e) = k. + aac_rewrite dot_idem. + Abort. + + Goal h (a+a) (a+b+c+d+e) = k. + aac_rewrite plus_idem. + Abort. + + Goal (a*a+a*a+b)*c = k. + aac_rewrite plus_idem. + Restart. + aac_rewrite dot_idem. + Abort. + + + + + Hypothesis dot_inv: forall x, x*f x = 1. + Hypothesis plus_inv: forall x, x+f x = 0. + Hypothesis dot_inv': forall x, f x*x = 1. + + Goal a*f(1)*b = k. + try aac_rewrite dot_inv. (* TODO: à terme, j'imagine qu'on souhaite accepter ça, même en aac *) + aacu_rewrite dot_inv. + Abort. + + Goal f(1) = k. + aacu_rewrite dot_inv. + Restart. + aacu_rewrite dot_inv'. + Abort. + + Goal b*f(b) = k. + aac_rewrite dot_inv. + Abort. + + Goal f(b)*b = k. + aac_rewrite dot_inv'. + Abort. + + Goal a*f(a*b)*a*b*c = k. + aac_rewrite dot_inv'. + Abort. + + Goal g (a*f(a*b)*a*b*c+d) = k. + aac_rewrite dot_inv'. + Abort. + + Goal g (a+f(a+b)+c+b+b) = k. + aac_rewrite plus_inv. + Abort. + + Goal g (a+f(0)+c) = k. + aac_rewrite plus_inv. + Abort. + + + + + + Goal forall R S, Equivalence R -> Equivalence S -> R a k -> S a k. + intros R S HR HS H. + try (aac_rewrite H ; fail 1 "ne doit pas passer"). + try (aac_instances H; fail 1 "ne doit pas passer"). + Abort. + + Goal forall R S, Equivalence R -> Equivalence S -> (forall x, R (f x) k) -> S (f a) k. + intros R S HR HS H. + try (aac_instances H; fail 1 "ne doit pas passer"). + try (aac_rewrite H ; fail 1 "ne doit pas passer"). + Abort. + + + + + + Hypothesis star_f: forall x y, x*f(y*x) = f(x*y)*x. + + Goal g (a+b*c*d*f(a*b*c*d)+b) = k. + aac_instances star_f. + aac_rewrite star_f. + Abort. + + Goal b*f(a*b)*f(b*b*f(a*b)) = k. + aac_instances star_f. + aac_rewrite star_f. + aac_rewrite star_f. + Abort. + + + + + + Hypothesis dot_select: forall x y, f x * y * g x = g y*x*f y. + + Goal f(a+b)*c*g(b+a) = k. + aac_rewrite dot_select. + Abort. + + Goal f(a+b)*g(b+a) = k. + try (aac_rewrite dot_select; fail 1 "ne doit pas passer"). + aacu_rewrite dot_select. + Abort. + + Goal f b*f(a+b)*g(b+a)*g b = k. + aacu_instances dot_select. + aac_instances dot_select. + aac_rewrite dot_select. + aacu_rewrite dot_select. + aacu_rewrite dot_select. + Abort. + + + + + Hypothesis galois_dot: forall x y z, h x (y*z) = h (x*y) z. + Hypothesis galois_plus: forall x y z, h x (y+z) = h (x+y) z. + + Hypothesis select_dot: forall x y, h x (y*x) = h (x*y) x. + Hypothesis select_plus: forall x y, h x (y+x) = h (x+y) x. + + Hypothesis h_dot: forall x y, h (x*y) (y*x) = h x y. + Hypothesis h_plus: forall x y, h (x+y) (y+x) = h x y. + +End abs. + diff --git a/Tutorial.v b/Tutorial.v new file mode 100644 index 0000000..84d40fc --- /dev/null +++ b/Tutorial.v @@ -0,0 +1,321 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** * Examples about uses of the aac_rewrite library *) + +(* + Depending on your installation, either uncomment the following two + lines, or add them to your .coqrc files, replacing path_to_aac_tactics + with the correct path for your installation: + + Add Rec LoadPath "path_to_aac_tactics". + Add ML Path "path_to_aac_tactics". +*) +Require Export AAC. +Require Instances. + +(** ** Introductory examples *) + +(** First, we settle in the context of Z, and show an usage of our +tactics: we rewrite an universally quantified hypothesis modulo +associativity and commutativity. *) + +Section introduction. + Import ZArith. + Import Instances.Z. + + Variables a b c : Z. + Hypothesis H: forall x, x + Zopp x = 0. + Goal a + b + c + Zopp (c + a) = b. + aac_rewrite H. + aac_reflexivity. + Qed. + Goal a + c+ Zopp (b + a + Zopp b) = c. + do 2 aac_rewrite H. + reflexivity. + Qed. + + (** Notes: + - the tactic handles arbitrary function symbols like [Zopp] (as + long as they are proper morphisms); + - here, ring would have done the job. + *) + +End introduction. + +(** Second, we show how to exploit binomial identities to prove a goal +about pythagorean triples, without breaking a sweat. By comparison, +even if the goal and the hypothesis are both in normal form, making +the rewrites using standard tools is difficult. +*) + +Section binomials. + + Import ZArith. + Import Instances.Z. + + Notation "x ^2" := (x*x) (at level 40). + Notation "2 ⋅ x" := (x+x) (at level 41). + 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. + + 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. + aacu_rewrite <- Hbin1. + aac_rewrite Hbin2. + aac_rewrite <- H. + aac_rewrite Hopp. + aac_reflexivity. + Qed. + + (** Note: after the [aac_rewrite <- H], one could use [ring] to close the proof.*) + +End binomials. + +(** ** 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; + however, to be able to use this plugin, one currently needs at least + one associative operator, and one associative-commutative + operator.) *) + +Section base. + + Context {X} {R} {E: Equivalence R} + {plus} {zero} + {dot} {one} + {A: @Op_A X R dot one} + {AC: Op_AC R plus zero}. + + Notation "x == y" := (R x y) (at level 70). + Notation "x * y" := (dot x y) (at level 40, left associativity). + Notation "1" := (one). + Notation "x + y" := (plus x y) (at level 50, left associativity). + Notation "0" := (zero). + + (** In the very first example, [ring] would have solved the + goal. Here, since [dot] does not necessarily distribute over [plus], + it is not possible to rely on it. *) + + 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. + Qed. + + (** Note: the tactic starts by normalizing terms, so that trailing + units are always eliminated. *) + + Goal ((a+b)+0+c)*((c+a)+b*1) == a+b+c. + aac_rewrite H. + aac_reflexivity. + Qed. + End reminder. + + (** We can deal with "proper" morphisms of arbitrary arity (here [f], + or [Zopp] earlier), and rewrite under morphisms (here [g]). *) + + Section morphisms. + Variable f : X -> X -> X. + 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). + aac_rewrite H. + reflexivity. + Qed. + End morphisms. + + (** ** Selecting what and where to rewrite *) + + (** There are sometimes several possible rewriting. We now show how + to interact with the tactic to select the desired one. *) + + Section occurrence. + Variable f : X -> X . + Variable a : X. + Hypothesis Hf : Proper (R ==> R) f. + 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 + the different solutions using the [aac_instances] tactic (in + proofgeneral, look at buffer *coq* ): *) + aac_instances H. + (** the default choice is the smallest possible context (number + 0), but one can choose the desired context; *) + aac_rewrite H subterm 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 context, but several substitutions; *) + aac_instances H. + (** we can select them with the proper keyword. *) + aac_rewrite H subst 1. + aac_rewrite H'. + aac_reflexivity. + Qed. + End subst. + + (** As expected, one can use both keyword together to select the + correct subterm and the correct substitution. *) + + Section both. + 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 subterm 1 subst 1. + aac_rewrite H. + aac_rewrite H'. + aac_reflexivity. + Qed. + + End both. + + (** We now turn on explaining the distinction between [aac_rewrite] + and [aacu_rewrite]: [aac_rewrite] rejects solutions in which + variables are instantiated by units, the companion tactic, + [aacu_rewrite] allows such solutions. *) + + Section dealing_with_units. + Variables a b c: X. + Hypothesis H: forall x, a*x*a == x. + Goal a*a == 1. + (** Here, x must be instantiated with 1, hence no solutions; *) + aac_instances H. + (** while we get solutions with the "aacu" tactic. *) + aacu_instances H. + aacu_rewrite H. + reflexivity. + 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'. + (** more than 52 with units. *) + aacu_instances H'. + Abort. + + End dealing_with_units. +End base. + +(** ** Declaring instances *) + +(** One can use one's own operations: it suffices to declare them as + instances of our classes. (Note that these instances are already + declared in file [Instances.v].) *) + +Section Peano. + Require Import Arith. + + Program Instance nat_plus : Op_AC eq plus O. + Solve All Obligations using firstorder. + + Program Instance nat_dot : Op_AC eq mult 1. + Solve All Obligations using firstorder. + + + (** Caveat: we need at least an instance of an operator that is AC + and one that is A for a given relation. However, one can reuse an + AC operator as an A operator. *) + + Definition default_a := AC_A nat_dot. Existing Instance default_a. +End Peano. + +(** ** Caveats *) + +Section Peano'. + Import Instances.Peano. + + (** 1. We have a special treatment for units, thus, [S x + x] does not + match [S 0], which is considered as a unit (one) of the mult + operation. *) + + Section caveat_one. + Definition double_plus_one x := 2*x + 1. + Hypothesis H : forall x, S x + x = double_plus_one x. + Goal S O = double_plus_one O. + try aac_rewrite H. (** 0 solutions (normal since it would use 0 to instantiate x) *) + try aacu_rewrite H. (** 0 solutions (abnormal) *) + Abort. + End caveat_one. + + (** 2. We cannot at the moment have two classes with the same + units: in the following example, [0] is understood as the unit of + [max] rather than as the unit of [plus]. *) + + Section max. + Program Instance aac_max : Op_AC eq Max.max O := Build_Op_AC _ _ _ Max.max_assoc Max.max_comm. + Variable a : nat. + Goal 0 + a = a. + try aac_reflexivity. + Abort. + End max. +End Peano'. + +(** 3. If some computations are possible in the goal or in the +hypothesis, the inference mechanism we use will make the +conversion. However, it seems that in most cases, these conversions +can be done by hand using simpl rather than rewrite. *) + +Section Z. + + (* The order of the following lines is important in order to get the right scope afterwards. *) + Import ZArith. + Open Scope Z_scope. + Opaque Zmult. + + Hypothesis dot_ann_left :forall x, x * 0 = 0. + Hypothesis dot_ann_right :forall x, 0 * x = 0. + + Goal forall a, a*0 = 0. + intros. aacu_rewrite dot_ann_left. reflexivity. + Qed. + + (** Here the tactic fails, since the 0*a is converted to 0, and no + rewrite can occur (even though Zmult is opaque). *) + Goal forall a, 0*a = 0. + intros. try aacu_rewrite dot_ann_left. + Abort. + + (** Here the tactic fails, since the 0*x is converted to 0 in the hypothesis. *) + Goal forall a, a*0 = 0. + intros. try aacu_rewrite dot_ann_right. + Abort. + + +End Z. + diff --git a/aac_rewrite.ml b/aac_rewrite.ml new file mode 100644 index 0000000..c4c88e0 --- /dev/null +++ b/aac_rewrite.ml @@ -0,0 +1,308 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** aac_rewrite -- rewriting modulo *) + +(* 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 = + Util.anomaly ("aac_tactics: " ^ msg) + +let user_error msg = + Util.error ("aac_tactics: " ^ msg) + +(* debug and timing functions *) +let debug = false +let printing = false +let time = false + +let debug x = + if debug then + Printf.printf "%s\n%!" x + +let pr_constr msg constr = + if printing then + ( Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg)); + Pp.msgnl (Printer.pr_constr constr); + ) + +let time msg tac = + if time then Coq.tclTIME msg tac + else tac + +let tac_or_exn tac exn msg = + fun gl -> try tac gl with e -> exn msg e + +(* helper to be used with the previous function: raise a new anomaly + except if a another one was previously raised *) +let push_anomaly msg = function + | Util.Anomaly _ as e -> raise e + | _ -> anomaly msg + +module M = Matcher + +open Term +open Names +open Coqlib +open Proof_type + + +(** [find_applied_equivalence goal eq] try to ensure that the goal is + an applied equivalence relation, with two operands of the same type. + + This function is transitionnal, as we plan to integrate with the + new rewrite features of Coq 8.3, that seems to handle this kind of + things. +*) +let find_applied_equivalence goal : Term.constr -> Coq.eqtype *Term.constr *Term.constr* Coq.goal_sigma = fun equation -> + let env = Tacmach.pf_env goal in + let evar_map = Tacmach.project goal in + match Coq.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 right = ca.(n-1) in + let left_type = Tacmach.pf_type_of goal left in + (* let right_type = Tacmach.pf_type_of goal right in *) + let partial_app = mkApp (c, Array.sub ca 0 (n-2) ) in + let eq_type = Coq.Classes.mk_equivalence left_type partial_app in + begin + try + let evar_map, equivalence = Typeclasses.resolve_one_typeclass env evar_map eq_type in + let goal = Coq.goal_update goal evar_map in + ((left_type, partial_app), equivalence),left, right, goal + with + | Not_found -> user_error "The goal is not an applied equivalence" + end + | _ -> user_error "The goal is not an equation" + + +(* [find_applied_equivalence_force] brutally decomposes the given + equation, and fail if we find a relation that is not the same as + the one we look for [r] *) +let find_applied_equivalence_force rlt goal : Term.constr -> Term.constr *Term.constr* Coq.goal_sigma = fun equation -> + match Coq.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 right = ca.(n-1) in + let partial_app = mkApp (c, Array.sub ca 0 (n-2) ) in + let _ = if snd rlt = partial_app then () else user_error "The goal and the hypothesis have different top-level relations" in + + left, right, goal + | _ -> user_error "The hypothesis is not an equation" + + + +(** Build a couple of [t] from an hypothesis (variable names are not + relevant) *) +let rec t_of_hyp goal rlt envs e = match Coq.decomp_term e with + | Prod (name,ty,c) -> let x, y = t_of_hyp goal rlt envs c + in x,y+1 + | _ -> + let l,r ,goal = find_applied_equivalence_force rlt goal e in + let l,goal = Theory.Trans.t_of_constr goal rlt envs l in + let r,goal = Theory.Trans.t_of_constr goal rlt envs r in + (l,r),0 + +(** @deprecated: [option_rip] will be removed as soon as a proper interface is + given to the user *) +let option_rip = function | Some x -> x | None -> raise Not_found + +let mk_hyp_app conv c env = + let l = Matcher.Subst.to_list env in + let l = List.sort (fun (x,_) (y,_) -> compare y x) l in + let l = List.map (fun x -> conv (snd x)) l in + let v = Array.of_list l in + mkApp (c,v) + + + +(** {1 Tactics} *) + +(** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that + is merely a proof of equality of two terms modulo AAC *) + +let by_aac_reflexivity eqt envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) : Proof_type.tactic = fun goal -> + let maps, reifier,reif_letins = Theory.Trans.mk_reifier eqt envs goal in + let ((x,r),e) = eqt in + + (* fold through a term and reify *) + let t = Theory.Trans.reif_constr_of_t reifier t in + let t' = Theory.Trans.reif_constr_of_t reifier t' in + + (* Some letins *) + let eval, eval_letin = Coq.mk_letin' "eval_name" (mkApp (Lazy.force Theory.eval, [|x;r; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_prd; maps.Theory.Trans.env_sum|])) in + let _ = pr_constr "left" t in + let _ = pr_constr "right" t' in + let t , t_letin = Coq.mk_letin "left" t in + let t', t_letin'= Coq.mk_letin "right" t' in + let apply_tac = Tactics.apply ( + mkApp (Lazy.force Theory.decide_thm, [|x;r;e; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_prd; maps.Theory.Trans.env_sum;t;t'|])) + in + Tactics.tclABSTRACT None + (Tacticals.tclTHENLIST + [ + tac_or_exn reif_letins anomaly "invalid letin (1)"; + tac_or_exn eval_letin anomaly "invalid letin (2)"; + tac_or_exn t_letin anomaly "invalid letin (3)"; + tac_or_exn t_letin' anomaly "invalid letin (4)"; + tac_or_exn apply_tac anomaly "could not apply the decision theorem"; + tac_or_exn (time "vm_norm" (Tactics.normalise_vm_in_concl)) anomaly "vm_compute failure"; + Tacticals.tclORELSE Tactics.reflexivity + (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) + ]) + goal + + +(** The core tactic for aac_rewrite *) +let core_aac_rewrite ?(l2r = true) envs eqt rew p subst left = fun goal -> + let rlt = fst eqt in + let t = Matcher.Subst.instantiate subst p in + let tr = Theory.Trans.raw_constr_of_t envs rlt t in + let tac_rew_l2r = + if l2r then Equality.rewriteLR rew else Equality.rewriteRL rew + in + pr_constr "transitivity through" tr; + Tacticals.tclTHENSV + (tac_or_exn (Tactics.transitivity tr) anomaly "Unable to make the transitivity step") + [| + (* si by_aac_reflexivity foire (pas un theoreme), il fait tclFAIL, et on rattrape ici *) + tac_or_exn (time "by_aac_refl" (by_aac_reflexivity eqt envs left t)) push_anomaly "Invalid transitivity step"; + tac_or_exn (tac_rew_l2r) anomaly "Unable to rewrite"; + |] goal + +exception NoSolutions + +(** Choose a substitution from a + [(int * Terms.t * Env.env Search.m) Search.m ] *) +let choose_subst subterm sol m= + try + let (depth,pat,envm) = match subterm with + | None -> (* first solution *) + option_rip (Matcher.Search.choose m) + | Some x -> + List.nth (List.rev (Matcher.Search.to_list m)) x + in + let env = match sol with + None -> option_rip (Matcher.Search.choose envm) + | Some x -> List.nth (List.rev (Matcher.Search.to_list envm)) x + in + pat, env + with + | _ -> raise NoSolutions + +(** rewrite the constr modulo AC from left to right in the + left member of the goal +*) +let aac_rewrite rew ?(l2r=true) ?(show = false) ?strict ?occ_subterm ?occ_sol : Proof_type.tactic = fun goal -> + let envs = Theory.Trans.empty_envs () in + let rew_type = Tacmach.pf_type_of goal rew in + let (gl : Term.types) = Tacmach.pf_concl goal in + let _ = pr_constr "h" rew_type in + let _ = pr_constr "gl" gl in + let eqt, left, right, goal = find_applied_equivalence goal gl in + let rlt = fst eqt in + let left,goal = Theory.Trans.t_of_constr goal rlt envs left in + let right,goal = Theory.Trans.t_of_constr goal rlt envs right in + let (hleft,hright),hn = t_of_hyp goal rlt envs rew_type in + let pattern = if l2r then hleft else hright in + let m = Matcher.subterm ?strict pattern left in + + let m = Matcher.Search.sort (fun (x,_,_) (y,_,_) -> x - y) m in + if show + then + let _ = Pp.msgnl (Pp.str "All solutions:") in + let _ = Pp.msgnl (Matcher.pp_all (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t envs rlt t) ) m) in + Tacticals.tclIDTAC goal + else + try + let pat,env = choose_subst occ_subterm occ_sol m in + let rew = mk_hyp_app (Theory.Trans.raw_constr_of_t envs rlt )rew env in + core_aac_rewrite ~l2r envs eqt rew pat env left goal + with + | NoSolutions -> Tacticals.tclFAIL 0 + (Pp.str (if occ_subterm = None && occ_sol = None + then "No matching subterm found" + else "No such solution")) goal + + +let aac_reflexivity : Proof_type.tactic = fun goal -> + let (gl : Term.types) = Tacmach.pf_concl goal in + let envs = Theory.Trans.empty_envs() in + let eqt, left, right, evar_map = find_applied_equivalence goal gl in + let rlt = fst eqt in + let left,goal = Theory.Trans.t_of_constr goal rlt envs left in + let right,goal = Theory.Trans.t_of_constr goal rlt envs right in + by_aac_reflexivity eqt envs left right goal + + +open Tacmach +open Tacticals +open Tacexpr +open Tacinterp +open Extraargs + + (* Adding entries to the grammar of tactics *) +TACTIC EXTEND _aac1_ +| [ "aac_reflexivity" ] -> [ aac_reflexivity ] +END + + +TACTIC EXTEND _aac2_ +| [ "aac_rewrite" orient(o) constr(c) "subterm" integer(i) "subst" integer(j)] -> + [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:i ~occ_sol:j c gl ] +END + +TACTIC EXTEND _aac3_ +| [ "aac_rewrite" orient(o) constr(c) "subst" integer(j)] -> + [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:0 ~occ_sol:j c gl ] +END + +TACTIC EXTEND _aac4_ +| [ "aac_rewrite" orient(o) constr(c) "subterm" integer(i)] -> + [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:i ~occ_sol:0 c gl ] +END + +TACTIC EXTEND _aac5_ +| [ "aac_rewrite" orient(o) constr(c) ] -> + [ fun gl -> aac_rewrite ~l2r:o ~strict:true c gl ] +END + +TACTIC EXTEND _aac6_ +| [ "aac_instances" orient(o) constr(c)] -> + [ fun gl -> aac_rewrite ~l2r:o ~strict:true ~show:true c gl ] +END + + + + +TACTIC EXTEND _aacu2_ +| [ "aacu_rewrite" orient(o) constr(c) "subterm" integer(i) "subst" integer(j)] -> + [ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:i ~occ_sol:j c gl ] +END + +TACTIC EXTEND _aacu3_ +| [ "aacu_rewrite" orient(o) constr(c) "subst" integer(j)] -> + [ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:0 ~occ_sol:j c gl ] +END + +TACTIC EXTEND _aacu4_ +| [ "aacu_rewrite" orient(o) constr(c) "subterm" integer(i)] -> + [ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:i ~occ_sol:0 c gl ] +END + +TACTIC EXTEND _aacu5_ +| [ "aacu_rewrite" orient(o) constr(c) ] -> + [ fun gl -> aac_rewrite ~l2r:o c gl ] +END + +TACTIC EXTEND _aacu6_ +| [ "aacu_instances" orient(o) constr(c)] -> + [ fun gl -> aac_rewrite ~l2r:o ~show:true c gl ] +END diff --git a/aac_rewrite.mli b/aac_rewrite.mli new file mode 100644 index 0000000..81818b6 --- /dev/null +++ b/aac_rewrite.mli @@ -0,0 +1,59 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Main module for the Coq plug-in ; provides the [aac_rewrite] and + [aac_reflexivity] tactics. + + This file defines the entry point for the tactic aac_rewrite. It + does Joe-the-plumbing, given a goal, reifies the interesting + subterms (rewrited hypothesis, goal) into abstract syntax tree + {!Matcher.Terms} (see {!Theory.Trans.t_of_constr}). Then, we use the + results from the matcher to rebuild terms and make a transitivity + step toward a term in which the hypothesis can be rewritten using + the standard rewrite. + + Doing so, we generate a sub-goal which we solve using a reflexive + decision procedure for the equality of terms modulo + AAC. Therefore, we also need to reflect the goal into a concrete + data-structure. See {i AAC.v} for more informations, + especially the data-type {b T} and the {b decide} theorem. + +*) + +(** {2 Transitional functions} + + We define some plumbing functions that will be removed when we + integrate the new rewrite features of Coq 8.3 +*) + +(** [find_applied_equivalence goal eq] checks that the goal is + an applied equivalence relation, with two operands of the same + type. + +*) +val find_applied_equivalence : Proof_type.goal Tacmach.sigma -> Term.constr -> Coq.eqtype * Term.constr * Term.constr * Proof_type.goal Tacmach.sigma + +(** Build a couple of [t] from an hypothesis (variable names are not + relevant) *) +val t_of_hyp : Proof_type.goal Tacmach.sigma -> Coq.reltype -> Theory.Trans.envs -> Term.types -> (Matcher.Terms.t * Matcher.Terms.t) * int + +(** {2 Tactics} *) + +(** the [aac_reflexivity] tactic solves equalities modulo AAC, by + reflection: it reifies the goal to apply theorem [decide], from + file {i AAC.v}, and then concludes using [vm_compute] + and [reflexivity] +*) +val aac_reflexivity : Proof_type.tactic + +(** [aac_rewrite] is the tactic for in-depth reqwriting modulo AAC +with some options to choose the orientation of the rewriting and a +solution (first the subterm, then the solution)*) + +val aac_rewrite : Term.constr -> ?l2r:bool -> ?show:bool -> ?strict: bool -> ?occ_subterm:int -> ?occ_sol:int -> Proof_type.tactic + @@ -0,0 +1,212 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Interface with Coq *) + +type constr = Term.constr + +open Term +open Names +open Coqlib + + +(* The contrib name is used to locate errors when loading constrs *) +let contrib_name = "aac_tactics" + +(* Getting constrs (primitive Coq terms) from exisiting Coq + libraries. *) +let find_constant contrib dir s = + Libnames.constr_of_global (Coqlib.find_reference contrib dir s) + +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 mk_letin (name: string) (constr: constr) : constr * Proof_type.tactic = + let name = (Names.id_of_string name) in + let letin = + (Tactics.letin_tac + None + (Name name) + constr + None (* or Some ty *) + nowhere + ) in + mkVar name, letin + +let mk_letin' (name: string) (constr: constr) : constr * Proof_type.tactic + = + constr, Tacticals.tclIDTAC + + + +(** {2 General functions} *) + +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 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 + c, (goal_update goal em) + +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) (rlt : constr * 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 (fst rlt) in + x,(goal_update gl em) + +let evar_binary (gl: goal_sigma) (rlt: constr * constr) = + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let x = fst rlt 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) + +(* decomp_term : constr -> (constr, types) kind_of_term *) +let decomp_term c = kind_of_term (strip_outer_cast c) + + +(** {2 Bindings with Coq' Standard Library} *) + +module Pair = struct + + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "prod") + let pair = lazy (init_constant path "pair") +end + +module Pos = struct + + let path = ["Coq" ; "NArith"; "BinPos"] + let typ = lazy (init_constant path "positive") + let xI = lazy (init_constant path "xI") + let xO = lazy (init_constant path "xO") + let xH = lazy (init_constant path "xH") + + (* A coq positive from an int *) + let of_int n = + let rec aux n = + begin match n with + | n when n < 1 -> assert false + | 1 -> Lazy.force xH + | n -> mkApp + ( + (if n mod 2 = 0 + then Lazy.force xO + else Lazy.force xI + ), [| aux (n/2)|] + ) + end + in + aux n +end + +module Nat = struct + let path = ["Coq" ; "Init"; "Datatypes"] + let typ = lazy (init_constant path "nat") + let _S = lazy (init_constant path "S") + 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 + | n when n < 0 -> assert false + | 0 -> Lazy.force _O + | n -> mkApp + ( + (Lazy.force _S + ), [| aux (n-1)|] + ) + end + 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 = + mkApp (Lazy.force cons, [| ty; h ; t |]) + 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 + let classes_path = ["Coq";"Classes"; ] + let morphism = lazy (init_constant (classes_path@["Morphisms"]) "Proper") + + (** build the constr [Proper rel t] *) + let mk_morphism ty rel t = + mkApp (Lazy.force morphism, [| ty; rel; t|]) + + let equivalence = lazy (init_constant (classes_path@ ["RelationClasses"]) "Equivalence") + + (** build the constr [Equivalence ty rel] *) + let mk_equivalence ty rel = + mkApp (Lazy.force equivalence, [| ty; rel|]) +end + +(** a [mset] is a ('a * pos) list *) +let mk_mset ty (l : (constr * int) list) = + let pos = Lazy.force Pos.typ in + let pair_ty = mkApp (Lazy.force Pair.typ , [| ty; pos|]) in + let pair (x : constr) (ar : int) = + mkApp (Lazy.force Pair.pair, [| ty ; pos ; x ; Pos.of_int ar|]) in + let rec aux = function + | [] -> List.nil pair_ty + | (t,ar)::q -> List.cons pair_ty (pair t ar) (aux q) + in + aux l + +(** x r *) +type reltype = Term.constr * Term.constr +(** x r e *) +type eqtype = reltype * Term.constr + + +(** {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 + r + +let tclDEBUG msg tac = fun gl -> + let _ = Pp.msgnl (Pp.str msg) in + tac gl + +let tclPRINT tac = fun gl -> + let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in + tac gl + @@ -0,0 +1,117 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Interface with Coq where 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; + - we also provide several handlers for standard coq tactics, in + order to provide a unified setting (we replace functions that + modify the evar_map by functions that operate on the whole + goal, and repack the modified evar_map with it). + +*) + +(** {2 Getting Coq terms from the environment} *) + +val init_constant : string list -> string -> Term.constr + +(** {2 General purpose functions} *) + +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 nf_evar : goal_sigma -> Term.constr -> Term.constr +val evar_unit :goal_sigma ->Term.constr*Term.constr-> Term.constr* goal_sigma +val evar_binary: goal_sigma -> Term.constr*Term.constr -> Term.constr* goal_sigma + + +(** [mk_letin name v] binds the constr [v] using a letin tactic *) +val mk_letin : string ->Term.constr ->Term.constr * Proof_type.tactic + +(** [mk_letin' name v] is a drop-in replacement for [mk_letin' name v] + that does not make a binding (useful to test whether using lets is + efficient) *) +val mk_letin' : string ->Term.constr ->Term.constr * Proof_type.tactic + +(* decomp_term : constr -> (constr, types) kind_of_term *) +val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term + + +(** {2 Bindings with Coq' Standard Library} *) + +(** Coq lists *) +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 + +(** Coq pairs *) +module Pair: +sig + val typ:Term.constr lazy_t + val pair:Term.constr lazy_t +end + +(** Coq positive numbers (pos) *) +module Pos: +sig + val typ:Term.constr lazy_t + val of_int: int ->Term.constr +end + +(** Coq unary numbers (peano) *) +module Nat: +sig + val typ:Term.constr lazy_t + val of_int: int ->Term.constr +end + + +(** Coq typeclasses *) +module Classes: +sig + val mk_morphism: Term.constr -> Term.constr -> Term.constr -> Term.constr + val mk_equivalence: Term.constr -> Term.constr -> Term.constr +end + +(** Both in OCaml and Coq, we represent finite multisets using + weighted lists ([('a*int) list]), see {!Matcher.mset}. + + [mk_mset ty l] constructs a Coq multiset from an OCaml multiset + [l] of Coq terms of type [ty] *) + +val mk_mset:Term.constr -> (Term.constr * int) list ->Term.constr + +(** pairs [(x,r)] such that [r: Relation x] *) +type reltype = Term.constr * Term.constr + +(** triples [((x,r),e)] such that [e : @Equivalence x r]*) +type eqtype = reltype * Term.constr + + +(** {2 Some tacticials} *) + +(** time the execution of a tactic *) +val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic + +(** emit debug messages to see which tactics are failing *) +val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic + +(** print the current goal *) +val tclPRINT : Proof_type.tactic -> Proof_type.tactic + + diff --git a/files.txt b/files.txt new file mode 100644 index 0000000..7fa1801 --- /dev/null +++ b/files.txt @@ -0,0 +1,7 @@ +matcher.ml +coq.ml +theory.ml +aac_rewrite.ml +AAC.v +Instances.v +Tutorial.v diff --git a/magic.txt b/magic.txt new file mode 100644 index 0000000..d0272c3 --- /dev/null +++ b/magic.txt @@ -0,0 +1,4 @@ +-custom "mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc" "$(MLIFILES)" doc +-custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxs +-custom "$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)" "$(CMOFILES)" aac_tactics.cma +-custom "$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend" "$(MLIFILES)" .depend diff --git a/make_makefile b/make_makefile new file mode 100755 index 0000000..3cfc096 --- /dev/null +++ b/make_makefile @@ -0,0 +1,49 @@ +# - set variable MLIFILES so that it can be used in custom targets to +# build documentation and dependencies for .mli files +# - remove useless ' -I . .../plugins/ ' lines so that we can read something in the compilation log +# - rename the rule for Makefile auto-regeneration, and replace it with an appropriate command +# - patch the rule for cleaning doc +# - include the .depend custom target, to take .mli dependencies into account + +( +coq_makefile -no-install -opt MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \ + | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g' +cat <<EOF + +# sanity checks +tests: Tests.vo + +# override inadequate coq_makefile auto-regeneration +Makefile: make_makefile magic.txt files.txt + . make_makefile + +# We want to keep the proofs only in the Tutorial +tutorial: Tutorial.vo Tutorial.glob + \$(COQDOC) --no-index --no-externals -html \$(COQDOCLIBS) -d html Tutorial.v + +world: \$(VOFILES) doc gallinahtml tutorial + +# additional dependencies for AAC (since aac_tactics.cmxs/cma are not +# around the first time we run make, coqdep issues a warning and +# ignores this dependency) +# (one can safely select one of theses dependencies according to +# coq' compilation mode--bytecode or native) +AAC.vo: aac_tactics.cmxs aac_tactics.cma + + +# .depend contains dependencies for .mli files +-include .depend +.SECONDARY: .depend + +EOF +) > Makefile + + + +# TOTHINK: coq_makefile est bête, [make all] compile systématiquement +# les .cmxs associés à chaque module, alors que ça ne sert à rien, +# seul aac_rewrite.cmxs compte + +# problemes lorsqu'un module porte un meme nom qu'un module predefini +# (matching par exemple), prendre garde si ce probleme s'etend a la +# confusion module/nom de librairie diff --git a/matcher.ml b/matcher.ml new file mode 100644 index 0000000..176b660 --- /dev/null +++ b/matcher.ml @@ -0,0 +1,980 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** 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. + + We proceed by structural decomposition of the pattern, and try all + possible non-deterministic split of the subject when needed. The + function {!matcher} is limited to top-level matching, that is, the + subject must make a perfect match against the pattern ([x+x] do + not match [a+a+b] ). We use a search monad {!Search} to perform + non-deterministic splits in an almost transparent way. We also + provide a function {!subterm} for finding a match that is a + subterm modulo AAC of the subject. Therefore, we are able to solve + the aforementioned case [x+x] against [a+b+a]. + + This file is structured as follows. First, we define the search + monad. Then,we define the two representations of terms (one + representing the AST, and one in normal form ), and environments + from variables to terms. Then, we use these parts to solve + matching problem. Finally, we wrap this function {!matcher} into + {!subterm} +*) + + +let debug = false +let time = false + + +let time f x fmt = + if time then + let t = Sys.time() in + let r = f x in + Printf.printf fmt (Sys.time () -. t); + r + else f x + + + +type symbol = int +type var = int + + +(****************) +(* Search Monad *) +(****************) + + +(** The {!Search} module contains a search monad that allows to + express, in a legible maner, programs that solves combinatorial + problems + + @see <http://spivey.oriel.ox.ac.uk/mike/search-jfp.pdf> the + inspiration of this module +*) +module Search : sig + (** A data type that represent a collection of ['a] *) + type 'a m + (** bind and return *) + val ( >> ) : 'a m -> ('a -> 'b m) -> 'b m + val return : 'a -> 'a m + (** non-deterministic choice *) + val ( >>| ) : 'a m -> 'a m -> 'a m + (** failure *) + val fail : unit -> 'a m + (** folding through the collection *) + val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b + (** derived facilities *) + val sprint : ('a -> string) -> 'a m -> string + val count : 'a m -> int + val choose : 'a m -> 'a option + val to_list : 'a m -> 'a list + val sort : ('a -> 'a -> int) -> 'a m -> 'a m + val is_empty: 'a m -> bool +end += struct + + 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 -> + (List.fold_left (fun acc x -> + match x with + | (N []) -> acc + | x -> aux acc x + ) acc l) + in + aux acc m + + + + let rec (>>) : 'a m -> ('a -> 'b m) -> 'b m = + fun m f -> + match m with + | F x -> f x + | N l -> + N (List.fold_left (fun acc x -> + match x with + | (N []) -> acc + | x -> (x >> f)::acc + ) [] l) + + 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) + | N l, F x -> N (F x::l) + | x,y -> N [x;y] + + let return : 'a -> 'a m = fun x -> F x + 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 + | F _ -> 1 + | N l -> List.fold_left (fun acc x -> acc+count x) 0 l + + 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 -> + 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))) +end + +open Search + + +type 'a mset = ('a * int) list +let linear p = + let rec ncons t l = function + | 0 -> l + | n -> t::ncons t l (n-1) + in + let rec aux = function + [ ] -> [] + | (t,n)::q -> let q = aux q in + ncons t q n + in aux p + + + +(** 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 + + - a private type {!Terms.nf_term} that represent an equivalence + class for terms that are equal modulo AAC. The constructions + functions on this type ensure the property that the term is in + normal form (that is, no sum can appear as a subterm of the same + sum, no trailing units, etc...). + +*) + +module Terms : sig + + (** {1 Abstract syntax tree of terms} + + Terms represented using this datatype are representation of the + AST of an expression. *) + + type t = + Dot of (symbol * t * t) + | One of symbol + | Plus of (symbol * t * t) + | Zero of symbol + | Sym of (symbol * t array) + | Var of var + + val equal_aac : t -> t -> bool + 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 {!Matcher} module, + one does not need to access the actual representation of this + type. *) + + type nf_term = private + | TAC of symbol * nf_term mset + | TA of symbol * nf_term list + | TSym of symbol *nf_term list + | TVar of var + + + (** {2 Constructors: we ensure that the terms are always + normalised} *) + val mk_TAC : symbol -> nf_term mset -> nf_term + val mk_TA : symbol -> nf_term list -> nf_term + val mk_TSym : symbol -> nf_term list -> nf_term + val mk_TVar : var -> nf_term + + (** {2 Comparisons} *) + + val nf_term_compare : nf_term -> nf_term -> int + val nf_equal : nf_term -> nf_term -> bool + + (** {2 Printing function} *) + val sprint_nf_term : nf_term -> string + + (** {2 Conversion functions} *) + val term_of_t : t -> nf_term + val t_of_term : nf_term -> t +end + = struct + + type t = + Dot of (symbol * t * t) + | One of symbol + | Plus of (symbol * t * t) + | Zero of symbol + | Sym of (symbol * t array) + | Var of var + + 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 + | TA of symbol * nf_term list + | TSym of symbol *nf_term list + | TVar of var + + + + (** {2 Comparison} *) + + let nf_term_compare = Pervasives.compare + let nf_equal a b = a = b + + (** {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' s l = match l with + | [t,0] -> TAC (s,[]) + | [t,1] -> t + | _ -> TAC (s,l) + let mk_TA' s l = match l with [t] -> t + | _ -> TA (s,l) + + + + (** [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. *) + let merge_ac (compare : 'a -> 'a -> int) (l : 'a mset) (l' : 'a mset) : 'a mset = + let rec aux l l'= + match l,l' with + | [], _ -> l' + | _, [] -> l + | (t,tar)::q, (t',tar')::q' -> + begin match compare t t' with + | 0 -> ( t,tar+tar'):: aux q q' + | -1 -> (t, tar):: aux q l' + | _ -> (t', tar'):: aux l q' + end + in aux l l' + + (** [merge_map f l] uses the combinator [f] to combine the head of the + list [l] with the merge_maped tail of [l] *) + let rec merge_map (f : 'a -> 'b list -> 'b list) (l : 'a list) : 'b list = + match l with + | [] -> [] + | t::q -> f t (merge_map f q) + + + (** This function has to deal with the arities *) + let rec merge l l' = + merge_ac nf_term_compare l l' + + let extract_A s t = + match t with + | TA (s',l) when s' = s -> l + | _ -> [t] + + let extract_AC s (t,ar) : nf_term mset = + match t with + | TAC (s',l) when s' = s -> List.map (fun (x,y) -> (x,y*ar)) l + | _ -> [t,ar] + + + (** {3 Constructors of {!nf_term}}*) + + let mk_TAC s (l : (nf_term *int) list) = + mk_TAC' s + (merge_map (fun u l -> merge (extract_AC s u) l) l) + let mk_TA s l = + mk_TA' s + (merge_map (fun u l -> (extract_A s u) @ l) l) + let mk_TSym s l = TSym (s,l) + let mk_TVar v = TVar v + + + (** {2 Printing function} *) + let print_binary_list single unit binary l = + let rec aux l = + match l with + [] -> unit + | [t] -> single t + | t::q -> + let r = aux q in + Printf.sprintf "%s" (binary (single t) r) + in + aux l + + let sprint_ac single (l : 'a mset) = + (print_binary_list + (fun (x,t) -> + if t = 1 + then single x + else Printf.sprintf "%i*%s" t (single x) + ) + "0" + (fun x y -> x ^ " , " ^ y) + l + ) + + let print_symbol single s l = + match l with + [] -> Printf.sprintf "%i" s + | _ -> + Printf.sprintf "%i(%s)" + s + (print_binary_list single "" (fun x y -> x ^ "," ^ y) l) + + + let print_ac_list single s l = + Printf.sprintf "[%i:AC]{%s}" + s + (print_binary_list + single + "0" + (fun x y -> x ^ " , " ^ y) + l + ) + + + let print_a single s l = + Printf.sprintf "[%i:A]{%s}" + s + (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 + | TAC (s,l) -> + Printf.sprintf "[%i:AC]{%s}" s + (sprint_ac + sprint_nf_term + l) + | TA (s,l) -> print_a sprint_nf_term s l + | TVar v -> Printf.sprintf "x%i" v + + + + (** {2 Conversion functions} *) + + (* rebuilds a tree out of a list *) + let rec binary_of_list f comb null l = + let l = List.rev l in + let rec aux = function + | [] -> null + | [t] -> f t + | t::q -> comb (aux q) (f t) + in + aux l + + let rec term_of_t : t -> nf_term = function + | Dot (s,l,r) -> + let l = term_of_t l in + let r = term_of_t r in + mk_TA s [l;r] + | Plus (s,l,r) -> + let l = term_of_t l in + let r = term_of_t r in + mk_TAC ( s) [l,1;r,1] + | One x -> + mk_TA ( x) [] + | Zero x -> + mk_TAC ( x) [] + | 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 -> + mk_TVar ( i) + + let rec t_of_term : nf_term -> t = function + | TAC (s,l) -> + (binary_of_list + t_of_term + (fun l r -> Plus ( s,l,r)) + (Zero ( s)) + (linear l) + ) + | TA (s,l) -> + (binary_of_list + t_of_term + (fun l r -> Dot ( s,l,r)) + (One ( s)) + l + ) + | 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 + + + let equal_aac x y = + nf_equal (term_of_t x) (term_of_t y) + end + +(** Terms environments defined as association lists from variables to + terms in normal form {! Terms.nf_term} *) +module Subst : sig + type t + + val find : t -> var -> Terms.nf_term option + val add : t -> var -> Terms.nf_term -> 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 + + (** Terms environments, with nf_terms, to avoid costly conversions + of {!Terms.nf_terms} to {!Terms.t}, that will be mostly discarded*) + type t = (var * nf_term) list + + let find : t -> var -> nf_term option = fun t x -> + try Some (List.assoc x t) with | _ -> None + let add t x v = (x,v) :: t + let empty = [] + + let sprint (l : t) = + 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 + (sprint_nf_term y) + ) + "" + (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 + | One _ as x -> x + | Zero _ 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 -> + begin match find t i with + | None -> Util.error "aac_tactics: instantiate failure" + | Some x -> t_of_term x + end + in aux x + + let to_list t = List.map (fun (x,y) -> x,Terms.t_of_term y) t +end + +(******************) +(* MATCHING UTILS *) +(******************) + +open Terms + +(** First, we need to be able to perform non-deterministic choice of + term splitting to satisfy a pattern. Indeed, we want to show that: + (x+a*b)*c <= a*b*c +*) +let a_nondet_split t : ('a list * 'a list) m = + let rec aux l l' = + match l' with + | [] -> + return ( l,[]) + | t::q -> + return ( l,l' ) + >>| 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 t >> + (fun left, right -> + a_nondet_split left >> + (fun left, middle -> return (left, middle, right)) + ) + +(** Non deterministic splits of ac lists *) +let dispatch f n = + let rec aux k = + if k = 0 then return (f n 0) + else return (f (n-k) k) >>| aux (k-1) + in + aux (n ) + +let add_with_arith x ar l = + if ar = 0 then l else (x,ar) ::l + +let ac_nondet_split (l : 'a mset) : ('a mset * 'a mset) m = + let rec aux = function + | [] -> return ([],[]) + | (t,tar)::q -> + aux q + >> + (fun (left,right) -> + dispatch (fun arl arr -> + add_with_arith t arl left, + add_with_arith t arr right + ) + tar + ) + in + aux l + +(** Try to affect the variable [x] to each left factor of [t]*) +let var_a_nondet_split ?(strict=false) env current x t = + a_nondet_split t + >> + (fun (l,r) -> + if strict && l=[] then fail() else + return ((Subst.add env x (mk_TA current l)), r) + ) + +(** Try to affect variable [x] to _each_ subset of t. *) +let var_ac_nondet_split ?(strict=false) (s : symbol) env (x : var) (t : nf_term mset) : (Subst.t * (nf_term mset)) m = + ac_nondet_split t + >> + (fun (subset,compl) -> + if strict && subset=[] then fail() else + return ((Subst.add env x (mk_TAC s subset)), compl) + ) + +(** 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 + | _ -> [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 + | _ -> [t] + +(** See the term [t] as an symbol [s]. Fail if it is not such + symbol. *) +let get_Sym s t = + match t with + | TSym (s',l) when s' = s -> return l + | _ -> fail () + +(*************) +(* A Removal *) +(*************) + +(** 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 + | t::q , t' :: q' when nf_equal t t' -> aux q q' + | [], q -> return q + | _, _ -> fail () + in + match v with + | TA (s,l) when s = current -> aux l t + | _ -> + begin match t with + | [] -> fail () + | t::q -> + if nf_equal v t + then return q + else fail () + end + + +(**************) +(* AC Removal *) +(**************) + +(** [fold_acc] gather all elements of a list that satisfies a + predicate, and combine them with the residual of the list. That + is, each element of the residual contains exactly one element less + than the original term. + + TODO : This function not as efficient as it could be +*) + +let pick_sym (s : symbol) (t : nf_term mset ) = + let rec aux front back = + match back with + | [] -> fail () + | (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 ) + >>| aux ((t,tar)::front) q + | _ -> aux ((t,tar)::front) q + end + in + aux [] t + + + +(** We have to check if we are trying to remove a unit from a term*) +let is_unit_AC s t = + nf_equal t (mk_TAC s []) + +let is_same_AC s t : nf_term mset option= + match t with + TAC (s',l) when s = s' -> Some l + | _ -> None + +(** We want to remove the term [v] from the term list [t] under an AC + 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 + | [] -> fail () + | (t,tar)::q -> + begin + if nf_equal v t + then + match () with + | _ when tar < v_ar -> fail () + | _ when tar = v_ar -> return (List.rev_append front q) + | _ -> return (List.rev_append front ((t,tar-v_ar)::q)) + else + aux ((t,tar) :: front) q + end + in + if is_unit_AC s v + then + return t + else + aux [] t + +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 + | Some l -> + (* We are trying to remove an AC factor *) + List.fold_left (fun acc (v,v_ar) -> + acc >> (single_AC_factor s v v_ar) + ) + (return t) + l + + + +(************) +(* Matching *) +(************) + + + +(** {!matching} is the generic matching judgement. Each time a + 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. + + {!matchingAC} is used to match two sums (with the subtlety that + [x+y] matches [f a] which is a function application or [a*b] which + is a product). + + {!matchingA} is used to match two products (with the subtlety that + [x*y] matches [f a] which is a function application, or [a+b] + which is a sum). + + +*) +let matching ?strict = + let rec matching env (p : nf_term) (t: nf_term) : Subst.t Search.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) + >> (fun t -> matchingSym env l t) + | 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 + + 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' + >> (fun env -> matchingAC env current q t')) + + | TAC (s,v)::q when s = current -> + assert false + | TVar x:: q -> + begin match Subst.find env x with + | None -> + (var_ac_nondet_split ?strict current env x t) + >> (fun (env,residual) -> matchingAC env current q residual) + | Some v -> + (factor_AC current v t) + >> (fun residual -> matchingAC env current q residual) + end + | h :: q ->(* PAC =/= curent or PA *) + (ac_nondet_split t) + >> + (fun (left,right) -> + matching env h (mk_TAC current left) + >> + ( + fun env -> + matchingAC env current q right + ) + ) + | [] -> 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 + | TSym (s,v) :: l -> + 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 -> + var_a_nondet_split ?strict env current x t + >> (fun (env,residual)-> matchingA env current l residual) + | Some v -> + (left_factor current v t) + >> (fun residual -> matchingA env current l residual) + end + | h :: l -> + a_nondet_split t + >> (fun (t,r) -> + matching env h (mk_TA current 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 + (fun acc p t -> acc >> (fun env -> matching env p t)) + (return env) + l + t + + in + matching + + + +(***********) +(* Subterm *) +(***********) + +(** [tri_fold f l acc] folds on the list [l] and give to f the + beginning of the list in reverse order, the considered element, and + the last part of the list + + as an exemple, on the list [1;2;3;4], we get the trace + f () [] 1 [2; 3; 4] + f () [1] 2 [3; 4] + f () [2;1] 3 [ 4] + f () [3;2;1] 4 [] + + 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 + [] -> acc + | _ -> + let _,_,acc = List.fold_left (fun acc (t : 'a) -> + let l,r,acc = acc in + let r = List.tl r in + l,r,f acc l t r + ) ([], l,acc) l + in acc + + +(** [subterm] solves a sub-term pattern matching. + + This function is more high-level than {!matcher}, thus takes {!t} + as arguments rather than terms in normal form {!nf_term}. + + We use three mutually recursive functions {!subterm}, + {!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. + + 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]. + + We rebuild the context on the fly, leaving the variables in the + pattern uninstantiated. We do so in order to allow interaction + with the user, to choose the env. + + Strange patterms like x*y*x can be instanciated by nothing, inside + a product. Therefore, we need to check that all the term is not + going into the context (hence the tests on the length of the + lists). With proper support for interaction with the user, we + should lift these tests. However, at the moment, they serve as + heuristics to return "interesting" matchings + +*) + +let return_non_empty raw_p m = + if Search.is_empty m + then + fail () + else + return (raw_p ,m) + +let subterm ?strict (raw_p:t) (raw_t:t): (int* t * Subst.t m) m= + let p = term_of_t raw_p in + let t = term_of_t raw_t in + let rec subterm (t:nf_term) : (t * Subst.t m) m= + match t with + | TAC (s,l) -> + (ac_nondet_split l) >> + (fun (left,right) -> + (subterm_AC s left) >> + (fun (p,m) -> + let p = if right = [] then p else + Plus (s,p,t_of_term (mk_TAC s right)) + in + return (p,m) + ) + + ) + | TA (s,l) -> + (a_nondet_middle l) + >> + (fun (left, middle, right) -> + (subterm_A s middle) >> + (fun (p,m) -> + let p = + if right = [] then p else + Dot (s,p,t_of_term (mk_TA s right)) + in + let p = + if left = [] then p else + Dot (s,t_of_term (mk_TA s left),p) + in + return (p,m) + ) + ) + | TSym (s, l) -> + let init = return_non_empty raw_p (matching ?strict 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 + return (p,m) + )) >>| acc + ) l init + | _ -> assert false + and subterm_AC s tl = + match tl with + [x,1] -> subterm x + | _ -> + return_non_empty raw_p (matching ?strict Subst.empty p (mk_TAC s tl)) + and subterm_A s tl = + match tl with + [x] -> subterm x + | _ -> + return_non_empty raw_p (matching ?strict Subst.empty p (mk_TA s tl)) + in + (subterm t >> fun (p,m) -> return (Terms.size p,p,m)) + +(* The functions we export, handlers for the previous ones. Some debug + information also *) +let subterm ?strict raw t = + let sols = time (subterm ?strict raw) t "%fs spent in subterm (including matching)\n" in + if debug then Printf.printf "%i possible solution(s)\n" + (Search.fold (fun (_,_,envm) acc -> count envm + acc) sols 0); + sols + + +let matcher ?strict p t = + let sols = time + (fun (p,t) -> + let p = (Terms.term_of_t p) in + let t = (Terms.term_of_t t) in + matching ?strict Subst.empty p t) (p,t) + "%fs spent in the matcher\n" + in + if debug then Printf.printf "%i solutions\n" (count sols); + sols + +(* A very basic way to interact with the envs, to choose a possible + solution *) +open Pp +let pp_env pt : Subst.t -> Pp.std_ppcmds = fun env -> + List.fold_left (fun acc (v,t) -> str (Printf.sprintf "x%i: " v) ++ pt t ++ str "; " ++ acc) (str "") (Subst.to_list env) + +let pp_envm pt : Subst.t Search.m -> Pp.std_ppcmds = fun m -> + let _,s = Search.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 + List.fold_left (fun acc s -> s ++ acc) (str "") (s) + +let pp_all pt : (int * Terms.t * Subst.t Search.m) Search.m -> Pp.std_ppcmds = fun m -> + let _,s = Search.fold + (fun (size,context,envm) (n,acc) -> + let s = str (Printf.sprintf "subterm %i\t" n) in + let s = s ++ (str "(context ") ++ pt context ++ (str ")\n") in + let s = s ++ str (Printf.sprintf "\t%i possible(s) substitutions" (Search.count envm) ) ++ fnl () in + let s = s ++ pp_envm pt envm in + n+1, s::acc + ) m (0,[]) in + List.fold_left (fun acc s -> s ++ str "\n" ++ acc) (str "") (s) + diff --git a/matcher.mli b/matcher.mli new file mode 100644 index 0000000..3e20e73 --- /dev/null +++ b/matcher.mli @@ -0,0 +1,192 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Standalone module containing the algorithm for matching modulo + associativity and associativity and commutativity (AAC). + + This module could be reused ouside of the Coq plugin. + + Matching modulo AAC a pattern [p] against a term [t] boils down to + finding a substitution [env] such that the pattern [p] instantiated + with [env] is equal to [t] modulo AAC. + + We proceed by structural decomposition of the pattern, trying all + possible non-deterministic split of the subject, when needed. The + 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 {!Search} to perform non-deterministic + choices in an almost transparent way. + + We also provide a function {!subterm} for finding a match that is + a subterm of the subject modulo AAC. In particular, this function + gives a solution to the aforementioned case ([x+x] against + [a+b+a]). +*) + +(** {2 Utility functions} *) + +type symbol = int +type var = int + +(** The {!Search} module contains a search monad that allows to + express our non-deterministic and back-tracking algorithm in a + legible maner. + + @see <http://spivey.oriel.ox.ac.uk/mike/search-jfp.pdf> the + inspiration of this module +*) +module Search : +sig + (** A data type that represent a collection of ['a] *) + type 'a m + (** bind and return *) + val ( >> ) : 'a m -> ('a -> 'b m) -> 'b m + val return : 'a -> 'a m + (** non-deterministic choice *) + val ( >>| ) : 'a m -> 'a m -> 'a m + (** failure *) + val fail : unit -> 'a m + (** folding through the collection *) + val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b + (** derived facilities *) + val sprint : ('a -> string) -> 'a m -> string + val count : 'a m -> int + val choose : 'a m -> 'a option + val to_list : 'a m -> 'a list + val sort : ('a -> 'a -> int) -> 'a m -> 'a m + val is_empty: 'a m -> bool +end + +(** The arguments of sums (or AC operators) are represented using finite multisets. + (Typically, [a+b+a] corresponds to [2.a+b], i.e. [Sum[a,2;b,1]]) *) +type 'a mset = ('a * int) list + +(** [linear] expands a multiset into a simple list *) +val linear : 'a mset -> 'a list + +(** Representations of 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 + representation for the above terms modulo AAC. The construction + functions on this type ensure that these terms are in normal form + (that is, no sum can appear as a subterm of the same sum, no + trailing units, lists corresponding to multisets are sorted, + etc...). + +*) +module Terms : +sig + + (** {2 Abstract syntax tree of terms and patterns} + + We represent both terms and patterns using the following datatype. + + Values of type [symbol] are used to index symbols. Typically, + given two associative operations [(^)] and [( * )], and two + morphisms [f] and [g], the term [f (a^b) (a*g b)] is represented + 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], + + Accordingly, the following value, that contains "variables" + [Sym(0,[| Dot(1, Var x, Dot(4,[||])); + Dot(4, Var x, Sym(5,[|Sym(3,[||])|])) |])] + represents the pattern [forall x, f (x^1) (x*g b)], where [1] is the + unit associated with [( * )]. + *) + + type t = + Dot of (symbol * t * t) + | One of symbol + | Plus of (symbol * t * t) + | Zero of symbol + | Sym of (symbol * t array) + | Var of var + + (** Test for equality of terms modulo AAC (relies on the following + canonical representation of terms) *) + val equal_aac : t -> t -> bool + + + (** {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 AAC + This representation is only used internally; it is exported here + for the sake of completeness *) + + type nf_term + + (** {3 Comparisons} *) + + val nf_term_compare : nf_term -> nf_term -> int + val nf_equal : nf_term -> nf_term -> bool + + (** {3 Printing function} *) + + val sprint_nf_term : nf_term -> string + + (** {3 Conversion functions} *) + + (** we have the following property: [a] and [b] are equal modulo AAC + iif [nf_equal (term_of_t a) (term_of_t b) = true] *) + val term_of_t : t -> nf_term + val t_of_term : nf_term -> t + +end + + +(** Substitutions (or environments) + + 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 : +sig + type t + val sprint : t -> string + val instantiate : t -> Terms.t-> Terms.t + val to_list : t -> (var*Terms.t) list +end + + +(** {2 Main functions exported by this module} *) + +(** [matcher p t] computes the set of solutions to the given top-level + matching problem ([p] is the pattern, [t] is the term). If the + [strict] flag is set, solutions where units are used to + instantiate some variables are excluded, unless this unit appears + directly under a function symbol (e.g., f(x) still matches f(1), + while x+x+y does not match a+b+c, since this would require to + assign 1 to x). +*) +val matcher : ?strict:bool -> Terms.t -> Terms.t -> Subst.t Search.m + +(** [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 -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t Search.m) Search.m + +(** pretty printing of the solutions *) +val pp_all : (Terms.t -> Pp.std_ppcmds) -> (int * Terms.t * Subst.t Search.m) Search.m -> Pp.std_ppcmds diff --git a/theory.ml b/theory.ml new file mode 100644 index 0000000..45a76f1 --- /dev/null +++ b/theory.ml @@ -0,0 +1,708 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** 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 + be of little interest to most readers. +*) + + +open Term + +let ac_theory_path = ["AAC"] + +module Sigma = struct + let sigma = lazy (Coq.init_constant ac_theory_path "sigma") + let sigma_empty = lazy (Coq.init_constant ac_theory_path "sigma_empty") + let sigma_add = lazy (Coq.init_constant ac_theory_path "sigma_add") + let sigma_get = lazy (Coq.init_constant ac_theory_path "sigma_get") + + 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 = + mkApp (Lazy.force sigma, [|ty|]) + + let to_fun ty null map = + mkApp (Lazy.force sigma_get, [|ty;null;map|]) + + let of_list ty null l = + let map = + List.fold_left + (fun acc (i,t) -> assert (i > 0); add ty (Coq.Pos.of_int i) t acc) + (empty ty) + l + in to_fun ty null map +end + + +module Sym = struct + type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} + + let path = ac_theory_path @ ["Sym"] + let typ = lazy (Coq.init_constant path "pack") + let mkPack = lazy (Coq.init_constant path "mkPack") + let typeof = lazy (Coq.init_constant path "type_of") + let relof = lazy (Coq.init_constant path "rel_of") + let value = lazy (Coq.init_constant path "value") + let null = lazy (Coq.init_constant path "null") + let mk_typeof : Coq.reltype -> int -> constr = fun (x,r) n -> + mkApp (Lazy.force typeof, [| x ; Coq.Nat.of_int n |]) + let mk_relof : Coq.reltype -> int -> constr = fun (x,r) n -> + mkApp (Lazy.force relof, [| x;r ; Coq.Nat.of_int n |]) + let mk_pack ((x,r): Coq.reltype) s = + mkApp (Lazy.force mkPack, [|x;r; s.ar;s.value;s.morph|]) + let null eqt witness = + let (x,r),e = eqt in + mkApp (Lazy.force null, [| x;r;e;witness |]) + +end + +module Sum = struct + type pack = {plus: Term.constr; zero: Term.constr ; opac: Term.constr} + + let path = ac_theory_path @ ["Sum"] + let typ = lazy (Coq.init_constant path "pack") + let mkPack = lazy (Coq.init_constant path "mkPack") + let cstr_zero = lazy (Coq.init_constant path "zero") + let cstr_plus = lazy (Coq.init_constant path "plus") + + let mk_pack: Coq.reltype -> pack -> Term.constr = fun (x,r) s -> + mkApp (Lazy.force mkPack , [| x ; r; s.plus; s.zero; s.opac|]) + + let zero: Coq.reltype -> constr -> constr = fun (x,r) pack -> + mkApp (Lazy.force cstr_zero, [| x;r;pack|]) + let plus: Coq.reltype -> constr -> constr = fun (x,r) pack -> + mkApp (Lazy.force cstr_plus, [| x;r;pack|]) + + +end + +module Prd = struct + type pack = {dot: Term.constr; one: Term.constr ; opa: Term.constr} + + let path = ac_theory_path @ ["Prd"] + let typ = lazy (Coq.init_constant path "pack") + let mkPack = lazy (Coq.init_constant path "mkPack") + let cstr_one = lazy (Coq.init_constant path "one") + let cstr_dot = lazy (Coq.init_constant path "dot") + + let mk_pack: Coq.reltype -> pack -> Term.constr = fun (x,r) s -> + mkApp (Lazy.force mkPack , [| x ; r; s.dot; s.one; s.opa|]) + let one: Coq.reltype -> constr -> constr = fun (x,r) pack -> + mkApp (Lazy.force cstr_one, [| x;r;pack|]) + let dot: Coq.reltype -> constr -> constr = fun (x,r) pack -> + mkApp (Lazy.force cstr_dot, [| x;r;pack|]) + + +end + + +let op_ac = lazy (Coq.init_constant ac_theory_path "Op_AC") +let op_a = lazy (Coq.init_constant ac_theory_path "Op_A") + +(** The constants from the inductive type *) +let _Tty = lazy (Coq.init_constant ac_theory_path "T") +let vTty = lazy (Coq.init_constant ac_theory_path "vT") + +let rsum = lazy (Coq.init_constant ac_theory_path "sum") +let rprd = lazy (Coq.init_constant ac_theory_path "prd") +let rsym = lazy (Coq.init_constant ac_theory_path "sym") +let vnil = lazy (Coq.init_constant ac_theory_path "vnil") +let vcons = lazy (Coq.init_constant ac_theory_path "vcons") +let eval = lazy (Coq.init_constant ac_theory_path "eval") +let decide_thm = lazy (Coq.init_constant ac_theory_path "decide") + +(** Rebuild an equality *) +let mk_equal = fun (x,r) left right -> + mkApp (r, [| left; right|]) + + +let anomaly msg = + Util.anomaly ("aac_tactics: " ^ 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. We + consider that raw morphisms ([Sym]) are coarser than [A] + operators, which in turn are coarser than [AC] operators. We + need to treat the units first. Indeed, considering [S] as a + morphism is problematic because [S O] is a unit. + + During this reification, we gather some informations that will + be used to rebuild Coq terms from AST ( type {!envs}) *) + + type pack = + | AC of Sum.pack (* the opac pack *) + | A of Prd.pack (* the opa pack *) + | Sym of Sym.pack (* the sym pack *) + + type head = + | Fun + | Plus + | Dot + | One + | Zero + + + (* discr is a map from {!Term.constr} to + (head * 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. + + However, for the transitivity process, we do not need to remember + if the constr was the unit or the binary operation. We will use + the projections from the module's record. + + The field [bloom] allows to give a unique number to each class we + found. *) + type envs = + { + discr : (constr , (head * pack) option) Hashtbl.t ; + + bloom : (pack, int ) Hashtbl.t; + bloom_back : (int, pack ) Hashtbl.t; + bloom_next : int ref; + } + + let empty_envs () = + { + discr = 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 + then () + else + 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 = + try Hashtbl.find envs.bloom pack + with Not_found -> assert false + + + (** try to infer the kind of operator we are dealing with *) + let is_morphism rlt papp ar goal = + let typeof = Sym.mk_typeof rlt ar in + let relof = Sym.mk_relof rlt ar in + let env = Tacmach.pf_env goal in + let evar_map = Tacmach.project goal in + let m = Coq.Classes.mk_morphism typeof relof papp in + try + let _ = Tacmach.pf_check_type goal papp typeof in + let evar_map,m = Typeclasses.resolve_one_typeclass env evar_map m in + let pack = {Sym.ar = (Coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in + Some (Coq.goal_update goal evar_map, Fun , Sym pack) + with + | Not_found -> None + | _ -> None + + (** gives back the class *) + let is_op gl (rlt: Coq.reltype) pack op null = + let (x,r) = rlt in + let ty = mkApp (pack ,[|x;r; op; null |]) in + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + try + let em,t = Typeclasses.resolve_one_typeclass env evar_map ty in + let op = Evarutil.nf_evar em op in + let null = Evarutil.nf_evar em null in + Some (Coq.goal_update gl em,t,op,null) + with Not_found -> None + + + let is_plus (rlt: Coq.reltype) plus goal= + let (zero,goal) = Coq.evar_unit goal rlt in + match is_op goal rlt (Lazy.force op_ac) plus zero + with + | None -> None + | Some (gl,s,plus,zero) -> + let pack = {Sum.plus=plus;Sum.zero=zero;Sum.opac=s} in + Some (gl, Plus , AC pack) + + let is_dot rlt dot goal= + let (one,goal) = Coq.evar_unit goal rlt in + match is_op goal rlt (Lazy.force op_a) dot one + with + | None -> None + | Some (goal,s,dot,one) -> + let pack = {Prd.dot=dot;Prd.one=one;Prd.opa=s} in + Some (goal, Dot, A pack) + + let is_zero rlt zero goal = + let (plus,goal) = Coq.evar_binary goal rlt in + match is_op goal rlt (Lazy.force op_ac) plus zero + with + | None -> None + | Some (goal,s,plus,zero) -> + let pack = {Sum.plus=plus;Sum.zero=zero;Sum.opac=s} in + Some (goal, Zero , AC pack) + + let is_one rlt one goal = + let (dot,goal) = Coq.evar_binary goal rlt in + match is_op goal rlt (Lazy.force op_a) dot one + with + | None -> None + | Some (goal,s,dot,one)-> + let pack = {Prd.dot=dot;Prd.one=one;Prd.opa=s} in + Some (goal, One, A pack) + + + let (>>) x y a = + match x a with | None -> y a | x -> x + + let is_unit rlt papp = + (is_zero rlt papp )>> (is_one rlt papp) + + let what_is_it rlt papp ar goal : + (Coq.goal_sigma * head * pack ) option = + match ar with + | 2 -> + begin + ( + (is_plus rlt papp)>> + (is_dot rlt papp)>> + (is_morphism rlt papp ar) + ) goal + end + | _ -> + is_morphism rlt papp ar goal + + + + + (** [discriminates goal envs rlt t ca] infer : + + - the nature of the application [t ca] (is the head symbol a + Plus, a Dot, so on), + + - its {! pack } (is it an AC operator, or an A operator, or a + Symbol ?), + + - the relevant partial application, + + - the vector of the remaining arguments + + We use an expansion to handle the special case of units, before + going back to the general discrimination procedure *) + let discriminate goal envs (rlt : Coq.reltype) t ca : Coq.goal_sigma * head * pack * constr * constr array = + let nb_params = Array.length ca in + let f cont x p_app ar = + assert (0 <= ar && ar <= nb_params); + match x with + | Some (goal, discr, pack) -> + Hashtbl.add envs.discr p_app (Some (discr, pack)); + add_bloom envs pack; + (goal, discr, pack, p_app, Array.sub ca (nb_params-ar) ar) + | None -> + begin + (* to memoise the failures *) + Hashtbl.add envs.discr p_app None; + (* will terminate, since [const] is + capped, and it is easy to find an + instance of a constant *) + cont goal (ar-1) + end + in + let rec aux goal ar :Coq.goal_sigma * head * pack * constr * constr array = + assert (0 <= ar && ar <= nb_params); + let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in + begin + try + begin match Hashtbl.find envs.discr p_app with + | None -> aux goal (ar-1) + | Some (discr,sym) -> + goal, + discr, + sym, + p_app, + Array.sub ca (nb_params -ar ) ar + end + with + Not_found -> (* Could not find this constr *) + f aux (what_is_it rlt p_app ar goal) p_app ar + end + in + match is_unit rlt (mkApp (t,ca)) goal with + | None -> aux goal (nb_params) + | x -> f (fun _ -> assert false) x (mkApp (t,ca)) 0 + + let discriminate goal envs rlt x = + try + match Coq.decomp_term x with + | Var _ -> + discriminate goal envs rlt x [| |] + | App (t,ca) -> + discriminate goal envs rlt t ca + | Construct c -> + discriminate goal envs rlt x [| |] + | _ -> + assert false + with + (* TODO: is it the only source of invalid use that fall into + this catch_all ? *) + e -> user_error "cannot handle this kind of hypotheses (higher order function symbols, variables occuring under a non-morphism, etc)." + + + (** [t_of_constr goal rlt envs cstr] builds the abstract syntax + tree of the term [cstr]. Doing so, it modifies the environment + of known stuff [envs], and eventually creates fresh + evars. Therefore, we give back the goal updated accordingly *) + let t_of_constr goal (rlt: Coq.reltype ) envs : constr -> Matcher.Terms.t *Coq.goal_sigma = + let r_evar_map = ref (goal) in + let rec aux x = + match Coq.decomp_term x with + | Rel i -> Matcher.Terms.Var i + | _ -> + let goal, sym, pack , p_app, ca = discriminate (!r_evar_map) envs rlt x in + r_evar_map := goal; + let k = find_bloom envs pack + in + match sym with + | Plus -> + assert (Array.length ca = 2); + Matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1)) + | Zero -> + assert (Array.length ca = 0); + Matcher.Terms.Zero ( k) + | Dot -> + assert (Array.length ca = 2); + Matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1)) + | One -> + assert (Array.length ca = 0); + Matcher.Terms.One ( k) + | Fun -> + Matcher.Terms.Sym ( k, Array.map aux ca) + in + ( + fun x -> let r = aux x in r, !r_evar_map + ) + + (** {1 From AST back to Coq } + + The next functions allow one to map OCaml abstract syntax trees + to Coq terms *) + + (** {2 Building raw, natural, terms} *) + + (** [raw_constr_of_t] rebuilds a term in the raw representation *) + let raw_constr_of_t envs (rlt : Coq.reltype) (t : Matcher.Terms.t) : Term.constr = + 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 + (fun x -> r := add x !r),(fun () -> !r) + in + let rec aux t = + match t with + | Matcher.Terms.Plus (s,l,r) -> + begin match Hashtbl.find envs.bloom_back s with + | AC s -> + mkApp (s.Sum.plus , [|(aux l);(aux r)|]) + | _ -> assert false + end + | Matcher.Terms.Dot (s,l,r) -> + begin match Hashtbl.find envs.bloom_back s with + | A s -> + mkApp (s.Prd.dot, [|(aux l);(aux r)|]) + | _ -> assert false + end + | Matcher.Terms.Sym (s,t) -> + begin match Hashtbl.find envs.bloom_back s with + | Sym s -> + mkApp (s.Sym.value, Array.map aux t) + | _ -> assert false + end + | Matcher.Terms.One x -> + begin match Hashtbl.find envs.bloom_back x with + | A s -> + s.Prd.one + | _ -> assert false + end + | Matcher.Terms.Zero x -> + begin match Hashtbl.find envs.bloom_back x with + | AC s -> + s.Sum.zero + | _ -> assert false + end + | Matcher.Terms.Var i -> add_set i; + let i = (Names.id_of_string (Printf.sprintf "x%i" i)) in + mkVar (i) + in + let x = fst rlt in + let rec cap c = function [] -> c + | t::q -> let i = (Names.id_of_string (Printf.sprintf "x%i" t)) in + cap (mkNamedProd i x c) q + in + cap ((aux t)) (get ()) + (* aux t is possible for printing only, but I wonder what + would be the status of such a term*) + + + (** {2 Building reified terms} *) + + (* Some informations to be able to build the maps *) + type reif_params = + { + a_null : constr; + ac_null : constr; + sym_null : constr; + a_ty : constr; + ac_ty : constr; + sym_ty : constr; + } + + type sigmas = { + env_sym : Term.constr; + env_sum : Term.constr; + env_prd : Term.constr; + } + (** A record containing the environments that will be needed by the + decision procedure, as a Coq constr. Contains also the functions + from the symbols (as ints) to indexes (as constr) *) + type sigma_maps = { + sym_to_pos : int -> Term.constr; + sum_to_pos : int -> Term.constr; + prd_to_pos : int -> Term.constr; + } + + (* convert the [envs] into the [sigma_maps] *) + let envs_to_list rlt envs = + let add x y (n,l) = (n+1, (x, ( n, y))::l) in + let nil = 1,[]in + Hashtbl.fold + (fun int pack (sym,sum,prd) -> + match pack with + |AC s -> + let s = Sum.mk_pack rlt s in + sym, add (int) s sum, prd + |A s -> + let s = Prd.mk_pack rlt s in + sym, sum, add (int) s prd + | Sym s -> + let s = Sym.mk_pack rlt s in + add (int) s sym, sum, prd + ) + envs.bloom_back + (nil,nil,nil) + + + + (** infers some stuff that will be required when we will build + environments (our environments need a default case, so we need + an Op_AC, an Op_A, and a symbol) *) + + (* 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 eqt = + let rlt = fst eqt in + let plus,goal = Coq.evar_binary goal rlt in + let dot ,goal = Coq.evar_binary goal rlt in + let one ,goal = Coq.evar_unit goal rlt in + let zero,goal = Coq.evar_unit goal rlt in + + let (x,r) = rlt in + let ty_ac = ( mkApp (Lazy.force op_ac, [| x;r;plus;zero|])) in + let ty_a = ( mkApp (Lazy.force op_a, [| x;r;dot;one|])) in + let a ,goal= + try Coq.resolve_one_typeclass goal ty_a + with Not_found -> user_error ("Unable to infer a default A operator.") + in + let ac ,goal= + try Coq.resolve_one_typeclass goal ty_ac + with Not_found -> user_error ("Unable to infer a default AC operator.") + in + let plus = Coq.nf_evar goal plus in + let dot = Coq.nf_evar goal dot in + let one = Coq.nf_evar goal one in + let zero = Coq.nf_evar goal zero in + + let record = + {a_null = Prd.mk_pack rlt {Prd.dot=dot;Prd.one=one;Prd.opa=a}; + ac_null= Sum.mk_pack rlt {Sum.plus=plus;Sum.zero=zero;Sum.opac=ac}; + sym_null = Sym.null eqt zero; + a_ty = (mkApp (Lazy.force Prd.typ, [| x;r; |])); + ac_ty = ( mkApp (Lazy.force Sum.typ, [| x;r|])); + sym_ty = mkApp (Lazy.force Sym.typ, [|x;r|]) + } + in + goal, record + + (** [build_sigma_maps] given a envs and some reif_params, we are + able to build the sigmas *) + let build_sigma_maps goal eqt envs : sigmas * sigma_maps * Proof_type.goal Evd.sigma = + let rlt = fst eqt in + let goal,rp = build_reif_params goal eqt in + let ((_,sym), (_,sum),(_,prd)) = envs_to_list rlt envs in + let f = List.map (fun (x,(y,z)) -> (x,Coq.Pos.of_int y)) in + let g = List.map (fun (x,(y,z)) -> (y,z)) in + let sigmas = + {env_sym = Sigma.of_list rp.sym_ty rp.sym_null (g sym); + env_sum = Sigma.of_list rp.ac_ty rp.ac_null (g sum); + env_prd = Sigma.of_list rp.a_ty rp.a_null (g prd); + } in + let sigma_maps = { + sym_to_pos = (let sym = f sym in fun x -> (List.assoc x sym)); + sum_to_pos = (let sum = f sum in fun x -> (List.assoc x sum)); + prd_to_pos = (let prd = f prd in fun x -> (List.assoc x prd)); + } + in + sigmas, sigma_maps , goal + + + + (** builders for the reification *) + type reif_builders = + { + rsum: constr -> constr -> constr -> constr; + rprd: constr -> constr -> constr -> constr; + rzero: constr -> constr; + rone: constr -> constr; + rsym: constr -> constr array -> 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 = + fun (x,t) f -> + 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 + | 0 -> vnil + | n -> let n = n-1 in + mkApp( vcons, + [| + (Coq.Nat.of_int n); + v.(ar - 1 - n); + (aux (n)) + |] + ) + in aux ar + + (* TODO: use a do notation *) + let mk_reif_builders (rlt: Coq.reltype) (env_sym:constr) :reif_builders*Proof_type.tactic = + let x,r = rlt in + let tty = mkApp (Lazy.force _Tty, [| x ; r ; env_sym|]) in + (Coq.mk_letin' "mk_rsum" (mkApp (Lazy.force rsum, [| x; r; env_sym|]))) >> + (fun rsum -> (Coq.mk_letin' "mk_rprd" (mkApp (Lazy.force rprd, [| x; r; env_sym|]))) + >> fun rprd -> ( Coq.mk_letin' "mk_rsym" (mkApp (Lazy.force rsym, [| x;r; env_sym|]))) + >> fun rsym -> (Coq.mk_letin' "mk_vnil" (mkApp (Lazy.force vnil, [| x;r; env_sym|]))) + >> fun vnil -> Coq.mk_letin' "mk_vcons" (mkApp (Lazy.force vcons, [| x;r; env_sym|])) + >> fun vcons -> + return { + rsum = + begin fun idx l r -> + mkApp (rsum, [| idx ; Coq.mk_mset tty [l,1 ; r,1]|]) + end; + rzero = + begin fun idx -> + mkApp (rsum, [| idx ; Coq.mk_mset tty []|]) + end; + rprd = + begin fun idx l r -> + let lst = Coq.List.of_list tty [l;r] in + mkApp (rprd, [| idx; lst|]) + end; + rone = + begin fun idx -> + let lst = Coq.List.of_list tty [] in + mkApp (rprd, [| idx; lst|]) end; + rsym = + begin fun idx v -> + let vect = mk_vect vnil vcons v in + mkApp (rsym, [| idx; vect|]) + end; + } + ) + + + + type reifier = sigma_maps * reif_builders + + let mk_reifier eqt envs goal : sigmas * reifier * Proof_type.tactic = + let s, sm, goal = build_sigma_maps goal eqt envs in + let env_sym, env_sym_letin = Coq.mk_letin "env_sym_name" (s.env_sym) in + let env_prd, env_prd_letin = Coq.mk_letin "env_prd_name" (s.env_prd) in + let env_sum, env_sum_letin = Coq.mk_letin "env_sum_name" (s.env_sum) in + let s = {env_sym = env_sym; env_prd = env_prd; env_sum = env_sum} in + let rb , tac = mk_reif_builders (fst eqt) (s.env_sym) in + let evar_map = Tacmach.project goal in + let tac = Tacticals.tclTHENLIST ( + [ Refiner.tclEVARS evar_map; + env_prd_letin ; + env_sum_letin ; + env_sym_letin ; + tac + ]) in + s, (sm, rb), tac + + + (** [reif_constr_of_t reifier t] rebuilds the term [t] in the + reified form. We use the [reifier] to minimise the size of the + terms (we make as much lets as possible)*) + let reif_constr_of_t (sm,rb) (t:Matcher.Terms.t) : constr = + let rec aux = function + | Matcher.Terms.Plus (s,l,r) -> + let idx = sm.sum_to_pos s in + rb.rsum idx (aux l) (aux r) + | Matcher.Terms.Dot (s,l,r) -> + let idx = sm.prd_to_pos s in + rb.rprd idx (aux l) (aux r) + | Matcher.Terms.Sym (s,t) -> + let idx = sm.sym_to_pos s in + rb.rsym idx (Array.map aux t) + | Matcher.Terms.One s -> + let idx = sm.prd_to_pos s in + rb.rone idx + | Matcher.Terms.Zero s -> + let idx = sm.sum_to_pos s in + rb.rzero idx + | Matcher.Terms.Var i -> + anomaly "call to reif_constr_of_t on a term with variables." + in aux t + + +end + + + diff --git a/theory.mli b/theory.mli new file mode 100644 index 0000000..85ad24b --- /dev/null +++ b/theory.mli @@ -0,0 +1,219 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Bindings for Coq constants that are specific to the plugin; + reification and translation functions. + + Note: this module is highly correlated with the definitions of {i + AAC.v}. + + This module interfaces with the above Coq module; it provides + facilities to interpret a term with arbitrary operators as an + abstract syntax tree, and to convert an AST into a Coq term + (either using the Coq "raw" terms, as written in the starting + goal, or using the reified Coq datatypes we define in {i + AAC.v}). +*) + + + + +(** Environments *) +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 + + (** [of_list ty null l] translates an OCaml association list into a Coq one *) + val of_list: Term.constr -> Term.constr -> (int * Term.constr ) list -> Term.constr + + (** [to_fun ty null map] converts a Coq association list into a Coq function (with default value [null]) *) + val to_fun: Term.constr ->Term.constr ->Term.constr ->Term.constr +end + +(** The constr associated with our typeclasses for AC or A operators *) +val op_ac:Term.constr lazy_t +val op_a:Term.constr lazy_t + +(** 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 + [compare (norm u) (norm v) = Eq -> eval u == eval v] *) +val decide_thm:Term.constr lazy_t + +(** {2 Packaging modules} *) + +(** Dynamically typed morphisms *) +module Sym: +sig + (** mimics the Coq record [Sym.pack] *) + type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} + + val typ: Term.constr lazy_t + + (** [mk_typeof rlt int] *) + val mk_typeof: Coq.reltype ->int ->Term.constr + + (** [mk_typeof rlt int] *) + val mk_relof: Coq.reltype ->int ->Term.constr + + (** [mk_pack rlt (ar,value,morph)] *) + val mk_pack: Coq.reltype -> pack -> Term.constr + + (** [null] builds a dummy symbol, given an {!Coq.eqtype} and a + constant *) + val null: Coq.eqtype -> Term.constr -> Term.constr + +end + +(** Dynamically typed AC operations *) +module Sum: +sig + + (** mimics the Coq record [Sum.pack] *) + type pack = {plus : Term.constr; zero: Term.constr ; opac: Term.constr} + + val typ: Term.constr lazy_t + + (** [mk_pack rlt (plus,zero,opac)] *) + val mk_pack: Coq.reltype -> pack -> Term.constr + + (** [zero rlt pack]*) + val zero: Coq.reltype -> Term.constr -> Term.constr + + (** [plus rlt pack]*) + val plus: Coq.reltype -> Term.constr -> Term.constr + +end + + +(** Dynamically typed A operations *) +module Prd: +sig + + (** mimics the Coq record [Prd.pack] *) + type pack = {dot: Term.constr; one: Term.constr ; opa: Term.constr} + + val typ: Term.constr lazy_t + + (** [mk_pack rlt (dot,one,opa)] *) + val mk_pack: Coq.reltype -> pack -> Term.constr + + (** [one rlt pack]*) + val one: Coq.reltype -> Term.constr -> Term.constr + + (** [dot rlt pack]*) + val dot: Coq.reltype -> Term.constr -> Term.constr + +end + + +(** [mk_equal rlt l r] builds the term [l == r] *) +val mk_equal : Coq.reltype -> Term.constr -> Term.constr -> Term.constr + + +(** {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 + {!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 + ... x_i], [i<=n] is a proper morphism, whether the partial + application with [i=n-2] yields an A or AC binary operator, and + 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: + - 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; the + behaviour in this case is almost unspecified: we simply give + priority to AC 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 + val empty_envs : unit -> envs + + (** {1 Reification: from Coq terms to AST {!Matcher.Terms.t} } *) + + (** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree + of the term [cstr]. We rely on the [goal] to perform typeclasses + resolutions to find morphisms compatible with the relation + [rlt]. Doing so, it modifies the reification environment + [envs]. Moreover, we need to create creates fresh evars; this is + why we give back the [goal], accordingly updated. *) + val t_of_constr : Coq.goal_sigma -> Coq.reltype -> envs -> Term.constr -> Matcher.Terms.t * Coq.goal_sigma + + (** {1 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 + {!t_of_constr}; second, reified Coq terms, that are required for + the reflexive decision procedure. *) + + (** {2 Building raw, natural, terms} *) + + (** [raw_constr_of_t] rebuilds a term in the raw representation *) + val raw_constr_of_t : envs -> Coq.reltype -> Matcher.Terms.t -> Term.constr + + (** {2 Building reified terms} *) + + (** The reification environments, as Coq constrs *) + type sigmas = { + env_sym : Term.constr; + env_sum : Term.constr; + env_prd : Term.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. + + 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.*) + type reifier + + val mk_reifier : Coq.eqtype -> envs -> Coq.goal_sigma -> sigmas * reifier * Proof_type.tactic + + (** [reif_constr_of_t reifier t] rebuilds the term [t] in the + reified form. *) + val reif_constr_of_t : reifier -> Matcher.Terms.t -> Term.constr +end |