Stream: Coq users

Topic: ✔ Induction principle for non-uniform parameterized types


view this post on Zulip Yiyuan Cao (Jul 22 2023 at 13:35):

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 *)

view this post on Zulip Notification Bot (Jul 22 2023 at 13:35):

yiyuan-cao has marked this topic as resolved.

view this post on Zulip Yiyuan Cao (Jul 22 2023 at 13:40):

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 *)

view this post on Zulip Yiyuan Cao (Jul 22 2023 at 13:42):

notice that X is introduced at the outmost position, while for the heterogeneous parameterized type above the Xs are (necessarily) introduced at each case branch.

view this post on Zulip Pierre Castéran (Jul 22 2023 at 13:54):

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.

view this post on Zulip Gaëtan Gilbert (Jul 22 2023 at 14:00):

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