- -

Agda のレコード型

C 言語での構造体に近い
複数のデータをまとめる
関数内で構築できる
構築時はrecord レコード名 {フィールド名 = 値}
複数ある場合は record Env {varn = 1 ; varn = 2}のように ; を使って列挙 +
Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数
CPS の関数は引数として継続を受け取って継続に計算結果を渡す
名前 : 引数 → (Code : fa → t) → t
t は継続
(Code : fa → t) は次の継続先
DataGear は Agda での CodeGear に使われる引数
-
```
1 record Env : Set where 
-2   field
-3     varn : Nat
-4     vari : Nat
+  whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) 
+                   → (Code : Env -> t) -> t
+whileTest c10 next = next (record {varn = c10 ; vari = 0} )
 
 
```
@@ -235,28 +207,46 @@
-
Agda の関数
+
Agda での Gears の記述(whileLoop)
- 関数にも型が必要(1行目) +
- 関数の動作を条件で変えたいときはパターンマッチを行う
- whileLoop は varn が 0 より大きい間ループする
  - 引き算はは自然数を２つ取って結果の自然数を返す
  - _ は任意の値、名前で使うと受け取った引数が順番に入る
  - lt は Nat を２つ受け取って値の大小を比較 +```AGDA +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} -> Env + -> (Code : Env -> t) -> t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = + whileLoop (record {varn = (varn env) - 1 + ; vari = (vari env) + 1}) next
- 関数本体は 関数名 = 値
- 関数ではパターンマッチがかける -
  - ここでは関数名に _ を使っているためNatの定義にから zero かそれ以外でパターンマッチ -
    -
    1 _-_ : Nat → Nat → Nat -2 x - zero = x -3 zero - _ = zero -4 (suc x) - (suc y) = x - y +
  + +
  lt : Nat → Nat → Bool
  +
```
+## Agda での DataGear
+- **DataGear** は CodeGear の引数
+- **データ型**と**レコード型**がある
+- データ型は一つのデータ
+```AGDA
+data Nat : Set where
+  zero : Nat
+  suc  : Nat → Nat
+
```
  +
  - レコード型は複数のデータをまとめる +
    +
    record Env : Set where +field + varn : Nat + vari : Nat
    
    -
    -
  +

@@ -276,10 +266,10 @@

refl は x == x の左右の項が等しいことの証明

1 ∧true : { x : Bool } →  x  ∧  true  ≡ x
-2 ∧true {x} with x
-3 ∧true {x} | false = refl
-4 ∧true {x} | true = refl
+  ∧true : { x : Bool } →  x  ∧  true  ≡ x
+∧true {x} with x
+∧true {x} | false = refl
+∧true {x} | true = refl

@@ -294,6 +284,146 @@

Gears をベースにした HoareLogic と証明(全体)

Gears をベースにした while Program で実行できる +
- これは証明も持っている
+
whileループを任意の回数にするためc10は引数

whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい +

+  proofGears : {c10 :  Nat } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
+       (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+

+

+    

+ + + +

+ +

Gears と HoareLogic をベースにした証明(whileTest)

最初の Command なので PreCondition がない
proof2は Post Condition が成り立つことの証明 +
- /\ は pi1 と pi2 のフィールドをもつレコード型
- ２つのものを引数に取り、両方が同時に成り立つことを示す
+

Gears での PostCondition は 引数 → (Code : fa → PostCondition → t) → t +

+  whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } → 
+      (Code : (env : Env)  → 
+          ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+hileTest' {_} {_} {c10} next = next env proof2
+where
+  env : Env
+  env = record {vari = 0 ; varn = c10}
+  proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)      <-- PostCondition
+  proof2 = record {pi1 = refl ; pi2 = refl}
+

+

+    

+ + + +

+ +

Gears と HoareLogic をベースにした証明(conversion)

conversion は Condition から LoopInvaliant への変換を行う CodeGear +
- Condition の条件は Loop 内では厳しいのでゆるくする
+
proof4 は LoopInvaliant の証明
Gears での HoareLogic の完全な記述は 引数 → PreCondition → (Code : fa → PostCondition → t) → t +```AGDA +conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t +conversion1 env {c10} p1 next = next env proof4 +where + proof4 : varn env + vari env ≡ c10

+ +


+
+##  Agdaでの証明(≡-Reasoning)
+- Agda では証明の項を書き換える構文が用意されている
+```AGDA
+    proof4 : varn env + vari env ≡ c10
+    proof4 = let open ≡-Reasoning  in
+      begin
+        varn env + vari env
+      ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
+        c10 + vari env
+      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
+        c10 + 0
+      ≡⟨ +-sym {c10} {0} ⟩
+        c10
+      ∎
+

