翻译-TPIL-04-量词与相等关系

1
2
3
4

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        -- 合取消除 全称消去

1
2
3
4

example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : α, p x :=
  fun h : ∀ x : α, p x ∧ q x =>   -- 箭头引入
  fun z : α =>                    -- 全称引入
  show p z from And.left (h z)    -- 合取消除 全称消去

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

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
-- trans_r : ∀ (x y z : α), r x y → r y z → r x z
#check trans_r a b c
-- trans_r a b c : r a b → r b c → r a c
#check trans_r a b c hab
-- trans_r a b c hab : r b c → r a c
#check trans_r a b c hab hbc
-- trans_r a b c hab hbc : r a c

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

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
-- trans_r : r ?m.4 ?m.5 → r ?m.5 ?m.6 → r ?m.4 ?m.6
#check trans_r hab
-- trans_r hab : r b ?m.6 → r a ?m.6
#check trans_r hab hbc
-- trans_r hab hbc : r a c

1
2
3
4
5
6
7
8

variable (α : Type) (r : α → α → Prop)

variable (refl_r : ∀ x, r x x)
variable (symm_r : ∀ {x y}, r x y → r y x)
variable (trans_r : ∀ {x y z}, r x y → r y z → r x z)

example (a b c d : α) (hab : r a b) (hcb : r c b) (hcd : r c d) : r a d :=
  trans_r (trans_r hab (symm_r hcb)) hcd

1
2
3
4
5

variable (α : Type) (p q : α → Prop)

example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := sorry
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := sorry
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := sorry

1
2
3
4
5
6

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example : α → ((∀ x : α, r) ↔ r) := sorry
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := sorry

1
2
3
4
5

variable (men : Type) (barber : men)
variable (shaves : men → men → Prop)

example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False :=
  sorry

1
2
3
4
5
6

#check Eq.refl
-- Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a
#check Eq.symm
-- Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a
#check Eq.trans
-- Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

1
2
3
4
5
6
7
8

universe u

#check @Eq.refl.{u}
-- @Eq.refl : ∀ {α : Sort u} (a : α), a = a
#check @Eq.symm.{u}
-- @Eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a
#check @Eq.trans.{u}
-- @Eq.trans : ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c

1
2
3
4
5

