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/subterm2.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/failure/subterm2.v')
-rw-r--r-- | test-suite/failure/subterm2.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/test-suite/failure/subterm2.v b/test-suite/failure/subterm2.v new file mode 100644 index 00000000..a420a4d7 --- /dev/null +++ b/test-suite/failure/subterm2.v @@ -0,0 +1,48 @@ +(* An example showing that prop-extensionality is incompatible with + powerful extensions of the guard condition. + Unlike the example in guard2, it is not exploiting the fact that + the elimination of False always produces a subterm. + + Example due to Cristobal Camarero on Coq-Club. + Adapted to nested types by Bruno Barras. + *) + +Axiom prop_ext: forall P Q, (P<->Q)->P=Q. + +Module Unboxed. + +Inductive True2:Prop:= I2: (False->True2)->True2. + +Theorem Heq: (False->True2)=True2. +Proof. +apply prop_ext. split. +- intros. constructor. exact H. +- intros. exact H. +Qed. + +Fail Fixpoint con (x:True2) :False := +match x with +I2 f => con (match Heq in _=T return T with eq_refl => f end) +end. + +End Unboxed. + +(* This boxed example shows that it is not enough to just require + that the return type of the match on Heq is an inductive type + *) +Module Boxed. + +Inductive box (T:Type) := Box (_:T). +Definition unbox {T} (b:box T) : T := let (x) := b in x. + +Inductive True2:Prop:= I2: box(False->True2)->True2. + +Definition Heq: (False->True2) <-> True2 := + conj (fun f => I2 (Box _ f)) (fun x _ => x). + +Fail Fixpoint con (x:True2) :False := +match x with +I2 f => con (unbox(match prop_ext _ _ Heq in _=T return box T with eq_refl => f end)) +end. + +End Boxed. |