coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:
Adam:Lemma unprovable :
forall q : H a, q = b.
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
- [Coq-Club] is this lemma provable?, Leonardo Rodriguez, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Thierry Martinez, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/18/2013
- [Coq-Club] Second Call for Papers, PxTP 2013, Laurent Théry, 03/18/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/18/2013
- Re: [Coq-Club] is this lemma provable?, Thierry Martinez, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Daniel Schepler, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/17/2013
Archive powered by MHonArc 2.6.18.