rose tree induction example

rose.v

Require Import List.

Inductive rose(X : Type) : Type :=
  | node : X -> list (rose X) -> rose X.

Fixpoint rose_map{X Y}(f : X -> Y)(r : rose X) : rose Y :=
  match r with
  | node _ x rs => node _ (f x) (List.map (rose_map f) rs)
  end.

Fixpoint rose_ind2(X : Type)(P : rose X -> Prop)(HP : forall (x : X)(rs : list (rose X)), Forall P rs -> P (node X x rs))(r : rose X) : P r.
Proof.
  destruct r.
  apply HP.
  induction l; constructor.
  - apply rose_ind2; auto.
  - exact IHl.
Qed.

Lemma rose_map_id : forall (X : Type)(r : rose X), rose_map (fun x => x) r = r.
Proof.
  intros.
  apply (@rose_ind2 _ (fun r0 => rose_map (fun x => x) r0 = r0)).
  intros.
  simpl.
  f_equal.
  induction rs.
  - reflexivity.
  - simpl.
    inversion H.
    rewrite H2.
    rewrite IHrs; auto.
Qed.