The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Dear José Grimm,

 

In your GAIA it is sometimes used = instead of <->. Accordingly the below opinion of Daniel Schepler it is not good. Should we rewrite GAIA to use <-> not = for propositions?

 

How we will maintain GAIA? Maybe I may become a maintainer? (I haven't yet decided to take time for this.)

Well, AFAIK, with <-> it does not work ~= constuct in declarative proofs.

Taking this into account, maybe we will leave =? What's your opinion Daniel Schepler?

17.11.2011, 05:57, "Daniel Schepler" <dschepler AT gmail.com>:

On Wed, Nov 16, 2011 at 6:12 AM, Victor Porton <porton AT narod.ru> wrote:

Dear Jose Grimm,

I consider to build a system of type classes expressing posets/lattices theory on the top of ZF in your GAIA (and afterward to formalize my research).

I am a beginner with Coq but consider to spend my time to learn it.

My questions:

What is the better way to express equivalence of propositions A and B: [A=B] or [A<->B]? When use [A=B] and when [A<->B]?

A<->B is better.  Even in classical mathematics, I never heard anybody talk about equality of propositions (except maybe regarding syntactic equality of proposition representations in model theory, which is strictly stronger), just equivalence.

Note that with "Require Import Setoid." you gain the ability to use rewrite with <-> statements.

How having [A<->B] to deduce [A=B] (and vice versa)?

It's easy to prove (P=Q) -> (P<->Q).

The reverse direction is what I think would be called "propositional extensionality".  One axiom from the standard library which implies this is Extensionality_Ensembles.  (Hint for the proof: "Prop" is essentially equivalent to "Ensemble unit".)  In fact, Extensionality_Ensembles is essentially propositional extensionality combined with a special case of functional extensionality.

Looking forward for your reply.

--
Best wishes.
Victor Porton - http://portonvictor.org

--
Daniel Schepler

--
Victor Porton - http://portonvictor.org