The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-22 11:08 GMT+02:00 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.

Not exactly, it says that the statements are equal, it does not say much on the proofs.
In Type, that could be illustrated with:

Inductive ns_dir : Type := North : ns_dir | South : ns_dir.
Inductive we_dir : Type := West : we_dir | East : we_dir.

Replace "~(c=c'):Prop" with "ns_dir:Type" and "~(F c = F c'):Prop" with "we_dir:Type",
and the statement I found dubious would be: ns_dir = we_dir.
 

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

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.
 

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

--
.../Sedrikov\...