coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Saulo Araujo <saulo2 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Tatic similar to discriminate
- Date: Tue, 10 Feb 2015 09:31:05 -0300
Hi,
I am trying to prove a theorem and got stuck. I have the following hypothesis
H0 : l = (c, p) :: l
which says that a list is equal to the tail of another list. This, I believe, is never true. Prooving another simpler theorem I also got in a situation like this and, in that simpler case, I could end the proof using the discriminate tactic, but in this case, Coq says:
Error: No primitive equality found.
Does anyone know what can I do?
Thanks in advance,
Saulo
- [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Frédéric Besson, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Pierre Casteran, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Jean-Francois Monin, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Cedric Auger, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Pierre Casteran, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Cedric Auger, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/13/2015
- Re: [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Pierre Casteran, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/10/2015
- Re: [Coq-Club] Tatic similar to discriminate, Saulo Araujo, 02/10/2015
Archive powered by MHonArc 2.6.18.