diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/failure/guard-cofix.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/failure/guard-cofix.v')
-rw-r--r-- | test-suite/failure/guard-cofix.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test-suite/failure/guard-cofix.v b/test-suite/failure/guard-cofix.v new file mode 100644 index 00000000..64faa0ce --- /dev/null +++ b/test-suite/failure/guard-cofix.v @@ -0,0 +1,43 @@ +(* This script shows, in two different ways, the inconsistency of the +propositional extensionality axiom with the guard condition for cofixpoints. It +is the dual of the problem on fixpoints (cf subterm.v, subterm2.v, +subterm3.v). Posted on Coq-club by Maxime Dénès (02/26/2014). *) + +(* First example *) + +CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse. + +CoInductive Pandora : Prop := C : CoFalse -> Pandora. + +Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q. + +Lemma foo : Pandora = CoFalse. +apply prop_ext. +constructor. +intro x; destruct x; assumption. +exact C. +Qed. + +Fail CoFixpoint loop : CoFalse := +match foo in (_ = T) return T with eq_refl => C loop end. + +Fail Definition ff : False := match loop with CF _ t => t end. + +(* Second example *) + +Inductive omega := Omega : omega -> omega. + +Lemma H : omega = CoFalse. +Proof. +apply prop_ext; constructor. + induction 1; assumption. +destruct 1; destruct H0. +Qed. + +Fail CoFixpoint loop' : CoFalse := + match H in _ = T return T with + eq_refl => + Omega match eq_sym H in _ = T return T with eq_refl => loop' end + end. + +Fail Definition ff' : False := match loop' with CF _ t => t end.
\ No newline at end of file |