Some extensions to `expand-record`

[patrick-nicodemus]

I think expand-record is potentially pretty valuable to me and I have an idea to extend it.

I am thinking about the following problem right now:

Record Graph := {
  Ob : Type;
  Hom : Ob -> Ob -> Type
}.
Record GraphHom (A B : Graph) := {
   f_ob :> Ob A -> Ob B;
   fmap : forall (x y : Ob A), Hom x y -> Hom (f_ob x) (f_ob y)
}.

Goal forall (A : Graph), GraphHom A A.

After record expansion this problem is easy to solve by a proof search tool like sauto.
But sauto doesn't perform induction, including destructing records, so I think the
utility of sauto could be much improved by this kind of reduction.

My idea here is to

1. extend the record_expansion to record declarations and not just definitions, so that one could use an elpi command to derive Record expand_GraphHom Ob_A Hom_A Ob_B Hom_B := { expand_f_ob : Ob_A -> Ob_A; expand_fmap : forall (x y : Ob_A), ... }.
2. write a tactic which would reduce the goal A : Graph |- GraphHom A A to Ob_A, Hom_A :- expand_GraphHom Ob_A Hom_A Ob_A Hom_A, after which you could apply a constructor and solve the goals.

There are many other small opportunities for improvement. For example one could ask that expand take a list of record arguments, not just one.

I'm wondering if you have any feedback on this plan or if you would accept a PR for such an extension, either the tactic or the plan to expand the command to records.

[gares]

Other than using unbundle as the name for the derivation, green light. I put @CohenCyril in the loop since he had a similar need at some point.

Please leave the POC simple, it is part of the doc, and add a more advanced derivation on the side.

[CohenCyril]

Thanks for pointing it out. Of course it's a useful generalization.

[patrick-nicodemus]

Currently there is an error message if you try to call record.expand on an indc, saying "it makes no sense to expand a constructor." I'm not sure I agree with that?

In the example I posted above,

Record Graph := {
  Ob : Type;
  Hom : Ob -> Ob -> Type
}.
Record GraphHom (A B : Graph) := {
   f_ob :> Ob A -> Ob B;
   fmap : forall (x y : Ob A), Hom x y -> Hom (f_ob x) (f_ob y)
}.

I might expect that

Elpi record.expand Graph Build_GraphHom "Unbundled".

defines

Definition UnbundledGraphHom Ob_A Hom_A Ob_B Hom_B 
      (f_ob : Ob_A -> Ob_B) (fmap : forall (x y : Ob_A), Hom_A x y -> Hom_B (f_ob x) (f_ob y)) 
      := @Build_GraphHom {| Ob_A Hom_A |} {| Ob_B Hom_B |} f_ob f_map.

This seems preferable in some cases to defining a second inductive record type, if the goal is to just give an alternate way to construct the record. What do you think? Is one more desirable than the other?

Admittedly, it is more like the unbundling of the eta expansion of the constructor, then the unbundling of the constructor itself.

Actually, it's literally just the unbundling of the eta expansion.

Check Build_GraphHom.
Definition Abc := fun (G H : Graph) => Build_GraphHom G H.
Elpi record.expand Graph Abc "Unbundled".
Print UnbundledAbc.
(* 
UnbundledAbc@{u u0 u1 u2} = fun (Ob : Type) (Arr : Ob -> Ob -> Type) (Ob0 : Type)
(Arr0 : Ob0 -> Ob0 -> Type) => Build_GraphHom {| Ob := Ob; Arr := Arr |} {| Ob := Ob0; Arr := Arr0 |}
*)

This would work for axioms too. We could just give the user a warning saying that because an axiom has no body we will be unbundling the eta expansion of the record as well.