coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] what is firstorder supposed to do?

From: Daniel Schepler <dschepler AT gmail.com>
To: coq-club AT inria.fr
Cc: Jonathan Leivent <jonikelee AT gmail.com>
Subject: Re: [Coq-Club] what is firstorder supposed to do?
Date: Sat, 07 Nov 2015 16:38:39 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f68.google.com
Ironport-phdr: 9a23:lc305BE1plzVwsPP0vIzg51GYnF86YWxBRYc798ds5kLTJ75o8ywAkXT6L1XgUPTWs2DsrQf27eQ7/irADFRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh730p8WYOlgZzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB0kflBtFB0D+5xH3RpP8qGOuuvF22CSCOcDsZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==

On Saturday, November 07, 2015 01:57:08 PM Jonathan Leivent wrote:
> I've been experimenting with firstorder - but, other than hitting bugs
> (4401), all I've succeeded in doing is convince myself that I don't
> really know what it is supposed to do. Can someone explain?

I don't know the details myself of what exactly it does. But here's a simple
example of a theorem that firstorder can prove, which tauto has no chance of
proving:

Goal forall (A B:Type) (f:A->B) (P:A->Prop) (Q:B->Prop),
(forall x:A, P x -> Q (f x)) -> ex P -> ex Q.
Proof.
firstorder.
Qed.
--
Daniel Schepler

[Coq-Club] what is firstorder supposed to do?, Jonathan Leivent, 11/07/2015
- Re: [Coq-Club] what is firstorder supposed to do?, Daniel Schepler, 11/08/2015
- Re: [Coq-Club] what is firstorder supposed to do?, Hugo Herbelin, 11/08/2015
  - Re: [Coq-Club] what is firstorder supposed to do?, Jonathan Leivent, 11/09/2015
    - Re: [Coq-Club] what is firstorder supposed to do?, Jonathan Leivent, 11/10/2015