refactor(library/logic/connectives): make dependence prop <- eq <- basic
This commit is contained in:
parent
8719dff361
commit
1011a8022c
4 changed files with 65 additions and 62 deletions
|
@ -11,7 +11,7 @@ namespace nonempty
|
|||
inductive nonempty (A : Type) : Prop :=
|
||||
nonempty_intro : A → nonempty A
|
||||
|
||||
definition nonempty_elim {A : Type} {B : Type} (H1 : nonempty A) (H2 : A → B) : B :=
|
||||
definition nonempty_elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
|
||||
nonempty_rec H2 H1
|
||||
|
||||
theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
|
||||
|
|
|
@ -2,61 +2,7 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
import general_notation .prop
|
||||
|
||||
-- implication
|
||||
-- -----------
|
||||
|
||||
abbreviation imp (a b : Prop) : Prop := a → b
|
||||
|
||||
|
||||
-- true and false
|
||||
-- --------------
|
||||
|
||||
inductive false : Prop
|
||||
|
||||
theorem false_elim (c : Prop) (H : false) : c :=
|
||||
false_rec c H
|
||||
|
||||
inductive true : Prop :=
|
||||
trivial : true
|
||||
|
||||
abbreviation not (a : Prop) := a → false
|
||||
prefix `¬` := not
|
||||
|
||||
|
||||
-- not
|
||||
-- ---
|
||||
|
||||
theorem not_intro {a : Prop} (H : a → false) : ¬a := H
|
||||
|
||||
theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
|
||||
|
||||
theorem absurd {a : Prop} (H1 : a) (H2 : ¬a) : false := H2 H1
|
||||
|
||||
theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
|
||||
assume Hna : ¬a, absurd Ha Hna
|
||||
|
||||
theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
|
||||
assume Ha : a, absurd (H1 Ha) H2
|
||||
|
||||
theorem absurd_elim {a : Prop} {b : Prop} (H1 : a) (H2 : ¬a) : b :=
|
||||
false_elim b (absurd H1 H2)
|
||||
|
||||
theorem absurd_not_true (H : ¬true) : false :=
|
||||
absurd trivial H
|
||||
|
||||
theorem not_false_trivial : ¬false :=
|
||||
assume H : false, H
|
||||
|
||||
theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
|
||||
assume Hna : ¬a, absurd (assume Ha : a, absurd_elim Ha Hna) H
|
||||
|
||||
theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
|
||||
assume Hb : b, absurd (assume Ha : a, Hb) H
|
||||
|
||||
theorem contrapos {a b : Prop} (Hab : a → b) : (¬b → ¬a) :=
|
||||
assume Hnb Ha, Hnb (Hab Ha)
|
||||
import general_notation .eq
|
||||
|
||||
|
||||
-- and
|
||||
|
@ -154,6 +100,8 @@ definition iff (a b : Prop) := (a → b) ∧ (b → a)
|
|||
infix `<->` := iff
|
||||
infix `↔` := iff
|
||||
|
||||
theorem iff_def {a b : Prop} : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl
|
||||
|
||||
theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2
|
||||
|
||||
theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and_rec H1 H2
|
||||
|
@ -190,6 +138,9 @@ iff_intro
|
|||
calc_refl iff_refl
|
||||
calc_trans iff_trans
|
||||
|
||||
theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb)
|
||||
|
||||
|
||||
-- comm and assoc for and / or
|
||||
-- ---------------------------
|
||||
|
|
|
@ -7,7 +7,7 @@
|
|||
|
||||
-- Equality.
|
||||
|
||||
import .basic
|
||||
import .prop
|
||||
|
||||
-- eq
|
||||
-- --
|
||||
|
@ -100,9 +100,6 @@ assume Ha, H2 ▸ (H1 Ha)
|
|||
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 ▸ Ha)
|
||||
|
||||
theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
||||
|
||||
|
||||
-- ne
|
||||
-- --
|
||||
|
|
|
@ -1,7 +1,62 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Leonardo de Moura, Jeremy Avigad
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import general_notation
|
||||
|
||||
definition Prop [inline] := Type.{0}
|
||||
|
||||
|
||||
-- implication
|
||||
-- -----------
|
||||
|
||||
abbreviation imp (a b : Prop) : Prop := a → b
|
||||
|
||||
|
||||
-- true and false
|
||||
-- --------------
|
||||
|
||||
inductive false : Prop
|
||||
|
||||
theorem false_elim (c : Prop) (H : false) : c :=
|
||||
false_rec c H
|
||||
|
||||
inductive true : Prop :=
|
||||
trivial : true
|
||||
|
||||
abbreviation not (a : Prop) := a → false
|
||||
prefix `¬` := not
|
||||
|
||||
|
||||
-- not
|
||||
-- ---
|
||||
|
||||
theorem not_intro {a : Prop} (H : a → false) : ¬a := H
|
||||
|
||||
theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
|
||||
|
||||
theorem absurd {a : Prop} (H1 : a) (H2 : ¬a) : false := H2 H1
|
||||
|
||||
theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
|
||||
assume Hna : ¬a, absurd Ha Hna
|
||||
|
||||
theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
|
||||
assume Ha : a, absurd (H1 Ha) H2
|
||||
|
||||
theorem absurd_elim {a : Prop} {b : Prop} (H1 : a) (H2 : ¬a) : b :=
|
||||
false_elim b (absurd H1 H2)
|
||||
|
||||
theorem absurd_not_true (H : ¬true) : false :=
|
||||
absurd trivial H
|
||||
|
||||
theorem not_false_trivial : ¬false :=
|
||||
assume H : false, H
|
||||
|
||||
theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
|
||||
assume Hna : ¬a, absurd (assume Ha : a, absurd_elim Ha Hna) H
|
||||
|
||||
theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
|
||||
assume Hb : b, absurd (assume Ha : a, Hb) H
|
||||
|
||||
theorem contrapos {a b : Prop} (Hab : a → b) : (¬b → ¬a) :=
|
||||
assume Hnb Ha, Hnb (Hab Ha)
|
||||
|
|
Loading…
Reference in a new issue