diff options
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 6a636ccc..ae79744f 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic.v 10304 2007-11-08 17:06:32Z emakarov $ i*) +(*i $Id: Logic.v 11735 2009-01-02 17:22:31Z herbelin $ i*) Set Implicit Arguments. @@ -150,6 +150,16 @@ Proof. intros; tauto. Qed. +Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A). +Proof. +intros A B []; split; trivial. +Qed. + +Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A). +Proof. +intros; tauto. +Qed. + (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes either [P] and [Q], or [~P] and [Q] *) @@ -245,8 +255,8 @@ Implicit Arguments eq_ind [A]. Implicit Arguments eq_rec [A]. Implicit Arguments eq_rect [A]. -Hint Resolve I conj or_introl or_intror refl_equal: core v62. -Hint Resolve ex_intro ex_intro2: core v62. +Hint Resolve I conj or_introl or_intror refl_equal: core. +Hint Resolve ex_intro ex_intro2: core. Section Logic_lemmas. @@ -339,7 +349,7 @@ Proof. destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity. Qed. -Hint Immediate sym_eq sym_not_eq: core v62. +Hint Immediate sym_eq sym_not_eq: core. (** Basic definitions about relations and properties *) |