198 lines
5 KiB
Text
198 lines
5 KiB
Text
--
|
||
-- 4. Quantifiers and Equality
|
||
--
|
||
|
||
-- The Universal Quantifier
|
||
|
||
example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y :=
|
||
fun h : ∀ x : α, p x ∧ q x =>
|
||
fun y : α =>
|
||
show p y from (h y).left
|
||
|
||
variable (α : Type) (r : α → α → Prop)
|
||
variable (trans_r : ∀ {x y z}, r x y → r y z → r x z)
|
||
|
||
variable (a b c : α)
|
||
variable (hab : r a b) (hbc : r b c)
|
||
|
||
#check trans_r
|
||
#check @trans_r
|
||
#check trans_r hab
|
||
#check trans_r hab hbc
|
||
|
||
-- Equality
|
||
|
||
#check Eq.refl
|
||
#check Eq.symm
|
||
#check Eq.trans
|
||
|
||
universe u
|
||
#check @Eq.refl.{u}
|
||
#check @Eq.symm.{u}
|
||
#check @Eq.trans.{u}
|
||
|
||
variable (a b c d : α)
|
||
variable (hab : a = b) (hcb : c = b) (hcd : c = d)
|
||
|
||
example : a = d :=
|
||
Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
|
||
example : a = d := (hab.trans hcb.symm).trans hcd
|
||
|
||
variable (α β : Type)
|
||
|
||
example (f : α → β) (a : α) : (fun x => f x) a = f a := Eq.refl _
|
||
example (f : α → β) (a : α) : (fun x => f x) a = f a := rfl
|
||
|
||
example (α : Type) (a b : α) (p : α → Prop)
|
||
(h1 : a = b) (h2 : p a) : p b :=
|
||
Eq.subst h1 h2
|
||
|
||
example (α : Type) (a b : α) (p : α → Prop)
|
||
(h1 : a = b) (h2 : p a) : p b :=
|
||
h1 ▸ h2
|
||
|
||
variable (α : Type)
|
||
variable (a b : α)
|
||
variable (f g : α → Nat)
|
||
variable (h₁ : a = b)
|
||
variable (h₂ : f = g)
|
||
|
||
example : f a = f b := congrArg f h₁
|
||
example : f a = g a := congrFun h₂ a
|
||
|
||
variable (a : Nat) in
|
||
example : a + 0 = a := Nat.add_zero a
|
||
|
||
-- Calculational Proofs
|
||
variable (a b c d : Nat) in
|
||
variable (h1 : a = b) in
|
||
variable (h2 : b = c + 1) in
|
||
variable (h3 : c = d) in
|
||
variable (h4 : e = 1 + d) in
|
||
theorem T : a = e :=
|
||
calc
|
||
a = b := h1
|
||
_ = c + 1 := h2
|
||
_ = d + 1 := congrArg Nat.succ h3
|
||
_ = 1 + d := Nat.add_comm d 1
|
||
_ = e := h4.symm
|
||
|
||
-- The Existential Quantifier
|
||
example : ∃ x : Nat, x > 0 :=
|
||
have h : 1 > 0 := Nat.zero_lt_succ 0
|
||
Exists.intro 1 h
|
||
|
||
variable (α : Type) (p q : α → Prop) in
|
||
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
|
||
Exists.elim h
|
||
fun w =>
|
||
fun hw : p w ∧ q w =>
|
||
Exists.intro w ⟨hw.right, hw.left⟩
|
||
|
||
#check @Exists.elim.{u}
|
||
|
||
#check Sigma
|
||
|
||
variable (α : Type) (p q : α → Prop) in
|
||
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
|
||
match h with
|
||
| ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩
|
||
|
||
|
||
-- More on the Proof Language
|
||
variable (f : Nat → Nat)
|
||
variable (h : ∀ x : Nat, f x ≤ f (x + 1))
|
||
|
||
example : f 0 ≤ f 3 :=
|
||
have : f 0 ≤ f 1 := h 0
|
||
have : f 0 ≤ f 2 := Nat.le_trans (by assumption) (h 1)
|
||
show f 0 ≤ f 3 from Nat.le_trans (by assumption) (h 2)
|
||
|
||
example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
|
||
fun _ : f 0 ≥ f 1 =>
|
||
fun _ : f 1 ≥ f 2 =>
|
||
have : f 0 ≥ f 2 := Nat.le_trans ‹f 1 ≥ f 2› ‹f 0 ≥ f 1›
|
||
have : f 0 ≤ f 2 := Nat.le_trans (h 0) (h 1)
|
||
show f 0 = f 2 from Nat.le_antisymm this ‹f 0 ≥ f 2›
|
||
|
||
-- Exercises
|
||
variable (α : Type) (p q : α → Prop)
|
||
|
||
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
|
||
have h1 : (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x :=
|
||
fun h =>
|
||
have h11 : ∀ (x : α), p x :=
|
||
fun x : α => (h x).left
|
||
have h12 : ∀ (x : α), q x :=
|
||
fun x : α => (h x).right
|
||
And.intro h11 h12
|
||
have h2 : ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x :=
|
||
fun h =>
|
||
fun x : α =>
|
||
⟨h.left x, h.right x⟩
|
||
Iff.intro h1 h2
|
||
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
|
||
fun h1 =>
|
||
fun h2 =>
|
||
fun x : α =>
|
||
show q x from (h1 x) (h2 x)
|
||
|
||
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
|
||
fun h =>
|
||
h.elim
|
||
(fun hp =>
|
||
fun x => Or.inl (hp x))
|
||
(fun hq =>
|
||
fun x => Or.inr (hq x))
|
||
|
||
variable (α : Type) (p q : α → Prop)
|
||
variable (r : Prop)
|
||
|
||
example : α → ((∀ x : α, r) ↔ r) :=
|
||
fun hα =>
|
||
have h1 := fun h => h hα
|
||
have h2 := fun hr => fun _ => hr
|
||
Iff.intro h1 h2
|
||
open Classical in
|
||
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
|
||
have h1 : (∀ (x : α), p x ∨ r) → (∀ (x : α), p x) ∨ r :=
|
||
fun h =>
|
||
sorry
|
||
have h2 : (∀ (x : α), p x) ∨ r → ∀ (x : α), p x ∨ r :=
|
||
fun h =>
|
||
h.elim
|
||
(fun hl =>
|
||
fun hx =>
|
||
Or.inl (hl hx))
|
||
(fun hr =>
|
||
fun hx =>
|
||
Or.inr hr)
|
||
Iff.intro h1 h2
|
||
|
||
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
|
||
have h1 : (∀ (x : α), r → p x) → r → ∀ (x : α), p x :=
|
||
fun h =>
|
||
fun hr =>
|
||
fun x =>
|
||
(h x) hr
|
||
have h2 : (r → ∀ (x : α), p x) → ∀ (x : α), r → p x :=
|
||
fun h =>
|
||
fun x =>
|
||
fun hr =>
|
||
(h hr) x
|
||
Iff.intro h1 h2
|
||
|
||
|
||
variable (men : Type) (barber : men)
|
||
variable (shaves : men → men → Prop)
|
||
|
||
open Classical in
|
||
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False :=
|
||
have hbarber : shaves barber barber ↔ ¬shaves barber barber :=
|
||
h barber
|
||
(em (shaves barber barber)).elim
|
||
(fun hbarberself =>
|
||
have hnbarbarself := hbarber.mp hbarberself
|
||
hnbarbarself hbarberself)
|
||
(fun hnbarbarself =>
|
||
hnbarbarself (hbarber.mpr hnbarbarself))
|