+ + + +

+ +

Gears と HoareLogic をベースにした証明(全体)

最終状態で返ってくる i の値は c10 と一致する

これにより証明が可能 +

+    proofGears : {c10 :  Nat } → Set
+  proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
+                 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+

+

+    

+ + + +

+ +

まとめと今後の課題

HoareLogic の while を使った例題を作成、証明を行った
Gears を用いた HoareLogic ベースの検証方法を導入した +
- 証明が引数として渡される記述のため証明とプログラムを一体化できた
+
今後の課題 +
- RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)
+

+ + + +

+ +

Agda 上での HoareLogic

Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと @@ -328,14 +458,14 @@
n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。

次のスライドから Agda 上 HoareLogic を実装し、その上でこの whileProgram の検証を行う

1 n = 10;
-2 i = 0;
-3
-4 while (n>0)
-5 {
-6   i++;
-7   n--;
-8 }
+   n = 10;
+ i = 0;
+
+ while (n>0)
+ {
+   i++;
+   n--;
+ }

@@ -354,13 +484,13 @@

varn、vari はそれぞれ変数 n、 i

Cond は Pre、Post の Condition で Env を受け取って Bool 値(true か false)を返す

1 record Env : Set where
-2   field
-3     varn : Nat
-4     vari : Nat
-5
-6 Cond : Set
-7 Cond = (Env → Bool) 
+   record Env : Set where
+   field
+     varn : Nat
+     vari : Nat
+
+ Cond : Set
+ Cond = (Env → Bool)

@@ -386,14 +516,14 @@

他にも何もしないコマンドやコマンドの停止などのコマンドもある

PrimComm は Env を受け取って Env を返す定義

1   data Comm : Set where
-2     PComm : PrimComm → Comm
-3     Seq   : Comm → Comm → Comm
-4     If    : Cond → Comm → Comm → Comm
-5     While : Cond → Comm → Comm
-6       
-7   PrimComm : Set
-8   PrimComm = Env → Env
+     data Comm : Set where
+     PComm : PrimComm → Comm
+     Seq   : Comm → Comm → Comm
+     If    : Cond → Comm → Comm → Comm
+     While : Cond → Comm → Comm
+       
+   PrimComm : Set
+   PrimComm = Env → Env

@@ -416,13 +546,13 @@

$ は () の糖衣で行頭から行末までを ( ) で囲う

見やすさのため改行しているが 3~7 行は1行

1 program : ℕ → Comm
-2 program c10 = 
-3    Seq ( PComm (λ env → record env {varn = c10}))                -- n = 10;
-4    $ Seq ( PComm (λ env → record env {vari = 0}))                -- i = 0;
-5    $ While (λ env → lt zero (varn env ) )                         -- while (n>0) {
-6      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++;
-7        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))   -- n--;
+   program : ℕ → Comm
+ program c10 = 
+    Seq ( PComm (λ env → record env {varn = c10}))                -- n = 10;
+    $ Seq ( PComm (λ env → record env {vari = 0}))                -- i = 0;
+    $ While (λ env → lt zero (varn env ) )                         -- while (n>0) {
+      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++;
+        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))   -- n--;

@@ -443,17 +573,17 @@

⇒ は pre, post の Condition をとって post の Condition が成り立つときに True を返す

1 data HTProof : Cond → Comm → Cond → Set where
-2 PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} →
-3              (pr : Axiom bPre pcm bPost) →
-4              HTProof bPre (PComm pcm) bPost
-5-- 次のスライドに続く
+   data HTProof : Cond → Comm → Cond → Set where
+ PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} →
+              (pr : Axiom bPre pcm bPost) →
+              HTProof bPre (PComm pcm) bPost
+-- 次のスライドに続く

1 Axiom : Cond → PrimComm → Cond → Set
-2 Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
+   Axiom : Cond → PrimComm → Cond → Set
+ Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true

@@ -473,18 +603,18 @@

SeqRule は Command を推移させる Seq の保証

IfRule は If の Command が正しく動くことを保証

 1-- HTProof の続き
