翻译-Lean Language Reference-13-项

def x := "global"
#eval
  let x := "local"
  x
  -- 前缀 x : 2 个标识符（分别是局部受缚变量、全局常量），优先考虑局部
-- "local"

#eval
  let x := "outer"
  let x := "inner"
  x
  -- 前缀 x : 2 个标识符（都是两个局部受缚变量），优先考虑近的
-- "inner"

namespace A
def x := "A.x"
namespace B
namespace C
def x := "A.B.C.x"

#eval x
-- "A.B.C.x"
-- 前缀 x : 2 个标识符（位于命名空间 C 的前缀 A.B.C、A 中），优先考虑命名空间前缀更长的

end C
#eval x
-- "A.x"

structure A where
  y : String
deriving Repr

structure B where
  y : A
deriving Repr

def y : B := ⟨⟨"shorter"⟩⟩
def y.y : A := ⟨"longer"⟩

#eval y.y.y
-- "longer"
-- 前缀 y.y.y : 无标识符
-- 前缀 y.y : 1 个标识符（最后的 .y 为结构项投影），优先考虑标识符前缀更长的
-- 前缀 y : 1 个标识符，最后的 .y.y 为结构项投影

namespace A
def x := "A.x"
end A

namespace B
def x := "B.x"
namespace C
open A
#eval x
-- "B.x"
-- 前缀 x : 2 个标识符（分别位于当前命名空间 B.C 的前缀 B 以及已打开的命名空间 A），优先考虑当前命名空间的前缀

def A.x := "A.x"
def B.x := "B.x"
open A
open B
#eval x
-- Ambiguous term
--   x
-- Possible interpretations:
--   B.x : String  
--   A.x : String

def C.x := "C.x"
def D.x := 3
open C
open D
#eval (x : String)
-- "C.x"

#eval show List Unit from .replicate 3 ()
-- [(), (), ()]

def MyList α := List α
#eval show MyList Unit from .replicate 3 ()
-- [(), (), ()]

def f {α : Type} : α → α := fun x => x
def g ⦃α : Type⦄ : α → α := fun x => x

example : f 2 = g 2 := rfl

example := f
-- don't know how to synthesize implicit argument `α`
--   @f ?m.3
-- context:
-- ⊢ Type

example := g

#check (fun x => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α

#check (fun {α} x => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
#check (fun {α} (x : α) => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α
#check (fun {α : Type} (x : α) => x : {α : Type} → α → α)
-- fun {α} x => x : {α : Type} → α → α

def sum3 (x y z : Nat) : Nat := x + y + z

#check sum3 4 3 8
-- sum3 4 3 8 : Nat

#check sum3 (x := 4) (y := 3) (z := 8)
-- sum3 4 3 8 : Nat

#check sum3 (y := 3) (x := 4) (z := 8)
-- sum3 4 3 8 : Nat

#check sum3 (y := 3) 8 (x := 4)
-- sum3 4 3 8 : Nat

#check sum3 8 (y := 3) (x := 4) 
-- sum3 4 3 8 : Nat

#check sum3 (y := 3)
-- fun x ↦ sum3 x 3 : Nat → Nat → Nat
-- fun x ↦ sum3 x 3 : (x z : Nat) → Nat

#check (sum3 (y := 3)) (x := 4)
-- (fun x ↦ sum3 x 3) 4 : Nat → Nat
-- (fun x ↦ sum3 x 3) 4 : (z : Nat) → Nat

#check let x := 8 ; sum3 (z := x)
-- let x := 8;
-- fun x_1 y ↦ sum3 x_1 y x : Nat → Nat
-- fun x_1 y ↦ sum3 x_1 y x : (x y : Nat) → Nat

#check (let x := 8 ; sum3 (z := x)) (x := 4)
-- (let x := 8;
--  fun x_1 y ↦ sum3 x_1 y x) 4
-- : Nat → Nat
-- : (y : Nat) → Nat

set_option pp.piBinderNames true in
#check let x := 8 ; sum3 (z := x)
-- let x := 8;
-- fun x_1 y ↦ sum3 x_1 y x : Nat → Nat
-- fun x_1 y ↦ sum3 x_1 y x : (x y : Nat) → Nat

def Username := String

