Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?


chronological Thread 
  • From: Nicolas Magaud <Nicolas.Magaud AT sophia.inria.fr>
  • To: coq-club AT pauillac.inria.fr
  • Cc: Nicolas.Magaud AT sophia.inria.fr
  • Subject: [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?
  • Date: Mon, 04 Nov 2002 10:58:53 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello everybody !

In a word: I would like to know whether I can safely add the 
following axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)
in the Coq system.

Let me explain why:
In recent experiments in Coq, I face the following problem:

I have 2 properties Mylt and Myle and I have 
Mylt_le : (n,m:nat)(Mylt n m)<->(Myle (S n) m) as an assumption.

I want to prove the following property:
(P:Prop->Prop)(n,m:nat)(P (Myle (S n) m))->(P (Mylt n m))
As far as I know, it is not possible in the Coq system without
adding an axiom.

If I knew (n,m:nat)(Mylt n m)==(Myle (S n) m) with eqT instead of
<->, I could have performed rewriting with this equality.
Here is the corresponding code in Coq:
-------------------------------------------------------------------
Parameters Mylt,Myle:nat->nat->Prop.
Axiom Mylt_le' : (n,m:nat)(Mylt n m)==(Myle (S n) m).

Goal (P:Prop->Prop)(n,m:nat)(P (Myle (S n) m))->(P (Mylt n m)).
Intros P n m H ; Rewrite Mylt_le' ; Assumption.
Qed.
--------------------------------------------------------------------

Unfortunately, in my development, I can not prove Mylt_le' (the property
featuring Leibniz equality in Type ==) on my actual data structures.
However, I can easily establish that (n,m:nat)(Mylt n m)<->(Myle (S n) m)
using iff.

In that case, I choose to add a proof-irrevelance like axiom:
Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q).

Thanks to this axiom, I can prove my goal (see the script at the end 
of the message). 

But there remains a question. Was I right to add such an axiom ?
Is it safe for Coq's consistency ?

Thanks in advance for any clue about this issue.

Nicolas

---------------------------------------------------------------------
Parameters Mylt,Myle:nat->nat->Prop.
Axiom Mylt_le : (n,m:nat)(Mylt n m)<->(Myle (S n) m).
Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q).

Goal (P:Prop->Prop)(n,m:nat)(P (Myle (S n) m))->(P (Mylt n m)).
Intros P n m H.
Cut (Mylt n m)==(Myle (S n) m).
Intros Hrew; Rewrite Hrew; Assumption.

Apply iff_implies_eqT.
Apply Mylt_le.
Qed.
-----------------------------------------------------------------------







Archive powered by MhonArc 2.6.16.

Top of Page