## Stream: Coq users

### Topic: ✔ Recursion principle for tree

#### Lessness (Jul 31 2022 at 08:55):

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

#### 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: Jun 18 2024 at 09:02 UTC