The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

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).