The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Related question: Is there any existing work on reifying to (P)HOAS syntax trees via canonical structures?

On Wed, Dec 6, 2017 at 12:43 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

I have cargo-culted code for reifying flat syntax trees using canonical structures.  However, I have a question:

Why does canonical structure resolution fail when I require a constant to be applied to particular types.  That is, why does this work:

~~~

Inductive expr :=

| Const (v : nat)

| Add (x y : expr)

| LetIn (v : expr) (f : nat -> expr).

Axiom let_in : nat -> (nat -> nat) -> nat.

Axiom add : nat -> nat -> nat.

Fixpoint denote (e : expr) : nat

  := match e with

     | Const v => v

     | Add x y => denote x + denote y

     | LetIn v f => let_in (denote v) (fun x => denote (f x))

     end.

Structure tagged_nat := tag { untag :> nat }.

Structure reifed_of :=

  reify { nat_of : tagged_nat ; reified_nat_of :> expr }.

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_add x y

  := reify (add_tag (nat_of x + nat_of y)) (Add x y).

Canonical Structure reify_let_in v f

  := reify (let_in_tag (let_in (untag (nat_of v)) (fun x => nat_of (f x))))

           (LetIn (reified_nat_of v) (fun x => reified_nat_of (f x))).

Ltac reify_rhs _ :=

  etransitivity;

  [ | refine (eq_refl : untag (nat_of _) = _) ];

  lazymatch goal with

  | [ |- _ = untag (nat_of ?v) ]

    => transitivity (denote (reified_nat_of v))

  end;

  cbv [reify_add reify_const reify_let_in nat_of const_tag let_in_tag add_tag untag reified_nat_of];

  [ | cbv [denote]; reflexivity ].

Goal exists v, v = let_in 5 (fun x => let_in 6 (fun y => x + y)).

Proof.

  eexists.

  reify_rhs ().

  lazymatch goal with |- _ = denote (LetIn (Const 5) (fun x => LetIn (Const 6) (fun y => Add (Const x) (Const y)))) => idtac end.

  (* success *)

Abort.

~~~~

but if I change Axiom let_in : nat -> (nat -> nat) -> nat. to Axiom let_in : forall {A B}, A -> (A -> B) -> B. then it fails (treats the whole thing as Const)?

Thanks,

Jason