Require Import 
  HoTT.Classes.interfaces.abstract_algebra.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Class AlmostNegate A := almost_negate : A -> A.

Class AlmostRing A {Aplus : Plus A} {Amult : Mult A}
  {Azero : Zero A} {Aone : One A} {Anegate : AlmostNegate A} :=
  { almost_ring_semiring : IsSemiCRing A
  ; almost_ring_neg_pr : forall x : A, almost_negate x = (almost_negate 1) * x }.

Section almostring_mor.
Context {A B : Type} {Aplus : Plus A} {Bplus : Plus B}
  {Amult : Mult A} {Bmult : Mult B} {Azero : Zero A} {Bzero : Zero B}
  {Aone : One A} {Bone : One B} {Aneg : AlmostNegate A} {Bneg : AlmostNegate B}.

Class AlmostRingPreserving (f : A -> B) :=
  { almostring_mor_sr_mor : IsSemiRingPreserving f
  ; almostring_mor_neg : forall x, f (almost_negate x) = almost_negate (f x) }.
End almostring_mor.

Module Quoting.

Inductive Expr (V:Type0) : Type0 :=
  | Var (v : V)
  | Zero
  | One
  | Plus (a b : Expr V)
  | Mult (a b : Expr V)
  | Neg (a : Expr V)
.

Arguments Var {V} v.
Arguments Zero {V}.
Arguments One {V}.
Arguments Plus {V} a b.
Arguments Mult {V} a b.
Arguments Neg {V} a.

Section contents.
Universe U.
Context (R:Type@{U}) `{AlmostRing R}.

Notation Vars V := (V -> R).

Fixpoint eval {V:Type0} (vs : Vars V) (e : Expr V) : R :=
  match e with
  | Var v => vs v
  | Zero => 0
  | One => 1
  | Plus a b => eval vs a + eval vs b
  | Mult a b => eval vs a * eval vs b
  | Neg a => almost_negate (eval vs a)
  end.

Lemma eval_ext {V:Type0} (vs vs' : Vars V) :
  pointwise_paths@{Set U} vs vs' ->
  pointwise_paths@{Set U} (eval vs) (eval vs').
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
vs, vs': Vars V
vs == vs' -> eval vs == eval vs'
Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
vs, vs': Vars V
vs == vs' -> eval vs == eval vs'
intros E e;induction e;simpl;auto;apply ap011;auto.
Qed.

Definition noVars : Vars Empty.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
Vars Empty
Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
Vars Empty intros []. Defined.

Definition singleton x : Vars Unit := fun _ => x.

Definition merge {A B:Type0 } (va:Vars A) (vb:Vars B) : Vars (sum@{Set Set} A B)
  := fun i => match i with inl i => va i | inr i => vb i end.

Section Lookup.

  Class Lookup {A:Type0 } (x: R) (f: Vars A)
    := { lookup: A; lookup_correct: f lookup = x }.

  Global Arguments lookup {A} x f {_}.

  Context (x:R) {A B:Type0 } (va : Vars A) (vb : Vars B).

  Local Instance lookup_l `{!Lookup x va} : Lookup x (merge va vb).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup0: Lookup x va
Lookup x (merge va vb)
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup0: Lookup x va
Lookup x (merge va vb)
  exists (inl (lookup x va)).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup0: Lookup x va
