From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- test-suite/success/Funind.v | 98 ++++++++++++++++++++++----------------------- 1 file changed, 49 insertions(+), 49 deletions(-) (limited to 'test-suite/success/Funind.v') diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 1c3e56f2..b17adef6 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -6,7 +6,7 @@ Definition iszero (n : nat) : bool := end. Functional Scheme iszero_ind := Induction for iszero Sort Prop. - + Lemma toto : forall n : nat, n = 0 -> iszero n = true. intros x eg. functional induction iszero x; simpl in |- *. @@ -14,7 +14,7 @@ trivial. inversion eg. Qed. - + Function ftest (n m : nat) : nat := match n with | O => match m with @@ -30,7 +30,7 @@ intros n m. Qed. Lemma test2 : forall m n, ~ 2 = ftest n m. -Proof. +Proof. intros n m;intro H. functional inversion H ftest. Qed. @@ -45,9 +45,9 @@ Require Import Arith. Lemma test11 : forall m : nat, ftest 0 m <= 2. intros m. functional induction ftest 0 m. -auto. auto. -auto with *. +auto. +auto with *. Qed. Function lamfix (m n : nat) {struct n } : nat := @@ -92,7 +92,7 @@ Function trivfun (n : nat) : nat := end. -(* essaie de parametre variables non locaux:*) +(* essaie de parametre variables non locaux:*) Parameter varessai : nat. @@ -101,7 +101,7 @@ Lemma first_try : trivfun varessai = 0. trivial. assumption. Defined. - + Functional Scheme triv_ind := Induction for trivfun Sort Prop. @@ -134,7 +134,7 @@ Function funex (n : nat) : nat := | S r => funex r end end. - + Function nat_equal_bool (n m : nat) {struct n} : bool := match n with @@ -150,7 +150,7 @@ Function nat_equal_bool (n m : nat) {struct n} : bool := Require Export Div2. - + Functional Scheme div2_ind := Induction for div2 Sort Prop. Lemma div2_inf : forall n : nat, div2 n <= n. intros n. @@ -177,7 +177,7 @@ intros n m. functional induction nested_lam n m; simpl;auto. Qed. - + Function essai (x : nat) (p : nat * nat) {struct x} : nat := let (n, m) := (p: nat*nat) in match n with @@ -187,7 +187,7 @@ Function essai (x : nat) (p : nat * nat) {struct x} : nat := | S r => S (essai r (q, m)) end end. - + Lemma essai_essai : forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p. intros x p. @@ -209,30 +209,30 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat := | false => S recapp end end. - + Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. intros a b. functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto. Qed. - + Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. intros n m. functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto. -rewrite <- hyp in y; simpl in y;tauto. +rewrite <- hyp in y; simpl in y;tauto. inversion hyp. Qed. - + Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. intros n m. functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto. inversion eg. inversion eg. Qed. - - + + Inductive istrue : bool -> Prop := istrue0 : istrue true. - + Functional Scheme plus_ind := Induction for plus Sort Prop. Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. @@ -242,7 +242,7 @@ auto with arith. auto with arith. Qed. - + Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. intros n. unfold plus in |- *. @@ -251,7 +251,7 @@ auto with arith. apply le_n_S. assumption. Qed. - + Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x. intros n. functional induction plus 0 n; intros; auto with arith. @@ -263,25 +263,25 @@ Function mod2 (n : nat) : nat := | S (S m) => S (mod2 m) | _ => 0 end. - + Lemma princ_mod2 : forall n : nat, mod2 n <= n. intros n. functional induction mod2 n; simpl in |- *; auto with arith. Qed. - + Function isfour (n : nat) : bool := match n with | S (S (S (S O))) => true | _ => false end. - + Function isononeorfour (n : nat) : bool := match n with | S O => true | S (S (S (S O))) => true | _ => false end. - + Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). intros n. functional induction isononeorfour n; intros istr; simpl in |- *; @@ -294,14 +294,14 @@ destruct n. inversion istr. destruct n. tauto. simpl in *. inversion H0. Qed. - + Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n). intros n. functional induction isononeorfour n; intros m istr; inversion istr. apply istrue0. rewrite H in y; simpl in y;tauto. Qed. - + Function ftest4 (n m : nat) : nat := match n with | O => match m with @@ -313,12 +313,12 @@ Function ftest4 (n m : nat) : nat := | S r => 1 end end. - + Lemma test4 : forall n m : nat, ftest n m <= 2. intros n m. functional induction ftest n m; auto with arith. Qed. - + Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. intros n m. assert ({n0 | n0 = S n}). @@ -332,7 +332,7 @@ inversion 1. auto with arith. auto with arith. Qed. - + Function ftest44 (x : nat * nat) (n m : nat) : nat := let (p, q) := (x: nat*nat) in match n with @@ -345,7 +345,7 @@ Function ftest44 (x : nat * nat) (n m : nat) : nat := | S r => 1 end end. - + Lemma test44 : forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2. intros pq n m o r s. @@ -355,7 +355,7 @@ auto with arith. auto with arith. auto with arith. Qed. - + Function ftest2 (n m : nat) {struct n} : nat := match n with | O => match m with @@ -364,12 +364,12 @@ Function ftest2 (n m : nat) {struct n} : nat := end | S p => ftest2 p m end. - + Lemma test2' : forall n m : nat, ftest2 n m <= 2. intros n m. functional induction ftest2 n m; simpl in |- *; intros; auto. Qed. - + Function ftest3 (n m : nat) {struct n} : nat := match n with | O => 0 @@ -378,7 +378,7 @@ Function ftest3 (n m : nat) {struct n} : nat := | S r => 0 end end. - + Lemma test3' : forall n m : nat, ftest3 n m <= 2. intros n m. functional induction ftest3 n m. @@ -390,7 +390,7 @@ intros. simpl in |- *. auto. Qed. - + Function ftest5 (n m : nat) {struct n} : nat := match n with | O => 0 @@ -399,7 +399,7 @@ Function ftest5 (n m : nat) {struct n} : nat := | S r => ftest5 p r end end. - + Lemma test5 : forall n m : nat, ftest5 n m <= 2. intros n m. functional induction ftest5 n m. @@ -411,21 +411,21 @@ intros. simpl in |- *. auto. Qed. - + Function ftest7 (n : nat) : nat := match ftest5 n 0 with | O => 0 | S r => 0 end. - + Lemma essai7 : forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2) - (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) + (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) (n : nat), ftest7 n <= 2. intros hyp1 hyp2 n. functional induction ftest7 n; auto. Qed. - + Function ftest6 (n m : nat) {struct n} : nat := match n with | O => 0 @@ -435,7 +435,7 @@ Function ftest6 (n m : nat) {struct n} : nat := end end. - + Lemma princ6 : (forall n m : nat, n = 0 -> ftest6 0 m <= 2) -> (forall n m p : nat, @@ -448,16 +448,16 @@ generalize hyp1 hyp2 hyp3. clear hyp1 hyp2 hyp3. functional induction ftest6 n m; auto. Qed. - + Lemma essai6 : forall n m : nat, ftest6 n m <= 2. intros n m. functional induction ftest6 n m; simpl in |- *; auto. Qed. -(* Some tests with modules *) +(* Some tests with modules *) Module M. -Function test_m (n:nat) : nat := - match n with +Function test_m (n:nat) : nat := + match n with | 0 => 0 | S n => S (S (test_m n)) end. @@ -470,14 +470,14 @@ reflexivity. simpl;rewrite IHn0;reflexivity. Qed. End M. -(* We redefine a new Function with the same name *) -Function test_m (n:nat) : nat := +(* We redefine a new Function with the same name *) +Function test_m (n:nat) : nat := pred n. Lemma test_m_is_pred : forall n, test_m n = pred n. -Proof. +Proof. intro n. -functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) +functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) reflexivity. Qed. -- cgit v1.2.3