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.v98
1 files changed, 49 insertions, 49 deletions
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 08:25:11 +0000