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)
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.
f generates evars you may want to call it inside the thunk passed to
refine treats the evars generated inside this thunk specially (IIRC it detects them as new goals)
Last updated: Nov 29 2023 at 22:01 UTC