diff options
Diffstat (limited to 'test-suite/success/Funind.v')
-rw-r--r-- | test-suite/success/Funind.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index b17adef6..ccce3bbe 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -9,7 +9,7 @@ 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 |- *. + functional induction iszero x; simpl. trivial. inversion eg. Qed. @@ -212,19 +212,19 @@ Function 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. - functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto. + functional induction plus_x_not_five'' a b; intros hyp; simpl; 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. + functional induction nat_equal_bool n m; simpl; intros hyp; auto. 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. + functional induction nat_equal_bool n m; simpl; intros eg; auto. inversion eg. inversion eg. Qed. @@ -245,7 +245,7 @@ Qed. Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. intros n. -unfold plus in |- *. +unfold plus. functional induction plus n 0; intros. auto with arith. apply le_n_S. @@ -266,7 +266,7 @@ Function mod2 (n : nat) : nat := Lemma princ_mod2 : forall n : nat, mod2 n <= n. intros n. - functional induction mod2 n; simpl in |- *; auto with arith. + functional induction mod2 n; simpl; auto with arith. Qed. Function isfour (n : nat) : bool := @@ -284,7 +284,7 @@ Function isononeorfour (n : nat) : bool := Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). intros n. - functional induction isononeorfour n; intros istr; simpl in |- *; + functional induction isononeorfour n; intros istr; simpl; inversion istr. apply istrue0. destruct n. inversion istr. @@ -367,7 +367,7 @@ Function ftest2 (n m : nat) {struct n} : nat := Lemma test2' : forall n m : nat, ftest2 n m <= 2. intros n m. - functional induction ftest2 n m; simpl in |- *; intros; auto. + functional induction ftest2 n m; simpl; intros; auto. Qed. Function ftest3 (n m : nat) {struct n} : nat := @@ -387,7 +387,7 @@ auto. intros. auto. intros. -simpl in |- *. +simpl. auto. Qed. @@ -408,7 +408,7 @@ auto. intros. auto. intros. -simpl in |- *. +simpl. auto. Qed. @@ -451,7 +451,7 @@ Qed. Lemma essai6 : forall n m : nat, ftest6 n m <= 2. intros n m. - functional induction ftest6 n m; simpl in |- *; auto. + functional induction ftest6 n m; simpl; auto. Qed. (* Some tests with modules *) |