Mercurial > hg > Members > ryokka > HoareLogic

changeset 14:a622d1700a1b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
make 10 variable
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Dec 2018 08:19:47 +0900
parents 575b849cab1a
children 8d546766a9a8
files whileTestGears.agda whileTestPrim.agda
diffstat 2 files changed, 111 insertions(+), 107 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Sun Dec 16 07:34:03 2018 +0900
+++ b/whileTestGears.agda	Sun Dec 16 08:19:47 2018 +0900
@@ -16,8 +16,8 @@
     vari : ℕ
 open Env
 
-whileTest : {l : Level} {t : Set l} -> (Code : Env -> t) -> t
-whileTest next = next (record {varn = 10 ; 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
@@ -27,18 +27,18 @@
     whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 
 test1 : Env
-test1 = whileTest (λ env → whileLoop env (λ env1 → env1 ))
+test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
 
 
-proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
+proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 = refl
 
-whileTest' : {l : Level} {t : Set l}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) /\ ((varn env) ≡ 10) -> t) -> t
-whileTest' next = next env proof2
+whileTest' : {l : Level} {t : Set l}  -> {c10 :  ℕ } → (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 = 10}
-    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ 10)
+    env = record {vari = 0 ; varn = c10}
+    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
     proof2 = record {pi1 = refl ; pi2 = refl}
 
 open import Data.Empty
@@ -46,15 +46,15 @@
 
 
 {-# TERMINATING #-}
-whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> ((varn env) + (vari env) ≡ 10) -> (Code : Env -> t) -> t
+whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) -> (Code : Env -> t) -> t
 whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
 whileLoop' env proof next | no p = next env 
-whileLoop' env proof next | yes p = whileLoop' env1 (proof3 p ) next
+whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
     where
       env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
       1<0 : 1 ≤ zero → ⊥
       1<0 ()
-      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ 10
+      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
       proof3 (s≤s lt) with varn  env
       proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
       proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
@@ -69,29 +69,29 @@
           ≡⟨⟩
              varn env + vari env
           ≡⟨ proof  ⟩
-             10
+             c10
           ∎
 
 
-conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) /\ ((varn env) ≡ 10)
-               -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ 10) -> t) -> t
-conversion1 env p1 next = next env proof4
+conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 :  ℕ } → ((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 ≡ 10
+      proof4 : varn env + vari env ≡ c10
       proof4 = let open ≡-Reasoning  in
           begin
             varn env + vari env
           ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
-            10 + vari env
-          ≡⟨ cong ( λ n → 10 + n ) (pi1 p1 ) ⟩
-            10 + 0
-          ≡⟨⟩
-            10
+            c10 + vari env
+          ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
+            c10 + 0
+          ≡⟨ +-sym {c10} {0} ⟩
+            c10
           ∎
 
 
-proofGears : Set
-proofGears = whileTest' (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ 10 )))) 
+proofGears : {c10 :  ℕ } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
-proofGearsMeta : whileTest' (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ 10 )))) 
-proofGearsMeta = refl
+proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+proofGearsMeta {c10} = {!!}
--- a/whileTestPrim.agda	Sun Dec 16 07:34:03 2018 +0900
+++ b/whileTestPrim.agda	Sun Dec 16 08:19:47 2018 +0900
@@ -31,17 +31,17 @@
 
 ---------------------------
 
-program : Comm
-program = 
-    Seq ( PComm (λ env → record env {varn = 10}))
+program : ℕ → Comm
+program c10 = 
+    Seq ( PComm (λ env → record env {varn = c10}))
     $ Seq ( PComm (λ env → record env {vari = 0}))
     $ While (λ env → lt zero (varn env ) )
       (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
         $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
 
-simple : Comm
-simple = 
-    Seq ( PComm (λ env → record env {varn = 10}))
+simple : ℕ → Comm
+simple c10 = 
+    Seq ( PComm (λ env → record env {varn = c10}))
     $  PComm (λ env → record env {vari = 0})
 
 {-# TERMINATING #-}
@@ -58,13 +58,13 @@
 ... | false = env
 
 test1 : Env
-test1 =  interpret ( record { vari = 0  ; varn = 0 } ) program
+test1 =  interpret ( record { vari = 0  ; varn = 0 } ) (program 10)
 
 eval-proof : vari test1 ≡ 10
 eval-proof = refl
 
 tests : Env
-tests =  interpret ( record { vari = 0  ; varn = 0 } ) simple
+tests =  interpret ( record { vari = 0  ; varn = 0 } ) (simple 10)
 
 
 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true 
@@ -114,72 +114,76 @@
 initCond : Cond
 initCond env = true
 
-stmt1Cond : Cond
-stmt1Cond env = Equal (varn env) 10
+stmt1Cond : {c10 : ℕ} → Cond
+stmt1Cond {c10} env = Equal (varn env) c10
 
-stmt2Cond : Cond
-stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0)
+stmt2Cond : {c10 : ℕ} → Cond
+stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
 
-whileInv : Cond
-whileInv env = Equal ((varn env) + (vari env)) 10
+whileInv : {c10 : ℕ} → Cond
+whileInv {c10} env = Equal ((varn env) + (vari env)) c10
 
-whileInv' : Cond
-whileInv' env = Equal ((varn env) + (vari env)) 11 ∧ lt zero (varn env)
+whileInv' : {c10 : ℕ} → Cond
+whileInv'{c10}  env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
 
-termCond : Cond
-termCond env = Equal (vari env) 10
+termCond : {c10 : ℕ} → Cond
+termCond {c10} env = Equal (vari env) c10
 
-proofs : HTProof initCond simple stmt2Cond
-proofs =
-      SeqRule {initCond} ( PrimRule empty-case )
-    $ PrimRule {stmt1Cond} {_} {stmt2Cond} lemma
+proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10})
+proofs c10 =
+      SeqRule {initCond} ( PrimRule {!!} )
+    $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma {c10})
   where
