Stream: Coq users

Topic: Any resources on writting proofs regarding `Forall`


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 16 2021 at 19:54):

you can also use lemma Forall_forall

view this post on Zulip Gaëtan Gilbert (Nov 16 2021 at 19:55):

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

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC