The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

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.
>