Stream: Coq users

Topic: ✔ Recursion principle for tree


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: Jan 29 2023 at 06:02 UTC