diff options
Diffstat (limited to 'theories/Arith/Plus.v')
| -rw-r--r-- | theories/Arith/Plus.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 6d510447..9b7c6261 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Plus.v 9750 2007-04-06 00:58:14Z letouzey $ i*) +(*i $Id$ i*) (** Properties of addition. [add] is defined in [Init/Peano.v] as: << -Fixpoint plus (n m:nat) {struct n} : nat := +Fixpoint plus (n m:nat) : nat := match n with | O => m | S p => S (p + m) @@ -65,7 +65,7 @@ Qed. Hint Resolve plus_assoc: arith v62. Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p). -Proof. +Proof. intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith. Qed. @@ -179,7 +179,7 @@ Definition plus_is_one : Proof. intro m; destruct m as [| n]; auto. destruct n; auto. - intros. + intros. simpl in H. discriminate H. Defined. @@ -187,18 +187,18 @@ Defined. Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q). Proof. - intros m n p q. + intros m n p q. rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q). rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc. Qed. (** * Tail-recursive plus *) -(** [tail_plus] is an alternative definition for [plus] which is +(** [tail_plus] is an alternative definition for [plus] which is tail-recursive, whereas [plus] is not. This can be useful when extracting programs. *) -Fixpoint tail_plus n m {struct n} : nat := +Fixpoint tail_plus n m : nat := match n with | O => m | S n => tail_plus n (S m) @@ -215,7 +215,7 @@ Lemma succ_plus_discr : forall n m, n <> S (plus m n). Proof. intros n m; induction n as [|n IHn]. discriminate. - intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; + intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; reflexivity. Qed. |