I have a proof starting with
forall). Locate points me to
Coq.Lists.Forall, this is new to me, I can't destruct and can't induce over it, is there any resources (paper, books, etc) for working with this type? I took a look at LF Lists chapter but it doens't say nothing about this
It's an inductive type that lives in
Prop so you cannot destruct it or perform induction on it to produce relevant things (in
You can use
induction if your goal lives in
Here is the definition:
Inductive Forall : list A -> Prop := | Forall_nil : Forall nil | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).
I would assume you could do induction on the list?
If you must land in
Type then you can perform induction on the list argument and use
inversion for instance.
you can also use lemma
induction H using Forall_rect may work (with H the Forall hypothesis)
I can do induction on list, yeah I will try that, thanks Ana!
Thanks Théo for the explanation, now makes much more sense to be why I couldn't use induction on this Forall. And Thanks @Gaëtan Gilbert too , I will take note on this lemma, it may be useful!
Last updated: Oct 01 2023 at 17:01 UTC