diff options
Diffstat (limited to 'theories/Logic/Berardi.v')
| -rw-r--r-- | theories/Logic/Berardi.v | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 9f01c565..d72f4072 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -67,18 +67,13 @@ Variables A B : Prop. Record retract : Prop := {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. - Record retract_cond : Prop := {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. - (** The dependent elimination above implies the axiom of choice: *) -Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. -Proof. -intros r. -case r; simpl. -trivial. -Qed. + +Lemma AC : forall r:retract_cond, retract -> forall a:A, r.(j2) (r.(i2) a) = a. +Proof. intros r. exact r.(inv2). Qed. End Retracts. @@ -114,7 +109,7 @@ Proof. exists g f. intro a. unfold f, g; simpl. -apply AC. +apply AC. exists (fun x:pow U => x) (fun x:pow U => x). trivial. Qed. @@ -132,9 +127,10 @@ Lemma not_has_fixpoint : R R = Not_b (R R). Proof. unfold R at 1. unfold g. -rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). +rewrite AC. +trivial. +exists (fun x:pow U => x) (fun x:pow U => x). trivial. -exists (fun x:pow U => x) (fun x:pow U => x); trivial. Qed. |