theory.quote_monoid

Require Import abstract_algebra.
Require universal_algebra.

Module ua := universal_algebra.

Require varieties.monoids.
Require monoid_normalization.

Notation msig := varieties.monoids.sig.
Notation Op := (ua.Op msig False).
Notation App := (ua.App msig False _ _).
Notation Term V := (ua.Term0 msig V tt).

Section contents.

  Context `{Monoid M}.

  Definition Vars V := V M.

  Definition novars: Vars False := False_rect _.
  Definition singlevar (x: M): Vars unit := fun _ => x.
  Definition merge {A B} (a: Vars A) (b: Vars B): Vars (A+B) :=
    fun i => match i with inl j => a j | inr j => b j end.

  Section Lookup.

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

    Global Implicit Arguments lookup [[A] [Lookup]].

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

    Global Instance lookup_left `{!Lookup x va}: Lookup x (merge va vb)
      := { lookup := inl (lookup x va) }.

    Global Instance lookup_right `{!Lookup x vb}: Lookup x (merge va vb)
      := { lookup := inr (lookup x vb) }.

    Global Program Instance: Lookup x (singlevar x) := { lookup := tt }.

  End Lookup.

  Instance: MonoidUnit (Term V) := λ V, ua.Op msig _ monoids.one.
  Instance: SemiGroupOp (Term V) :=
    λ V x, ua.App msig _ _ _ (ua.App msig _ _ _ (ua.Op msig _ monoids.mult) x).

  Notation eval V vs := (ua.eval _ (λ _, (vs: Vars V))).

  Section Quote.

    Class Quote {V} (l: Vars V) (n: M) {V'} (r: Vars V') :=
      { quote: Term (V + V')
      ; eval_quote: @eval (V+V') (merge l r) quote n }.

    Implicit Arguments quote [[V] [l] [V'] [r] [Quote]].

    Global Program Instance quote_zero V (v: Vars V): Quote v mon_unit novars := { quote := mon_unit }.

    Global Program Instance quote_mult V (v: Vars V) n V' (v': Vars V') m V'' (v'': Vars V'')
      `{!Quote v n v'} `{!Quote (merge v v') m v''}: Quote v (n & m) (merge v' v'') :=
        { quote := ua.map_var msig (obvious: (V+V')→(V+(V'+V''))) (quote n) & ua.map_var msig (obvious:((V+V')+V'')→(V+(V'+V''))) (quote m) }.


    Global Program Instance quote_old_var V (v: Vars V) x {i: Lookup x v}:
      Quote v x novars | 8 := { quote := ua.Var msig _ (inl (lookup x v)) tt }.

    Global Program Instance quote_new_var V (v: Vars V) x: Quote v x (singlevar x) | 9
      := { quote := ua.Var msig _ (inr tt) tt }.

  End Quote.

  Definition quote': x {V'} {v: Vars V'} {d: Quote novars x v}, Term _ := @quote _ _.

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

  Implicit Arguments quote' [[V'] [v] [d]].
  Implicit Arguments eval_quote' [[V'] [v] [d]].

  Lemma quote_equality `{v: Vars V} `{v': Vars V'} (l r: M) `{!Quote novars l v} `{!Quote v r v'}:
    let heap := (merge v v') in
    eval _ heap (ua.map_var msig (obvious: False + V V + V') quote) = eval _ heap quote l = r.

  Lemma equal_by_normal `{v: Vars V} `{v': Vars V'} (l r: M) `{!Quote novars l v} `{!Quote v r v'}:
   ` (monoid_normalization.simplify _ (ua.map_var msig (obvious: False + V V + V') quote))
   ` (monoid_normalization.simplify _ quote) l = r.

  Ltac monoid := apply (equal_by_normal _ _); vm_compute; reflexivity.

  Example ex x y z: x & (y & z) & mon_unit = mon_unit & (x & y) & z.

End contents.