variable (α : Type) (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

1
2
3
4
5

variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d := 
  (hab.trans hcb.symm).trans hcd

1
2
3
4
5

variable (α β : Type)

example (f : α → β) (a : α) : (fun x => f x) a = f a := Eq.refl _
example (a : α) (b : β) : (a, b).1 = a := Eq.refl _
example : 2 + 3 = 5 := Eq.refl _

1
2
3
4
5

variable (α β : Type)

example (f : α → β) (a : α) : (fun x => f x) a = f a := rfl
example (a : α) (b : β) : (a, b).1 = a := rfl
example : 2 + 3 = 5 := rfl

1
2
3
4
5
6
7
8

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2
--h1.subst h2   -- 这样写也行

example (α : Type) (a b : α) (p : α → Prop)
  (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20

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₁
--:=by rw [h₁]              -- 这样写也行 4.3 节会解释
--:=h₁ ▸ Eq.refl (f a)      -- 这样写也行 注意：这里用 subst 会报错，在高阶合一那里有解释

example : f a = g a
  :=congrFun h₂ a
--:=by rw [h₂]              -- 这样写也行
--:=h₂ ▸ Eq.refl (f a)      -- 这样写也行

example : f a = g b
  :=congr h₂ h₁
--:=by rw [h₂, h₁]          -- 这样写也行
--:=h₂ ▸ h₁ ▸ Eq.refl (f a) -- 这样写也行

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

variable (a b c : Nat)

example : a + 0 = a := Nat.add_zero a
example : 0 + a = a := Nat.zero_add a
example : a * 1 = a := Nat.mul_one a
example : 1 * a = a := Nat.one_mul a
example : a + b = b + a := Nat.add_comm a b
example : a + b + c = a + (b + c) := Nat.add_assoc a b c
example : a * b = b * a := Nat.mul_comm a b
example : a * b * c = a * (b * c) := Nat.mul_assoc a b c
example : a * (b + c) = a * b + a * c := Nat.mul_add a b c
example : a * (b + c) = a * b + a * c := Nat.left_distrib a b c
example : (a + b) * c = a * c + b * c := Nat.add_mul a b c
example : (a + b) * c = a * c + b * c := Nat.right_distrib a b c

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y
  :=have h1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y
    :=Nat.mul_add (x + y) x y
    have h2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y)
      -- (x + y)² = x² + y² + (xy + yx)
    :=(Nat.add_mul x y x) ▸
      -- (x + y)² = (x² + yx) + (xy + y²) , 将 (x + y) * x 展开为 x * x + y * x
      (Nat.add_mul x y y) ▸
      -- (x + y)² = (x + y)x  + (xy + y²) , 将 (x + y)y 展开为 xy + y²
      h1
      -- (x + y)² = (x + y)x + (x + y)y
    h2.trans (Nat.add_assoc
        (x * x + y * x)
        (x * y)
        (y * y)
        -- 得到 x² + yx + xy + y² = x² + yx + (xy + y²)
      ).symm
      -- 得到 x² + yx + (xy + y²) = x² + yx + xy + y²
    -- 得到 (x + y)² = x² + yx + xy + y²

1
2
3
4
5

calc
  <expr>_0  'op_1'  <expr>_1  ':='  <proof>_1
  '_'       'op_2'  <expr>_2  ':='  <proof>_2
  ...
  '_'       'op_n'  <expr>_n  ':='  <proof>_n

1
2
3
4
5

calc <expr>_0
  '_' 'op_1' <expr>_1 ':=' <proof>_1
  '_' 'op_2' <expr>_2 ':=' <proof>_2
  ...
  '_' 'op_n' <expr>_n ':=' <proof>_n

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

variable (a b c d e : Nat)

variable (h1 : a = b)
variable (h2 : b = c + 1)
variable (h3 : c = d)
variable (h4 : e = 1 + d)

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      := Eq.symm h4

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

variable (a b c d e : Nat)

theorem T : 
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d)
    a = e :=
  calc
    a = b      := by rw [h1]
    _ = c + 1  := by rw [h2]
    _ = d + 1  := by rw [h3]
    _ = 1 + d  := by rw [Nat.add_comm]
    _ = e      := by rw [h4]

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

variable (a b c d e : Nat)

theorem T
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) :
    a = e :=
  calc
    a = d + 1  := by rw [h1, h2, h3]
    _ = 1 + d  := by rw [Nat.add_comm]
    _ = e      := by rw [h4]

1
2
3
4
5
6
7
8
9

variable (a b c d e : Nat)

theorem T
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) :
    a = e :=
  by rw [h1, h2, h3, Nat.add_comm, h4]

1
2
3
4
5
6
7
8
9

variable (a b c d e : Nat)

theorem T
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) :
    a = e :=
  by simp [h1, h2, h3, Nat.add_comm, h4]

1
2
3
4
5
6
7
8

variable (a b c d : Nat)

example (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d :=
  calc
    a = b     := h1
    _ < b + 1 := Nat.lt_succ_self b
    _ ≤ c + 1 := Nat.succ_le_succ h2
    _ < d     := h3

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

def divides (x y : Nat) : Prop :=
  ∃ k, k*x = y

def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z :=
  let ⟨k₁, d₁⟩ := h₁
  let ⟨k₂, d₂⟩ := h₂
  ⟨k₁ * k₂, by rw [Nat.mul_comm k₁ k₂, Nat.mul_assoc, d₁, d₂]⟩

def divides_mul (x : Nat) (k : Nat) : divides x (k*x) :=
  ⟨k, rfl⟩

instance : Trans divides divides divides where
  trans := divides_trans

example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
  calc
    divides x y     := h₁
    _ = z           := h₂
    divides _ (2*z) := divides_mul ..

infix:50 " ∣ " => divides

example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
  calc
    x ∣ y   := h₁
    _ = z    := h₂
    _ ∣ 2*z := divides_mul ..

1
2
3
4
5
6
7
8

variable (x y : Nat)

example : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  calc
    (x + y) * (x + y) = (x + y) * x + (x + y) * y  := by rw [Nat.mul_add]
    _ = x * x + y * x + (x + y) * y                := by rw [Nat.add_mul]
    _ = x * x + y * x + (x * y + y * y)            := by rw [Nat.add_mul]
    _ = x * x + y * x + x * y + y * y              := by rw [←Nat.add_assoc]