quote.classquote

Require Import Morphisms Program Unicode.Utf8.


Module simple.


  Inductive Expr := Plus (a b: Expr) | Mult (a b: Expr) | Zero | One.

  Fixpoint eval (e: Expr): nat :=
    match e with
    | Plus a b => eval a + eval b
    | Mult a b => eval a * eval b
    | Zero => 0
    | One => 1
    end.


  Module approach_A.

    Class Quote (n: nat) := quote: Expr.

    Implicit Arguments quote [[Quote]].

    Section instances.

      Context n m `{Quote n} `{Quote m}.

      Global Instance: Quote 0 := Zero.
      Global Instance: Quote 1 := One.
      Global Instance: Quote (n + m) := Plus (quote n) (quote m).
      Global Instance: Quote (n * m) := Mult (quote n) (quote m).

    End instances.

    Ltac do_quote :=
      match goal with
      |- (?a = ?b) => change (eval (quote a) = eval (quote b))
      end.

    Lemma example: (1 + 0 + 1) * (1 + 1) = (1 + 1) + (1 + 1).

  End approach_A.


  Module approach_B.

    Class Quote (n: nat) := { quote: Expr; eval_quote: n = eval quote }.

    Implicit Arguments quote [[Quote]].
    Implicit Arguments eval_quote [[Quote]].

    Section instances.

      Context n m `{Quote n} `{Quote m}.

      Global Program Instance: Quote 0 := { quote := Zero }.
      Global Program Instance: Quote 1 := { quote := One }.

      Global Instance: Quote (n + m) := { quote := Plus (quote n) (quote m) }.

      Global Instance: Quote (n * m) := { quote := Mult (quote n) (quote m) }.

    End instances.

    Lemma do_quote {n m} `{Quote n} `{Quote m}: eval (quote n) = eval (quote m) n = m.

    Lemma example: (1 + 0 + 1) * (1 + 1) = (1 + 1) + (1 + 1).

  End approach_B.

End simple.


Module with_vars.


Lemma sum_assoc {A B C}: (A+B)+C A+(B+C).
Lemma bla {A B C}: (A+B) A+(B+C).
Lemma monkey {A B}: False + A A + B.

Section obvious.

  Class Obvious (T: Type) := obvious: T.

  Context (A B C: Type).

  Global Instance: Obvious (A A) := id.
  Global Instance: Obvious (False A) := False_rect _.
  Global Instance: Obvious (A A + B) := inl.
  Global Instance: Obvious (A B + A) := inr.
  Global Instance obvious_sum_src `{Obvious (A C)} `{Obvious (B C)}: Obvious (A+B C).
  Global Instance obvious_sum_dst_l `{Obvious (A B)}: Obvious (A B+C).
  Global Instance obvious_sum_dst_r `{Obvious (A B)}: Obvious (A C+B).

End obvious.


Inductive Expr (V: Type) := Mult (a b: Expr V) | Zero | Var (v: V).

Implicit Arguments Var [[V]].
Implicit Arguments Zero [[V]].
Implicit Arguments Mult [[V]].




Definition Value := nat.
Definition Vars V := V Value.

Fixpoint eval {V} (vs: Vars V) (e: Expr V): Value :=
  match e with
  | Zero => 0
  | Mult a b => eval vs a * eval vs b
  | Var v => vs v
  end.

Instance eval_proper V: Proper (pointwise_relation _ eq ==> eq ==> eq) (@eval V).


Definition novars: Vars False := False_rect _.
Definition singlevar (x: Value): 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: Value) (f: Vars A) := { lookup: A; lookup_correct: f lookup = x }.

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

  Context (x: Value) {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.


Definition map_var {V W: Type} (f: V W): Expr V Expr W :=
  fix F (e: Expr V): Expr W :=
    match e with
    | Mult a b => Mult (F a) (F b)
    | Zero => Zero
    | Var v => Var (f v)
    end.


Lemma eval_map_var {V W} (f: V W) v e:
  eval v (map_var f e) = eval (v f) e.


Section Quote.


  Class Quote {V} (l: Vars V) (n: Value) {V'} (r: Vars V') :=
    { quote: Expr (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 0 novars := { quote := Zero }.


  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 := Mult (map_var bla (quote n)) (map_var sum_assoc (quote m)) }.



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


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

End Quote.



Definition quote': x {V'} {v: Vars V'} {d: Quote novars x v}, Expr _ := @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]].


Goal x y (P: Value Prop), P ((x * y) * (x * 0)).


Section inspect.
  Variables x y: Value.
  Eval compute in quote' ((x * y) * (x * 0)).




End inspect.


Lemma quote_equality {V} {v: Vars V} {V'} {v': Vars V'} (l r: Value) `{!Quote novars l v} `{!Quote v r v'}:
  let heap := (merge v v') in
  eval heap (map_var monkey quote) = eval heap quote l = r.

Goal x y, x * y = y * x.

End with_vars.