diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2013-12-21 13:50:11 -0500 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2013-12-21 13:50:11 -0500 |
commit | 66e426a93fc00682128a0441d6dda3425e0be252 (patch) | |
tree | 87a5994466b91c7cf027aa3a68a9fd524ab0be6a /test-suite/failure | |
parent | 8ba7983f467a6e235ba88e10be90381c9429cad2 (diff) |
Test case for the buggy commutative cut subterm rule.
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/subterm3.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/failure/subterm3.v b/test-suite/failure/subterm3.v new file mode 100644 index 000000000..2cef63575 --- /dev/null +++ b/test-suite/failure/subterm3.v @@ -0,0 +1,29 @@ +(* An example showing that prop-extensionality is incompatible with + powerful extensions of the guard condition. + This is a variation on the example in subterm2, exploiting + missing typing constraints in the commutative cut subterm rule + (subterm2 is using the same flaw but for the match rule). + + Example due to Cristóbal Camarero on Coq-Club. + *) + +Axiom prop_ext: forall P Q, (P <-> Q) -> P=Q. + +Inductive True2 : Prop := I3 : (False -> True2) -> True2. + +Theorem T3T: True2 = True. +Proof. +apply prop_ext; split; auto. +intros; constructor; apply False_rect. +Qed. + +Theorem T3F_FT3F : (True2 -> False) = ((False -> True2) -> False). +Proof. +rewrite T3T. +apply prop_ext; split; auto. +Qed. + +Fail Fixpoint loop (x : True2) : False := +match x with +I3 f => (match T3F_FT3F in _=T return T with eq_refl=> loop end) f +end. |