From 0cc6076e7d4d92c1d899d450b2336dadbeb5f1b1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 25 Apr 2008 18:07:44 +0000 Subject: 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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- test-suite/output/Fixpoint.out | 14 ++++++++++++++ test-suite/output/Fixpoint.v | 23 +++++++++++++++++++++++ 2 files changed, 37 insertions(+) (limited to 'test-suite/output') 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. -- cgit v1.2.3