[derive] `derive.induction` fails on predicates of rose trees

[Columbus240]

For some reason derive.induction fails without explicit error message. Though I think a suitable induction principle should be derivable. This is the large example I mentioned on Zulip, reduced by quite a bit. All the other limitations I mentioned I can work around, by adapting the definitions. This one I probably can't avoid.

Require Import List.
Import ListNotations.

From elpi.apps Require Import derive.

derive list.

derive
Inductive RoseTree : Type :=
| RT_ctr (branches : list RoseTree).

Inductive Pred : RoseTree -> Type :=
| Pred_ctr branches :
    list_is_list _ Pred branches ->
    Pred (RT_ctr branches).

Elpi derive.param1 list_is_list.
Elpi derive.param1 Pred.
Fail Elpi derive.induction Pred.

Coq v8.13.2, coq-elpi master branch.

[gares]

Hum, on the branch #269

derive
Inductive RoseTree : Type :=
| RT_ctr (branches : list RoseTree).

Elpi derive.param1 list_is_list.
#[verbose] derive
Inductive Pred : RoseTree -> Type :=
| Pred_ctr branches :
    list_is_list _ Pred branches ->
    Pred (RT_ctr branches).

fails to derive induction, but param1 works:

Deriving
Derivation isK
Derivation map
Derivation projK
Derivation param1
Derivation param1_congr
Derivation param1_inhab
Derivation param1_inhab failed
Derivation param1_trivial
Derivation param1_trivial failed
Derivation param1_functor
Derivation induction
Derivation induction failed

I'll look into it tomorrow, thanks for reporting.

[gares]

OK, I got the problem but I need to better understand your usecase. In particular there are 2 undocumented (sorry) derivations that seem to help to do what you want (instead of induction), but I can't be sure.

One works on this example, the other one does not (a bug). The first one generates Pred.Predinv an inductive like Pred where the index is turned into a parameter and the value of the index prescribed by the constructor into an equation. This derivation is called derive.invert.

The one not working, but fixable, is derive.idx2inv which maps a x : Pred r to a y : Pred.Predinv r. Then by case analysis on y one can implement an inversion on x. This is buggy, but it is fixable (it lacks the mapping of x0):

Check
  fix rec (H : RoseTree) (x : Pred H) {struct x} : Pred.Predinv H :=
  match x in (Pred H0) return (Pred.Predinv H0) with
  | Pred_ctr branches x0 =>
      let x0 := list_is_list_functor _ _ _ rec branches x0 in (* current code skips this line *)
      Pred.Pred_ctrinv (RT_ctr branches) branches x0 eq_refl
  end.

So, I'm heading toward fixing idx2inv, but I don't know if this is sufficient to cover your use case.

Repairing induction is a matter of fixing the derivations that fail. The first one is

Fail Elpi derive.param1.inhab Pred.is_Pred. 
(* derive.param1_inhab: wrong shape Pred.is_Pred. It does not look like a unary parametricity translation of an inductive with no indexes. *)

Indeed, if the inductive (Pred here) has indexes then things are tricky

Require Import ssreflect.
Lemma xxx : forall (r : RoseTree) pr p, Pred.is_Pred r pr p.
intros.
case: p pr => bl l pl.
case: pl. (* hum... *)

but become simpler if the indexes are turned into an equation. This very same problem will also bug you when using Pred in general, I'm afraid.

As I was saying invert and idx2inv are not documented/finished, but they seem easier to fix than induction, IMO.

[Columbus240]

I'll describe my use-case on Zulip. I don't think it fits here.

[lgaeher]

but become simpler if the indexes are turned into an equation.

Could you elaborate on how to transform the definition?

I'm facing a very similar problem: the type for which I would like to derive an induction principle is, essentially, a "heterogeneous rose tree" (definition is greatly simplified; in my real use case, the index of StructLty is also a heterogeneous list depending on rts, instead of nat):

Inductive hlist {A} (F: A → Type) : list A → Type :=
  | hnil : hlist F []
  | hcons {X Xs} : F X → hlist F Xs → hlist F (X :: Xs).

Inductive lty : Type → Type :=
  | StructLty (rts : list Type) (lts : hlist lty rts) : lty nat.

hlist here seems isomorphic to list_is_list above.

[gares]

I'm not so sure the transformation works when the index is a Type, but well, here it is (handwritten/untested):

Inductive ltyinv (T : Type) : Type :=
  | StructLty (rts : list Type) (lts : hlist ltyinv rts) (h : T = nat) : ltyinv T.

This is what I meant.

[lgaeher]

Ah, thank you! I will try and see if I can make it work like that.