From 63fe9ca9438693fcf4d601c05f77a4db50588b40 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 20 May 2010 20:31:42 +0000
Subject: Added examples for checking that the guard condition excludes
 subterms in impredicative types.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13024 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/failure/fixpoint3.v | 13 +++++++++++++
 test-suite/failure/fixpoint4.v | 19 +++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 test-suite/failure/fixpoint3.v
 create mode 100644 test-suite/failure/fixpoint4.v

diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v
new file mode 100644
index 0000000000..42f06916b2
--- /dev/null
+++ b/test-suite/failure/fixpoint3.v
@@ -0,0 +1,13 @@
+(* Check that arguments of impredicative types are not considered
+   subterms for the guard condition (an example by Thierry Coquand) *)
+
+Inductive I : Prop :=
+| C: (forall P:Prop, P->P) -> I.
+
+Definition i0 := C (fun _ x => x).
+
+Definition Paradox : False :=
+ (fix ni i : False :=
+  match i with
+  | C f => ni (f _ i)
+  end) i0.
diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v
new file mode 100644
index 0000000000..fd9563738e
--- /dev/null
+++ b/test-suite/failure/fixpoint4.v
@@ -0,0 +1,19 @@
+(* Check that arguments of impredicative types are not considered
+   subterms even through commutative cuts on functional arguments
+   (example prepared by Bruno) *)
+
+Inductive IMP : Prop :=
+  CIMP : (forall A:Prop, A->A) -> IMP
+| LIMP : (nat->IMP)->IMP.
+
+Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))).
+
+Definition Paradox : False :=
+ (fix F y o {struct o} : False :=
+  match y with
+  | tt => fun f =>
+     match f 0 with
+     | CIMP h => F y (h _ o)
+     | _ => F y (f 0)
+     end
+  end match o with LIMP f => f | _ => fun _ => o end) tt i0.
-- 
cgit v1.2.3