diff options
Diffstat (limited to 'AAC.v')
| -rw-r--r-- | AAC.v | 689 |
1 files changed, 689 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". |