I defined such type: `Inductive tree (A: Type) := forest: ∀ (L: list (tree A)), tree A.`

. Then I tried to prove good induction and recursion principles for it (because automatically generated principles wasn't good enough).

I had success with the induction principle, but the same approach isn't working for recursion.

Do you have any hints? Here's the code.

```
Require Import Utf8.
Set Implicit Arguments.
Inductive tree (A: Type) := forest: ∀ (L: list (tree A)), tree A.
Definition tree_induction A (P: tree A → Prop): (∀ L, List.Forall 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.
Definition tree_recursion A (P: tree A → Type): (∀ L, (∀ x, List.In x L → P x) → P (forest L)) → ∀ t, P t.
Proof.
intros H. refine (fix IHt (t: tree A) := match t with forest l => _ end).
refine (H l _). intros. induction l; intros.
+ elim H0.
+ simpl in H0. admit.
Admitted.
```

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!

Lessness has marked this topic as resolved.

Last updated: Jun 18 2024 at 09:02 UTC