- 2   SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} →
- 3           {cm2 : Comm} → {bPost : Cond} →
- 4           HTProof bPre cm1 bMid →
- 5           HTProof bMid cm2 bPost →
- 6           HTProof bPre (Seq cm1 cm2) bPost
- 7   IfRule : {cmThen : Comm} → {cmElse : Comm} →
- 8          {bPre : Cond} → {bPost : Cond} →
- 9          {b : Cond} →
-10          HTProof (bPre /\ b) cmThen bPost →
-11          HTProof (bPre /\ neg b) cmElse bPost →
-12          HTProof bPre (If b cmThen cmElse) bPost
+  -- HTProof の続き
+   SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} →
+           {cm2 : Comm} → {bPost : Cond} →
+           HTProof bPre cm1 bMid →
+           HTProof bMid cm2 bPost →
+           HTProof bPre (Seq cm1 cm2) bPost
+   IfRule : {cmThen : Comm} → {cmElse : Comm} →
+          {bPre : Cond} → {bPost : Cond} →
+          {b : Cond} →
+          HTProof (bPre /\ b) cmThen bPost →
+          HTProof (bPre /\ neg b) cmElse bPost →
+          HTProof bPre (If b cmThen cmElse) bPost

@@ -503,22 +633,22 @@

Tautology は Condition と不変条件が等しく成り立つ

WhileRule はループ不変条件が成り立つ間 Comm を繰り返す

 1-- HTProof の続き
- 2   WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} →
- 3               {bPost' : Cond} → {bPost : Cond} →
- 4               Tautology bPre bPre' →
- 5               HTProof bPre' cm bPost' →
- 6               Tautology bPost' bPost →
- 7               HTProof bPre cm bPost
- 8   WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} →
- 9               HTProof (bInv /\ b) cm bInv →
-10               HTProof bInv (While b cm) (bInv /\ neg b)
+  -- HTProof の続き
+   WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} →
+               {bPost' : Cond} → {bPost : Cond} →
+               Tautology bPre bPre' →
+               HTProof bPre' cm bPost' →
+               Tautology bPost' bPost →
+               HTProof bPre cm bPost
+   WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} →
+               HTProof (bInv /\ b) cm bInv →
+               HTProof bInv (While b cm) (bInv /\ neg b)

1 Tautology : Cond → Cond → Set
-2 Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
+   Tautology : Cond → Cond → Set
+ Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true

@@ -538,20 +668,20 @@

Condititon は initCond や termCond のようにそれぞれ定義する必要がある

program に近い形で証明を記述できる

 1 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
- 2 proof1 c10 =
- 3       SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
- 4       $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
- 5       $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
- 6          WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
- 7          $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
- 8             $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
- 9
-10 initCond : Cond
-11 initCond env = true
-12
-13 termCond : {c10 : Nat} → Cond
-14 termCond {c10} env = Equal (vari env) c10
+   proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
+ proof1 c10 =
+       SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
+       $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
+       $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
+          WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
+          $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
+             $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
+
+ initCond : Cond
+ initCond env = true
+
+ termCond : {c10 : Nat} → Cond
+ termCond {c10} env = Equal (vari env) c10

@@ -586,22 +716,22 @@

≡-Reasoning は Agda での等式変形

 1  lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10}) 
- 2         (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
- 3  lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
- 4    begin
- 5      (Equal (varn env) c10 ) ∧ true
- 6    ≡⟨ ∧true ⟩
- 7      Equal (varn env) c10 
- 8    ≡⟨ cond ⟩
- 9      true
-10    ∎ )
-11      
-12  stmt1Cond : {c10 : ℕ} → Cond
-13  stmt1Cond {c10} env = Equal (varn env) c10
-14   
-15  stmt2Cond : {c10 : ℕ} → Cond
-16  stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
+    lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10}) 
+         (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+  lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
+    begin
+      (Equal (varn env) c10 ) ∧ true
+    ≡⟨ ∧true ⟩
+      Equal (varn env) c10 
+    ≡⟨ cond ⟩
+      true
+    ∎ )
+      
+  stmt1Cond : {c10 : ℕ} → Cond
+  stmt1Cond {c10} env = Equal (varn env) c10
+   
+  stmt2Cond : {c10 : ℕ} → Cond
+  stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)

@@ -617,187 +747,6 @@

- -

Agda での Gears

Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数
CPS の関数は引数として継続を受け取って継続に計算結果を渡す
名前 : 引数 → (Code : fa → t) → t
t は継続
(Code : fa → t) は次の継続先

