The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2014-07-21 4:47 GMT+02:00 Alexander Kogtenkov 
<kwaxer AT mail.ru>:
>> Didn’t you mean "Axiom A: forall c c': C, (~ (c = c')) <-> (~ (F c = F> 
>> c'))"?
>
> Yes, that works as well.

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

It is indeed provable if you suppose decidability of equality on C. I
don't know if there is a weaker suitable supposition.

Best regards,
Pierre

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.



>
> Regards,
> Alexander Kogtenkov
>
>
> Sun, 20 Jul 2014 22:52:56 +0200 от Cédric 
> <sedrikov AT gmail.com>:
>> Le Sun, 20 Jul 2014 21:39:34 +0200, 
>> <kwaxer AT mail.ru>
>>  a écrit:
>>
>> > Hi,
>> >
>> > Given the following environment
>> >
>> > Variable C: Set.
>> > Variable N: Set.
>> > Variable F: C-> N.
>> > Axiom A: forall c c': C, (~ (c = c')) = (~ (F c = F c')).
>>
>> Didn’t you mean "Axiom A: forall c c': C, (~ (c = c')) <-> (~ (F c = F
>> c'))"?
>> Your original axiom seems dubious to me.
>>
>> >
>> > how one can prove
>> >
>> > Theorem T: forall (n: N) (c: С), F c = n -> forall c': C, F c' = n -> c
>> > = c'.
>> >
>> > ?
>> >
>> > I believe this requires the proof of
>> >
>> > Lemma L: forall A B: Prop, (~ A) = (~ B) -> A = B.
>> >
>> > How can it be done? Can this be avoided as I guess the lemma requires
>> > classical logic?
>> >
>> > Thank you,
>> > Alexander Kogtenkov
>>
>>
>> --
>> ---
>> Cédric AUGER