attempt at PHOAS canonical structures reification

cs_reif.v

Require Import Coq.ZArith.ZArith.
Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'nlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'nlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'zlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'zlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
         (at level 200, f at level 200, format "'elet'  x  :=  v  'in' '//' f").
Reserved Notation "'olet' x := v 'in' f"
         (at level 200, f at level 200, format "'olet'  x  :=  v  'in' '//' f").
Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
  := let x := v in f x.
(*Axiom Let_In : forall {A P} (v : A) (f : forall x : A, P x), P v.*)
(*Axiom plus : Z -> Z -> Z.
Infix "+" := plus : Z_scope.*)
Local Open Scope Z_scope.
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).
Definition Let_In_nat : nat -> (nat -> nat) -> nat
  := (@Let_In nat (fun _ => nat)).
Definition Let_In_Z : Z -> (Z -> Z) -> Z
  := (@Let_In Z (fun _ => Z)).
Notation "'nlet' x .. y := v 'in' f"
  := (Let_In_nat v (fun x => .. (fun y => f) .. )).
Notation "'zlet' x .. y := v 'in' f"
  := (Let_In_Z v (fun x => .. (fun y => f) .. )).

Module Import PHOAS.
  Inductive expr {var : Type} : Type :=
  | LetIn (v : expr) (f : var -> expr)
  | Var (v : var)
  | Const (v : Z)
  | Add (x y : expr).
  Bind Scope expr_scope with expr.
  Delimit Scope expr_scope with expr.
  Infix "+" := Add : expr_scope.
  Notation "'elet' x := v 'in' f" := (LetIn v (fun x => f%expr)) : expr_scope.
  Notation "' x" := (Const x) (at level 9, format "' x") : expr_scope.
  Notation "$$ x" := (Var x) (at level 9, format "$$ x") : expr_scope.
  Fixpoint denote (e : @expr Z) : Z
    := match e with
       | LetIn v f => dlet x := denote v in denote (f x)
       | Var v => v
       | Const x => x
       | Add x y => denote x + denote y
     end.

  Definition Expr := forall var, @expr var.
  Definition Denote (e : Expr) := denote (e _).
End PHOAS.

Module HOAS.
  Inductive expr : Type :=
  | LetIn (v : expr) (f : Z -> expr)
  | Const (v : Z)
  | Add (x y : expr).

  Bind Scope expr_scope with expr.
  Delimit Scope expr_scope with expr.
  Infix "+" := Add : expr_scope.
  Notation "'elet' x := v 'in' f" := (LetIn v (fun x => f%expr)) : expr_scope.
  Notation "$$ x" := (Const x) (at level 9, format "$$ x") : expr_scope.

  Fixpoint denote (e : expr) : Z
    := match e with
       | LetIn v f => dlet x := denote v in denote (f x)
       | Const x => x
       | Add x y => denote x + denote y
     end.
End HOAS.
Fixpoint big (a : Z) (sz : nat) : Z
  := match sz with
     | O => a
     | S sz' => dlet a' := a + a in big a' sz'
     end.

Module CanonicalStructures.
  Import HOAS.
  (* structure for packaging a Z expr and its reification *)

  Structure tagged_Z := tag { untag :> Z }.
  Structure reifed_of :=
    reify { Z_of : tagged_Z ; reified_Z_of :> expr }.
  (* tags to control the order of application *)
  Definition const_tag := tag.
  Definition let_in_tag := const_tag.
  Canonical Structure add_tag n := let_in_tag n.
  Canonical Structure reify_const n := reify (const_tag n) (Const n).
  (*Canonical Structure reify_var n v := reify (var_tag n (Some v)) (Var v).*)
  Canonical Structure reify_add x y := reify (add_tag (Z_of x + Z_of y))
                                             (Add x y).
  (* XXX FIXME *)
  (* this works, but only for HOAS, not PHOAS, and only if [Let_In] is an axiom, not a definition *)
  (*Canonical Structure reify_let_in v f
    := reify (let_in_tag (zlet x := untag (Z_of v) in Z_of (f x)))
             (elet x := reified_Z_of v in reified_Z_of (f x)).*)
  Ltac pre_reify_rhs _ :=
    etransitivity;
    [
    | change (@Let_In Z (fun _ => Z)) with Let_In_Z;
      refine (_ : untag (Z_of _) = _) ];
    [ lazymatch goal with
      | [ |- _ = untag (Z_of ?v) ]
        => transitivity (denote (reified_Z_of v))
      end
    | ].
  Ltac do_reify_rhs _ :=
    [ > .. | refine eq_refl ].
  Ltac post_reify_rhs _ :=
    cbv [reify_add reify_const (*reify_let_in*) Z_of const_tag let_in_tag add_tag untag reified_Z_of];
    [ > | cbv [denote]; reflexivity ].
  Ltac reify_rhs _ :=
    pre_reify_rhs (); do_reify_rhs (); post_reify_rhs ().

  Opaque Let_In_Z Z.add.
  Strategy -100 [add_tag let_in_tag const_tag].

  Notation n := 10%nat.
  Goal exists v, v = big 1 n.
  Proof.
      eexists.
      Time cbv [big (*Let_In*)].
      Time pre_reify_rhs ().
      (*Set Debug Auto.
      Set Debug Cbv.
      Set Debug Eauto.
      Set Debug RAKAM.
      Set Debug Tactic Unification.
      Set Debug Trivial.
      Set Debug Typeclasses.
      Set Debug Unification.*)
      Opaque Let_In_Z.
      Time all:do_reify_rhs ().
      Time all:post_reify_rhs ().