-     lemma : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
-     lemma env with stmt1Cond env
-     lemma env | false = refl
-     lemma env | true = refl
+     lemma : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+     lemma env with (stmt1Cond {c10}) env
+     lemma env | false = {!!}
+     lemma env | true = {!!}
 
 open import Data.Empty
 
 open import Data.Nat.Properties
 
-proof1 : HTProof initCond program termCond
-proof1 =
-      SeqRule {λ e → true} ( PrimRule empty-case )
-    $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
-    $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
-            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
+proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
+proof1 c10 =
+      SeqRule {λ e → true} ( PrimRule {!!} )
+    $ 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
   where
-     lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
-     lemma1 env with stmt1Cond env
-     lemma1 env | false = refl
-     lemma1 env | true = refl
-     lemma21 : {env : Env } → stmt2Cond env ≡ true → varn env ≡ 10
+     lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+     lemma1 {c10} env with (stmt1Cond {c10}) env
+     lemma1 {c10} env | false = {!!}
+     lemma1 {c10} env | true = {!!}
+     lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
      lemma21 eq = Equal→≡ (∧-pi1 eq)
-     lemma22 : {env : Env } → stmt2Cond env ≡ true → vari env ≡ 0
+     lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
      lemma22 eq = Equal→≡ (∧-pi2 eq)
-     lemma23 :  {env : Env } → stmt2Cond env ≡ true → varn env + vari env ≡ 10
-     lemma23 {env} eq = let open ≡-Reasoning  in
+     lemma23 :  {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
+     lemma23 {env} {c10} eq = let open ≡-Reasoning  in
           begin
             varn env + vari env
           ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
-            10 + vari env
-          ≡⟨ cong ( \ x -> 10 + x) (lemma22 eq  ) ⟩
-            10
+            c10 + vari env
+          ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} {!!}  ) ⟩
+            c10 + 0
+          ≡⟨ +-sym {c10} {0} ⟩
+            0 + c10 
+          ≡⟨⟩
+            c10 
           ∎
-     lemma2 :  Tautology stmt2Cond whileInv
-     lemma2 env = bool-case (stmt2Cond env) (
+     lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv
+     lemma2 {c10} env = bool-case (stmt2Cond env) (
         λ eq → let open ≡-Reasoning  in
           begin
             (stmt2Cond env)  ⇒  (whileInv env)
           ≡⟨⟩
-            (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) 10 )
-          ≡⟨  cong ( \ x -> (stmt2Cond env)  ⇒ ( Equal x 10 ) ) ( lemma23 {env} eq ) ⟩
-            (stmt2Cond env)  ⇒ (Equal 10 10)
-          ≡⟨⟩
-            (stmt2Cond env)  ⇒  true
+            (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) c10 )
+          ≡⟨  cong ( \ x -> (stmt2Cond  {c10} env)  ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
+            (stmt2Cond env)  ⇒ (Equal c10 c10)
+          ≡⟨ {!!} ⟩
+            (stmt2Cond {c10} env)  ⇒  true
           ≡⟨ ⇒t ⟩
             true
           ∎
@@ -188,8 +192,8 @@
           begin
             (stmt2Cond env)  ⇒  (whileInv env)
           ≡⟨ cong ( \ x -> x  ⇒  (whileInv env) ) ne ⟩
-             false  ⇒  (whileInv env)
-          ≡⟨ f⇒ {whileInv env} ⟩
+             false  ⇒  (whileInv {c10} env)
+          ≡⟨ f⇒ {whileInv {c10} env} ⟩
             true
           ∎
         ) 
