Mercurial > hg > Members > ryokka > HoareLogic
changeset 8:e4f087b823d4
add proofs
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Dec 2018 11:38:55 +0900 |
| parents | e7d6bdb6039d |
| children | 46b301ad4478 |
| files | whileTestPrim.agda |
| diffstat | 1 files changed, 127 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestPrim.agda Fri Dec 14 22:35:38 2018 +0900 +++ b/whileTestPrim.agda Sat Dec 15 11:38:55 2018 +0900 @@ -43,6 +43,73 @@ Equal x y | yes p = true Equal x y | no ¬p = false +--------------------------- + +implies : Bool → Bool → Bool +implies false _ = true +implies true true = true +implies true false = false + +impl-1 : {x : Bool} → implies x true ≡ true +impl-1 {x} with x +impl-1 {x} | false = refl +impl-1 {x} | true = refl + +impl-2 : {x : Bool} → implies false x ≡ true +impl-2 {x} with x +impl-2 {x} | false = refl +impl-2 {x} | true = refl + +and-lemma-1 : { x y : Bool } → x ∧ y ≡ true → x ≡ true +and-lemma-1 {x} {y} eq with x | y | eq +and-lemma-1 {x} {y} eq | false | b | () +and-lemma-1 {x} {y} eq | true | false | () +and-lemma-1 {x} {y} eq | true | true | refl = refl + +and-lemma-2 : { x y : Bool } → x ∧ y ≡ true → y ≡ true +and-lemma-2 {x} {y} eq with x | y | eq +and-lemma-2 {x} {y} eq | false | b | () +and-lemma-2 {x} {y} eq | true | false | () +and-lemma-2 {x} {y} eq | true | true | refl = refl + +bool-case : ( x : Bool ) { p : Set } → ( x ≡ true → p ) → ( x ≡ false → p ) → p +bool-case x T F with x +bool-case x T F | false = F refl +bool-case x T F | true = T refl + +impl : {x y : Bool} → (x ≡ true → y ≡ true ) → implies x y ≡ true +impl {x} {y} p = bool-case x (λ x=t → let open ≡-Reasoning in + begin + implies x y + ≡⟨ cong ( \ z -> implies x z ) (p x=t ) ⟩ + implies x true + ≡⟨ impl-1 ⟩ + true + ∎ + ) ( λ x=f → let open ≡-Reasoning in + begin + implies x y + ≡⟨ cong ( \ z -> implies z y ) x=f ⟩ + true + ∎ + ) + +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 + +eqlemma1 : { x y : ℕ } → Equal x y ≡ Equal (suc x) (suc y) +eqlemma1 {x} {y} with x ≟ y +eqlemma1 {x} {.x} | yes refl = refl +eqlemma1 {x} {y} | no ¬p = refl + +add-lemma1 : { x : ℕ } → x + 1 ≡ suc x +add-lemma1 {zero} = refl +add-lemma1 {suc x} = cong ( \ z -> suc z ) ( add-lemma1 {x} ) + +--------------------------- + program : Comm program = Seq ( PComm (λ env → record env {varn = 10})) @@ -72,6 +139,9 @@ test1 : Env test1 = interpret ( record { vari = 0 ; varn = 0 } ) program +eval-proof : vari test1 ≡ 10 +eval-proof = refl + tests : Env tests = interpret ( record { vari = 0 ; varn = 0 } ) simple @@ -79,10 +149,6 @@ 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 @@ -142,11 +208,6 @@ 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 ) @@ -157,6 +218,9 @@ lemma env | false = refl lemma env | true = refl +open import Data.Empty + +open import Data.Nat.Properties proof1 : HTProof initCond program termCond proof1 = @@ -171,17 +235,61 @@ lemma1 env with stmt1Cond env lemma1 env | false = refl lemma1 env | true = refl + lemma21 : {env : Env } → stmt2Cond env ≡ true → varn env ≡ 10 + lemma21 eq = eqlemma (and-lemma-1 eq) + lemma22 : {env : Env } → stmt2Cond env ≡ true → vari env ≡ 0 + lemma22 eq = eqlemma (and-lemma-2 eq) + lemma23 : {env : Env } → stmt2Cond env ≡ true → varn env + vari env ≡ 10 + lemma23 {env} 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 + ∎ 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 = {!!} + lemma2 env = bool-case (stmt2Cond env) ( + λ eq → let open ≡-Reasoning in + begin + implies (stmt2Cond env) (whileInv env) + ≡⟨⟩ + implies (stmt2Cond env) ( Equal (varn env + vari env) 10 ) + ≡⟨ cong ( \ x -> implies (stmt2Cond env) ( Equal x 10 ) ) ( lemma23 {env} eq ) ⟩ + implies (stmt2Cond env) (Equal 10 10) + ≡⟨⟩ + implies (stmt2Cond env) true + ≡⟨ impl-1 ⟩ + true + ∎ + ) ( + λ ne → let open ≡-Reasoning in + begin + implies (stmt2Cond env) (whileInv env) + ≡⟨ cong ( \ x -> implies x (whileInv env) ) ne ⟩ + implies false (whileInv env) + ≡⟨ impl-2 {whileInv env} ⟩ + true + ∎ + ) lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ 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 ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond - lemma5 = {!!} + lemma3 env = impl ( λ cond → let open ≡-Reasoning in + begin + whileInv' (record { varn = varn env ; vari = vari env + 1 }) + ≡⟨⟩ + 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 ) add-lemma1 ⟩ + Equal (suc (varn env + vari env)) 11 + ≡⟨ sym eqlemma1 ⟩ + Equal ((varn env + vari env) ) 10 + ≡⟨ and-lemma-1 cond ⟩ + true + ∎ ) + lemma4 : Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv + lemma4 env = {!!} + lemma5 : Tautology ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond + lemma5 env = {!!}