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.
-----------------------------------------------------------------------
- [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?, Nicolas Magaud
- <Possible follow-ups>
- [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?,
Alexandre Miquel
- Re: [Coq-Club] Adding "Axiom iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q)." in Coq ?, Jean Goubault-Larrecq
Archive powered by MhonArc 2.6.16.