def Username.validate (name : Username) : Except String Unit := do
  if " ".isPrefixOf name then
    throw "Unexpected leading whitespace"
  if name.any notOk then
    throw "Unexpected character"
  return ()
where
  notOk (c : Char) : Bool :=
    !c.isAlpha &&
    !c.isDigit &&
    !c ∈ ['_', ' ']

def adminUser : Username := "admin"

#eval "admin".validate
-- Invalid field `validate`: The environment does not contain 
-- `String.validate`, so it is not possible to 
-- project the field `validate` from an expression
--   "admin"
-- of type `String`

#eval adminUser.validate
-- Except.ok ()

#eval adminUser.any (· == 'm')
-- true

def Nat.half : Nat → Nat
  | 0 | 1 => 0
  | n + 2 => n.half + 1
#check Nat.half Nat.zero
-- Nat.zero.half : Nat

attribute [pp_nodot] Nat.half
#check Nat.half Nat.zero
-- Nat.half Nat.zero : Nat

#eval "Hello!" |> String.toList |> List.reverse |> List.head!
-- '!'

#eval List.head! <| List.reverse <| String.toList <| "Hello!"
-- '!'

#eval #[1, 2, 3] |> Array.push 4
-- failed to synthesize instance of type class
--   OfNat (Array ?m.4) 4
-- numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
--   Array ?m.4
-- due to the absence of the instance above
-- 
-- Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

#eval #[1, 2, 3] |>.push 4
-- #[1, 2, 3, 4]

#eval #[1, 2, 3] |>.push 4 |>.reverse |>.push 0 |>.reverse
-- #[0, 1, 2, 3, 4]

inductive Parity : Nat → Type where
  | even (h : Nat) : Parity (h + h)
  | odd (h : Nat) : Parity ((h + h) + 1)

def Nat.parity (n : Nat) : Parity n :=
  match n with
  | 0 => .even 0
  | n' + 1 => match n'.parity with
    | .even h => .odd h
    | .odd h =>
      have eq : (h + 1) + (h + 1) = (h + h + 1 + 1) :=
        by omega
      eq ▸ .even (h + 1)

def half (n : Nat) : Nat :=
  match n, n.parity with
  | .(h + h),     .even h => h
  | .(h + h + 1), .odd h  => h

inductive BalancedTree (α : Type u) : Nat → Type u where
  | empty : BalancedTree α 0
  | branch
    (left : BalancedTree α n)
    (val : α)
    (right : BalancedTree α n) :
    BalancedTree α (n + 1)
  | lbranch
    (left : BalancedTree α (n + 1))
    (val : α)
    (right : BalancedTree α n) :
    BalancedTree α (n + 2)
  | rbranch
    (left : BalancedTree α n)
    (val : α)
    (right : BalancedTree α (n + 1)) :
    BalancedTree α (n + 2)

def BalancedTree.filledWith
  (x : α) (depth : Nat) : BalancedTree α depth 
  := _
-- 第一个空洞导致如下报错：
-- don't know how to synthesize placeholder
-- context:
--  α:Type u
--  x:α
--  depth:Nat
-- ⊢ BalancedTree α depth

def BalancedTree.filledWith
  (x : α) (depth : Nat) :
  BalancedTree α depth 
  :=match depth with
    | 0 => _
    | n + 1 => _
-- 第一个空洞导致如下报错：
-- don't know how to synthesize placeholder
-- context:
--   α:Type u
--   x:α
--   depth:Nat
-- ⊢ BalancedTree α 0 -- depth 已被替换为 0
-- 第二个空洞导致如下报错：
-- don't know how to synthesize placeholder
-- context:
--   α:Type u
--   x:α
--   depth n:Nat
-- ⊢ BalancedTree α (n + 1) -- depth 已被替换为 n + 1

def BalancedTree.isPerfectlyBalanced
  (n : Nat) (t : BalancedTree α n) : Bool 
  :=match n, t with
    | 0, .empty => true
    | 0, .branch left val right => -- 此处报错
      isPerfectlyBalanced left &&
      isPerfectlyBalanced right
    | _, _ => false
-- Type mismatch
--   left.branch val right
-- has type
--   BalancedTree ?m.13 (?m.12 + 1)
-- but is expected to have type
--   BalancedTree α 0

