• Agda学习笔记1


    Agda学习笔记1

    好久没写博客了,诈尸一波。

    说句题外话,期中有点小爆炸,开始后悔选实验班了。要读信科的后辈诸君,我劝你选计概A普通班拿4.0。

    开学的时候老是想着多学点东西,现在:绩点绩点绩点

    快捷键

    • C-c C-l : 加载,把问号转换成goal
    • C-c C-f/C-b : 在goal之间切换
    • C-c C-, : goal&context
    • C-c C-. : goal&context&type
    • C-c C-r : refine 有时可以自动填充
    • C-c C-c spilt:
      • 直接回车:补上变量
      • 输入变量:把这个变量解释成所有定义
    • C-c C-a : 自动填充(一般用不上)

    refl

    表示左右相等

    Natural Number

    自然数集合

    data " role="presentation"> : Set where

    zero : " role="presentation">

    suc : " role="presentation">

    即只能从这两条推出其他的性质

    解释一个 ℕ 变量的时候就会展开成这两个元素

    operations

    1. _+_:" role="presentation">_+_:

      zero + n = n

      suc m + n = suc (m + n)

    2. __:" role="presentation">__:

      zero * n = zero

      suc m * n = n + (m * n)

    3. pred:" role="presentation">pred:

      pred 0 = 0

      pred (suc n) = n

    rewrite

    大概是用于递归的一个东西,相当于把rewrite的东西带入原式

    cong

    cong f : 把 f 添加到左右两边

    例:

    +0 : ∀ (y : ℕ) -> y ≡ y + zero 
    +0 zero = refl
    +0 (suc y) = cong suc (+0 y)
    

    加法结合律

    +assoc : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
    +assoc zero y z = refl
    +assoc (suc x) y z rewrite +assoc x y z = refl
    

    就是运用suc对+的结合律

    加法交换律

    依旧是利用suc递归...

    +suc : ∀ (x y : ℕ) → suc x + y ≡ x + suc y
    +suc zero y = refl
    +suc (suc x) y rewrite +suc x y = refl 
    
    +comm : ∀ (x y : ℕ) → x + y ≡ y + x
    +comm zero y = +0 y
    +comm (suc x) y rewrite +comm x y = +suc y x
    

    也可以用rewrite这样写:

    +comm : ∀ (x y : ℕ) → x + y ≡ y + x
    +comm zero y = +0 y
    +comm (suc x) y rewrite +comm x y | +suc y x = refl
    

    rewrite加竖线就是从左到右替换

    乘法分配律

    同上

    *distribr : ∀ (x y z : ℕ) → (x + y) * z ≡ x * z + y * z
    *distribr zero y z = refl
    *distribr (suc x) y z rewrite *distribr x y z | +assoc z (x * z) (y * z) = refl
    

    比较大小

    _<_ : ℕ → ℕ → 𝔹
    0 < 0 = ff
    0 < (suc y) = tt
    (suc x) < (suc y) = x < y
    (suc x) < 0 = ff
    _=ℕ_ : ℕ → ℕ → 𝔹
    0 =ℕ 0 = tt
    suc x =ℕ suc y = x =ℕ y
    _ =ℕ _ = ff
    _≤_ : ℕ → ℕ → 𝔹
    x ≤ y = (x < y) || x =ℕ y
    _>_ : ℕ → ℕ → 𝔹
    a > b = b < a
    _≥_ : ℕ → ℕ → 𝔹
    a ≥ b = b ≤ a
    

    注意相等是 _=ℕ_

    衍生的一些证明

    其实上面的定义不用记,反正也会忘

    写作业和考试前看看就好了

    <-0 : ∀ (x : ℕ) → x < 0 ≡ false
    <-0 0 = refl
    <-0 (suc y) = refl
    
    𝔹-contra : false ≡ true → ∀{ℓ} {P : Set ℓ} → P
    𝔹-contra ()
    
    <-trans : ∀ {x y z : ℕ} → x < y ≡ true → y < z ≡ true → x < z ≡ true
    <-trans {x} {0} p1 p2 rewrite <-0 x = 𝔹-contra p1
    <-trans {0} {suc y} {0} p1 ()
    <-trans {0} {suc y} {suc z} p1 p2 = refl
    <-trans {suc x} {suc y} {0} p1 ()
    <-trans {suc x} {suc y} {suc z} p1 p2 = <-trans {x} {y} {z} p1 p2
    

    其中 () 代表荒谬匹配,即出现 false==true 时就可以直接写 (),也可以像第一条一样,用大括号加上(必要的)参数之后用定义的 𝔹-contra(有点搞不懂原理)

    =ℕ-refl : ∀ (x : ℕ) → (x =ℕ x) ≡ tt
    =ℕ-refl 0 = refl
    =ℕ-refl (suc x) = =ℕ-refl x
    
    =ℕ-from-≡ : ∀ {x y : ℕ} → x ≡ y → x =ℕ y ≡ tt
    =ℕ-from-≡ {x} refl = =ℕ-refl x
    

    也可以用 refl 替换一个等式

    begin-qed

    一种语法,如下:

    +0 : ∀ (y : ℕ) -> y ≡ y + zero 
    +0 zero = refl
    +0 (suc y) = 
        begin
            suc y
        ≡⟨ cong suc (+0 y) ⟩
            suc (y + zero)
        ≡⟨⟩
            suc y + zero
        ∎
    

    <>里的是依据,某些根据定义的依据可以不用写(如zero+x=x)

    作业题

    乘法交换律

    惨淡的证明:

    +assoc' : ∀ (x y z : ℕ) → (x + y) + z ≡ x + (y + z)
    +assoc' x y z rewrite +assoc x y z = refl
    
    *0 : ∀ (x : ℕ) → zero ≡ x * zero
    *0 zero = refl
    *0 (suc x) = *0 x
    
    *suc : (x y : ℕ) → x + x * y ≡ x * suc y 
    *suc zero y = refl
    *suc (suc x) y rewrite +assoc x y (x * y) | +comm x y | +assoc' y x (x * y) | *suc x y = refl
    
    *-comm : (x y : ℕ) → x * y ≡ y * x
    *-comm zero zero = refl
    *-comm zero (suc y) = *-comm zero y
    *-comm (suc x) y rewrite *-comm x y = *suc y x
    

    优化:使用 sym x == y -> y == x,即把+assoc' y x (x * y) 换成 sym ( +assoc y x (x * y) )

    乘法结合律

    精简的证明:

    *-assoc : (x y z : ℕ) → (x * y) * z ≡ x * (y * z)
    *-assoc zero y z = refl
    *-assoc (suc x) y z rewrite *distribr y (x * y) z | *-assoc x y z = refl
    

    一些比较大小

    n≮n : (n : ℕ) → n < n ≡ false
    n≮n zero = refl
    n≮n (suc x) = n≮n x
    
    -- problem 2.2
    <-antisym : (x y : ℕ) → x < y ≡ true → y < x ≡ false
    <-antisym zero (suc y) p1 = refl
    <-antisym (suc x) (suc y) = <-antisym x y 
    
    
    -- problem 2.3
    <-trichotomy : (x y : ℕ) → x < y ∨ x =ℕ y ∨ y < x ≡ true
    <-trichotomy zero zero = refl
    <-trichotomy zero (suc y) = refl
    <-trichotomy (suc x) zero = refl
    <-trichotomy (suc x) (suc y) = <-trichotomy x y
    
  • 相关阅读:
    【020】基于Springboot+Vue的学生成绩教务管理系统(含教师、学生、管理员身份)含源码、数据库、运行教程
    scrapy的安装和使用
    浅谈基于PLC和Modbus的配电室现场环境监控系统设计及产品选型
    手机银行体验性测试:如何获取用户真实感受
    21款奔驰EQC350升级原厂360全景影像 感受上帝视野
    页面置换算法
    TortoiseSVN小乌龟的使用
    【重拾C语言】六、批量数据组织(四)线性表—栈和队列
    QML与C++通信
    idea搭建ssm项目全过程详解:
  • 原文地址:https://www.cnblogs.com/lcyfrog/p/16859343.html