coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: roconnor AT theorem.ca
- To: Chung Kil Hur <ckh25 AT cam.ac.uk>
- Cc: Agda mailing list <agda AT lists.chalmers.se>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Agda with the excluded middle is inconsistent ?
- Date: Fri, 8 Jan 2010 09:50:45 -0500 (EST)
I spent some time trying to extend Chung-Kil's proof to an outright contradiction, but Agda's predicativity thwarted my attempts. If Agda had an impredictiave Prop universe like Coq does, there would be an outright contradiciton. Below is my proof that Coq has non-injective type constructors:
Definition Type1 := Type.
Inductive I : (Type1 -> Type1) -> Type1 := .
Section ChungKil.
Hypothesis InjI : forall x y, I x = I y -> x = y.
Definition P (x:Type1) : Type1 := exists a, I a = x /\ (inhabited (a x) ->
False).
Definition p := I P.
Lemma contradiction : inhabited (P p) <-> (inhabited (P p) -> False).
Proof.
unfold P at 1.
unfold p at 1.
split.
intros [[a [Ha0 Ha1]]].
replace a with P in Ha1; [assumption|].
firstorder.
intros H.
constructor.
exists P.
firstorder.
Qed.
Lemma absurd : False.
assert (Z:=contradiction).
tauto.
Qed.
End ChungKil.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
- [Coq-Club] Agda with the excluded middle is inconsistent ?, Chung Kil Hur
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?, Dan Doel
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?, roconnor
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?, roconnor
- Message not available
- Message not available
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Andreas Abel
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Andreas Abel
- [Coq-Club] Re: [Agda] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
- Message not available
- Re: [Coq-Club] Agda with the excluded middle is inconsistent ?,
Chung Kil Hur
Archive powered by MhonArc 2.6.16.