Hello. I have a question that I couldn't answer myself by reading the docs and the ltac2 testsuite. Is it theoretically possible to implement `destruct`

tactic in pure Ltac2? To put it another way, given an arbitrary inductive type, is it possible to create a constr that contains a `match`

statement for a variable of that type?

Background: I am trying to use Ltac2 to automate generation of boilerplate code, and destruct oftentimes creates code that is unnecessarily convoluted.

(Side note: Have you tried the `case`

tactic? destruct has some extra smarts, and those might cause the problem you see.)

Have you tried the case tactic? destruct has some extra smarts, and those might cause the problem you see.

I think it will lead to the same result. To give an example (this is Ltac1, but I guess it doesn't really matter, since `case`

is builtin?):

```
Inductive operation :=
| var | log | self.
(* Boilerplate code that I'm trying to generate,
it should return different values depending on the argument *)
Defintion opType (op : operation) : Type.
case op. (* I get the hypotheses, but information about
the constructor is lost, so no luck *)
Abort.
(* This works, but creates a messy definition: *)
Defintion opType (op : operation) : Type.
case op eqn:H.
match goal ...
```

here is an example of defining equality of bytes by pattern matching in ltac2 (the equivalent for bool would be `fun a => if a then (fun b => if b then True else False) else (fun b => if b then False else True)`

)

```
Require Import Init.Byte Ltac2.Ltac2.
Import Ltac2.Control Ltac2.Constr.Unsafe.
Definition noconf : byte -> byte -> Prop.
Proof.
intros a.
let byteind := match kind 'byte with Ind v _ => v | _ => throw Not_found end in
let ci := case byteind in
let _True := 'True in
let _False := 'False in
let outerpred := '(fun _ : byte => byte -> Prop) in
let innerpred := '(fun _ : byte => Prop) in
let innerbind := match kind '(fun b : byte => b) with Lambda b _ => b | _ => throw Not_found end in
let brs := Array.init 256 (fun i =>
let innerbrs := Array.init 256 (fun j =>
if Int.equal i j then _True else _False)
in
make (Lambda innerbind (make (Case ci innerpred NoInvert (make (Rel 1)) innerbrs))))
in
let c := make (Case ci outerpred NoInvert &a brs) in
exact $c.
Defined.
```

To give an example (this is Ltac1, but I guess it doesn't really matter, since case is builtin?):

What do you want it do do? ie if you had

```
Definition opType (op : operation) : Type.
dotherightthing op.
```

what should the resulting goal and proof term be?

It's a bit hard to give enough context without steering completely off-topic, but here's a bigger example:

```
(* This inductive type serves as a user-friendly name
for the "handler" (whatever it means is irrelevant) *)
Inductive handlerId :=
| var | log | self.
(* User can create a specification of the "composite handler",
that associates different constructors of handlerId with
various typeclasses *)
Ltac2 handlers () := ['var, '(Var.t nat);
'log, '(@Log.t nat);
'self, '(Self.t)].
(* I want to use this specification to create various helper functions,
for example: *)
Definition opType (op : handlerId) : Type :=
match op with
| var => Var.req_t
| log => Log.req_t
| self => Self.req_t
end.
```

So it's not really a proof that I am trying to create, but a definition.

P.S. Thanks for the example, I suspected that `Constr.Unsafe`

might be the missing piece, but I couldn't find any examples of code using it.

I see the challenge, but you might not need to replace the `case`

tactic, just to introspect the datatype to find the order of its constructors. case without eqn will produce the right match, and the order of subgoals should match the order of branches.

More concretely, the code below is self-contained and produces a (variant of) `opType`

using `case`

. You must just learn the constructor order to sort the types accordingly — in your example, `handlers`

happens to be already sorted.

```
From Coq Require Fin.
Inductive handlerId :=
| var | log | self.
Definition opType (op : handlerId) : Type :=
match op with
| var => Fin.t 1
| log => Fin.t 2
| self => Fin.t 3
end.
Definition opType' (op : handlerId) : Type.
case op.
exact (Fin.t 1).
exact (Fin.t 2).
exact (Fin.t 3).
Defined.
Goal opType = opType'.
reflexivity. Qed.
```

Thanks to @Gaëtan Gilbert I was able to achieve the expected result. Posting the code here in case anyone has the same question in the future:

```
From Ltac2 Require Import Init List Ind Env Control Option Constr Std Array.
Ltac2 indRef (ident : ident list) : inductive :=
let a := Option.get (Env.get ident) in
match a with
| Std.IndRef a => a
| _ => throw_invalid_argument "Argument must be a reference to an inductive type"
end.
Ltac2 constructor2constr (d : Ind.data) (i : int) : constr :=
let c := Ind.get_constructor d i in
let c := Std.ConstructRef c in
Env.instantiate c.
Ltac2 makeCase0 (ind : ident list) (f : inductive -> int -> constr) :=
let (indref : inductive) := indRef ind in
let (indt : constr) := Env.instantiate (Std.IndRef indref) in
let innerpred := '(fun _ : $indt => Type) in
let binder := match kind '(fun b : $indt => b) with Lambda b _ => b | _ => throw Not_found end in
let d := Ind.data indref in
let n := Ind.nconstructors d in
let branches := Array.init n (f indref) in
let ast := make (Case (case indref) innerpred NoInvert (make (Rel 1)) branches) in
let ast := make (Lambda binder ast) in
Control.refine (fun () => ast).
Ltac2 makeCase (ind : ident list) (f : constr -> constr) :=
let iter ind i := f (constructor2constr (Ind.data ind) i) in
makeCase0 ind iter.
```

Not the prettiest code, but it works for my simple case.

if `f`

generates evars you may want to call it inside the thunk passed to `Control.refine`

`refine`

treats the evars generated inside this thunk specially (IIRC it detects them as new goals)

Last updated: Jun 23 2024 at 01:02 UTC