From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- test-suite/success/Funind.v | 119 +++++++++++++++++++++----------------------- 1 file changed, 56 insertions(+), 63 deletions(-) (limited to 'test-suite/success/Funind.v') diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 84a58a3a..939d06c7 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -5,25 +5,17 @@ Definition iszero (n : nat) : bool := | _ => false end. - Functional Scheme iszer_ind := Induction for iszero. +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 |- *. trivial. - subst x. -inversion H_eq_. +inversion eg. Qed. -(* We can even reuse the proof as a scheme: *) - - Functional Scheme toto_ind := Induction for iszero. - - - - -Definition ftest (n m : nat) : nat := +Function ftest (n m : nat) : nat := match n with | O => match m with | O => 0 @@ -32,27 +24,25 @@ Definition ftest (n m : nat) : nat := | S p => 0 end. - Functional Scheme ftest_ind := Induction for ftest. - Lemma test1 : forall n m : nat, ftest n m <= 2. intros n m. functional induction ftest n m; auto. Qed. - +Require Import Arith. Lemma test11 : forall m : nat, ftest 0 m <= 2. intros m. functional induction ftest 0 m. auto. -auto. +auto. +auto with *. Qed. - -Definition lamfix (m : nat) := - fix trivfun (n : nat) : nat := match n with - | O => m - | S p => trivfun p - end. +Function lamfix (m n : nat) {struct n } : nat := + match n with + | O => m + | S p => lamfix m p + end. (* Parameter v1 v2 : nat. *) @@ -68,12 +58,12 @@ Defined. (* polymorphic function *) Require Import List. - Functional Scheme app_ind := Induction for app. +Functional Scheme app_ind := Induction for app Sort Prop. Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'. intros A l l'. functional induction app A l l'; intuition. - rewrite <- H1; trivial. + rewrite <- H0; trivial. Qed. @@ -83,7 +73,7 @@ Qed. Require Export Arith. -Fixpoint trivfun (n : nat) : nat := +Function trivfun (n : nat) : nat := match n with | O => 0 | S m => trivfun m @@ -97,18 +87,16 @@ Parameter varessai : nat. Lemma first_try : trivfun varessai = 0. functional induction trivfun varessai. trivial. -simpl in |- *. assumption. Defined. - Functional Scheme triv_ind := Induction for trivfun. + Functional Scheme triv_ind := Induction for trivfun Sort Prop. Lemma bisrepetita : forall n' : nat, trivfun n' = 0. intros n'. functional induction trivfun n'. trivial. -simpl in |- *. assumption. Qed. @@ -118,14 +106,14 @@ Qed. -Fixpoint iseven (n : nat) : bool := +Function iseven (n : nat) : bool := match n with | O => true | S (S m) => iseven m | _ => false end. -Fixpoint funex (n : nat) : nat := +Function funex (n : nat) : nat := match iseven n with | true => n | false => match n with @@ -134,7 +122,7 @@ Fixpoint funex (n : nat) : nat := end end. -Fixpoint nat_equal_bool (n m : nat) {struct n} : bool := +Function nat_equal_bool (n m : nat) {struct n} : bool := match n with | O => match m with | O => true @@ -149,6 +137,7 @@ Fixpoint 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. functional induction div2 n. @@ -157,34 +146,27 @@ auto. apply le_S. apply le_n_S. -exact H. +exact IHn0. Qed. (* reuse this lemma as a scheme:*) - Functional Scheme div2_ind := Induction for div2_inf. -Fixpoint nested_lam (n : nat) : nat -> nat := +Function nested_lam (n : nat) : nat -> nat := match n with | O => fun m : nat => 0 | S n' => fun m : nat => m + nested_lam n' m end. - Functional Scheme nested_lam_ind := Induction for nested_lam. Lemma nest : forall n m : nat, nested_lam n m = n * m. intros n m. - functional induction nested_lam n m; auto. -Qed. - -Lemma nest2 : forall n m : nat, nested_lam n m = n * m. -intros n m. pattern n, m in |- *. -apply nested_lam_ind; simpl in |- *; intros; auto. + functional induction nested_lam n m; simpl;auto. Qed. -Fixpoint essai (x : nat) (p : nat * nat) {struct x} : nat := - let (n, m) := p in +Function essai (x : nat) (p : nat * nat) {struct x} : nat := + let (n, m) := (p: nat*nat) in match n with | O => 0 | S q => match x with @@ -198,12 +180,12 @@ Lemma essai_essai : intros x p. functional induction essai x p; intros. inversion H. -simpl in |- *; try abstract auto with arith. -simpl in |- *; try abstract auto with arith. +auto with arith. + auto with arith. Qed. -Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat := +Function plus_x_not_five'' (n m : nat) {struct n} : nat := let x := nat_equal_bool m 5 in let y := 0 in match n with @@ -218,21 +200,18 @@ Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat := Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. intros a b. -unfold plus_x_not_five'' in |- *. 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. -unfold nat_equal_bool in |- *. functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto. -inversion hyp. +rewrite <- hyp in H1; simpl in H1;tauto. inversion hyp. Qed. Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. intros n m. -unfold nat_equal_bool in |- *. functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto. inversion eg. inversion eg. @@ -242,6 +221,8 @@ 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. intros n m. functional induction plus n m; intros. @@ -264,7 +245,7 @@ intros n. functional induction plus 0 n; intros; auto with arith. Qed. -Fixpoint mod2 (n : nat) : nat := +Function mod2 (n : nat) : nat := match n with | O => 0 | S (S m) => S (mod2 m) @@ -276,13 +257,13 @@ intros n. functional induction mod2 n; simpl in |- *; auto with arith. Qed. -Definition isfour (n : nat) : bool := +Function isfour (n : nat) : bool := match n with | S (S (S (S O))) => true | _ => false end. -Definition isononeorfour (n : nat) : bool := +Function isononeorfour (n : nat) : bool := match n with | S O => true | S (S (S (S O))) => true @@ -294,15 +275,22 @@ intros n. functional induction isononeorfour n; intros istr; simpl in |- *; inversion istr. apply istrue0. +destruct n. inversion istr. +destruct n. tauto. +destruct n. inversion istr. +destruct n. inversion istr. +destruct n. tauto. +simpl in *. inversion H1. 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 H0; simpl in H0;tauto. Qed. -Definition ftest4 (n m : nat) : nat := +Function ftest4 (n m : nat) : nat := match n with | O => match m with | O => 0 @@ -321,13 +309,20 @@ Qed. Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. intros n m. - functional induction ftest4 (S n) m. +assert ({n0 | n0 = S n}). +exists (S n);reflexivity. +destruct H as [n0 H1]. +rewrite <- H1;revert H1. + functional induction ftest4 n0 m. +inversion 1. +inversion 1. + auto with arith. auto with arith. Qed. -Definition ftest44 (x : nat * nat) (n m : nat) : nat := - let (p, q) := x in +Function ftest44 (x : nat * nat) (n m : nat) : nat := + let (p, q) := (x: nat*nat) in match n with | O => match m with | O => 0 @@ -349,7 +344,7 @@ auto with arith. auto with arith. Qed. -Fixpoint ftest2 (n m : nat) {struct n} : nat := +Function ftest2 (n m : nat) {struct n} : nat := match n with | O => match m with | O => 0 @@ -363,7 +358,7 @@ intros n m. functional induction ftest2 n m; simpl in |- *; intros; auto. Qed. -Fixpoint ftest3 (n m : nat) {struct n} : nat := +Function ftest3 (n m : nat) {struct n} : nat := match n with | O => 0 | S p => match m with @@ -384,7 +379,7 @@ simpl in |- *. auto. Qed. -Fixpoint ftest5 (n m : nat) {struct n} : nat := +Function ftest5 (n m : nat) {struct n} : nat := match n with | O => 0 | S p => match m with @@ -405,7 +400,7 @@ simpl in |- *. auto. Qed. -Definition ftest7 (n : nat) : nat := +Function ftest7 (n : nat) : nat := match ftest5 n 0 with | O => 0 | S r => 0 @@ -416,11 +411,10 @@ Lemma essai7 : (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) (n : nat), ftest7 n <= 2. intros hyp1 hyp2 n. -unfold ftest7 in |- *. functional induction ftest7 n; auto. Qed. -Fixpoint ftest6 (n m : nat) {struct n} : nat := +Function ftest6 (n m : nat) {struct n} : nat := match n with | O => 0 | S p => match ftest5 p 0 with @@ -445,7 +439,6 @@ Qed. Lemma essai6 : forall n m : nat, ftest6 n m <= 2. intros n m. -unfold ftest6 in |- *. functional induction ftest6 n m; simpl in |- *; auto. Qed. -- cgit v1.2.3