Lean 學習筆記 Day 2 - 來上課 AI 當老師 - Lesson 1 HW 1.1 歸納型落地
Github: https://github.com/neojou/lean_study/tree/main/mylogic
學習資料：
--
靈機一動，來請 AI 自己寫教材，出作業，我來當學生，
學怎麼用 Lean code 寫一個 自己的邏輯系統;
和 Grok AI 討論之後，設計了這條學習之路 : TASKS.md
上面的 Lesson 1 即是 AI 設計的教材，不過感覺有點薄弱，看不大懂 ^_^
我在 Grok build 上用的 prompt :
不要自己實作, 而是扮演一位大學教授, 將需要的知識紀錄到 mylogic/docs/lession1.md,
並對應循序漸進規劃出幾個 HomeWork, 由我來實作, 預期當這些 Homework 都做好時, phase 1 也完成了
而在 browser 介面, 下底下這個 prompt 給 Grok AI :
專案是 : https://github.com/neojou/lean_study/tree/main/mylogic
請先閱讀 https://github.com/neojou/lean_study/blob/main/mylogic/docs/handoff.md ,
接下來扮演一位熟知數學, 邏輯學, 和 LEAN 的大學教授, 我是學生;
我會開始閱讀
https://github.com/neojou/lean_study/blob/main/mylogic/docs/lesson-1.md
並做作業; 期間有不了解的, 會在這對話中提問討論;
了解後請說 OK, 並開始先做一段自我介紹；
有趣的是, AI 會說他叫 林老師 ^_^
---
畢竟 Lean 也是程式的一種, 先來看官網提供的這個;
中文可以參考這個
而目前在研究的邏輯學，最相關的是這個：
--
在 Introduction 這邊有個例子 :
在 1.3 的 Functions and Definitions 有解說def add1 (n : Nat) : Nat := n + 1
#eval add1 7
定義
def hello : String := "world"
def [名稱] : [型態] := [值]
若從 值 可以判斷出 型態 時, 型態宣告可以省略
--
而第一個例子，是一個 函數宣告定義
def [函數名稱] ( [參數名] : [參數型態] ) : [回傳值] := [函數主體]
--
如果函數是多行組成的話，加一個 do
可以參考 2.1.4 組合 IO 活動
--
第二行 #eval 是在一開始 1.1 求值表達式 有介紹，因為 Lean 在編譯期間就做相關的語法處理動作，所以這指令前面有個 # ;
推薦可以先用 VSCode 跑看看; 有個 Lean InfoView
滑鼠移到 Nat 時，也會有相關說明;
---
inductive
[函數名稱] : [參數 1 類型] -> [參數 2 類型] -> ... -> [函數回傳值]
---
註解
/-
...
-/
或檔案開頭模組說明
/-!
...
-/
--
函式參數呼叫
一開始都寫錯，問了AI才知道，參數用空格即可 ^_^
-- p ⋀ q（令 p = 0、q = 1）
def ex1 : Formula Nat
:= Formula.and (Formula.atom 0) (Formula.atom 1)
--
作業 1
讀完第 1–6 節再做。
- 新建
Mylogic/Formula.lean。 namespace Mylogic…end Mylogic。- 定義
inductive Formula (α : Type)，五個 constructor，名稱如上。沒有neg。 - 檔案開頭用繁中註解（至少三句）說明：這是對象語法、不是 Lean 的
Prop、原語只有這五個。 - 每個 constructor 一行中文註解。
- 在 namespace 內寫三個
def（名字自訂），型別都是Formula ℕ，只用 constructor、不用記號：p ⋀ q（令p = 0、q = 1）(p ⋀ q) ⇒ ⟂p ⇒ (q ⋁ ⟂)
- 此時還不要定義
∼、還不要notation。
驗收。 lake build 仍綠（若尚未改入口，至少 Formula.lean 本身無錯）。#check 那三個 def 看得到 Formula ℕ。禁寫清單沒被違反。
--
寫在 Formula.lean
---Grok AI 林老師 批改作業 HW 1.1
通過了 ^_^
留言
張貼留言