Gaëtan Gilbert (Jul 31 2022 at 09:11): Gaëtan Gilbert (Jul 31 2022 at 09:11):indeed In isn't strong enough, at a high level the reason is that you can't tell the index of an element from having a proof of In
you need to define a type which is like Forall but in Type. This is often called hlist for "heterogeneous list". Then the proof is the same as with Prop:
Section hlist.
Context {iT : Type}.
Variable F : iT -> Type.
Inductive hlist : list iT -> Type :=
| Hnil : hlist nil
| Hcons : forall l ls, F l -> hlist ls -> hlist (l :: ls).
End hlist.
Definition tree_recursion A (P: tree A → Type): (∀ L, hlist P L → P (forest L)) → ∀ t, P t.
Proof.
intros H. refine (fix IHt (t: tree A) := match t with forest l => _ end).
refine (H l _). induction l; intros.
+ constructor.
+ constructor.
- apply IHt.
- exact IHl.
Defined.
Thank you!
Notification Bot (Jul 31 2022 at 09:15):Lessness has marked this topic as resolved.
Last updated: Jan 29 2023 at 06:02 UTC