The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Benoit,

You could feel that such a suggestion is a bit ironic

>> Another suggestion: try to avoid proving an equality between two proof
>> terms. :)
> 
> I wish I could in that case. :)

but from experience, I can tell you that this is indeed
a very good suggestion that you will follow the next
time you work with sigma types ...

When working with a sigma type Y = { x | P x }, you for
example can not built surjective maps onto Y because
there is no way to ensure you map to all the possible
proofs.

I see two paths around this problem. If P is decidable,
then put it in the form P x := f x = true and then you
know that two proofs of P x are equal because
(@eq bool x y) only has one proof. Although I am not
a specialist, this is in the ssreflect spirit I think.

If P is not decidable, then you can replace maps
f : X -> Y = { x | P x } with relations
r_f : X -> Y -> Prop and then you can "map" to several
values for one input value. Working with relations
instead of maps is more painful but it could work.

It is sometimes possible to prove the identity of
two proofs but unless you fully control how those
proofs are built (ie forget about libraries or
automation...), you are doomed.

Best,

Dominique

--------------------

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