Stream: Coq users

Topic: ✔ Recursion principle for tree


view this post on Zulip 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.
  + simpl in H0. admit.
Admitted.

view this post on Zulip 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.

view this post on Zulip Lessness (Jul 31 2022 at 09:15):

Thank you!

view this post on Zulip Notification Bot (Jul 31 2022 at 09:15):

Lessness has marked this topic as resolved.


Last updated: Mar 29 2024 at 09:02 UTC