Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] is this lemma provable?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is this lemma provable?


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] is this lemma provable?
  • Date: Mon, 18 Mar 2013 11:38:53 -0400

Certainly the alternate proof that someone else suggested later is nicer than what I suggested, but mine didn't rely on any axioms. ;)

On 03/17/2013 08:36 AM, Thierry Martinez wrote:
Leonardo:
Lemma unprovable :
forall q : H a, q = b.
Adam:
Require Import Eqdep_dec.
or without relying on an extra-CiC axiom:

Proof.
intro q.
exact (match q with | b => eq_refl end).
Qed.

I don’t know how to ask tactics to build such a term



Archive powered by MHonArc 2.6.18.

Top of Page