Lessness (Jul 31 2022 at 08:55): 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.
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.
Thank you!
Notification Bot (Jul 31 2022 at 09:15):Lessness has marked this topic as resolved.
Last updated: Oct 01 2023 at 19:01 UTC