The Coq mailing list

[Alexander Kogtenkov <kwaxer AT mail.ru>]

Hi Pierre,

Thanks a lot for clarification. I'm coming from engineering and traditional 
software background
and trying to formalize description of a system with a set of rules and prove 
that it satisfies
some properties. This formalization step does not look trivial for me either. 
It's quite possible
that the translation from the natural language into the formal one can be 
done differently
(either because of different interpretations of the original text or because 
of implicit assumptions
used during this translation). In particular, I wonder if such different 
translations require
different assumptions (such as classical logic) or even may lead to the 
statements that cannot
be proved at all.

The goal is to verify that indeed the system has all the expected properties 
as soon as all
the rules are met. It may require changes to the original wording of the 
rules, of course.

Just to give you an example, the original rule for the axiom I mention sounds 
like

    It is valid for a set of named objects to include an object c if and only 
if no other object of the set has the same name.

(I used N to denote a set of names, C to denote a set of objects, and F to 
denote the names associated with the objects.)

And the expected property is:

   If n is a name of a known object, then it denotes the object with this 
name.

(Or, in my words, given a name of an object present in the set, we can find 
exactly one object with this name.)

With the correction about equality, does the formalization reflect the 
original?

Best regards,
Alexander Kogtenkov


Tue, 22 Jul 2014 11:08:05 +0200 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