changeset 13:575b849cab1a

add todo
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Dec 2018 07:34:03 +0900
parents 247ce3e67b5f
children a622d1700a1b
files Hoare.agda Todo whileTest.agda whileTestGears.agda
diffstat 4 files changed, 7 insertions(+), 382 deletions(-) [+]
line wrap: on
line diff
--- a/Hoare.agda	Sat Dec 15 17:24:35 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-{-# OPTIONS --universe-polymorphism #-}
-
-open import Level
-open import Data.Nat
-open import Data.Product
-open import Relation.Binary
-open import Relation.Nullary
-open import SET
-
-module Hoare
-    (Cond : Set)
-    (PrimComm : Set)
-    (neg : Cond -> Cond)
-    (_/\_ : Cond -> Cond -> Cond)
-    (Tautology : Cond -> Cond -> Set)
-    (State : Set)
-    (SemCond : Cond -> Pred State)
-    (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
-                 (s : State) -> SemCond b1 s -> SemCond b2 s)
-    (respNeg : (b : Cond) -> (s : State) ->
-               Iff (SemCond (neg b) s) (¬ SemCond b s))
-    (respAnd : (b1 b2 : Cond) -> (s : State) ->
-               Iff (SemCond (b1 /\ b2) s)
-                   ((SemCond b1 s) × (SemCond b2 s)))
-    (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l)
-    (Axiom : Cond -> PrimComm -> Cond -> Set)
-    (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
-                  (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
-                  SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2)
- where
-
-open import RelOp
-module RelOpState = RelOp State
-
-_\/_ : Cond -> Cond -> Cond
-b1 \/ b2 = neg (neg b1 /\ neg b2)
-
-_==>_ : Cond -> Cond -> Cond
-b1 ==> b2 = neg (b1 \/ b2)
-
-data Comm : Set where
-  Skip  : Comm
-  Abort : Comm
-  PComm : PrimComm -> Comm
-  Seq   : Comm -> Comm -> Comm
-  If    : Cond -> Comm -> Comm -> Comm
-  While : Cond -> Comm -> Comm
-
--- Hoare Triple
--- data HT : Set where
---   ht : Cond -> Comm -> Cond -> HT
-
-{-
-                prPre              pr              prPost
-             -------------  ------------------  ----------------
-             bPre => bPre'  {bPre'} c {bPost'}  bPost' => bPost
-Weakening : ----------------------------------------------------
-                       {bPre} c {bPost}
-
-Assign: ----------------------------
-         {bPost[v<-e]} v:=e {bPost}
-
-             pr1                pr2
-      -----------------  ------------------
-      {bPre} cm1 {bMid}  {bMid} cm2 {bPost}
-Seq: ---------------------------------------
-      {bPre} cm1 ; cm2 {bPost}
-
-               pr1                         pr2
-     -----------------------  ---------------------------
-     {bPre /\ c} cm1 {bPost}  {bPre /\ neg c} cm2 {bPost}
-If: ------------------------------------------------------
-     {bPre} If c then cm1 else cm2 fi {bPost}
-
-                          pr
-                 -------------------
-                 {inv /\ c} cm {inv}
-While: ---------------------------------------
-        {inv} while c do cm od {inv /\ neg c}
--}
-
--- Hoare Triple Proof
-
-data HTProof : Cond -> Comm -> Cond -> Set where
-  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
-             (pr : Axiom bPre pcm bPost) ->
-             HTProof bPre (PComm pcm) bPost
-  SkipRule : (b : Cond) -> HTProof b Skip b
-  AbortRule : (bPre : Cond) -> (bPost : Cond) ->
-              HTProof bPre Abort bPost
-  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
-  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
-  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
-              HTProof (bInv /\ b) cm bInv ->
-              HTProof bInv (While b cm) (bInv /\ neg b)
-
--- semantics of commands
-SemComm : Comm -> Rel State (Level.zero)
-SemComm Skip = RelOpState.deltaGlob
-SemComm Abort = RelOpState.emptyRel
-SemComm (PComm pc) = PrimSemComm pc
-SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
-SemComm (If b c1 c2)
-  = RelOpState.union
-      (RelOpState.comp (RelOpState.delta (SemCond b))
-                       (SemComm c1))
-      (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
-                       (SemComm c2))
-SemComm (While b c)
-  = RelOpState.unionInf
-      (λ (n : ℕ) ->
-        RelOpState.comp (RelOpState.repeat
-                           n
-                           (RelOpState.comp
-                             (RelOpState.delta (SemCond b))
-                             (SemComm c)))
-                         (RelOpState.delta (NotP (SemCond b))))
-
-Satisfies : Cond -> Comm -> Cond -> Set
-Satisfies bPre cm bPost
-  = (s1 : State) -> (s2 : State) ->
-      SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
-
-Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
-            HTProof bPre cm bPost -> Satisfies bPre cm bPost
-Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
-  = axiomValid bPre cm bPost pr s1 s2 q1 q2
-Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
-  = substId1 {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
-Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
-Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
-          s1 s2 q1 q2
-  = let hyp : Satisfies bPre' cm bPost'
-        hyp = Soundness pr
-        r1 : SemCond bPre' s1
-        r1 = tautValid bPre bPre' tautPre s1 q1
-        r2 : SemCond bPost' s2
-        r2 = hyp s1 s2 r1 q2
-    in tautValid bPost' bPost tautPost s2 r2
-Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
-           s1 s2 q1 q2
-  = let hyp1 : Satisfies bPre cm1 bMid
-        hyp1 = Soundness pr1
-        hyp2 : Satisfies bMid cm2 bPost
-        hyp2 = Soundness pr2
-        sMid : State
-        sMid = proj₁ q2
-        r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2
-        r1 = proj₂ q2
-        r2 : SemComm cm1 s1 sMid
-        r2 = proj₁ r1
-        r3 : SemComm cm2 sMid s2
-        r3 = proj₂ r1
-        r4 : SemCond bMid sMid
-        r4 = hyp1 s1 sMid q1 r2
-    in hyp2 sMid s2 r4 r3
-Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
-          s1 s2 q1 q2
-  = let hypThen : Satisfies (bPre /\ b) cmThen bPost
-        hypThen = Soundness pThen
-        hypElse : Satisfies (bPre /\ neg b) cmElse bPost
-        hypElse = Soundness pElse
-        rThen : RelOpState.comp
-                  (RelOpState.delta (SemCond b))
-                  (SemComm cmThen) s1 s2 ->
-                SemCond bPost s2
-        rThen = λ h ->
-                  let t1 : SemCond b s1 × SemComm cmThen s1 s2
-                      t1 = (proj₂ (RelOpState.deltaRestPre
-                                     (SemCond b)
-                                     (SemComm cmThen) s1 s2)) h
-                      t2 : SemCond (bPre /\ b) s1
-                      t2 = (proj₂ (respAnd bPre b s1))
-                           (q1 , proj₁ t1)
-                  in hypThen s1 s2 t2 (proj₂ t1)
-        rElse : RelOpState.comp
-                  (RelOpState.delta (NotP (SemCond b)))
-                  (SemComm cmElse) s1 s2 ->
-                SemCond bPost s2
-        rElse = λ h ->
-                  let t10 : (NotP (SemCond b) s1) ×
-                            (SemComm cmElse s1 s2)
-                      t10 = proj₂ (RelOpState.deltaRestPre
-                                    (NotP (SemCond b)) (SemComm cmElse) s1 s2)
-                            h
-                      t6 : SemCond (neg b) s1
-                      t6 = proj₂ (respNeg b s1) (proj₁ t10)
-                      t7 : SemComm cmElse s1 s2
-                      t7 = proj₂ t10
-                      t8 : SemCond (bPre /\ neg b) s1
-                      t8 = proj₂ (respAnd bPre (neg b) s1)
-                           (q1 , t6)
-                  in hypElse s1 s2 t8 t7
-    in when rThen rElse q2
-Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
-  = proj₂ (respAnd bInv (neg b) s2) t20
-    where
-      hyp : Satisfies (bInv /\ b) cm' bInv
-      hyp = Soundness pr
-      n : ℕ
-      n = proj₁ q2
-      Rel1 : ℕ -> Rel State (Level.zero)
-      Rel1 = λ m ->
-               RelOpState.repeat
-                 m
-                 (RelOpState.comp (RelOpState.delta (SemCond b))
-                                  (SemComm cm'))
-      t1 : RelOpState.comp
-             (Rel1 n)
-             (RelOpState.delta (NotP (SemCond b))) s1 s2
-      t1 = proj₂ q2
-      t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2)
-      t15 = proj₂ (RelOpState.deltaRestPost
-                    (NotP (SemCond b)) (Rel1 n) s1 s2)
-              t1
-      t16 : Rel1 n s1 s2
-      t16 = proj₁ t15
-      t17 : NotP (SemCond b) s2
-      t17 = proj₂ t15
-      lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 ->
-             SemCond bInv ss2
-      lem1 ℕ.zero ss2 h
-        = substId1 (proj₂ h) (SemCond bInv) q1
-      lem1 (ℕ.suc n) ss2 h
-        = let hyp2 : (z : State) -> Rel1 n s1 z ->
-                     SemCond bInv z
-              hyp2 = lem1 n
-              s20 : State
-              s20 = proj₁ h
-              t21 : Rel1 n s1 s20
-              t21 = proj₁ (proj₂ h)
-              t22 : (SemCond b s20) × (SemComm cm' s20 ss2)
-              t22 = proj₂ (RelOpState.deltaRestPre
-                            (SemCond b) (SemComm cm') s20 ss2)
-                    (proj₂ (proj₂ h))
-              t23 : SemCond (bInv /\ b) s20
-              t23 = proj₂ (respAnd bInv b s20)
-                    (hyp2 s20 t21 , proj₁ t22)
-          in hyp s20 ss2 t23 (proj₂ t22)
-      t20 : SemCond bInv s2 × SemCond (neg b) s2
-      t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Todo	Sun Dec 16 07:34:03 2018 +0900
@@ -0,0 +1,6 @@
+Sun Dec 16 07:32:06 JST 2018
+
+    Gears の方に term condition を入れる
+    initial condition に変数を入れる (証明でしか計算できないようにするため)
+    Gears 側の証明をメタ計算的にする
+    メタ計算以外は元の計算を保存する用にする
--- a/whileTest.agda	Sat Dec 15 17:24:35 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-module whileTest where
-
-open import Data.Nat
-open import Data.Bool hiding (_≟_)
-open import Data.Product
-open import Relation.Nullary
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
-open import SET
-import Level
-
-record Env : Set where
-  field
-    varn : ℕ
-    vari : ℕ
-open Env
-
-PrimComm = Env → Env
-
-Cond = Env → Bool
-
-neg : (Env → Bool) → (Env → Bool)
-neg x e = not (x e)
- 
-and : (Env → Bool) → (Env → Bool)  → (Env → Bool)
-and x y e = (x e) ∧ (y e)
-
-data Comm : Set where
-  Skip  : Comm
-  Abort : Comm
-  PComm : PrimComm -> Comm
-  Seq   : Comm -> Comm -> Comm
-  If    : Cond -> Comm -> Comm -> Comm
-  While : Cond -> Comm -> Comm
-
-data HTProof : Cond -> Comm -> Cond -> Set (Level.suc (Level.suc Level.zero)) where
-  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
-             (pr :  Cond -> PrimComm -> Cond -> Set (Level.suc Level.zero)) ->
-             HTProof bPre (PComm pcm) bPost
-  SkipRule : (b : Cond) -> HTProof b Skip b
-  AbortRule : (bPre : Cond) -> (bPost : Cond) ->
-              HTProof bPre Abort bPost
-  WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
-                {bPost' : Cond} -> {bPost : Cond} ->
-                bPre ≡ bPre' ->
-                HTProof bPre' cm bPost' ->
-                bPost' ≡ bPost ->
-                HTProof bPre cm bPost
-  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 (and bPre b) cmThen bPost ->
-           HTProof (and bPre (neg b)) cmElse bPost ->
-           HTProof bPre (If b cmThen cmElse) bPost
-  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
-              HTProof (and bInv b) cm bInv ->
-              HTProof bInv (While b cm) (and bInv (neg b))
-  Rule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> {w : Cond} ->
-              HTProof w cm bInv ->
-              HTProof bInv (While b cm) (and bInv (neg b))
-
-
-lt : ℕ → ℕ → Bool
-lt x y with x <? y
-lt x y | yes p = true
-lt x y | no ¬p = false
-
-_-_ : ℕ → ℕ → ℕ
-x - zero = x
-zero - (suc _) = zero
-(suc x) - (suc y) = x - y
-
-_==_ : ℕ → ℕ → Bool
-x == y with x ≟ y
-(x == y) | yes p = true
-(x == y) | no ¬p = false
-
-
-program : Comm
-program = 
-    Seq ( PComm (λ env → record env {varn = 10}))
-    (Seq ( PComm (λ env → record env {vari = 0}))
-    (While (λ env → lt 0 (varn env) )
-      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
-        (PComm (λ env → record env {varn = ((varn env) - 1)} )))))
-
-{-# TERMINATING #-}
-interpret : Env → Comm → Env
-interpret env Skip = env
-interpret env Abort = env
-interpret env (PComm  x) = x env
-interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
-interpret env (If x then else) with x env
-... | true = interpret env then
-... | false = interpret env else
-interpret env (While x comm) with x env
-... | true = interpret (interpret env comm) (While x comm)
-... | false = env
-
-test1 = interpret (record {vari = 0 ; varn = 0}) program
-
-initCond : Env → Bool
-initCond _ = true
-
-termCond : Env → Bool
-termCond env = (vari env) == 10
-
-iff : Bool → Bool → Bool
-iff true true = true
-iff false false = true
-iff _ _ = false
-
-proposition1 : Cond → PrimComm → Cond → Env → Set
-proposition1 pre cmd post = λ (env : Env) → {!!} -- iff (pre env) (post (cmd env))
-
-proof1 : HTProof initCond program termCond
-proof1 = SeqRule (PrimRule {!!} )
-         (SeqRule (PrimRule {!!} )
-         (Rule {!!}  (WhileRule ?)))
-
--- a/whileTestGears.agda	Sat Dec 15 17:24:35 2018 +0900
+++ b/whileTestGears.agda	Sun Dec 16 07:34:03 2018 +0900
@@ -63,7 +63,7 @@
           ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
              n' + (1 + vari env ) 
           ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-             (n' + 1 ) + vari env 
+             (n' + 1) + vari env 
           ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
              (suc n' ) + vari env 
           ≡⟨⟩