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 = {!!}