Case analysis in pure Ltac2? · Ltac2

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.

Paolo Giarrusso (Jul 15 2023 at 12:02):

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

k32 (Jul 15 2023 at 12:13):

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

Gaëtan Gilbert (Jul 15 2023 at 12:17):

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.

Gaëtan Gilbert (Jul 15 2023 at 12:19):

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

k32 (Jul 15 2023 at 12:36):

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.

k32 (Jul 15 2023 at 12:43):

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.

Paolo Giarrusso (Jul 15 2023 at 16:38):

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.

Paolo Giarrusso (Jul 15 2023 at 16:45):

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.

k32 (Jul 22 2023 at 20:08):

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.

Gaëtan Gilbert (Jul 22 2023 at 20:18):

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)

Stream: Ltac2

Topic: Case analysis in pure Ltac2?

k32 (Jul 15 2023 at 11:45):