merge va vb (inl (lookup x va)) = x exact lookup_correct.
  Defined.

  Local Instance lookup_r `{!Lookup x vb} : Lookup x (merge va vb).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup0: Lookup x vb
Lookup x (merge va vb)
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup0: Lookup x vb
Lookup x (merge va vb)
  exists (inr (lookup x vb)).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup0: Lookup x vb
merge va vb (inr (lookup x vb)) = x exact lookup_correct.
  Defined.

  Local Instance lookup_single : Lookup x (singleton x).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup x (singleton x)
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
Lookup x (singleton x)
  exists tt.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
x: R
A, B: Type0
va: Vars A
vb: Vars B
singleton x tt = x reflexivity.
  Defined.

End Lookup.

Fixpoint expr_map {V W:Type0 } (f : V -> W) (e : Expr V) : Expr W :=
  match e with
  | Var v => Var (f v)
  | Zero => Zero
  | One => One
  | Plus a b => Plus (expr_map f a) (expr_map f b)
  | Mult a b => Mult (expr_map f a) (expr_map f b)
  | Neg a => Neg (expr_map f a)
  end.

Lemma eval_map {V W:Type0 } (f : V -> W) v e
  : eval v (expr_map f e) = eval (Compose@{Set Set U} v f) e.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V, W: Type0
f: V -> W
v: Vars W
e: Expr V
eval v (expr_map f e) = eval (v ∘ f) e
Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V, W: Type0
f: V -> W
v: Vars W
e: Expr V
eval v (expr_map f e) = eval (v ∘ f) e
induction e;simpl;try reflexivity;apply ap011;auto.
Qed.

Section Quote.

  Class Quote {V:Type0 } (l: Vars V) (n: R) {V':Type0 } (r: Vars V') :=
    { quote : Expr (V |_| V')
    ; eval_quote : @eval (V |_| V') (merge l r) quote = n }.

  Global Arguments quote {V l} n {V' r _}.
  Global Arguments eval_quote {V l} n {V' r _}.

  Definition sum_assoc {A B C}: (A |_| B) |_| C -> A |_| (B |_| C).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
A, B, C: Type
A + B + C -> A + (B + C)
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
A, B, C: Type
A + B + C -> A + (B + C)
  intros [[?|?]|?];auto.
  Defined.

  Definition sum_aux {A B C}: (A |_| B) -> A |_| (B |_| C).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
A, B, C: Type
A + B -> A + (B + C)
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
A, B, C: Type
A + B -> A + (B + C)
  intros [?|?];auto.
  Defined.

  Local Instance quote_zero (V:Type0) (v: Vars V): Quote v 0 noVars.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
Quote v 0 noVars
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
Quote v 0 noVars
  exists Zero.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
eval (merge v noVars) Zero = 0
  reflexivity.
  Defined.

  Local Instance quote_one (V:Type0) (v: Vars V): Quote v 1 noVars.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
Quote v 1 noVars
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
Quote v 1 noVars
  exists One.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
eval (merge v noVars) One = 1
  reflexivity.
  Defined.

  Lemma quote_plus_ok (V:Type0) (v: Vars V) n
    (V':Type0) (v': Vars V') m (V'':Type0) (v'': Vars V'')
    `{!Quote v n v'} `{!Quote (merge v v') m v''}
    : eval (merge v (merge v' v''))
      (Plus (expr_map sum_aux (quote n)) (expr_map sum_assoc (quote m))) = 
      n + m.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (Plus (expr_map sum_aux (quote n))
     (expr_map sum_assoc (quote m))) = n + m
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (Plus (expr_map sum_aux (quote n))
     (expr_map sum_assoc (quote m))) = n + m
  simpl.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) +
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m)) = n + m
  rewrite <-(eval_quote n), <-(eval_quote m),
    2!eval_map.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v'') ∘ sum_aux) (quote n) +