DataGear は Agda での CodeGear に使われる引数 -

1_-_ : {t : Set} → Nat → Nat → (Code : Nat → t) → t
-2x - zero = (λ next → next x)
-3zero - _ = (λ next → next zero)
-4(suc x) - (suc y) = (x - y)
-

- - - -

- -

Gears をベースにした HoareLogic と証明(全体)

Gears をベースにした while Program -
- これは証明でもある
-
whileループを任意の回数にするためc10は引数

whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい -

1  proofGears : {c10 :  Nat } → Set
-2  proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
-3                 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
-

- - - -

- -

Gears と HoareLogic をベースにした証明(whileTest)

ここは代入する Command
最初の Command なので PreCondition がない
もとの whileProgram では PComm を2回していたがまとめた
proof2は Post Condition が成り立つことの証明 -
- /\ は pi1 と pi2 のフィールドをもつレコード型
- ２つのものを引数に取り、両方が同時に成り立つことを示す
-

Gears での PostCondition は 引数 → (Code : fa → PostCondition → t) → t -

1  whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } → 
-2              (Code : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-3  whileTest' {_} {_} {c10} next = next env proof2
-4    where
-5      env : Env
-6      env = record {vari = 0 ; varn = c10}
-7      proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)      <-- PostCondition
-8      proof2 = record {pi1 = refl ; pi2 = refl}
-

- - - -

- -

Gears と HoareLogic をベースにした証明(conversion)

conversion は Condition から LoopInvaliant への変換を行う CodeGear
proof4 は LoopInvaliant の証明

Gears での HoareLogic の完全な記述は 引数 → PreCondition → (Code : fa → PostCondition → t) → t -

 1  conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  Nat } → 
- 2                     ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
- 3                     → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
- 4  conversion1 env {c10} p1 next = next env proof4
- 5    where
- 6      proof4 : varn env + vari env ≡ c10
- 7      proof4 = let open ≡-Reasoning  in
- 8        begin
- 9          varn env + vari env
-10        ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
-11          c10 + vari env
-12        ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
-13          c10 + 0
-14        ≡⟨ +-sym {c10} {0} ⟩
-15          c10
-16        ∎
-

- - - -

- -

Gears と HoareLogic をベースにした証明(whileLoop)

