The Coq mailing list

[Frédéric Loulergue <frederic.loulergue AT univ-orleans.fr>]

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