@@ -198,43 +202,43 @@
           begin
             whileInv' (record { varn = varn env ; vari = vari env + 1 }) 
           ≡⟨⟩
-             Equal (varn env + (vari env + 1)) 11 ∧ (lt 0 (varn env) )
-          ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) 11 ∧ z ) (∧-pi2 cond )  ⟩
-             Equal (varn env + (vari env + 1)) 11 ∧ true
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
+          ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond )  ⟩
+             Equal (varn env + (vari env + 1)) (suc c10) ∧ true
           ≡⟨ ∧true ⟩
-            Equal (varn env + (vari env + 1)) 11
-          ≡⟨ cong ( \ x -> Equal x 11 ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
-            Equal ((varn env + vari env) + 1) 11
-          ≡⟨ cong ( \ x -> Equal x 11 ) +1≡suc ⟩
-            Equal (suc (varn env + vari env)) 11
+            Equal (varn env + (vari env + 1)) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
+            Equal ((varn env + vari env) + 1) (suc c10)
+          ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
+            Equal (suc (varn env + vari env)) (suc c10)
           ≡⟨ sym Equal+1 ⟩
-            Equal ((varn env + vari env) ) 10
+            Equal ((varn env + vari env) ) c10
           ≡⟨ ∧-pi1  cond ⟩
             true
           ∎ )
-     lemma41 : (env : Env ) → (varn env + vari env) ≡ 11 → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) 10 ≡ true
-     lemma41 env c1 c2 =  let open ≡-Reasoning  in
+     lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) c10 ≡ true
+     lemma41 env {c10} c1 c2 =  let open ≡-Reasoning  in
           begin
-            Equal ((varn env - 1) + vari env) 10
-          ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) 10 ) (sym (suc-predℕ=n c2) )  ⟩
-            Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) 10
+            Equal ((varn env - 1) + vari env) c10
+          ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-predℕ=n c2) )  ⟩
+            Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
           ≡⟨⟩
-            Equal ((predℕ {varn env} c2 ) + vari env) 10
+            Equal ((predℕ {varn env} c2 ) + vari env) c10
           ≡⟨  Equal+1 ⟩
-            Equal ((suc (predℕ {varn env} c2 )) + vari env) 11
-          ≡⟨ cong ( λ z → Equal (z  +  vari env ) 11 ) (suc-predℕ=n c2 )  ⟩
-            Equal (varn env + vari env) 11
-          ≡⟨ cong ( λ z → (Equal z 11 )) c1 ⟩
-            Equal 11 11
-          ≡⟨⟩
+            Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
+          ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-predℕ=n c2 )  ⟩
+            Equal (varn env + vari env) (suc c10)
+          ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
+            Equal (suc c10) (suc c10)
+          ≡⟨ {!!} ⟩
             true
           ∎
-     lemma4 :  Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
-     lemma4 env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+     lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
+     lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
           begin
             whileInv (record { varn = varn env - 1 ; vari = vari env })
           ≡⟨⟩
-            Equal ((varn env - 1) + vari env) 10
+            Equal ((varn env - 1) + vari env) c10
           ≡⟨ lemma41 env (Equal→≡ (∧-pi1  cond)) (∧-pi2  cond) ⟩
             true
           ∎
@@ -246,16 +250,16 @@
      lemma51 z refl | _ | no ¬p with varn z
      lemma51 z refl | _ | no ¬p | zero = refl
      lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) )
-     lemma5 :  Tautology ((λ e → Equal (varn e + vari e) 10) and (neg (λ z → lt zero (varn z)))) termCond
-     lemma5 env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+     lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
+     lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
          begin
             termCond env
           ≡⟨⟩
-             Equal (vari env) 10 
+             Equal (vari env) c10 
           ≡⟨⟩
-             Equal (zero + vari env) 10 
-          ≡⟨ cong ( λ z →  Equal (z + vari env) 10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
-             Equal (varn env + vari env) 10 
+             Equal (zero + vari env) c10 
+          ≡⟨ cong ( λ z →  Equal (z + vari env) c10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
+             Equal (varn env + vari env) c10 
           ≡⟨ ∧-pi1  cond  ⟩
              true
           ∎