Mercurial > hg > Members > ryokka > HoareLogic

annotate whileTestPrim.agda @ 22:e88ad1d70faf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate Hoare with whileTestPrim
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Dec 2018 08:24:54 +0900
parents 5e4abc1919b4
children 3968822b9693
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module whileTestPrim where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Function
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Bool hiding ( _≟_ )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Level renaming ( suc to succ ; zero to Zero )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Relation.Nullary using (¬_; Dec; yes; no)
4
64bd5c236002 add whileTestGears
ryokka
parents: 3
diff changeset
8 open import Relation.Binary.PropositionalEquality
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
21
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
10 open import utilities hiding ( _/\_ )
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 record Env : Set where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 field
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 varn : ℕ
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 vari : ℕ
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 PrimComm : Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 PrimComm = Env → Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 Cond : Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 Cond = (Env → Bool)
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
22
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
24 Axiom : Cond -> PrimComm -> Cond -> Set
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
25 Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
26
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
27 Tautology : Cond -> Cond -> Set
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
28 Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
29
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
30 _and_ : Cond -> Cond -> Cond
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
31 x and y = λ env → x env ∧ y env
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
32
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
33 neg : Cond -> Cond
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
34 neg x = λ env → not ( x env )
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
35
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
36 open import HoareData PrimComm Cond Axiom Tautology _and_ neg
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
38 ---------------------------
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
39
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
40 program : ℕ → Comm
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
41 program c10 =
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
42 Seq ( PComm (λ env → record env {varn = c10}))
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 $ Seq ( PComm (λ env → record env {vari = 0}))
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
44 $ While (λ env → lt zero (varn env ) )
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
48 simple : ℕ → Comm
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
49 simple c10 =
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
50 Seq ( PComm (λ env → record env {varn = c10}))
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 $ PComm (λ env → record env {vari = 0})
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 {-# TERMINATING #-}
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 interpret : Env → Comm → Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 interpret env Skip = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 interpret env Abort = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 interpret env (PComm x) = x env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 interpret env (If x then else) with x env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 ... | true = interpret env then
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ... | false = interpret env else
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 interpret env (While x comm) with x env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ... | true = interpret (interpret env comm) (While x comm)
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 ... | false = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 test1 : Env
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
67 test1 = interpret ( record { vari = 0 ; varn = 0 } ) (program 10)
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
69 eval-proof : vari test1 ≡ 10
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
70 eval-proof = refl
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
71
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
72 tests : Env
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
73 tests = interpret ( record { vari = 0 ; varn = 0 } ) (simple 10)
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
74
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 empty-case _ = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 initCond : Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 initCond env = true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
84 stmt1Cond : {c10 : ℕ} → Cond
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
85 stmt1Cond {c10} env = Equal (varn env) c10
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
15
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
87 init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
88 init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
89
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
90 init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Cond {c10})
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
91 init-type {c10} env = init-case env
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
92
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
93 stmt2Cond : {c10 : ℕ} → Cond
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
94 stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
96 whileInv : {c10 : ℕ} → Cond
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
97 whileInv {c10} env = Equal ((varn env) + (vari env)) c10
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
99 whileInv' : {c10 : ℕ} → Cond
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
100 whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
102 termCond : {c10 : ℕ} → Cond
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
103 termCond {c10} env = Equal (vari env) c10
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104
15
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
105 lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
106 lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
107 begin
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
108 (Equal (varn env) c10 ) ∧ true
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
109 ≡⟨ ∧true ⟩
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
110 Equal (varn env) c10
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
111 ≡⟨ cond ⟩
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
112 true
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
113 ∎ )
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
114
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
115 proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10})
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
116 proofs c10 =
15
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
117 SeqRule {initCond} ( PrimRule (init-case {c10} ))
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
118 $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10})
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
120 open import Data.Empty
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
121
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
122 open import Data.Nat.Properties
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
124 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
125 proof1 c10 =
15
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
126 SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
127 $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 )
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
128 $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 (
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
129 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
130 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 )
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
131 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 where
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
133 lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
134 lemma21 eq = Equal→≡ (∧-pi1 eq)
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
135 lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
136 lemma22 eq = Equal→≡ (∧-pi2 eq)
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
137 lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
138 lemma23 {env} {c10} eq = let open ≡-Reasoning in
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
139 begin
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
140 varn env + vari env
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
141 ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
142 c10 + vari env
15
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
143 ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
144 c10 + 0
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
145 ≡⟨ +-sym {c10} {0} ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
146 0 + c10
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
147 ≡⟨⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
148 c10
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
149 ∎
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
150 lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
151 lemma2 {c10} env = bool-case (stmt2Cond env) (
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
152 λ eq → let open ≡-Reasoning in
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
153 begin
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
154 (stmt2Cond env) ⇒ (whileInv env)
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
155 ≡⟨⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
156 (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 )
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
157 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
158 (stmt2Cond env) ⇒ (Equal c10 c10)
15
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
159 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
160 (stmt2Cond {c10} env) ⇒ true
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
161 ≡⟨ ⇒t ⟩
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
162 true
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
163 ∎
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
164 ) (
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
165 λ ne → let open ≡-Reasoning in
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
166 begin
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
167 (stmt2Cond env) ⇒ (whileInv env)
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
168 ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
169 false ⇒ (whileInv {c10} env)
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
170 ≡⟨ f⇒ {whileInv {c10} env} ⟩
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
171 true
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
172 ∎
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
173 )
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
174 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
175 lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
176 begin
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
177 whileInv' (record { varn = varn env ; vari = vari env + 1 })
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
178 ≡⟨⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
179 Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
180 ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
181 Equal (varn env + (vari env + 1)) (suc c10) ∧ true
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
182 ≡⟨ ∧true ⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
183 Equal (varn env + (vari env + 1)) (suc c10)
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
184 ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
185 Equal ((varn env + vari env) + 1) (suc c10)
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
186 ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
187 Equal (suc (varn env + vari env)) (suc c10)
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
188 ≡⟨ sym Equal+1 ⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
189 Equal ((varn env + vari env) ) c10
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
190 ≡⟨ ∧-pi1 cond ⟩
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
191 true
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
192 ∎ )
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
193 lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
194 lemma41 env {c10} c1 c2 = let open ≡-Reasoning in
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
195 begin
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
196 Equal ((varn env - 1) + vari env) c10
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
197 ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
198 Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
199 ≡⟨⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
200 Equal ((predℕ {varn env} c2 ) + vari env) c10
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
201 ≡⟨ Equal+1 ⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
202 Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
203 ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
204 Equal (varn env + vari env) (suc c10)
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
205 ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
206 Equal (suc c10) (suc c10)
15
8d546766a9a8 Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
207 ≡⟨ ≡→Equal refl ⟩
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
208 true
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
209 ∎
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
210 lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
211 lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
212 begin
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
213 whileInv (record { varn = varn env - 1 ; vari = vari env })
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
214 ≡⟨⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
215 Equal ((varn env - 1) + vari env) c10
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
216 ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
217 true
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
218 ∎
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
219 )
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
220 lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
17
b95a3cf9727c add Gears1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
221 lemma51 z cond with varn z
b95a3cf9727c add Gears1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
222 lemma51 z refl | zero = refl
b95a3cf9727c add Gears1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
223 lemma51 z () | suc x
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
224 lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
225 lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
226 begin
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
227 termCond env
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
228 ≡⟨⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
229 Equal (vari env) c10
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
230 ≡⟨⟩
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
231 Equal (zero + vari env) c10
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
232 ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
233 Equal (varn env + vari env) c10
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
234 ≡⟨ ∧-pi1 cond ⟩
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
235 true
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
236 ∎
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
237 )
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
238
21
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
239 --- necessary definitions for Hoare.agda ( Soundness )
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
240
21
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
241 State : Set
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
242 State = Env
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
243
21
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
244 open import RelOp
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
245 module RelOpState = RelOp State
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
246
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
247 open import Data.Product
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
248 open import Relation.Binary
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
249
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
250 NotP : {S : Set} -> Pred S -> Pred S
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
251 NotP X s = ¬ X s
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
252
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
253 _/\_ : Cond -> Cond -> Cond
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
254 b1 /\ b2 = b1 and b2
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
255
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
256 _\/_ : Cond -> Cond -> Cond
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
257 b1 \/ b2 = neg (neg b1 /\ neg b2)
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
258
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
259 _==>_ : Cond -> Cond -> Cond
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
260 b1 ==> b2 = neg (b1 \/ b2)
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
261
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
262 SemCond : Cond -> State -> Set
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
263 SemCond c p = c p ≡ true
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
264
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
265 tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
266 (s : State) -> SemCond b1 s -> SemCond b2 s
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
267 tautValid b1 b2 taut s cond with b1 s | b2 s | taut s
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
268 tautValid b1 b2 taut s () | false | false | refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
269 tautValid b1 b2 taut s _ | false | true | refl = refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
270 tautValid b1 b2 taut s _ | true | false | ()
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
271 tautValid b1 b2 taut s _ | true | true | refl = refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
272
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
273 respNeg : (b : Cond) -> (s : State) ->
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
274 Iff (SemCond (neg b) s) (¬ SemCond b s)
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
275 respNeg b s = ( left , right ) where
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
276 left : not (b s) ≡ true → (b s) ≡ true → ⊥
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
277 left ne with b s
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
278 left refl | false = λ ()
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
279 left () | true
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
280 right : ((b s) ≡ true → ⊥) → not (b s) ≡ true
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
281 right ne with b s
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
282 right ne | false = refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
283 right ne | true = ⊥-elim ( ne refl )
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
284
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
285 respAnd : (b1 b2 : Cond) -> (s : State) ->
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
286 Iff (SemCond (b1 /\ b2) s)
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
287 ((SemCond b1 s) × (SemCond b2 s))
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
288 respAnd b1 b2 s = ( left , right ) where
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
289 left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true) × (b2 s ≡ true)
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
290 left and with b1 s | b2 s
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
291 left () | false | false
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
292 left () | false | true
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
293 left () | true | false
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
294 left refl | true | true = ( refl , refl )
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
295 right : (b1 s ≡ true) × (b2 s ≡ true) → b1 s ∧ b2 s ≡ true
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
296 right ( x1 , x2 ) with b1 s | b2 s
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
297 right (() , ()) | false | false
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
298 right (() , _) | false | true
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
299 right (_ , ()) | true | false
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
300 right (refl , refl) | true | true = refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
301
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
302 PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
303 PrimSemComm prim s1 s2 = Id State (prim s1) s2
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
304
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
305 axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
306 (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
307 SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
308 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
309 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
310 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
311 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
312 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
313
22
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
314 open import Hoare
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
315 Cond
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
316 PrimComm
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
317 neg
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
318 _and_
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
319 Tautology
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
320 State
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
321 SemCond
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
322 tautValid
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
323 respNeg
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
324 respAnd
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
325 PrimSemComm
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
326 Axiom
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
327 axiomValid
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
328
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
329 PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
330 HTProof bPre cm bPost -> Satisfies bPre cm bPost
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
331 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht