diff options
Diffstat (limited to 'theories/Bool/Zerob.v')
| -rwxr-xr-x | theories/Bool/Zerob.v | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 7880251619..6487d08e98 100755 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -8,29 +8,31 @@ (*i $Id$ i*) -Require Arith. -Require Bool. +Require Import Arith. +Require Import Bool. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Definition zerob : nat->bool - := [n:nat]Cases n of O => true | (S _) => false end. +Definition zerob (n:nat) : bool := + match n with + | O => true + | S _ => false + end. -Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true. -NewDestruct n; [Trivial with bool | Inversion 1]. +Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true. +destruct n; [ trivial with bool | inversion 1 ]. Qed. -Hints Resolve zerob_true_intro : bool. +Hint Resolve zerob_true_intro: bool. -Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O). -NewDestruct n; [Trivial with bool | Inversion 1]. +Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0. +destruct n; [ trivial with bool | inversion 1 ]. Qed. -Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false. -NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool]. +Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false. +destruct n; [ destruct 1; auto with bool | trivial with bool ]. Qed. -Hints Resolve zerob_false_intro : bool. +Hint Resolve zerob_false_intro: bool. -Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O). -NewDestruct n; [Intro H; Inversion H | Auto with bool]. -Qed. +Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. +destruct n; [ intro H; inversion H | auto with bool ]. +Qed.
\ No newline at end of file |