The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Kirill,

You don’t have to change your functions that take in the records, just prove that they are respectful morphisms, i.e., prove "Proper (projEquiv ==> eq) f” for your function f, where projEquiv is the equivalence relation on the predicative (non-Prop) parts of your records and Proper and the ==> notation are defined in Coq.Classes.Morphisms. Then, if you have “f r1” in a goal in your proof window, and the assumption “projEquiv r1 r2”, you can use the setoid rewrite tactic (I forget what it is called, it might even just be “rewrite”) to rewrite that to “f r2”.

-Eddy

On Oct 23, 2014, at 11:55 AM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Eddy,

That's how I do it currently (use special truncation equality).
But it isn't very convenient, because Prop values still occur in proof window as arguments to functions, because I can't rewrite function that acts on records into function that takes only material (non-Prop) field. So these huge Prop values blow proof session window into 10k lines.

Maybe it is just enough to change my proof style little bit to avoid such situations.

Sincerely,
Kirill Taran

On Thu, Oct 23, 2014 at 10:06 PM, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

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