The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Indeed Eqdep_dec.eq_proofs_unicity is axiom-free.

You can import it from the standard library with
From Coq Require Import Eqdep_dec.

I think the idiomatic way to do it in mathcomp is using eq_irrelevance lemma 
from eqtype:

Lemma foo p proof_of another_proof_of :
  MC p (proof_of p) = MC p (another_proof_of p).
Proof. by congr MC; apply: eq_irrelevance. Qed.

-Anton


> On 24 Apr 2019, at 18:15, Siddharth Bhat 
> <siddu.druid AT gmail.com>
>  wrote:
> 
> Does that not assume UIP? Is that standard in Coq? 
> 
> Thanks 
> Siddharth
> 
> sent from my phone, please excuse any typos!
> 
> On Wed, 24 Apr, 2019, 20:37 Gaëtan Gilbert, 
> <gaetan.gilbert AT skyskimmer.net>
>  wrote:
> 
>  > proof_of p = another_proof_of p
> 
> You should be able to prove that by applying Eqdep_dec.eq_proofs_unicity
> 
> 
> Gaëtan Gilbert
> 
> On 24/04/2019 16:27, Benoît Viguier wrote:
> > Dear all,
> > 
> > I have a type defined in the following kind:
> > 
> >    Definition oncurve (p : point K) := (     match p with     | 
> > EC_Inf    => true     | EC_In x y => M#b * y^+2 == x^+3 + M#a * x^+2 + x 
> >      end).   Inductive mc : Type := MC p of oncurve p.   Coercion 
> > point_of_mc p := let: MC p _ := p in p.
> > 
> > and at some point I am trying to prove that :
> > 
> > MC p (proof_of p) = MC p (another_proof_of p).
> > 
> > Reflexivity do not work in this case because : (proof_of_p p) and 
> > (another_proof_of p) while being the same in some senses are not the 
> > same object.
> > 
> > However by doing f_equal, the goal becomes:
> > 
> > proof_of p = another_proof_of p
> > 
> > I can unfold both of them and the subsequent definitions, applying a 
> > compute leads me to the following state:
> > 
> > match   match     introTF (c:=true) idP       (equivPif idP (fun 
> > _view_subject_ : true = true => _view_subject_)          (fun 
> > _view_subject_ : true = true => _view_subject_)) in     (_ = y) return 
> > (y = true)   with   | Logic.eq_refl => Logic.eq_refl   end in (_ = y) 
> > return (y = true) with | Logic.eq_refl =>     match       introTF 
> > (c:=true) idP         (equivPif idP (fun _view_subject_ : true = true => 
> > _view_subject_)            (fun _view_subject_ : true = true => 
> > _view_subject_)) in       (_ = y) return (y = true)     with     | 
> > Logic.eq_refl => Logic.eq_refl     end end = is_true_true
> > 
> > Thus my question would be is there anyway to un-opaque those last part ? 
> > It says that introTF is defined as Opaque, thus Transparent does not go 
> > through either. How can I proceed forward?
> > 
> >  From which I cannot work further as introTF etc are opaque. Is there 
> > any other way I can prove my equality?
> > 
> > Thanks a lot for any help or insight you can provide me with.
> > 
> > Kind Regards,
> > 
> > Benoit Viguier.
> >