## Stream: Coq users

### Topic: Any resources on writting proofs regarding `Forall`

#### Daniel Hilst Selli (Nov 16 2021 at 19:43):

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`

#### Théo Winterhalter (Nov 16 2021 at 19:51):

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`.

#### Ana de Almeida Borges (Nov 16 2021 at 19:52):

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?

#### Théo Winterhalter (Nov 16 2021 at 19:52):

If you must land in `Type` then you can perform induction on the list argument and use `inversion` for instance.

#### Gaëtan Gilbert (Nov 16 2021 at 19:54):

you can also use lemma `Forall_forall`

#### Gaëtan Gilbert (Nov 16 2021 at 19:55):

or `induction H using Forall_rect` may work (with H the Forall hypothesis)

#### Daniel Hilst Selli (Nov 16 2021 at 22:16):

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: Jun 24 2024 at 12:02 UTC