The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.edu>]

Thank you Samuel and Yannick for your helpful answers. This is good news !

I will go through both possibilities. Actually we had thought a while back MetaCoq could be useful for our project, but I had not realized it may be the case here.

Just for the record, the aim is to build tactics to help link Coq with our drag-and-drop Actema proof interface. You can play with a small prototype here :

http://actema.xyz/

The idea being to have this as a front-end for Coq, or Coq as a back-end for Actema.

All the best,

Benjamin

Le 16 juin 2022 à 00:34, Samuel Gruetter <gruetter AT mit.edu> a écrit :

Hi Benjamin,

Below is some Ltac code that works on your example, as well as on one
additional example. Whether such Ltac code is the most principled,
readable and beautiful solution that everyone should use all the time,
that's a different question though... ;-)

Best,
Samuel Gruetter

===========


Notation "'subst!' y 'for' x 'in' f" :=
 (match y with x => f end) (at level 10, f at level 200).

Ltac beta1 func arg :=
 lazymatch func with
 | (fun a => ?f) => constr:(subst! arg for a in f)
 end.

Ltac wrap names vals t :=
 lazymatch names with
 | nil => t
 | cons ?y ?ys => constr:(let (v0, rest0) := vals in ltac:(
     let t' := wrap ys rest0 t in
     lazymatch eval pattern y in t' with
     | ?f y => let t'' := beta1 f v0 in exact t''
     end))
 end.

Lemma test_wrap: forall a b c: nat,
   (fun (z: pp 3) => ltac:(
     let r := wrap (cons a (cons b (cons c nil))) z (a + b = c) in
     exact r)) (a, (b, (c, I))) =
   (fun (z: pp 3) => a + b = c) (a, (b, (c, I))).
Proof. intros. reflexivity. all: fail. Abort.

Ltac reify_rec n env t :=
 lazymatch t with
 | ?a -> ?b =>
     let ra := reify_rec n env a in
     let rb := reify_rec n env b in
     constr:(imp n ra rb)
 | forall x: nat, @?body' x =>
     let y := fresh "y" in
     lazymatch constr:(fun y: nat => ltac:(
       let body := beta1 body' y in
       let r := reify_rec (S n) (cons y env) body in
       exact r))
     with
     | (fun _: nat => ?r) => constr:(fa n r)
     end
 | _ => constr:(Hole n (fun (z: pp n) =>
    ltac:(let r := wrap env z t in exact r)))
 end.

Ltac reify_goal :=
 lazymatch goal with
 | |- ?g => let r := reify_rec 0 (@nil nat) g in change (coerce 0 r I)
 end.

Set Ltac Backtrace. (* helps with debugging Ltac *)

Goal forall x : nat,  x=2 -> x=3.
 reify_goal. simpl.
Abort.

Goal forall a: nat, a + a = 2 -> forall b: nat, a + b = 3 -> b = 2.
 reify_goal. simpl.
Abort.


-----Original Message-----
From: Benjamin Werner <benjamin.werner AT inria.fr>
Reply-To: coq-club AT inria.fr
To: coq-club AT inria.fr
Subject: [Coq-Club] dealing with open terms in Ltac or Ltac2
Date: Wed, 15 Jun 2022 15:02:16 +0200

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