Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Tatic similar to discriminate

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tatic similar to discriminate


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page