The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-22 12:57 GMT+02:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

014-07-22 11:57 GMT+02:00 Cedric Auger <sedrikov AT gmail.com>:
> 2014-07-22 11:08 GMT+02:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:
>> Be warned that in Coq the two versions are far from being equivalent.
>> Your version is indeed probably inconsistent for most instances of F.
>> You should definitely favor Cédric's one. In one word: your version
>> states that the proofs of equalities are *equal* whereas Cédric's one
>> only states that they can be derived from each other.
>
> Not exactly, it says that the statements are equal, it does not say much on
> the proofs.

Right, it is even more wrong then.


> In fact decidability won’t help much I fear. Decidability helps for "∀ (x y
> : A) (p q : x = y), p = q" which not what we have here, or so it seems to
> me.

Combined with the axiom A it does, as shown by the proof below. But
Arnaud gave a better solution.

My bad, I had in mind that you meant that axiom A was provable using decidability. But I forgot that the main subject of this thread was theorem T and not axiom A.
 

P.

>> Variable C N: Set.
>> Variable F: C-> N.
>> Axiom A: forall c c': C, (~ (c = c')) <-> (~ (F c = F c')).
>> Axiom Cdec: forall c c':C, { c=c' } + { c<>c' }  .
>>
>> Theorem T: forall (n: N) (c: C), F c = n -> forall c': C, F c' = n -> c =
>> c'.
>> Proof.
>>   intros n c H c' H0.
>>   destruct (Cdec c c').
>>   - assumption.
>>   - rewrite <- H in H0.
>>     assert (F c <> F c').
>>     { apply A.
>>       assumption. }
>>     symmetry in H0.
>>     contradiction.
>> Qed.
>>
>>

--
.../Sedrikov\...