coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Eddy Westbrook <westbrook AT kestrel.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proving equalities for records with Prop component
- Date: Thu, 23 Oct 2014 11:06:05 -0700
Kirill,
You can use the proof irrelevance axiom, in Coq.Logic.ProofIrrelevance. However, this sort of situation is best avoided: unless you really need equality of the records themselves, I would suggest you instead formulate an equivalence relation on your records which holds between r1 and r2 iff r1.number = r2.number. You can even use setoid rewriting with such an equivalence, if you declare your functions that take these records as input to respect the record equivalence.
-Eddy
On Oct 23, 2014, at 10:37 AM, Kirill Taran <kirill.t256 AT gmail.com> wrote:
Ah, seems that it can't.
I (incorrectly) thought that if all Prop is erased than we can drop it during the proof.Sincerely,
Kirill TaranOn Thu, Oct 23, 2014 at 9:27 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:Frederic,
Sorry, bad example. Is there a way for not-decidable equalities?
Can such problem be solved at all? I'm not sure about it.Sincerely,
Kirill TaranOn Thu, Oct 23, 2014 at 7:56 PM, Frédéric Loulergue <frederic.loulergue AT univ-orleans.fr> wrote:Hi,
For decidable types, there is uniqueness of identity proofs, i.e. only one proof of x = x.
The Coq library provides this theorem in a module in Coq.Logic.Eqdep_dec.
Require Import Arith.
Require Import Coq.Logic.Eqdep_dec.
Record R := { number : nat; proof : exists n, n + number = 100 }.
Module NatDec.
Definition U := nat.
Lemma eq_dec : forall x y:U, {x = y} + {x <> y}.
decide equality.
Qed.
End NatDec.
Module Dec := DecidableEqDep NatDec.
Lemma r_eq (x y : R) : number x = number y -> x = y.
Proof.
intro H.
destruct x as [x Hx]; destruct y as [y Hy]; simpl in H; subst.
destruct Hx as [n H]; destruct Hy as [n' H'].
assert(n = n') by
(rewrite <-H' in H; rewrite <- NPeano.Nat.add_cancel_r; eauto).
subst.
assert(H = H') as HH' by apply Dec.UIP.
now rewrite HH'.
Qed.
Best,
Frederic
Le 23/10/2014 17:27, Kirill Taran a écrit :
Hello,
I have such problem:
Record R := { number : nat; proof : exists n, n + number = 100 }.
Lemma r_eq (x y : R) : number x = number y -> x = y.
Admitted.
Is it possible to solve it and how?
Sincerely,
Kirill Taran
- [Coq-Club] Proving equalities for records with Prop component, Kirill Taran, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Frédéric Loulergue, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Kirill Taran, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Kirill Taran, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Eddy Westbrook, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Kirill Taran, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Eddy Westbrook, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Kirill Taran, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Eddy Westbrook, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Kirill Taran, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Kirill Taran, 10/23/2014
- Re: [Coq-Club] Proving equalities for records with Prop component, Frédéric Loulergue, 10/23/2014
Archive powered by MHonArc 2.6.18.