diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
| commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
| tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Bool/IfProp.v | |
| parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) | |
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool/IfProp.v')
| -rwxr-xr-x | theories/Bool/IfProp.v | 53 |
1 files changed, 27 insertions, 26 deletions
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 48180678f..bde404cf7 100755 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -8,42 +8,43 @@ (*i $Id$ i*) -Require Bool. +Require Import Bool. -Inductive IfProp [A,B:Prop] : bool-> Prop - := Iftrue : A -> (IfProp A B true) - | Iffalse : B -> (IfProp A B false). +Inductive IfProp (A B:Prop) : bool -> Prop := + | Iftrue : A -> IfProp A B true + | Iffalse : B -> IfProp A B false. -Hints Resolve Iftrue Iffalse : bool v62. +Hint Resolve Iftrue Iffalse: bool v62. -Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Auto with bool. +Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A. +destruct 1; intros; auto with bool. +case diff_true_false; auto with bool. Qed. -Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Trivial with bool. +Lemma Iffalse_inv : + forall (A B:Prop) (b:bool), IfProp A B b -> b = false -> B. +destruct 1; intros; auto with bool. +case diff_true_false; trivial with bool. Qed. -Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A. -Intros. -Inversion H. -Assumption. +Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. +intros. +inversion H. +assumption. Qed. -Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B. -Intros. -Inversion H. -Assumption. +Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. +intros. +inversion H. +assumption. Qed. -Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B. -NewDestruct 1; Auto with bool. +Lemma IfProp_or : forall (A B:Prop) (b:bool), IfProp A B b -> A \/ B. +destruct 1; auto with bool. Qed. -Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}. -NewDestruct b; Intro H. -Left; Inversion H; Auto with bool. -Right; Inversion H; Auto with bool. -Qed. +Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. +destruct b; intro H. +left; inversion H; auto with bool. +right; inversion H; auto with bool. +Qed.
\ No newline at end of file |