aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-25 18:07:44 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-25 18:07:44 +0000
commit0cc6076e7d4d92c1d899d450b2336dadbeb5f1b1 (patch)
tree388057bb70957e0b06431e57e3e248e47f4f0272 /test-suite/output
parenta4bd836942106154703e10805405e8b4e6eb11ee (diff)
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Fixpoint.out14
-rw-r--r--test-suite/output/Fixpoint.v23
2 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 62c9d3952..cbb387ce9 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,3 +9,17 @@ let fix f (m : nat) : nat := match m with
| S m' => f m'
end in f 0
: nat
+fix even_pos_odd_pos 2
+ with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+ omega.
+
+ apply odd_pos_even_pos in H.
+ omega.
+
+ intros.
+ destruct H.
+ apply even_pos_odd_pos in H.
+ omega.
+
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index fc27e8d28..2b13c2041 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -16,3 +16,26 @@ Check
end
in f 0.
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0.
+Proof.
+fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+ omega.
+ apply odd_pos_even_pos in H.
+ omega.
+ intros.
+ destruct H.
+ apply even_pos_odd_pos in H.
+ omega.
+Show Script.
+Qed.