The Coq mailing list

[Yannick Forster <yannick.forster AT inria.fr>]

Dear Benjamin,

the good news first: No caml code necessary! I don't know of a pure Ltac 
solution, but  the Template-Coq part of MetaCoq can do the job.


Based on that, Johannes Hostert has implemented a reflection of the 
first-order fragment of Coq into a deep embedding of first-order logic, 
which was part of the following contribution to the Coq Workshop 21.

A Toolbox for Mechanised First-Order Logic
Johannes Hostert, Mark Koch and Dominik Kirst
https://coq-workshop.gitlab.io/2021/abstracts/Coq2021-02-01-fol-toolbox.pdf


MetaCoq is a big project, but it is not necessary to dive into the 
details to use it for your purpose:

After installing MetaCoq (currently only possible from source if you are 
using Coq 8.14, clone the right branch and run make template-coq && make 
-C template-coq install) and executing

From MetaCoq.Template Require Import All Loader.

there is a command

MetaCoq Test Quote

to get used to the type Ast.term, which is the target of reification 
(https://github.com/MetaCoq/metacoq/blob/coq-8.14/template-coq/theories/Ast.v), 
and a tactic quote_term, which expects a term and a continuation. You 
can use Coq, Ltac or Ltac2 to process the result. If needed, 
Template-Coq also provides tools to reflect a reified term back into an 
actual Coq term.

If you think that Template-Coq be of help to you, feel free to ask 
further questions!

Best
Yannick

On 6/15/22 15:02, Benjamin Werner wrote:
> Hello,
>
> I am sorry in case this topic has already been covered, please feel free to 
> refer me to older posts.
>
> I want to write a tactic which does a reification, like in the first step of, 
> say, the ring tactic. The problem
> is I want to construct a structure which includes some binders, which means 
> the tactic probably needs
> to deal with open terms, and this seems problematic if sticking to Ltac or 
> Ltac2.
>
> Here is a simple example. It is not precisely what I want to do, but if one 
> can do the following, it would
> be a good step. From what I understand, one probably needs to dive into caml 
> code, but I would be very
> happy if this was not the case.
>
> Thank you in advance, best wishes,
>
> Benjamin
>
>
> ===========
>
>
> Fixpoint pp (n : nat) : Type :=
>    match n with
>    | 0 => True
>    | S n => nat * (pp n)
> end.
>
> (* a first-order fragment of Prop *)
>
> Inductive cx : nat -> Type :=
> | Hole : forall n,  ((pp n) -> Prop) -> (cx n)
> | imp : forall n, (cx n) -> (cx n) -> (cx n)
> | fa : forall n, cx (S n) -> cx n.
>
> (* translating back into Prop *)
>
> Fixpoint coerce  (n:nat) (c:cx n) : (pp n) -> Prop :=
>    match c with
> | Hole _ P => P
> | imp _ c d => fun x => ((coerce _ c x)  -> (coerce _ d x))
> | fa _ c => fun x =>  forall p:nat, (coerce _ c (p, x))
> end.
>
> (* stupid example *)
> Goal forall x : nat,  x=2 -> x=3.
>
>    (* I want a tactic able to do something like that :    *)
>    (* but without me having to type the cx explicitely  *)
> change (coerce 0
>                   (fa 0
>                       (imp 1
>                            (Hole 1 (fun z =>  let (x,_) := z in  (x=2)))
>                            (Hole 1 (fun z =>  let (x,_) := z in (x=3)))))
>           I).
>