variable P : Prop
variables A B : Type
variable R : A → B → Prop
variable PP : A → Prop
variable QQ : A → Prop
open classical
theorem raa : ¬ ¬ P → P :=
begin
assume nnp,
cases (em P) with p np,
exact p,
have f : false,
apply nnp,
exact np,
cases f,
end
example : ¬ (∃ x : A, PP x) ↔ (∀ x : A, ¬PP x) :=
begin
constructor,
assume h a ppa,
apply h,
existsi a,
exact ppa,
assume nppx eppx,
cases eppx with x ppx,
apply nppx,
exact ppx,
end
example : ¬(∀ x : A, PP x) ↔ ∃ x : A, ¬ PP x :=
begin
constructor,
assume h,
apply raa,
assume ppx,
apply h,
assume x,
apply raa,
assume nppa,
apply ppx,
existsi x,
exact nppa,
assume h hh,
cases h with a nppa,
apply nppa,
apply hh,
end
/-
bool = True
bool = {tt , ff}
-/
namespace bool
/-
Inductive bool : Type
| tt : bool
| ff : bool
tt and ff are the only elements of bool.
∀ x : bool, x=tt ∨ x=ff
-/
example : ∀ x : bool, x=tt ∨ x=ff :=
begin
assume x,
cases x,
right,
reflexivity,
left,
reflexivity,
end
example : tt ≠ ff :=
begin
assume h,
contradiction,
end
def bnot : bool → bool
| tt := ff
| ff := tt
#eval bnot (bnot tt)
example : ∀ x:bool, bnot (bnot x) = x :=
begin
assume x,
cases x,
-- dsimp [bnot],
reflexivity,
-- dsimp [bnot],
reflexivity,
end
/-
def band : bool → bool → bool
| ff ff := ff
| ff tt := ff
| tt ff := ff
| tt tt := tt
-/
def band : bool → bool → bool
| tt x := x
| ff x := ff
def bor : bool → bool → bool
| tt x := tt
| ff x := x
end bool