The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

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