# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1544772409 -32400
# Node ID 6be8ee856666720f0faf79b0111f7b55e1921798
# Parent  b05a4156da01c2a9a7bda167921152b19f6f3bab
add simple Hoare logic example

diff -r b05a4156da01 -r 6be8ee856666 whileTestPrim.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/whileTestPrim.agda	Fri Dec 14 16:26:49 2018 +0900
@@ -0,0 +1,185 @@
+module whileTestPrim where
+
+open import Function
+open import Data.Nat
+open import Data.Bool hiding ( _≟_ )
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary.Core 
+
+
+
+record Env : Set where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
+PrimComm : Set
+PrimComm = Env → Env
+
+Cond : Set
+Cond = (Env → Bool) 
+
+data Comm : Set where
+  Skip  : Comm
+  Abort : Comm
+  PComm : PrimComm -> Comm
+  Seq   : Comm -> Comm -> Comm
+  If    : Cond -> Comm -> Comm -> Comm
+  While : Cond -> Comm -> Comm
+
+_-_ : ℕ -> ℕ -> ℕ
+x - zero  = x
+zero - _  = zero
+(suc x) - (suc y)  = x - y
+
+lt : ℕ -> ℕ -> Bool
+lt x y with (suc x ) ≤? y
+lt x y | yes p = true
+lt x y | no ¬p = false
+
+Equal : ℕ -> ℕ -> Bool
+Equal x y with x ≟ y
+Equal x y | yes p = true
+Equal 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 (varn env ) zero )
+      (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}))
+    $  PComm (λ env → record env {vari = 0})
+
+{-# 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 : Env
+test1 =  interpret ( record { vari = 0  ; varn = 0 } ) program
+
+
+empty-case : (env : Env) → (( λ e → true ) env ) ≡ true 
+empty-case _ = refl
+
+implies : Bool → Bool → Bool
+implies false _ = true
+implies true true = true
+implies true false = false
+
+Axiom : Cond -> PrimComm -> Cond -> Set
+Axiom pre comm post = ∀ (env : Env) →  implies (pre env) ( post (comm env)) ≡ true
+
+Tautology : Cond -> Cond -> Set
+Tautology pre post = ∀ (env : Env) →  implies (pre env) (post env) ≡ true
+
+_/\_ :  Cond -> Cond -> Cond
+x /\ y =  λ env → x env ∧ y env 
+
+neg :  Cond -> Cond 
+neg x  =  λ env → not ( x env )
+
+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)
+
+initCond : Cond
+initCond env = true
+
+stmt1Cond : Cond
+stmt1Cond env = Equal (varn env) 10
+
+stmt2Cond : Cond
+stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0)
+
+whileInv : Cond
+whileInv env = Equal ((varn env) + (vari env)) 10
+
+whileInv' : Cond
+whileInv' env = Equal ((varn env) + (vari env)) 11
+
+termCond : Cond
+termCond env = Equal (vari env) 10
+
+eqlemma : { x y : ℕ } →  Equal x y ≡ true → x ≡ y
+eqlemma {x} {y} eq with x ≟ y
+eqlemma {x} {y} refl | yes refl = refl
+eqlemma {x} {y} () | no ¬p 
+
+proofs : HTProof initCond simple stmt2Cond
+proofs =
+      SeqRule {initCond} ( PrimRule empty-case )
+    $ PrimRule {stmt1Cond} {_} {stmt2Cond} lemma
+  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
+
+
+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}
+            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt (varn e) zero } 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
+     lemma2 :  Tautology stmt2Cond whileInv
+     lemma2 env with stmt2Cond env | Equal (varn env + vari env) 10
+     lemma2 env | false | false = refl
+     lemma2 env | false | true = refl
+     lemma2 env | true | true = refl
+     lemma2 env | true | false = {!!}
+     lemma3 : Axiom (whileInv /\ (λ env → lt (varn env) zero)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
+     lemma3 = {!!}
+     lemma4 :  Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
+     lemma4 = {!!}
+     lemma5 :  Tautology (whileInv /\ neg (λ z → lt (varn z) zero)) termCond
+     lemma5 = {!!}
+
+