The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

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 Taran

On 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 Taran

On 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