I have a proof starting with Forall
(not 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 Forall
It's an inductive type that lives in Prop
so you cannot destruct it or perform induction on it to produce relevant things (in Type
or Set
).
You can use destruct
or induction
if your goal lives in Prop
.
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 Forall_forall
or 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 13 2024 at 01:02 UTC