The Coq mailing list

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

Hi Cao Qinxiang,

Thank you for your quick answer. :)

On 4/24/19 4:54 PM, Cao Qinxiang wrote:

A short answer is: when you prove [introTF], use [Defined] instead of [Qed].

Unfortunately, I don't have control over that code unless I create a fork of ssreflect:

Locate on introTF gives me: Constant Coq.ssr.ssrbool.introTF

Another suggestion: try to avoid proving an equality between two proof terms. :)

I wish I could in that case. :)

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Wed, Apr 24, 2019 at 10:28 PM Benoît Viguier <beviguier AT gmail.com> 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.