The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

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.