Library AAC_tactics.AAC
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 normalise reified terms, then compare them. This allows us to close transitivity steps automatically, in the aac_rewrite tactic.
We restrict ourselves to the case where all symbols operate on a single fixed type. In particular, this means that we cannot handle situations like
H: forall x y, nat_of_pos (pos_of_nat (x) + y) + x = ....
where one occurrence of + operates on nat while the other one operates on positive.
Require Import Arith NArith.
Require Import List.
Require Import FMapPositive FMapFacts.
Require Import RelationClasses Equality.
Require Export Morphisms.
Local Open Scope signature_scope.
Section sigma.
Definition sigma := PositiveMap.t.
Definition sigma_get A (null : A) (map : sigma A) (n : positive) : A :=
match PositiveMap.find n map with
| None => null
| Some x => x
end.
Definition sigma_add := @PositiveMap.add.
Definition sigma_empty := @PositiveMap.empty.
End sigma.
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
}.
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
Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E}
{HR: @Transitive X R} {HER: subrelation E R}: AAC_lift R E | 3.
Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E}
{HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4.
Module Internal.
Section copy.
Context {X} {R} {HR: @Equivalence X R} {plus}
(op: Associative R plus) (op': Commutative R plus) (po: Proper (R ==> R ==> R) plus).
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)).
Lemma copy_xH : forall x, R (copy 1 x) x.
Lemma copy_Psucc : forall n x, R (copy (Psucc n) x) (plus x (copy n x)).
Global Instance copy_compat n: Proper (R ==> R) (copy n).
End copy.
Utilities for positive numbers
which we use as:- indices for morphisms and symbols
- multiplicity of terms in sums
Local 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.
Local 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).
| 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).
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).
Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j.
| 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).
Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j.
Local 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.
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.
Lemma reflect_eqdep_eq: reflect_eqdep ->
forall A u v, @f A A u v = Eq -> u = v.
Lemma reflect_eqdep_weak_spec: reflect_eqdep ->
forall A u v, compare_weak_spec u v (@f A A u v).
End dep.
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
lexicographic composition of comparisons (this is a notation to keep it lazy)
comparison functions
Section c.
Variables A B: Type.
Variable compare: A -> B -> comparison.
Fixpoint list_compare h k :=
match h,k with
| nil x, nil y => compare x y
| nil x, _ => Lt
| _, nil x => Gt
| u::h, v::k => lex (compare u v) (list_compare h k)
end.
End 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).
Lemma list_compare_weak_spec: forall h k,
compare_weak_spec h k (list_compare compare h k).
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).
Lemma mset_compare_weak_spec: forall h k,
compare_weak_spec h k (mset_compare compare h k).
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 (h1,n1) => fun l2 => insert n1 h1 l2
| (h1,n1)::t1 =>
let fix merge_aux l2 :=
match l2 with
| 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
| 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.
Fixpoint fold_map l :=
match l with
| nil x => map x
| u::l => b2 (map u) (fold_map l)
end.
mapping and merging
Variable merge: A -> nelist B -> nelist B.
Fixpoint merge_map (l: nelist A): nelist B :=
match l with
| nil x => nil (map x)
| u::l => merge u (merge_map l)
end.
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.
type of an arity
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.
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
helper to build default values, when filling reification environments
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.
End Bin.
Section s.
Context {X} {R: relation X} {E: @Equivalence X R}.
Infix "==" := R (at level 80).
Variable e_sym: idx -> @Sym.pack X R.
Variable e_bin: idx -> @Bin.pack X R.
packaging units (depends on e_bin)
Record unit_of u := mk_unit_for {
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:- 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
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 -> 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).
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)
| 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
| vnil, vnil => Eq
| vnil, _ => Lt
| _, vnil => Gt
| vcons _ u us, vcons _ v vs => lex (compare u v) (vcompare us vs)
end.
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)
| 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
| vnil, vnil => Eq
| vnil, _ => Lt
| _, vnil => Gt
| vcons _ u us, vcons _ v vs => lex (compare u v) (vcompare us vs)
end.
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.
Instance eval_aux_compat i (l: vT i): Proper (@Sym.rel_of X R i ==> R) (eval_aux l).
Definition is_unit_of j i :=
List.existsb (fun p => eq_idx_bool j (uf_idx p)) (u_desc (e_unit i)).
Definition is_commutative i :=
match Bin.comm (e_bin i) with Some _ => true | None => false end.
with vcompare_reflect_eqdep: forall i us j vs (H: i=j), vcompare us vs = Eq -> cast vT H us = vs.
Instance eval_aux_compat i (l: vT i): Proper (@Sym.rel_of X R i ==> R) (eval_aux l).
Definition is_unit_of j i :=
List.existsb (fun p => eq_idx_bool j (uf_idx p)) (u_desc (e_unit i)).
Definition is_commutative i :=
match Bin.comm (e_bin i) with Some _ => true | None => false end.
Inductive discr {A} : Type :=
| Is_op : A -> discr
| Is_unit : idx -> discr
| Is_nothing : discr .
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.
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 Is_op l else Is_nothing
| unit j => if is_unit j then Is_unit j else Is_nothing
| u => Is_nothing
end.
Definition copy_mset n (l: mset T): mset T :=
match n with
| 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 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
| nil u => u
| _ => prd i u
end.
Definition is_prd (u: T) : @discr (nelist T) :=
match u with
| prd j l => if eq_idx_bool j i then Is_op l else Is_nothing
| unit j => if is_unit j then Is_unit j else Is_nothing
| 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.
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 => 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
| vnil => vnil
| vcons _ u l => vcons (norm u) (vnorm l)
end.
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)).
Instance Binvalue_Commutative i (H : is_commutative i = true) : Commutative R (@Bin.value _ _ (e_bin i) ).
Instance Binvalue_Associative i :Associative R (@Bin.value _ _ (e_bin i) ).
Instance Binvalue_Proper i : Proper (R ==> R ==> R) (@Bin.value _ _ (e_bin i) ).
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 is_sum_spec u : is_sum_spec_ind u (is_sum i is_unit u).
Instance assoc : @Associative X R (Bin.value (e_bin i)).
Instance proper : Proper (R ==> R ==> R)(Bin.value (e_bin i)).
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) .
Lemma eval_sum_nil x:
eval (sum i (nil (x,xH))) == (eval x).
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))).
Inductive compat_sum_unit : @m idx (mset T) -> Prop :=
| csu_left : forall x, is_unit x = true-> compat_sum_unit (left x)
| csu_right : forall m, compat_sum_unit (right m)
.
Lemma compat_sum_unit_return x n : compat_sum_unit (return_sum i is_unit x n).
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).
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)).
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.
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))).
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)).
Instance compat_sum_unit_Unit : forall p, compat_sum_unit (left p) ->
@Unit X R (Bin.value (e_bin i)) (eval (unit p)).
Lemma copy_n_unit : forall j n, is_unit j = true ->
eval (unit j) == @copy _ (Bin.value (e_bin i)) n (eval (unit j)).
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))).
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).
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))).
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).
auxiliary lemmas about products
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).
Lemma prd'_prd : forall (l: nelist T), eval (prd' i l) == eval (prd i l).
Lemma eval_prd_nil x: eval (prd i (nil x)) == eval x.
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)).
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)).
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).
Lemma compat_prd_unit_add : forall x h,
compat_prd_unit h
->
compat_prd_unit
(add_to_prd i is_unit x
h).
Instance compat_prd_Unit : forall p, compat_prd_unit (left p) ->
@Unit X R (Bin.value (e_bin i)) (eval (unit p)).
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)))).
Lemma z1' a : eval (prd i (run_list (return_prd i is_unit a))) == eval (prd i (nil a)).
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))).
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).
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.
corollaries, for goal normalisation or decision
Lemma normalise : forall (u v: T), eval (norm u) == eval (norm v) -> eval u == eval v.
Lemma compare_reflect_eq: forall u v, compare u v = Eq -> eval u == eval v.
Lemma decide: forall (u v: T), compare (norm u) (norm v) = Eq -> eval u == eval v.
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).
End s.
End Internal.