diff options
Diffstat (limited to 'AAC.v')
| -rw-r--r-- | AAC.v | 1058 |
1 files changed, 752 insertions, 306 deletions
@@ -13,7 +13,7 @@ quoted) expressions (with morphisms). We then define a reflexive decision procedure to decide the - equality of reified terms: first normalize reified terms, then + equality of reified terms: first normalise reified terms, then compare them. This allows us to close transitivity steps automatically, in the [aac_rewrite] tactic. @@ -23,7 +23,7 @@ [H: forall x y, nat_of_pos (pos_of_nat (x) + y) + x = ....] - where one occurence of [+] operates on nat while the other one + where one occurrence of [+] operates on nat while the other one operates on positive. *) Require Import Arith NArith. @@ -33,8 +33,8 @@ Require Import RelationClasses Equality. Require Export Morphisms. Set Implicit Arguments. -Unset Automatic Introduction. -Open Scope signature_scope. + +Local Open Scope signature_scope. (** * Environments for the reification process: we use positive maps to index elements *) @@ -49,123 +49,78 @@ Section sigma. 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. -*) +(** * Classes for properties of operators *) -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) +Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) := + law_assoc : forall x y z, R (dot x (dot y z)) (dot (dot x y) z). +Class Commutative (X:Type) (R: relation X) (plus: X -> X -> X) := + law_comm: forall x y, R (plus x y) (plus y x). +Class Unit (X:Type) (R:relation X) (op : X -> X -> X) (unit:X) := { + law_neutral_left: forall x, R (op unit x) x; + law_neutral_right: forall x, R (op x unit) 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) +(** Class used to find the equivalence relation on which operations + are A or AC, starting from the relation appearing in the goal *) + +Class AAC_lift X (R: relation X) (E : relation X) := { + aac_lift_equivalence : Equivalence E; + aac_list_proper : Proper (E ==> E ==> iff) R }. +(** simple instances, when we have a subrelation, or an equivalence *) -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. +Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E} + {HR: @Transitive X R} {HER: subrelation E R}: AAC_lift R E | 3. +Proof. + constructor; trivial. + intros ? ? H ? ? H'. split; intro G. + rewrite <- H, G. apply HER, H'. + rewrite H, G. apply HER. symmetry. apply H'. +Qed. +Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E} + {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4. -(** 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. +Module Internal. (** * 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}. + Context {X} {R} {HR: @Equivalence X R} {plus} + (op: Associative R plus) (op': Commutative R plus) (po: Proper (R ==> R ==> R) plus). (* copy n x = x+...+x (n times) *) - Definition copy n x := Prect (fun _ => X) x (fun _ xn => plus x xn) n. - + Fixpoint copy' n x := match n with + | xH => x + | xI n => let xn := copy' n x in plus (plus xn xn) x + | xO n => let xn := copy' n x in (plus xn xn) + end. + Definition copy n x := Prect (fun _ => X) x (fun _ xn => plus x xn) n. + Lemma copy_plus : forall n m x, R (copy (n+m) x) (plus (copy n x) (copy m x)). Proof. unfold copy. induction n using Pind; intros m x. - rewrite Prect_base. rewrite <- Pplus_one_succ_l. rewrite Prect_succ. reflexivity. - rewrite Pplus_succ_permute_l. rewrite 2Prect_succ. rewrite IHn. apply plus_assoc. + rewrite Prect_base. rewrite <- Pplus_one_succ_l. rewrite Prect_succ. reflexivity. + rewrite Pplus_succ_permute_l. rewrite 2Prect_succ. rewrite IHn. apply op. Qed. + Lemma copy_xH : forall x, R (copy 1 x) x. + Proof. intros; unfold copy; rewrite Prect_base. reflexivity. Qed. + Lemma copy_Psucc : forall n x, R (copy (Psucc n) x) (plus x (copy n x)). + Proof. intros; unfold copy; rewrite Prect_succ. reflexivity. Qed. Global Instance copy_compat n: Proper (R ==> R) (copy n). Proof. unfold copy. induction n using Pind; intros x y H. rewrite 2Prect_base. assumption. - rewrite 2Prect_succ. apply plus_compat; auto. + rewrite 2Prect_succ. apply po; auto. Qed. End copy. @@ -173,9 +128,9 @@ End copy. (** * Utilities for positive numbers which we use as: - indices for morphisms and symbols - - multiplicity of terms in sums - *) -Notation idx := positive. + - multiplicity of terms in sums *) + +Local Notation idx := positive. Fixpoint eq_idx_bool i j := match i,j with @@ -196,9 +151,9 @@ Fixpoint idx_compare i j := | xO _, xI _ => Lt end. -Notation pos_compare := idx_compare (only parsing). +Local Notation pos_compare := idx_compare (only parsing). -(** specification predicate for boolean binary functions *) +(** 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. @@ -222,9 +177,9 @@ Proof. induction i; destruct j; simpl; try constructor; case (IHi j); intros; co 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). + +Local Notation cast T H u := (eq_rect _ T u _ H). Section dep. Variable U: Type. @@ -239,10 +194,12 @@ Section dep. (* 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. + 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). + 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. @@ -250,31 +207,56 @@ Section dep. End dep. -(** * Utilities about lists and multisets *) + +(** * Utilities about (non-empty) lists and multisets *) + +Inductive nelist (A : Type) : Type := +| nil : A -> nelist A +| cons : A -> nelist A -> nelist A. + +Local Notation "x :: y" := (cons x y). + +Fixpoint nelist_map (A B: Type) (f: A -> B) l := + match l with + | nil x => nil ( f x) + | cons x l => cons ( f x) (nelist_map f l) + end. + +Fixpoint appne A l l' : nelist A := + match l with + nil x => cons x l' + | cons t q => cons t (appne A q l') + end. + +Local Notation "x ++ y" := (appne x y). (** finite multisets are represented with ordered lists with multiplicities *) -Definition mset A := list (A*positive). +Definition mset A := nelist (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). +Local Notation lex e f := (match e with Eq => f | _ => e end). Section lists. - (** comparison function *) + (** comparison functions *) + 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) + | nil x, nil y => compare x y + | nil x, _ => Lt + | _, nil x => Gt + | u::h, v::k => lex (compare u v) (list_compare h k) end. End 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)). + 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. @@ -282,10 +264,13 @@ Section lists. 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). + 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 (Hcompare a a0 ); try constructor. + case (Hcompare u v ); try constructor. case (IHh k); intros; constructor. Defined. End list_compare_weak_spec. @@ -296,7 +281,8 @@ Section lists. 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). + 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]. @@ -306,17 +292,40 @@ Section lists. End mset_compare_weak_spec. (** (sorted) merging functions *) + Section m. Variable A: Type. Variable compare: A -> A -> comparison. - + Definition insert n1 h1 := + let fix insert_aux l2 := + match l2 with + | nil (h2,n2) => + match compare h1 h2 with + | Eq => nil (h1,Pplus n1 n2) + | Lt => (h1,n1):: nil (h2,n2) + | Gt => (h2,n2):: nil (h1,n1) + end + | (h2,n2)::t2 => + match compare h1 h2 with + | Eq => (h1,Pplus n1 n2):: t2 + | Lt => (h1,n1)::l2 + | Gt => (h2,n2)::insert_aux t2 + end + end + in insert_aux. + Fixpoint merge_msets l1 := match l1 with - | nil => fun l2 => l2 + | nil (h1,n1) => fun l2 => insert n1 h1 l2 | (h1,n1)::t1 => let fix merge_aux l2 := match l2 with - | nil => l1 + | nil (h2,n2) => + match compare h1 h2 with + | Eq => (h1,Pplus n1 n2) :: t1 + | Lt => (h1,n1):: merge_msets t1 l2 + | Gt => (h2,n2):: l1 + end | (h2,n2)::t2 => match compare h1 h2 with | Eq => (h1,Pplus n1 n2)::merge_msets t1 t2 @@ -328,44 +337,119 @@ Section lists. 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 + | nil x => map x | 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 := + + Variable merge: A -> nelist B -> nelist B. + Fixpoint merge_map (l: nelist A): nelist B := match l with - | nil => nil + | nil x => nil (map x) | u::l => merge u (merge_map l) end. - End m. + Variable ret : A -> B. + Variable bind : A -> B -> B. + Fixpoint fold_map' (l : nelist A) : B := + match l with + | nil x => ret x + | u::l => bind u (fold_map' l) + end. + End m. End lists. +(** * 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 *) + Definition null: pack := mkPack 1 (fun x => x) (fun _ _ H => H). + + End t. + +End Sym. + +(** ** binary operations *) + +Module Bin. + Section t. + Context {X} {R: relation X}. + + Record pack := mk_pack { + value:> X -> X -> X; + compat: Proper (R ==> R ==> R) value; + assoc: Associative R value; + comm: option (Commutative R value) + }. + End t. + (* See #<a href="Instances.html">Instances.v</a># for concrete instances of these classes. *) + +End Bin. (** * 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_bin: idx -> @Bin.pack X R. - 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. + + (** packaging units (depends on e_bin) *) + + Record unit_of u := mk_unit_for { + uf_idx: idx; + uf_desc: Unit R (Bin.value (e_bin uf_idx)) u + }. + Record unit_pack := mk_unit_pack { + u_value:> X; + u_desc: list (unit_of u_value) + }. + Variable e_unit: positive -> unit_pack. + + Hint Resolve e_bin e_unit: typeclass_instances. (** ** Almost normalised syntax a term in [T] is in normal form if: @@ -379,10 +463,12 @@ Section s. 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 + | prd: idx -> nelist T -> T | sym: forall i, vT (Sym.ar (e_sym i)) -> T + | unit : idx -> T with vT: nat -> Type := | vnil: vT O | vcons: forall n, T -> vT n -> vT (S n). @@ -394,10 +480,14 @@ Section s. | 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) + | unit i , unit j => idx_compare i j + | unit _ , _ => Lt + | _ , unit _ => Gt | sum _ _, _ => Lt | _ , sum _ _ => Gt | prd _ _, _ => Lt | _ , prd _ _ => Gt + end with vcompare i j (us: vT i) (vs: vT j) := match us,vs with @@ -406,12 +496,27 @@ Section s. | _, 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) - *) + (** ** Evaluation from syntax to the abstract domain *) + Fixpoint eval u: X := + match u with + | sum i l => let o := Bin.value (e_bin i) in + fold_map (fun un => let '(u,n):=un in @copy _ o n (eval u)) o l + | prd i l => fold_map eval (Bin.value (e_bin i)) l + | sym i v => eval_aux v (Sym.value (e_sym i)) + | unit i => e_unit 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. + + (** 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. @@ -421,12 +526,15 @@ Section s. 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. + case (list_compare_weak_spec compare tcompare_weak_spec n n0); 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. + rewrite <- (vcompare_reflect_eqdep _ _ _ _ eq_refl Hv). constructor. + destruct v; simpl; try constructor. + case_eq (idx_compare p p0); intro Hi; try constructor. + apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst. constructor. induction us; destruct vs; simpl; intros H Huv; try discriminate. apply cast_eq, eq_nat_dec. @@ -437,22 +545,6 @@ Section s. 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. @@ -460,55 +552,149 @@ Section s. apply IHl, H. reflexivity. Qed. + + (* is [i] a unit for [j] ? *) + Definition is_unit_of j i := + List.existsb (fun p => eq_idx_bool j (uf_idx p)) (u_desc (e_unit i)). + + (* is [i] commutative ? *) + Definition is_commutative i := + match Bin.comm (e_bin i) with Some _ => true | None => false end. + (** ** 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 + Inductive discr {A} : Type := + | Is_op : A -> discr + | Is_unit : idx -> discr + | Is_nothing : discr . + + (* This is called sum in the std lib *) + Inductive m {A} {B} := + | left : A -> m + | right : B -> m. + + Definition comp A B (merge : B -> B -> B) (l : B) (l' : @m A B) : @m A B := + match l' with + | left _ => right l + | right l' => right (merge l l') end. - Definition is_sum i (u: T): option (mset T) := + + (** auxiliary functions, to clean up sums *) + + Section sums. + Variable i : idx. + Variable is_unit : idx -> bool. + + Definition sum' (u: mset T): T := + match u with + | nil (u,xH) => u + | _ => sum i u + end. + + Definition is_sum (u: T) : @discr (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 + | sum j l => if eq_idx_bool j i then Is_op l else Is_nothing + | unit j => if is_unit j then Is_unit j else Is_nothing + | u => Is_nothing 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 + + Definition copy_mset n (l: mset T): mset T := + match n with + | xH => l + | _ => nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l + end. + + Definition return_sum u n := + match is_sum u with + | Is_nothing => right (nil (u,n)) + | Is_op l' => right (copy_mset n l') + | Is_unit j => left j + end. + + Definition add_to_sum u n (l : @m idx (mset T)) := + match is_sum u with + | Is_nothing => comp (merge_msets compare) (nil (u,n)) l + | Is_op l' => comp (merge_msets compare) (copy_mset n l') l + | Is_unit _ => l end. - Definition prd' i (u: list T): T := + + Definition norm_msets_ norm (l: mset T) := + fold_map' + (fun un => let '(u,n) := un in return_sum (norm u) n) + (fun un l => let '(u,n) := un in add_to_sum (norm u) n l) l. + + + End sums. + + (** similar functions for products *) + + Section prds. + + Variable i : idx. + Variable is_unit : idx -> bool. + Definition prd' (u: nelist T): T := match u with - | u::nil => u + | nil u => u | _ => prd i u end. - Definition is_prd i (u: T): option (list T) := + + Definition is_prd (u: T) : @discr (nelist 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 + | prd j l => if eq_idx_bool j i then Is_op l else Is_nothing + | unit j => if is_unit j then Is_unit j else Is_nothing + | u => Is_nothing end. + + + Definition return_prd u := + match is_prd u with + | Is_nothing => right (nil (u)) + | Is_op l' => right (l') + | Is_unit j => left j + end. + + Definition add_to_prd u (l : @m idx (nelist T)) := + match is_prd u with + | Is_nothing => comp (@appne T) (nil (u)) l + | Is_op l' => comp (@appne T) (l') l + | Is_unit _ => l + end. + + Definition norm_lists_ norm (l : nelist T) := + fold_map' + (fun u => return_prd (norm u)) + (fun u l => add_to_prd (norm u) l) l. + + End prds. - (** we deduce the normalisation function *) - Fixpoint norm u := + + Definition run_list x := match x with + | left n => nil (unit n) + | right l => l + end. + + Definition norm_lists norm i l := + let is_unit := is_unit_of i in + run_list (norm_lists_ i is_unit norm l). + + Definition run_msets x := match x with + | left n => nil (unit n, xH) + | right l => l + end. + + Definition norm_msets norm i l := + let is_unit := is_unit_of i in + run_msets (norm_msets_ i is_unit norm l). + + Fixpoint norm u {struct 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) + | sum i l => if is_commutative i then sum' i (norm_msets norm i l) else u + | prd i l => prd' i (norm_lists norm i l) | sym i l => sym i (vnorm l) + | unit i => unit i end with vnorm i (l: vT i): vT i := match l with @@ -516,167 +702,402 @@ Section s. | 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)). + Lemma is_unit_of_Unit : forall i j : idx, + is_unit_of i j = true -> Unit R (Bin.value (e_bin i)) (eval (unit j)). 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. + intros. unfold is_unit_of in H. + rewrite existsb_exists in H. + destruct H as [x [H H']]. + revert H' ; case (eq_idx_spec); [intros H' _ ; subst| intros _ H'; discriminate]. + simpl. destruct x. simpl. auto. 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). + + Instance Binvalue_Commutative i (H : is_commutative i = true) : Commutative R (@Bin.value _ _ (e_bin i) ). Proof. - intros i [j l|j l|j l]; simpl; try constructor. - case eq_idx_spec; intro. - subst. constructor. - econstructor. eassumption. + unfold is_commutative in H. + destruct (Bin.comm (e_bin i)); auto. + discriminate. Qed. - Lemma eval_is_sum: forall i (a: T) k, is_sum i a = Some k -> eval (sum i k) = eval a. + Instance Binvalue_Associative i :Associative R (@Bin.value _ _ (e_bin i) ). 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. + destruct ((e_bin i)); auto. 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. + + Instance Binvalue_Proper i : Proper (R ==> R ==> R) (@Bin.value _ _ (e_bin i) ). Proof. - intros. destruct n; try reflexivity. - simpl. induction l as [|[a l] IHl]; simpl; congruence. + destruct ((e_bin i)); auto. Qed. + Hint Resolve Binvalue_Proper Binvalue_Associative Binvalue_Commutative. + (** auxiliary lemmas about sums *) + + Hint Resolve is_unit_of_Unit. + Section sum_correctness. + Variable i : idx. + Variable is_unit : idx -> bool. + Hypothesis is_unit_sum_Unit : forall j, is_unit j = true-> @Unit X R (Bin.value (e_bin i)) (eval (unit j)). + + Inductive is_sum_spec_ind : T -> @discr (mset T) -> Prop := + | is_sum_spec_op : forall j l, j = i -> is_sum_spec_ind (sum j l) (Is_op l) + | is_sum_spec_unit : forall j, is_unit j = true -> is_sum_spec_ind (unit j) (Is_unit j) + | is_sum_spec_nothing : forall u, is_sum_spec_ind u (Is_nothing). - Lemma 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 is_sum_spec u : is_sum_spec_ind u (is_sum i is_unit u). + Proof. + unfold is_sum; case u; intros; try constructor. + case_eq (eq_idx_bool p i); intros; subst; try constructor; auto. + revert H. case eq_idx_spec; try discriminate. auto. + case_eq (is_unit p); intros; try constructor. auto. + Qed. + + Instance assoc : @Associative X R (Bin.value (e_bin i)). + Proof. + destruct (e_bin i). simpl. assumption. + Qed. + Instance proper : Proper (R ==> R ==> R)(Bin.value (e_bin i)). + Proof. + destruct (e_bin i). simpl. assumption. + Qed. + Hypothesis comm : @Commutative X R (Bin.value (e_bin i)). + + Lemma sum'_sum : forall (l: mset T), eval (sum' i l) ==eval (sum i l) . + Proof. + intros [[a n] | [a n] l]; destruct n; simpl; reflexivity. + Qed. + + Lemma eval_sum_nil x: + eval (sum i (nil (x,xH))) == (eval x). + Proof. rewrite <- sum'_sum. reflexivity. Qed. + + Lemma eval_sum_cons : forall n a (l: mset T), + (eval (sum i ((a,n)::l))) == (@Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval a)) (eval (sum i l))). + Proof. + intros n a [[? ? ]|[b m] l]; simpl; reflexivity. + Qed. + + Inductive compat_sum_unit : @m idx (mset T) -> Prop := + | csu_left : forall x, is_unit x = true-> compat_sum_unit (left x) + | csu_right : forall m, compat_sum_unit (right m) + . - 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. + Lemma compat_sum_unit_return x n : compat_sum_unit (return_sum i is_unit x n). + Proof. + unfold return_sum. + case is_sum_spec; intros; try constructor; auto. + Qed. + + Lemma compat_sum_unit_add : forall x n h, + compat_sum_unit h + -> + compat_sum_unit + (add_to_sum i (is_unit_of i) x n + h). + Proof. + unfold add_to_sum;intros; inversion H; + case_eq (is_sum i (is_unit_of i) x); + intros; simpl; try constructor || eauto. apply H0. + Qed. + + (* Hint Resolve copy_plus. : this lags because of the inference of the implicit arguments *) + Hint Extern 5 (copy (?n + ?m) (eval ?a) == Bin.value (copy ?n (eval ?a)) (copy ?m (eval ?a))) => apply copy_plus. + Hint Extern 5 (?x == ?x) => reflexivity. + Hint Extern 5 ( Bin.value ?x ?y == Bin.value ?y ?x) => apply Bin.comm. + + Lemma eval_merge_bin : forall (h k: mset T), + eval (sum i (merge_msets compare h k)) == @Bin.value _ _ (e_bin i) (eval (sum i h)) (eval (sum i k)). + Proof. + induction h as [[a n]|[a n] h IHh]; intro k. + simpl. + induction k as [[b m]|[b m] k IHk]; simpl. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. apply copy_plus; auto. + + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl; auto. + rewrite copy_plus,law_assoc; auto. + rewrite IHk; clear IHk. rewrite 2 law_assoc. apply proper. apply law_comm. reflexivity. + + induction k as [[b m]|[b m] k IHk]; simpl; simpl in IHh. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. + rewrite (law_comm _ (copy m (eval a))), law_assoc, <- copy_plus, Pplus_comm; auto. + rewrite <- law_assoc, IHh. reflexivity. + rewrite law_comm. reflexivity. + + simpl in IHk. + destruct (tcompare_weak_spec a b) as [a|a b|a b]; simpl. + rewrite IHh; clear IHh. rewrite 2 law_assoc. rewrite (law_comm _ (copy m (eval a))). rewrite law_assoc, <- copy_plus, Pplus_comm; auto. + rewrite IHh; clear IHh. simpl. rewrite law_assoc. reflexivity. + rewrite 2 (law_comm (copy m (eval b))). rewrite law_assoc. apply proper; [ | reflexivity]. + rewrite <- IHk. reflexivity. + Qed. + + Lemma copy_mset' n (l: mset T): copy_mset n l = nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l. + Proof. + unfold copy_mset. destruct n; try reflexivity. + + simpl. induction l as [|[a l] IHl]; simpl; try congruence. destruct a. reflexivity. + Qed. + + + Lemma copy_mset_succ n (l: mset T): eval (sum i (copy_mset (Psucc n) l)) == @Bin.value _ _ (e_bin i) (eval (sum i l)) (eval (sum i (copy_mset n l))). + Proof. + rewrite 2 copy_mset'. + + induction l as [[a m]|[a m] l IHl]. + simpl eval. rewrite <- copy_plus; auto. rewrite Pmult_Sn_m. reflexivity. + + simpl nelist_map. rewrite ! eval_sum_cons. rewrite IHl. clear IHl. + rewrite Pmult_Sn_m. rewrite copy_plus; auto. rewrite <- !law_assoc. + apply Binvalue_Proper; try reflexivity. + rewrite law_comm . rewrite <- !law_assoc. apply proper; try reflexivity. + apply law_comm. + Qed. + + Lemma copy_mset_copy : forall n (m : mset T), eval (sum i (copy_mset n m)) == @copy _ (@Bin.value _ _ (e_bin i)) n (eval (sum i m)). + Proof. + induction n using Pind; intros. + + unfold copy_mset. rewrite copy_xH. reflexivity. + rewrite copy_mset_succ. rewrite copy_Psucc. rewrite IHn. reflexivity. + Qed. + + Instance compat_sum_unit_Unit : forall p, compat_sum_unit (left p) -> + @Unit X R (Bin.value (e_bin i)) (eval (unit p)). + Proof. + intros. + inversion H. subst. auto. + Qed. + + Lemma copy_n_unit : forall j n, is_unit j = true -> + eval (unit j) == @copy _ (Bin.value (e_bin i)) n (eval (unit j)). + Proof. + intros. + induction n using Prect. + rewrite copy_xH. reflexivity. + rewrite copy_Psucc. rewrite <- IHn. apply is_unit_sum_Unit in H. rewrite law_neutral_left. reflexivity. + Qed. - (** 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 z0 l r (H : compat_sum_unit r): + eval (sum i (run_msets (comp (merge_msets compare) l r))) == eval (sum i ((merge_msets compare) (l) (run_msets r))). + Proof. + unfold comp. unfold run_msets. + case_eq r; intros; subst. + rewrite eval_merge_bin; auto. + rewrite eval_sum_nil. + apply compat_sum_unit_Unit in H. rewrite law_neutral_right. reflexivity. + 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)). + Lemma z1 : forall n x, + eval (sum i (run_msets (return_sum i (is_unit) x n ))) + == @copy _ (@Bin.value _ _ (e_bin i)) n (eval x). + Proof. + intros. unfold return_sum. unfold run_msets. + case (is_sum_spec); intros; subst. + rewrite copy_mset_copy. + reflexivity. + + rewrite eval_sum_nil. apply copy_n_unit. auto. + reflexivity. + Qed. + Lemma z2 : forall u n x, compat_sum_unit x -> + eval (sum i ( run_msets + (add_to_sum i (is_unit) u n x))) + == + @Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval u)) (eval (sum i (run_msets x))). + Proof. + intros u n x Hix . + unfold add_to_sum. + case is_sum_spec; intros; subst. + + rewrite z0 by auto. rewrite eval_merge_bin. rewrite copy_mset_copy. reflexivity. + rewrite <- copy_n_unit by assumption. + apply is_unit_sum_Unit in H. + rewrite law_neutral_left. reflexivity. + + + rewrite z0 by auto. rewrite eval_merge_bin. reflexivity. + Qed. + End sum_correctness. + Lemma eval_norm_msets i norm + (Comm : Commutative R (Bin.value (e_bin i))) + (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (sum i (norm_msets norm i h)) == eval (sum i h). Proof. - intros i a [|b l]; simpl. - rewrite dot_neutral_right. reflexivity. - reflexivity. - Qed. + unfold norm_msets. + assert (H : + forall h : mset T, + eval (sum i (run_msets (norm_msets_ i (is_unit_of i) norm h))) == eval (sum i h) /\ compat_sum_unit (is_unit_of i) (norm_msets_ i (is_unit_of i) norm h)). + + induction h as [[a n] | [a n] h [IHh IHh']]; simpl norm_msets_; split. + rewrite z1 by auto. rewrite Hnorm . reflexivity. auto. + apply compat_sum_unit_return. + + rewrite z2 by auto. rewrite IHh. + rewrite eval_sum_cons. rewrite Hnorm. reflexivity. apply compat_sum_unit_add, IHh'. + + apply H. + Defined. + + (** auxiliary lemmas about products *) - 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. + Section prd_correctness. + Variable i : idx. + Variable is_unit : idx -> bool. + Hypothesis is_unit_prd_Unit : forall j, is_unit j = true-> @Unit X R (Bin.value (e_bin i)) (eval (unit j)). + + Inductive is_prd_spec_ind : T -> @discr (nelist T) -> Prop := + | is_prd_spec_op : + forall j l, j = i -> is_prd_spec_ind (prd j l) (Is_op l) + | is_prd_spec_unit : + forall j, is_unit j = true -> is_prd_spec_ind (unit j) (Is_unit j) + | is_prd_spec_nothing : + forall u, is_prd_spec_ind u (Is_nothing). + + Lemma is_prd_spec u : is_prd_spec_ind u (is_prd i is_unit u). + Proof. + unfold is_prd; case u; intros; try constructor. + case (eq_idx_spec); intros; subst; try constructor; auto. + case_eq (is_unit p); intros; try constructor; auto. + Qed. + + Lemma prd'_prd : forall (l: nelist T), eval (prd' i l) == eval (prd i l). + Proof. + intros [?|? [|? ?]]; simpl; reflexivity. + Qed. + + + Lemma eval_prd_nil x: eval (prd i (nil x)) == eval x. + Proof. + rewrite <- prd'_prd. simpl. reflexivity. + Qed. + Lemma eval_prd_cons a : forall (l: nelist T), eval (prd i (a::l)) == @Bin.value _ _ (e_bin i) (eval a) (eval (prd i l)). + Proof. + intros [|b l]; simpl; reflexivity. + Qed. + Lemma eval_prd_app : forall (h k: nelist T), eval (prd i (h++k)) == @Bin.value _ _ (e_bin i) (eval (prd i h)) (eval (prd i k)). + Proof. + induction h; intro k. simpl; try reflexivity. + simpl appne. rewrite 2 eval_prd_cons, IHh, law_assoc. reflexivity. + Qed. + + Inductive compat_prd_unit : @m idx (nelist T) -> Prop := + | cpu_left : forall x, is_unit x = true -> compat_prd_unit (left x) + | cpu_right : forall m, compat_prd_unit (right m) + . + + Lemma compat_prd_unit_return x: compat_prd_unit (return_prd i is_unit x). + Proof. + unfold return_prd. + case (is_prd_spec); intros; try constructor; auto. + Qed. + + Lemma compat_prd_unit_add : forall x h, + compat_prd_unit h + -> + compat_prd_unit + (add_to_prd i is_unit x + h). + Proof. + intros. + unfold add_to_prd. + unfold comp. + case (is_prd_spec); intros; try constructor; auto. + unfold comp; case h; try constructor. + unfold comp; case h; try constructor. + 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. + + Instance compat_prd_Unit : forall p, compat_prd_unit (left p) -> + @Unit X R (Bin.value (e_bin i)) (eval (unit p)). + Proof. + intros. + inversion H; subst. apply is_unit_prd_Unit. assumption. + Qed. - Lemma eval_prd_to_list: forall i a, eval (prd i (prd_to_list i a)) = eval a. + Lemma z0' : forall l (r: @m idx (nelist T)), compat_prd_unit r -> + eval (prd i (run_list (comp (@appne T) l r))) == eval (prd i ((appne (l) (run_list r)))). + Proof. + intros. + unfold comp. unfold run_list. case_eq r; intros; auto; subst. + rewrite eval_prd_app. + rewrite eval_prd_nil. + apply compat_prd_Unit in H. rewrite law_neutral_right. reflexivity. + reflexivity. + Qed. + + Lemma z1' a : eval (prd i (run_list (return_prd i is_unit a))) == eval (prd i (nil a)). + Proof. + intros. unfold return_prd. unfold run_list. + case (is_prd_spec); intros; subst; reflexivity. + Qed. + Lemma z2' : forall u x, compat_prd_unit x -> + eval (prd i ( run_list + (add_to_prd i is_unit u x))) == @Bin.value _ _ (e_bin i) (eval u) (eval (prd i (run_list x))). + Proof. + intros u x Hix. + unfold add_to_prd. + case (is_prd_spec); intros; subst. + rewrite z0' by auto. rewrite eval_prd_app. reflexivity. + apply is_unit_prd_Unit in H. rewrite law_neutral_left. reflexivity. + rewrite z0' by auto. rewrite eval_prd_app. reflexivity. + Qed. + + End prd_correctness. + + + + + Lemma eval_norm_lists i (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (prd i (norm_lists norm i h)) == eval (prd i h). Proof. - intros. unfold prd_to_list. - case_eq (is_prd i a). - intros k Hk. apply eval_is_prd. assumption. - reflexivity. - Qed. + unfold norm_lists. + assert (H : forall h : nelist T, + eval (prd i (run_list (norm_lists_ i (is_unit_of i) norm h))) == + eval (prd i h) + /\ compat_prd_unit (is_unit_of i) (norm_lists_ i (is_unit_of i) norm h)). + + + induction h as [a | a h [IHh IHh']]; simpl norm_lists_; split. + rewrite z1'. simpl. apply Hnorm. + + apply compat_prd_unit_return. + + rewrite z2'. rewrite IHh. rewrite eval_prd_cons. rewrite Hnorm. reflexivity. apply is_unit_of_Unit. + auto. + apply compat_prd_unit_add. auto. + apply H. + Defined. (** correctness of the normalisation function *) + Theorem eval_norm: forall u, eval (norm u) == eval u with eval_norm_aux: forall i (l: vT i) (f: Sym.type_of i), 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. + induction u as [ p m | p l | ? | ?]; simpl norm. + case_eq (is_commutative p); intros. + rewrite sum'_sum. + apply eval_norm_msets; auto. + 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. + rewrite prd'_prd. + apply eval_norm_lists; auto. - simpl. apply eval_norm_aux, Sym.morph. + apply eval_norm_aux, Sym.morph. + reflexivity. - induction l; simpl; intros f Hf. - reflexivity. - rewrite eval_norm. apply IHl, Hf. reflexivity. + 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. + + 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. @@ -685,5 +1106,30 @@ Section s. Lemma decide: forall (u v: T), compare (norm u) (norm v) = Eq -> eval u == eval v. Proof. intros u v H. apply normalise. apply compare_reflect_eq. apply H. Qed. + Lemma lift_normalise {S} {H : AAC_lift S R}: + forall (u v: T), (let x := norm u in let y := norm v in + S (eval x) (eval y)) -> S (eval u) (eval v). + Proof. destruct H. intros u v; simpl; rewrite 2 eval_norm. trivial. Qed. + End s. +End Internal. + + +(** * Lemmas for performing transitivity steps + given an instance of AAC_lift *) + +Section t. + Context `{AAC_lift}. + + Lemma lift_transitivity_left (y x z : X): E x y -> R y z -> R x z. + Proof. destruct H as [Hequiv Hproper]; intros G;rewrite G. trivial. Qed. + + Lemma lift_transitivity_right (y x z : X): E y z -> R x y -> R x z. + Proof. destruct H as [Hequiv Hproper]; intros G. rewrite G. trivial. Qed. + + Lemma lift_reflexivity {HR :Reflexive R}: forall x y, E x y -> R x y. + Proof. destruct H. intros ? ? G. rewrite G. reflexivity. Qed. + +End t. + Declare ML Module "aac_tactics". |