whileLoop は loopInvaliant が true の間 WhileLoop を回し続けるCodeGear
この CodeGear は Agda がループが終わることが証明できてないため {-# TERMINATING #-} で明示

false になると次の CodeGear へ -

1  {-# TERMINATING #-}
-2  whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
-3  whileLoop env next with lt 0 (varn env)
-4  whileLoop env next | false = next env
-5  whileLoop env next | true =
-6      whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
-

- - - -

- -

Gears と HoareLogic をベースにした証明(全体)

最終状態で返ってくる i の値は c10 と一致する

これにより証明が可能 -

1  proofGears : {c10 :  Nat } → Set
-2  proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
-3                 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
-

- - - -

- -

まとめと今後の課題

HoareLogic の while を使った例題を作成、証明を行った
Gears を用いた HoareLogic ベースの検証方法を導入した -
- 証明が引数として渡される記述のため証明とプログラムを一体化できた
-
今後の課題 -
- RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)
-

diff -r fde9ee0cc8ae -r b711209123f7 slide/slide.md --- a/slide/slide.md Tue Jan 15 16:52:28 2019 +0900 +++ b/slide/slide.md Tue Jan 15 17:47:18 2019 +0900 @@ -48,22 +48,33 @@ - Agda の文法については次のスライドから軽く説明する ## Agda での Gears の記述(whileLoop) -- Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 -- CPS の関数は引数として継続を受け取って継続に計算結果を渡す +- Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数 +- 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す - **名前 : 引数 → (Code : fa → t) → t** - **t** は継続 - **(Code : fa → t)** は次の継続先 - DataGear は Agda での CodeGear に使われる引数 ```AGDA - whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t - whileTest c10 next = next (record {varn = c10 ; vari = 0} ) +whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) + → (Code : Env -> t) -> t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) +``` - {-# TERMINATING #-} - whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t - whileLoop env next with lt 0 (varn env) - whileLoop env next | false = next env - whileLoop env next | true = - whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next +## Agda での Gears の記述(whileLoop) +- 関数の動作を条件で変えたいときはパターンマッチを行う +- whileLoop は varn が 0 より大きい間ループする + - lt は Nat を２つ受け取って値の大小を比較 +```AGDA +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} -> Env + -> (Code : Env -> t) -> t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = + whileLoop (record {varn = (varn env) - 1 + ; vari = (vari env) + 1}) next + +lt : Nat → Nat → Bool ``` ## Agda での DataGear @@ -71,18 +82,16 @@ - **データ型**と**レコード型**がある - データ型は一つのデータ ```AGDA - data Nat : Set where - zero : Nat - suc : Nat → Nat +data Nat : Set where + zero : Nat + suc : Nat → Nat ``` - レコード型は複数のデータをまとめる -- 構築時は**record レコード名 {フィールド名 = 値}** -- 複数ある場合は **record Env {varn = 1 ; varn = 2}**のように **;** を使って列挙 ```AGDA - record Env : Set where - field - varn : Nat - vari : Nat +record Env : Set where + field + varn : Nat + vari : Nat ``` ## Agda での証明 @@ -93,65 +102,73 @@ - 下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明 - **refl** は **x == x** の左右の項が等しいことの証明 ```AGDA - ∧true : { x : Bool } → x ∧ true ≡ x - ∧true {x} with x - ∧true {x} | false = refl - ∧true {x} | true = refl +∧true : { x : Bool } → x ∧ true ≡ x +∧true {x} with x +∧true {x} | false = refl +∧true {x} | true = refl ``` ## Gears をベースにした HoareLogic と証明(全体) -- Gears をベースにした while Program - - これは証明でもある +- Gears をベースにした while Program で実行できる + - これは証明も持っている - whileループを任意の回数にするため**c10**は引数 - whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい ```AGDA - proofGears : {c10 : Nat } → Set - proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 - (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +proofGears : {c10 : Nat } → Set +proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) ``` ## Gears と HoareLogic をベースにした証明(whileTest) -- ここは代入する Command - 最初の Command なので PreCondition がない -- もとの whileProgram では PComm を2回していたがまとめた - proof2は Post Condition が成り立つことの証明 - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型 - ２つのものを引数に取り、両方が同時に成り立つことを示す - Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** ```AGDA - whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → - (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t - whileTest' {_} {_} {c10} next = next env proof2 - where - env : Env - env = record {vari = 0 ; varn = c10} - proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) <-- PostCondition - proof2 = record {pi1 = refl ; pi2 = refl} +whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → + (Code : (env : Env) → + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t +hileTest' {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) <-- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl} ``` ## Gears と HoareLogic をベースにした証明(conversion) - conversion は Condition から LoopInvaliant への変換を行う CodeGear + - Condition の条件は Loop 内では厳しいのでゆるくする - proof4 は LoopInvaliant の証明 - Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t** ```AGDA - conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → - ((vari env) ≡ 0) /\ ((varn env) ≡ c10) - → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t - conversion1 env {c10} p1 next = next env proof4 - where - proof4 : varn env + vari env ≡ c10 - proof4 = let open ≡-Reasoning in - begin - varn env + vari env - ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ - c10 + vari env - ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ - c10 + 0 - ≡⟨ +-sym {c10} {0} ⟩ - c10 - ∎ +conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t +conversion1 env {c10} p1 next = next env proof4 + where + proof4 : varn env + vari env ≡ c10 + ``` + +## Agdaでの証明(≡-Reasoning) +- Agda では証明の項を書き換える構文が用意されている +```AGDA + proof4 : varn env + vari env ≡ c10 + proof4 = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ + c10 + vari env + ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + c10 + ∎ +``` + ## Gears と HoareLogic をベースにした証明(全体) - 最終状態で返ってくる i の値は c10 と一致する - これにより証明が可能

Agda のデータ型

Agda での Gears の記述(whileLoop)

Agda のレコード型

Agda の関数

Agda での Gears の記述(whileLoop)

Gears をベースにした HoareLogic と証明(全体)

Gears と HoareLogic をベースにした証明(whileTest)

Gears と HoareLogic をベースにした証明(conversion)

Gears と HoareLogic をベースにした証明(全体)

まとめと今後の課題

Agda 上での HoareLogic

Agda での Gears

Gears をベースにした HoareLogic と証明(全体)

Gears と HoareLogic をベースにした証明(whileTest)

Gears と HoareLogic をベースにした証明(conversion)

Gears と HoareLogic をベースにした証明(whileLoop)

Gears と HoareLogic をベースにした証明(全体)

まとめと今後の課題