diff options
author | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-27 15:12:27 +0000 |
---|---|---|
committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-27 15:12:27 +0000 |
commit | c7b40c6ce35eb54f708d5d91ef264f6be92949c0 (patch) | |
tree | 88325df730614deb1832f5f5634f63d8a1e9aae3 /test-suite/success | |
parent | 97ad592fc2b52d6d2fc3ec3f6196b96380830457 (diff) |
Adding tests for the "functional induction" facility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Funind.v | 371 |
1 files changed, 371 insertions, 0 deletions
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v new file mode 100644 index 000000000..9e509a21d --- /dev/null +++ b/test-suite/success/Funind.v @@ -0,0 +1,371 @@ +Require Export Arith. + +Fixpoint trivfun [n : nat] : nat := + Cases n of O => O | (S m) => (trivfun m) end. + + +(* essaie de parametre variables non locaux:*) + +Parameter varessai:nat. + +Lemma first_try (trivfun varessai) = O. +Functional Induction trivfun varessai. +Trivial. +Simpl. +Assumption. +Defined. + + +Functional Scheme triv_ind := Induction for trivfun. + +Lemma bisrepetita:(n' : nat) (trivfun n') = O. +Intros n'. +Functional Induction trivfun n'. +Trivial. +Simpl. +Assumption. +Save. + + +Fixpoint iseven [n : nat] : bool := + Cases n of O => true | (S (S m)) => (iseven m) | _ => false end. + +Fixpoint funex [n : nat] : nat := + Cases (iseven n) of + true => n + | false => + Cases n of O => O | (S r) => (funex r) end + end. + +Fixpoint nat_equal_bool [n : nat] : nat -> bool := + [m : nat] Cases n of + O => + Cases m of O => true | _ => false end + | (S p) => + Cases m of O => false | (S q) => (nat_equal_bool p q) end + end. +Require Export Div2. + +Lemma div2_inf: (n : nat) (le (div2 n) n). +Intros n. +(Functional Induction div2 n). +Auto with arith. +Auto with arith. + +Simpl. +Apply le_S. +Apply le_n_S. +Exact H. +Qed. + +Fixpoint essai [x : nat] : nat * nat -> nat := + [p : nat * nat] ( Case p of [n, m : ?] Cases n of + O => O + | (S q) => + Cases x of + O => (S O) + | (S r) => (S (essai r (q, m))) + end + end end ). + +Lemma essai_essai: + (x : nat) + (p : nat * nat) ( Case p of [n, m : ?] (lt O n) -> (lt O (essai x p)) end ). +Intros x p. +(Functional Induction essai x p); Intros. +Inversion H. +Simpl; Try Abstract ( Auto with arith ). +Simpl; Try Abstract ( Auto with arith ). +Qed. + +Fixpoint plus_x_not_five' [n : nat] : nat -> nat := + [m : nat] Cases n of + O => O + | (S q) => + Cases m of + O => (S (plus_x_not_five' q O)) + | (S r) => (S (plus_x_not_five' q (S r))) + end + end. + +Lemma notplusfive': + (x, y : nat) y = (S (S (S (S (S O))))) -> (plus_x_not_five' x y) = x. +Intros x y. +(Functional Induction plus_x_not_five' x y); Intros hyp. +Auto. +Inversion hyp. +Intros. +Simpl. +Auto. +Qed. + +Fixpoint plus_x_not_five [n : nat] : nat -> nat := + [m : nat] + Cases n of + O => O + | (S q) => + Cases (nat_equal_bool m (S q)) of true => (S (plus_x_not_five q m)) + | false => (S (plus_x_not_five q m)) + end + end. + +Lemma notplusfive: + (x, y : nat) y = (S (S (S (S (S O))))) -> (plus_x_not_five x y) = x. +Intros x y. +Unfold plus_x_not_five. +(Functional Induction plus_x_not_five x y) ; Simpl; Intros hyp; + Fold plus_x_not_five. +Auto. +Auto. +Auto. +Qed. + +Fixpoint plus_x_not_five'' [n : nat] : nat -> nat := + [m : nat] let x = (nat_equal_bool m (S (S (S (S (S O)))))) in + let y = O in + Cases n of + O => y + | (S q) => + let recapp = (plus_x_not_five'' q m) in + Cases x of true => (S recapp) | false => (S recapp) end + end. + +Lemma notplusfive'': + (x, y : nat) y = (S (S (S (S (S O))))) -> (plus_x_not_five'' x y) = x. +Intros a b. +Unfold plus_x_not_five''. +(Functional Induction plus_x_not_five'' a b); Intros hyp; Simpl; Auto. +Qed. + +Lemma iseq_eq: (n, m : nat) n = m -> (nat_equal_bool n m) = true. +Intros n m. +Unfold nat_equal_bool. +(Functional Induction nat_equal_bool n m); Simpl; Intros hyp; Auto. +Inversion hyp. +Inversion hyp. +Qed. + +Lemma iseq_eq': (n, m : nat) (nat_equal_bool n m) = true -> n = m. +Intros n m. +Unfold nat_equal_bool. +(Functional Induction nat_equal_bool n m); Simpl; Intros eg; Auto. +Inversion eg. +Inversion eg. +Qed. + +Definition iszero : nat -> bool := + [n : nat] Cases n of O => true | _ => false end. + +Inductive istrue : bool -> Prop := + istrue0: (istrue true) . + +Lemma toto: (n : nat) n = O -> (istrue (iszero n)). +Intros x. +(Functional Induction iszero x); Intros eg; Simpl. +Apply istrue0. +Inversion eg. +Qed. + +Lemma inf_x_plusxy': (x, y : nat) (le x (plus x y)). +Intros n m. +(Functional Induction plus n m); Intros. +Auto with arith. +Auto with arith. +Qed. + + +Lemma inf_x_plusxy'': (x : nat) (le x (plus x O)). +Intros n. +Unfold plus. +(Functional Induction plus n O); Intros. +Auto with arith. +Apply le_n_S. +Assumption. +Qed. + +Lemma inf_x_plusxy''': (x : nat) (le x (plus O x)). +Intros n. +(Functional Induction plus O n); Intros;Auto with arith. +Qed. + +Fixpoint mod2 [n : nat] : nat := + Cases n of O => O + | (S (S m)) => (S (mod2 m)) + | _ => O end. + +Lemma princ_mod2: (n : nat) (le (mod2 n) n). +Intros n. +(Functional Induction mod2 n); Simpl; Auto with arith. +Qed. + +Definition isfour : nat -> bool := + [n : nat] Cases n of (S (S (S (S O)))) => true | _ => false end. + +Definition isononeorfour : nat -> bool := + [n : nat] Cases n of (S O) => true + | (S (S (S (S O)))) => true + | _ => false end. + +Lemma toto'': (n : nat) (istrue (isfour n)) -> (istrue (isononeorfour n)). +Intros n. +(Functional Induction isononeorfour n); Intros istr; Simpl; Inversion istr. +Apply istrue0. +Qed. + +Lemma toto': (n, m : nat) n = (S (S (S (S O)))) -> (istrue (isononeorfour n)). +Intros n. +(Functional Induction isononeorfour n); Intros m istr; Inversion istr. +Apply istrue0. +Qed. + +Definition ftest : nat -> nat -> nat := + [n, m : nat] Cases n of + O => + Cases m of O => O | _ => (S O) end + | (S p) => O + end. + +Lemma test1: (n, m : nat) (le (ftest n m) (S (S O))). +Intros n m. +(Functional Induction ftest n m); Auto with arith. +Qed. + +Lemma test11: (m : nat) (le (ftest O m) (S (S O))). +Intros m. +(Functional Induction ftest O m). +Auto with arith. +Auto with arith. +Qed. + +Definition ftest4 : nat -> nat -> nat := + [n, m : nat] Cases n of + O => + Cases m of O => O | (S q) => (S O) end + | (S p) => + Cases m of O => O | (S r) => (S O) end + end. + +Lemma test4: (n, m : nat) (le (ftest n m) (S (S O))). +Intros n m. +(Functional Induction ftest n m); Auto with arith. +Qed. + +Lemma test4': (n, m : nat) (le (ftest4 (S n) m) (S (S O))). +Intros n m. +(Functional Induction ftest4 (S n) m). +Auto with arith. +Auto with arith. +Qed. + +Definition ftest44 : nat * nat -> nat -> nat -> nat := + [x : nat * nat] + [n, m : nat] + ( Case x of [p, q : ?] Cases n of + O => + Cases m of O => O | (S q) => (S O) end + | (S p) => + Cases m of O => O | (S r) => (S O) end + end end ). + +Lemma test44: + (pq : nat * nat) (n, m, o, r, s : nat) (le (ftest44 pq n (S m)) (S (S O))). +Intros pq n m o r s. +(Functional Induction ftest44 pq n (S m)). +Auto with arith. +Auto with arith. +Auto with arith. +Auto with arith. +Qed. + +Fixpoint ftest2 [n : nat] : nat -> nat := + [m : nat] Cases n of + O => + Cases m of O => O | (S q) => O end + | (S p) => (ftest2 p m) + end. + +Lemma test2: (n, m : nat) (le (ftest2 n m) (S (S O))). +Intros n m. +(Functional Induction ftest2 n m) ; Simpl; Intros; Auto. +Qed. + +Fixpoint ftest3 [n : nat] : nat -> nat := + [m : nat] Cases n of + O => O + | (S p) => + Cases m of O => (ftest3 p O) | (S r) => O end + end. + +Lemma test3: (n, m : nat) (le (ftest3 n m) (S (S O))). +Intros n m. +(Functional Induction ftest3 n m). +Intros. +Auto. +Intros. +Auto. +Intros. +Simpl. +Auto. +Qed. + +Fixpoint ftest5 [n : nat] : nat -> nat := + [m : nat] Cases n of + O => O + | (S p) => + Cases m of O => (ftest5 p O) | (S r) => (ftest5 p r) end + end. + +Lemma test5: (n, m : nat) (le (ftest5 n m) (S (S O))). +Intros n m. +(Functional Induction ftest5 n m). +Intros. +Auto. +Intros. +Auto. +Intros. +Simpl. +Auto. +Qed. + +Definition ftest7 : (n : nat) nat := + [n : nat] Cases (ftest5 n O) of O => O | (S r) => O end. + +Lemma essai7: + (Hrec : (n : nat) (ftest5 n O) = O -> (le (ftest7 n) (S (S O)))) + (Hrec0 : (n, r : nat) (ftest5 n O) = (S r) -> (le (ftest7 n) (S (S O)))) + (n : nat) (le (ftest7 n) (S (S O))). +Intros hyp1 hyp2 n. +Unfold ftest7. +(Functional Induction ftest7 n); Auto. +Qed. + +Fixpoint ftest6 [n : nat] : nat -> nat := + [m : nat] + Cases n of + O => O + | (S p) => + Cases (ftest5 p O) of O => (ftest6 p O) | (S r) => (ftest6 p r) end + end. + + +Lemma princ6: + ((n, m : nat) n = O -> (le (ftest6 O m) (S (S O)))) -> + ((n, m, p : nat) + (le (ftest6 p O) (S (S O))) -> + (ftest5 p O) = O -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) -> + ((n, m, p, r : nat) + (le (ftest6 p r) (S (S O))) -> + (ftest5 p O) = (S r) -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) -> + (x, y : nat) (le (ftest6 x y) (S (S O))). +Intros hyp1 hyp2 hyp3 n m. +Generalize hyp1 hyp2 hyp3. +Clear hyp1 hyp2 hyp3. +(Functional Induction ftest6 n m);Auto. +Qed. + +Lemma essai6: (n, m : nat) (le (ftest6 n m) (S (S O))). +Intros n m. +Unfold ftest6. +(Functional Induction ftest6 n m); Simpl; Auto. +Qed. + |