From 66e426a93fc00682128a0441d6dda3425e0be252 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 21 Dec 2013 13:50:11 -0500 Subject: Test case for the buggy commutative cut subterm rule. --- test-suite/failure/subterm3.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 test-suite/failure/subterm3.v (limited to 'test-suite/failure') 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. -- cgit v1.2.3