eval (merge v (merge v' v'') ∘ sum_assoc) (quote m) =
eval (merge v v') (quote n) +
eval (merge (merge v v') v'') (quote m)
  apply ap011;apply eval_ext.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_aux == merge v v'
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_assoc ==
merge (merge v v') v''
  -
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_aux == merge v v' intros [?|?];reflexivity.
  -
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_assoc ==
merge (merge v v') v'' intros [[?|?]|?];reflexivity.
  Qed.

  Local Instance quote_plus (V:Type0) (v: Vars V) n
  (V':Type0) (v': Vars V') m (V'':Type0) (v'': Vars V'')
  `{!Quote v n v'} `{!Quote (merge v v') m v''}: Quote v (n + m) (merge v' v'').
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
Quote v (n + m) (merge v' v'')
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
Quote v (n + m) (merge v' v'')
  econstructor.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v'')) ?quote = n + m apply quote_plus_ok.
  Defined.

  Lemma quote_mult_ok (V:Type0) (v: Vars V) n
    (V':Type0) (v': Vars V') m (V'':Type0) (v'': Vars V'')
    `{!Quote v n v'} `{!Quote (merge v v') m v''}
    : eval (merge v (merge v' v''))
      (Mult (expr_map sum_aux (quote n)) (expr_map sum_assoc (quote m))) = 
      n * m.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (Mult (expr_map sum_aux (quote n))
     (expr_map sum_assoc (quote m))) = n * m
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (Mult (expr_map sum_aux (quote n))
     (expr_map sum_assoc (quote m))) = n * m
  simpl.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) *
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m)) = n * m
  rewrite <-(eval_quote n), <-(eval_quote m),
    2!eval_map.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v'') ∘ sum_aux) (quote n) *
eval (merge v (merge v' v'') ∘ sum_assoc) (quote m) =
eval (merge v v') (quote n) *
eval (merge (merge v v') v'') (quote m)
  apply ap011;apply eval_ext.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_aux == merge v v'
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_assoc ==
merge (merge v v') v''
  -
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_aux == merge v v' intros [?|?];reflexivity.
  -
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
merge v (merge v' v'') ∘ sum_assoc ==
merge (merge v v') v'' intros [[?|?]|?];reflexivity.
  Qed.

  Local Instance quote_mult (V:Type0) (v: Vars V) n
    (V':Type0) (v': Vars V') m (V'':Type0) (v'': Vars V'')
    `{!Quote v n v'} `{!Quote (merge v v') m v''}
    : Quote v (n * m) (merge v' v'').
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
Quote v (n * m) (merge v' v'')
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
Quote v (n * m) (merge v' v'')
  econstructor.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v'')) ?quote = n * m apply quote_mult_ok.
  Defined.

  Lemma quote_neg_ok@{} (V:Type0) (v : Vars V) n (V':Type0) (v' : Vars V')
    `{!Quote v n v'}
    : eval (merge v v') (Neg (quote n)) = almost_negate n.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
Quote0: Quote v n v'
eval (merge v v') (Neg (quote n)) = almost_negate n
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
Quote0: Quote v n v'
eval (merge v v') (Neg (quote n)) = almost_negate n
  simpl.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
Quote0: Quote v n v'
almost_negate (eval (merge v v') (quote n)) =
almost_negate n apply ap,eval_quote.
  Qed.

  Local Instance quote_neg (V:Type0) (v : Vars V) n (V':Type0) (v' : Vars V')
    `{!Quote v n v'}
    : Quote v (almost_negate n) v'.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
Quote0: Quote v n v'
Quote v (almost_negate n) v'
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
Quote0: Quote v n v'
Quote v (almost_negate n) v'
  exists (Neg (quote n)).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
Quote0: Quote v n v'
eval (merge v v') (Neg (quote n)) = almost_negate n
  apply quote_neg_ok.
  Defined.

  Local Instance quote_old_var (V:Type0) (v: Vars V) x {i: Lookup x v}
    : Quote v x noVars | 8.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
x: R
i: Lookup x v
Quote v x noVars
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
x: R
i: Lookup x v
Quote v x noVars
  exists (Var (inl (lookup x v))).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
x: R
i: Lookup x v
eval (merge v noVars) (Var (inl (lookup x v))) = x
  exact lookup_correct.
  Defined.

  Local Instance quote_new_var (V:Type0) (v: Vars V) x
    : Quote v x (singleton x) | 9.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
x: R
Quote v x (singleton x)
  Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
x: R
Quote v x (singleton x)
  exists (Var (inr tt)).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
x: R
eval (merge v (singleton x)) (Var (inr tt)) = x
  reflexivity.
  Defined.

End Quote.

Definition quote': forall x {V':Type0 } {v: Vars V'} {d: Quote noVars x v}, Expr _
  := @quote _ _.

Definition eval_quote': forall x {V':Type0} {v: Vars V'} {d: Quote noVars x v},
  eval (merge noVars v) (quote x) = x
  := @eval_quote _ _.

Class EqQuote {V:Type0 } (l: Vars V) (n m: R) {V':Type0 } (r: Vars V') :=
    { eqquote_l : Expr V
    ; eqquote_r : Expr (V |_| V')
    ; eval_eqquote : eval (merge l r) (expr_map inl eqquote_l)
                   = eval (merge l r) eqquote_r -> n = m }.

Lemma eq_quote_ok (V:Type0) (v: Vars V) n
  (V':Type0) (v': Vars V') m (V'':Type0) (v'': Vars V'')
  `{!Quote v n v'} `{!Quote (merge v v') m v''}
  : eval (merge v (merge v' v'')) (expr_map sum_aux (quote n))
  = eval (merge v (merge v' v'')) (expr_map sum_assoc (quote m))
  -> n = m.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m)) -> n = m
Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m)) -> n = m
intros E.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
n = m
rewrite <-(eval_quote n), <-(eval_quote m).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
eval (merge v v') (quote n) =
eval (merge (merge v v') v'') (quote m)
path_via (eval (merge v (merge v' v'')) (expr_map sum_aux (quote n)));
[|path_via (eval (merge v (merge v' v'')) (expr_map sum_assoc (quote m)))].
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
eval (merge v v') (quote n) =
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n))
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m)) =
eval (merge (merge v v') v'') (quote m)
-
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
eval (merge v v') (quote n) =
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) rewrite eval_map.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
eval (merge v v') (quote n) =
eval (merge v (merge v' v'') ∘ sum_aux) (quote n) apply eval_ext.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
merge v v' == merge v (merge v' v'') ∘ sum_aux
  intros [?|?];reflexivity.
-
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m)) =
eval (merge (merge v v') v'') (quote m) rewrite eval_map.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
eval (merge v (merge v' v'') ∘ sum_assoc) (quote m) =
eval (merge (merge v v') v'') (quote m) apply eval_ext.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
merge v (merge v' v'') ∘ sum_assoc ==
merge (merge v v') v''
  intros [[?|?]|?];reflexivity.
Qed.

Local Instance eq_quote (V:Type0) (v: Vars V) n
  (V':Type0) (v': Vars V') m (V'':Type0) (v'': Vars V'')
  `{!Quote v n v'} `{!Quote (merge v v') m v''}
  : EqQuote (merge v v') n m v''.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
EqQuote (merge v v') n m v''
Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
EqQuote (merge v v') n m v''
econstructor.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) =
eval (merge (merge v v') v'') ?eqquote_r -> n = m
intros E.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) =
eval (merge (merge v v') v'') ?eqquote_r
n = m
apply (@eq_quote_ok _ _ _ _ _ _ _ _ Quote0 Quote1).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) =
eval (merge (merge v v') v'') ?eqquote_r
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
etransitivity;[etransitivity;[|exact E]|].
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) =
eval (merge (merge v v') v'') ?eqquote_r
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l)
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) =
eval (merge (merge v v') v'') ?eqquote_r
eval (merge (merge v v') v'') ?eqquote_r =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m))
-
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) =
eval (merge (merge v v') v'') ?eqquote_r
eval (merge v (merge v' v''))
  (expr_map sum_aux (quote n)) =
eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) rewrite 2!eval_map.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl ?eqquote_l) =
eval (merge (merge v v') v'') ?eqquote_r
eval (merge v (merge v' v'') ∘ sum_aux) (quote n) =
eval (merge (merge v v') v'' ∘ inl) ?eqquote_l apply eval_ext.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl (quote n)) =
eval (merge (merge v v') v'') ?eqquote_r
merge v (merge v' v'') ∘ sum_aux ==
merge (merge v v') v'' ∘ inl intros [?|?];reflexivity.
-
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl (quote n)) =
eval (merge (merge v v') v'') ?eqquote_r
eval (merge (merge v v') v'') ?eqquote_r =
eval (merge v (merge v' v''))
  (expr_map sum_assoc (quote m)) rewrite (eval_map sum_assoc).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl (quote n)) =
eval (merge (merge v v') v'') ?eqquote_r
eval (merge (merge v v') v'') ?eqquote_r =
eval (merge v (merge v' v'') ∘ sum_assoc) (quote m)
  apply eval_ext.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
n: R
V': Type0
v': Vars V'
m: R
V'': Type0
v'': Vars V''
Quote0: Quote v n v'
Quote1: Quote (merge v v') m v''
E: eval (merge (merge v v') v'')
  (expr_map inl (quote n)) =
eval (merge (merge v v') v'') (quote m)
merge (merge v v') v'' ==
merge v (merge v' v'') ∘ sum_assoc intros [[?|?]|?];reflexivity.
Defined.

Definition sum_forget {A B} : Empty |_| A -> A |_| B.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
A, B: Type
Empty + A -> A + B
Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
A, B: Type
Empty + A -> A + B
intros [[]|?];auto.
Defined.

Lemma quote_equality {V:Type0} {v: Vars V}
  {V':Type0} {v': Vars V'} (l r: R)
  `{!Quote noVars l v} `{!Quote v r v'}
  : let heap := (merge v v') in
  eval heap (expr_map sum_forget (quote l)) = eval heap (quote r) -> l = r.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
let heap := merge v v' in
eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r) -> l = r
Proof.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
let heap := merge v v' in
eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r) -> l = r
intros ? E.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
heap:= merge v v': Vars (V + V')
E: eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r)
l = r
rewrite <-(eval_quote l),<-(eval_quote r).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
heap:= merge v v': Vars (V + V')
E: eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r)
eval (merge noVars v) (quote l) =
eval (merge v v') (quote r)
path_via (eval heap (expr_map sum_forget (quote l))).
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
heap:= merge v v': Vars (V + V')
E: eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r)
eval (merge noVars v) (quote l) =
eval heap (expr_map sum_forget (quote l))
rewrite eval_map.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
heap:= merge v v': Vars (V + V')
E: eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r)
eval (merge noVars v) (quote l) =
eval (heap ∘ sum_forget) (quote l) apply eval_ext.
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
heap:= merge v v': Vars (V + V')
E: eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r)
merge noVars v == heap ∘ sum_forget
intros [[]|?].
R: Type
Aplus: canonical_names.Plus R
Amult: canonical_names.Mult R
Azero: canonical_names.Zero R
Aone: canonical_names.One R
Anegate: AlmostNegate R
H: AlmostRing R
V: Type0
v: Vars V
V': Type0
v': Vars V'
l, r: R
Quote0: Quote noVars l v
Quote1: Quote v r v'
heap:= merge v v': Vars (V + V')
E: eval heap (expr_map sum_forget (quote l)) =
eval heap (quote r)
v0: V
merge noVars v (inr v0) = (heap ∘ sum_forget) (inr v0) reflexivity.
Qed.

End contents.

Module Export Instances.
  Existing Instances lookup_l lookup_r lookup_single quote_zero quote_one quote_plus quote_mult quote_neg eq_quote.
  Existing Instance quote_old_var | 8.
  Existing Instance quote_new_var | 9.
End Instances.

End Quoting.