def last? (xs : List α) : Except String α :=
  match h : xs with
  | [] =>
    .error "Can't take first element of empty list"
  | _ :: _ =>
    .ok <| xs.getLast (show xs ≠ [] by intro h'; simp_all)

def last?' (xs : List α) : Except String α :=
  match xs with
  | [] =>
    .error "Can't take first element of empty list"
  | _ :: _ =>
    .ok <| xs.getLast (show xs ≠ [] by intro h'; simp_all)
-- simp_all made no progress

#eval
  match 5, rfl with
  | 5, rfl => "ok"
-- Invalid match expression: This pattern contains metavariables:
--   Eq.refl ?m.14

#eval
  match (motive := (n : Nat) → n = 5 → String) 5, rfl with
  | 5, rfl => "ok"
-- "ok"

def f (n : Nat) (p : n = 3) : String :=
  match p with
  | rfl => "ok"

#print f
-- def f : (n : Nat) → n = 3 → String :=
-- fun n p =>
--   match 3, p with
--   | .(n), ⋯ => "ok"

def boolCases (b : Bool)
    (ifTrue : b = true → α)
    (ifFalse : b = false → α) :
    α :=
  match h : b with
  | true  => ifTrue  h -- 换成 rfl 就可以运行
  | false => ifFalse h -- 换成 rfl 就可以运行
-- Application type mismatch: The argument
--   h
-- has type
--   b = true
-- but is expected to have type
--   true = true
-- in the application
--   ifTrue h

def boolCases (b : Bool)
    (ifTrue : b = true → α)
    (ifFalse : b = false → α) :
    α :=
  match (generalizing := false) h : b with
  | true  => ifTrue  h
  | false => ifFalse h

def nonzero (n : Nat) : Bool :=
  match n with
  | 0 => false
  | 1 + k => true

-- Invalid pattern(s): 
-- `k` is an explicit pattern variable, 
-- but it only occurs in positions that are 
-- inaccessible to pattern matching:
--   .(Nat.add 1 k)

def add : Nat → Nat → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

def isZero : Nat → Bool :=
  fun
    | 0 => true
    | _ => false

def isZero' : Nat → Bool :=
  fun n =>
    match n with
    | 0 => true
    | _ => false

example : isZero = isZero' := rfl

#print isZero
-- def isZero : Nat → Bool :=
-- fun x =>
--   match x with
--   | 0 => true
--   | x => false

#print isZero'
-- def isZero' : Nat → Bool :=
-- fun n =>
--   match n with
--   | 0 => true
--   | x => false

example (p1 : x = "Hello") (p2 : x = "world") : False :=
  nomatch p1, p2

example : x = "Hello" → x = "world" → False := nofun

example (n : Nat) := by
  induction n
  next => rfl
  next n' ih =>
    simp only [HAdd.hAdd, Add.add, Nat.add] at *
    rewrite [ih]
    rfl
-- Invalid rewrite argument: Expected an
--   equality or
--   iff proof or
--   definition name, 
-- but `ih` is a proof of
--   0 ≍ n'

example (n : Nat) := show 0 + n = n by
  induction n
  next => rfl
  next n' ih =>
    simp only [HAdd.hAdd, Add.add, Nat.add] at *
    rewrite [ih]
    rfl

example := do
  return 5
-- typeclass instance problem is stuck
--   Pure ?m.12
-- 
-- Note: Lean will not try to resolve this typeclass instance problem 
-- because the type argument to `Pure` is a metavariable. 
-- This argument must be fully determined 
-- before Lean will try to resolve the typeclass.
-- 
-- Hint: Adding type annotations and supplying implicit arguments to functions 
-- can give Lean more information for typeclass resolution. For example, 
-- if you have a variable `x` that you intend to be a `Nat`, 
-- but Lean reports it as having an unresolved type like `?m`, 
-- replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

example := show StateM String _ from do
  return 5

def Colors := List String

#check ([] : Colors)
-- [] : List String

#check (show Colors from [])
-- have this := [];
-- this : Colors

def Colors.hasYellow (cs : Colors) : Bool :=
  cs.any (·.toLower == "yellow")

#eval ([] : Colors).hasYellow
-- Invalid field `hasYellow`: The environment 
-- does not contain `List.hasYellow`, so 
-- it is not possible to project the field `hasYellow` 
-- from an expression
--   []
-- of type `List String`

#eval (show Colors from []).hasYellow
-- false