The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

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