Lean 4 極簡教學 (Using VS Code on macOS)

 1. Install Lean Environment:
https://lean-lang.org/install/

試著完Step one, two, three

2. 在VS code下，建一新的project:
取名Hello_World

3. 嘗試執行Main.lean:

一開始：

fit0721@FIT0721deMacBook-Pro Hello_World % lean --run Main.lean

Main.lean:1:0: error: unknown module prefix 'HelloWorld'

No directory 'HelloWorld' or file 'HelloWorld.olean' in the search path entries:

/Users/fit0721/.elan/toolchains/leanprover--lean4---v4.34.0/lib/lean

之後將lean --run Main.lean, 改成

lake build

lake env lean --run Main.lean

:

fit0721@FIT0721deMacBook-Pro Hello_World % lake build

lake env lean --run Main.lean

Build completed successfully (8 jobs).

Hello, world!

lake env 的意思是：先載入目前 Lean 專案的 Lake 環境，再執行後面的命令。

所以：

lake env lean --run Main.lean

可以拆成：

lake env   lean --run Main.lean
^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^
設定專案環境     真正執行 Lean

lake env 會幫你把目前專案的套件、.olean 模組搜尋路徑、Lean toolchain 等環境設定好。

4. 嘗試加入一個新的定理，在Main.lean改寫如下：

import HelloWorld

def main : IO Unit :=

IO.println s!"Hello, {hello}!"

def double (n : Nat) : Nat :=

n + n

theorem double_ge (n : Nat) : n ≤ double n := by

unfold double

exact Nat.le_add_right n n

以上可以正常build，只是執行時，還是只會print Hello, world!

這邊可以小玩一下，故意改成錯的：

import HelloWorld

def main : IO Unit :=

IO.println s!"Hello, {hello}!"

def double (n : Nat) : Nat :=

n + n

theorem double_ge (n : Nat) : n + n + n ≤ double n := by

unfold double

exact Nat.le_add_right n n

就會顯示：

注意11行，會有錯誤叉叉。

Note: 

≤ 在Lean4中打 \le 再按空白鍵

類似的常用符號還有：\ge → ≥、\ne → ≠、\and → ∧、\or → ∨、\to → →、\forall → ∀、\exists → ∃。

Basic Blind Chess的兩大問題 (Android version only)

Note: 以下指Andorid version pygame的 v0.8.2之前，後來Unity版出的已有改善

Basic Blind Chess已經好久沒更新了，

Windows版可以獲得最好的遊戲体驗，

但是Android版的，不只是比較舊，

它其實存在兩大問題：

1. 拿子移動時，顯示怪怪的，只顯示前幾個移動的殘影。

這個只有在最早的版本，沒有這個問題，

但是最早的版本實機測試時，連續敲幾下螢幕，就會當掉。

所以後來就改成移動時，顯示怪怪的版本，

至少手機實機測試是不會當的。

真的受不了的話，建議玩Windows的版本，

就沒有這個問題。

2.  DarkChess-0.8.2-release.apk是pygame Android的最後一版，

但是印像中，它其實比0.8.2更舊，只是比0.8.0新，

當初是想，過一陣子，

再把DarkChess-0.8.2-release.apk完全升到v0.8.2,

但是過了幾年，直到現在，一直沒有把它真正升到v0.8.2.

(v0.8.2是把Windows的v0.8.2當標的)

Lua, 7 kyu, 排隊問題

 7 kyu, Lost Lineup

這題很簡單，我一開始實作的方法是：

local function find_lineup(distances)
  local a, d = {}, #distances
  for i = 1, d do
    a[i] = -1
  end
  for i = 1, d do
    local n = distances[i] + 1
    if -1 == a[n] then
      a[n] = i
    else
      return {}
    end
  end
  for i = 1, d do
    if -1 == a[i] then
      return {}
    end
  end
  return a
end

return find_lineup

後來看了別人的方法，

主要有兩點，會比我簡潔：

1. 利用a = {}時，空的table, 裡面的元素預設值是nil

例如 a[2] = nil

2. 利用排隊正常時，會排完，且每個人只佔住一個號碼，

因此排隊號碼，不可能大於總人數。

由以上兩點，我改寫如下：

local function find_lineup(distances)
  local a, d = {}, #distances
  for i = 1, d do
    local n = distances[i] + 1
    if nil == a[n] and n <= d then
      a[n] = i
    else
      return {}
    end
  end
  return a
end

return find_lineup

Lua的table，不能直接比較

 今天在寫

7 kyu: [BUG] XCOM-388: Mass spectrometer crashes

這一題時，

發現empty table的變數跟empty table的值用不相等比較時，

預期會是false (非不相等)，但其實會傳回true,

如下：

> a = {}

> if a ~= {} then

>>  print(a)

>> end

table: 0x600002bbc640

> if a == {} then

>>  print(a)

>> end

> 

(後記，非空table比對，也是一樣)

如果要檢查，table是否空時，

可用next檢查，next()為true時，不為空table.

寫出程設題，如下：

local spectrometer = {}

function spectrometer.get_heaviest(atomic_masses)
  if atomic_masses and next(atomic_masses)then
    if #atomic_masses < 500000 then
      return math.max(table.unpack(atomic_masses))
    else
      local m = 0
      for i = 1, #atomic_masses do
        if atomic_masses[i] > m then
          m = atomic_masses[i]
        end
      end
      return m
    end
  else
    return 0
  end
end

return spectrometer

別人寫的跟我的大致類似，
除非用第三方的API，才有比較簡潔的寫法。