summaryrefslogtreecommitdiff
path: root/test-suite/success/Funind.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/Funind.v')
-rw-r--r--test-suite/success/Funind.v119
1 files changed, 56 insertions, 63 deletions
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 20:10:17 +0000