thank you, I made a typo, my bad! now I get the right induction principle : )

```
Inductive tree' (X : Type) : Type :=
| leaf' (x : X)
| node' (t : tree' (X * X)).
Check tree'_ind.
(* tree'_ind *)
(* : forall P : forall X : Type, tree' X -> Prop, *)
(* (forall (X : Type) (x : X), P X (leaf' X x)) -> *)
(* (forall (X : Type) (t : tree' (X * X)), P (X * X)%type t -> P X (node' X t)) -> *)
(* forall (X : Type) (t : tree' X), P X t *)
```

yiyuan-cao has marked this topic as resolved.

for the convenience of other adventurous novices, here's a homogeneous parameterized type as comparison:

```
Inductive tree (X:Type) : Type :=
| leaf (x : X)
| node (t1 t2 : tree X).
Check tree_ind.
(* tree_ind *)
(* : forall (X : Type) (P : tree X -> Prop), *)
(* (forall x : X, P (leaf X x)) -> *)
(* (forall t1 : tree X, P t1 -> forall t2 : tree X, P t2 -> P (node X t1 t2)) -> *)
(* forall t : tree X, P t *)
```

notice that `X`

is introduced at the outmost position, while for the heterogeneous parameterized type above the `X`

s are (necessarily) introduced at each case branch.

Out of curiosity, I tried the heterogeneous definition on a simple use case: compute the fringe of a `tree'`

.

There should be a better solution, I hope so.

```
Fixpoint pairs (n:nat) (X:Type) :=
match n with 0 => X | S p => (pairs p X * pairs p X)%type
end.
Lemma pairs_eq: forall X n, pairs n (X * X)%type =
(pairs n X * pairs n X)%type.
Proof.
induction n.
- reflexivity.
- simpl; now rewrite IHn.
Defined.
Fixpoint height X (t: tree' X) : nat :=
match t with
leaf' _ _ => 0
| node' _ t' => S (height _ t')
end.
Definition fringe' X (t: tree' X) : pairs (height _ t) X .
Proof.
induction t.
- exact x.
- rewrite pairs_eq in IHt; exact IHt.
Defined.
Example t3 := node' _ (node' _ (leaf' _ (3, 4, (5, 6)))).
Compute fringe' _ t3.
(* = (3, 4, (5, 6))
: pairs (height nat t3) nat *)
```

Note that the `tree'`

type describes thread-like trees.

if you do

```
Fixpoint pairs (n:nat) (X:Type) :=
match n with 0 => X | S p => pairs p (X * X)%type
end.
```

you don't need the pairs_eq lemma

you could also return a `list X`

instead of `pairs (height _ t) X`

Last updated: Jun 23 2024 at 03:02 UTC