翻译-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
7
8

variable 
(α : Type) 
(p q : α → Prop)
(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
6
7

variable 
(men : Type) 
(barber : men)
(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
 9
10
11
12
13
14
15

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2-- 根据等式 h1 对 h2 的内容进行替换
--h1.subst h2   -- 这样写也行

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

#print Eq.subst
-- theorem Eq.subst.{u} 
-- : ∀ {α : Sort u} {motive : α → Prop} {a b : α}, 
--   a = b → motive a → motive b
-- :=fun {α} {motive} {a b} h₁ h₂ ↦ h₁ ▸ h₂
-- 这里 h₁ : a = b , h₂ : motive a

 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
28
29
30
31
32
33
34
35
36
37
38
39
40
41

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) -- 这样写也行

#print congrArg
-- theorem congrArg.{u, v}
-- : ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α}
--   (f : α → β), a₁ = a₂ → f a₁ = f a₂
-- :=fun {α} {β} {a₁ a₂} f h ↦ h ▸ rfl
-- 这里 h : a₁ = a₂ , rfl : f a₁ = f a₁

#print congrFun
-- theorem congrFun.{u, v}
-- : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x},
--   f = g → ∀ (a : α), f a = g a
-- :=fun {α} {β} {f g} h a ↦ h ▸ rfl
-- 这里 h : f = g , rfl : f a = f a

#print congr
-- theorem congr.{u, v}
-- : ∀ {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α},
--   f₁ = f₂ → a₁ = a₂ → f₁ a₁ = f₂ a₂
-- :=fun {α} {β} {f₁ f₂} {a₁ a₂} h₁ h₂ ↦ h₁ ▸ h₂ ▸ rfl
-- 这里 h₁ : f₁ = f₂ , h₂ : a₁ = a₂ , rfl : f₁ a₁ = 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
20
21
22
23
24
25
26
27

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
    :=-- (x + y)x + (x + y)y
      Nat.mul_add (x + y) x y -- ↑ , (x + y)(x + y) 被展开为 (x + y)x + (x + y)y
      -- (x + y)²
    have h2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y)
    :=-- (x² + yx) + (xy + y²)
      (Nat.add_mul x y x) ▸   -- ↑ , (x + y)x       被展开为 x² + yx
      -- (x + y)x  + (xy + y²)
      (Nat.add_mul x y y) ▸   -- ↑ , (x + y)y       被展开为 xy + y²
      -- (x + y)x  + (x + y)y
      h1                      -- ↑ , (x + y)(x + y) 被展开为 (x + y)x + (x + y)y
      -- (x + y)²

    -- (x + y)²
    h2.trans               -- ↓ , (x + y)(x + y)      被展开为 x² + yx + (xy + y²)
      (-- (x² + yx) + (xy + y²)
        (-- (x² + yx) + xy + y²
          Nat.add_assoc    -- ↓ , x² + yx + xy + y²   被展开为 x² + yx + (xy + y²)
          (x * x + y * x)
          (x * y)
          (y * y)
        -- (x² + yx) + (xy + y²)
        ).symm             -- ↓ , x² + yx + (xy + y²) 被展开为 x² + yx + xy + y²
      -- (x² + yx) + xy + 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
15
16
17
18

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      := h1
    -- ↓ , h2           : b = c + 1
    _ = c + 1  := h2
    -- ↓ , h3           : c = d
    _ = d + 1  := congrArg Nat.succ h3
    -- ↓ , Nat.add_comm : d + 1 = 1 + d
    _ = 1 + d  := Nat.add_comm d 1
    -- ↓ , h4.symm      : e = 1 + d
    _ = e      := Eq.symm h4

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

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]
    -- ↓ , h2           : b = c + 1
    _ = c + 1  := by rw [h2]
    -- ↓ , h3           : c = d
    _ = d + 1  := by rw [h3]
    -- ↓ , Nat.add_comm : d + 1 = 1 + d
    _ = 1 + d  := by rw [Nat.add_comm]
    -- ↑ , h4           : e = 1 + d
    _ = e      := by rw [h4]

 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
28

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 [
      -- a
      h1,          -- ↓ , a     被换成 b
      -- b
      h2,          -- ↓ , b     被换成 c + 1
      -- c + 1
      h3           -- ↓ , c     被换成 d
      -- d + 1
    ]
    _ = 1 + d  := by rw [
      -- d + 1
      Nat.add_comm -- ↓ , d + 1 被换成 1 + d
      -- 1 + d
    ]
    _ = e      := by rw [
      -- 1 + d
      h4           -- ↑ , 1 + d 被换成 e
      -- e
    ]

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

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 [
    -- a
    h1,           -- ↓ , a     被换成 b
    -- b
    h2,           -- ↓ , b     被换成 c + 1
    -- c + 1
    h3,           -- ↓ , c     被换成 d
    -- d + 1
    Nat.add_comm, -- ↓ , d + 1 被换成 1 + d
    -- 1 + d
    h4            -- ↑ , 1 + d 被换成 e
    -- e
  ]

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

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]
--by simp [h3, h1, Nat.add_comm, h4, h2] -- 这样写也行

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

variable (a b c d : Nat)

example
  (h1 : a = b)
  (h2 : b ≤ c)
  (h3 : c + 1 < d) :
  a < d
  :=calc
    a = b     := h1
    -- ↓ , Nat.lt_succ_self b  : b     < b + 1
    _ < b + 1 := Nat.lt_succ_self b
    -- ↓ , Nat.succ_le_succ h2 : b + 1 ≤ c + 1
    _ ≤ c + 1 := Nat.succ_le_succ h2
    -- ↓ , h3                  : c + 1 < d
    _ < 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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

variable (x y z k : Nat)

def divides : 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 [
      -- (k₁ * k₂) * x
      Nat.mul_comm k₁ k₂, -- ↓ , (k₁ * k₂) * x 被换成 (k₂ * k₁) * x
      -- (k₂ * k₁) * x
      Nat.mul_assoc,      -- ↓ , (k₂ * k₁) * x 被换成 k₂ * (k₁ * x)
      -- k₂ * (k₁ * x) = z
      d₁,                 -- ↓ , k₁ * x        被换成 y
      -- k₂ * y
      d₂                  -- ↓ , k₂ * y        被换成 z
      -- z
  ]⟩

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

instance : Trans divides divides divides where
  trans := @divides_trans
--trans :=  divides_trans _ _ _ -- 这样写也行

#print 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 ..