diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2014-04-08 22:07:58 -0400 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2014-07-22 17:55:06 -0400 |
commit | 4cd0becc84208525443d7ca4e9cc8214d00df319 (patch) | |
tree | b8088558a7a4f3841776bdfc2d1d2d871b0f10c1 /test-suite/failure | |
parent | 3c9f42251c7552d4a53f93af27b3134c64a3f916 (diff) |
Add test-suite file for guard condition on cofixpoints.
Diffstat (limited to 'test-suite/failure')
-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 000000000..64faa0ce0 --- /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 |