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/subterm3.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/failure/subterm3.v')
-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 00000000..2cef6357 --- /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. |