Mercurial > hg > Members > ryokka > HoareLogic

annotate whileTestPrim.agda @ 7:e7d6bdb6039d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix test1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Dec 2018 22:35:38 +0900
parents 64bd5c236002
children e4f087b823d4
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
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 record Env : Set where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 field
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 varn : ℕ
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 vari : ℕ
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 PrimComm : Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 PrimComm = Env → Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 Cond : Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 Cond = (Env → Bool)
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 data Comm : Set where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 Skip : Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 Abort : Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 PComm : PrimComm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 Seq : Comm -> Comm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 If : Cond -> Comm -> Comm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 While : Cond -> Comm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 _-_ : ℕ -> ℕ -> ℕ
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 x - zero = x
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 zero - _ = zero
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 (suc x) - (suc y) = x - y
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 lt : ℕ -> ℕ -> Bool
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
37 lt x y with suc x ≤? y
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 lt x y | yes p = true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 lt x y | no ¬p = false
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 Equal : ℕ -> ℕ -> Bool
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 Equal x y with x ≟ y
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 Equal x y | yes p = true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 Equal x y | no ¬p = false
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 program : Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 program =
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 Seq ( PComm (λ env → record env {varn = 10}))
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 $ Seq ( PComm (λ env → record env {vari = 0}))
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
50 $ While (λ env → lt zero (varn env ) )
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 (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
52 $ 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
53
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 simple : Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 simple =
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 Seq ( PComm (λ env → record env {varn = 10}))
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 $ PComm (λ env → record env {vari = 0})
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 {-# TERMINATING #-}
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 interpret : Env → Comm → Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 interpret env Skip = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 interpret env Abort = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 interpret env (PComm x) = x env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 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
65 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
66 ... | true = interpret env then
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 ... | false = interpret env else
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 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
69 ... | 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
70 ... | false = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 test1 : Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 test1 = interpret ( record { vari = 0 ; varn = 0 } ) program
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
75 tests : Env
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
76 tests = interpret ( record { vari = 0 ; varn = 0 } ) simple
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
77
3
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 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
80 empty-case _ = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 implies : Bool → Bool → Bool
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 implies false _ = true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 implies true true = true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 implies true false = false
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 Axiom : Cond -> PrimComm -> Cond -> Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 Axiom pre comm post = ∀ (env : Env) → implies (pre env) ( post (comm env)) ≡ true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 Tautology : Cond -> Cond -> Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 Tautology pre post = ∀ (env : Env) → implies (pre env) (post env) ≡ true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 _/\_ : Cond -> Cond -> Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 x /\ y = λ env → x env ∧ y env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 neg : Cond -> Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 neg x = λ env → not ( x env )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 data HTProof : Cond -> Comm -> Cond -> Set where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 (pr : Axiom bPre pcm bPost) ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 HTProof bPre (PComm pcm) bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 SkipRule : (b : Cond) -> HTProof b Skip b
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 HTProof bPre Abort bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 {bPost' : Cond} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 Tautology bPre bPre' ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 HTProof bPre' cm bPost' ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 Tautology bPost' bPost ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 HTProof bPre cm bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 {cm2 : Comm} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 HTProof bPre cm1 bMid ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 HTProof bMid cm2 bPost ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 HTProof bPre (Seq cm1 cm2) bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 {bPre : Cond} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 {b : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 HTProof (bPre /\ b) cmThen bPost ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 HTProof (bPre /\ neg b) cmElse bPost ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 HTProof bPre (If b cmThen cmElse) bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 HTProof (bInv /\ b) cm bInv ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 HTProof bInv (While b cm) (bInv /\ neg b)
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 initCond : Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 initCond env = true
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 stmt1Cond : Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 stmt1Cond env = Equal (varn env) 10
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 stmt2Cond : Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0)
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 whileInv : Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 whileInv env = Equal ((varn env) + (vari env)) 10
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 whileInv' : Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 whileInv' env = Equal ((varn env) + (vari env)) 11
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 termCond : Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 termCond env = Equal (vari env) 10
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 eqlemma : { x y : ℕ } → Equal x y ≡ true → x ≡ y
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 eqlemma {x} {y} eq with x ≟ y
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 eqlemma {x} {y} refl | yes refl = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 eqlemma {x} {y} () | no ¬p
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 proofs : HTProof initCond simple stmt2Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 proofs =
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 SeqRule {initCond} ( PrimRule empty-case )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 $ PrimRule {stmt1Cond} {_} {stmt2Cond} lemma
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 lemma : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 lemma env with stmt1Cond env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 lemma env | false = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 lemma env | true = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 proof1 : HTProof initCond program termCond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 proof1 =
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 SeqRule {λ e → true} ( PrimRule empty-case )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 (
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
167 $ 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
168 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 lemma1 env with stmt1Cond env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 lemma1 env | false = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 lemma1 env | true = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 lemma2 : Tautology stmt2Cond whileInv
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 lemma2 env with stmt2Cond env | Equal (varn env + vari env) 10
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 lemma2 env | false | false = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 lemma2 env | false | true = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 lemma2 env | true | true = refl
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 lemma2 env | true | false = {!!}
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
180 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181 lemma3 = {!!}
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
182 lemma4 : Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 lemma4 = {!!}
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
184 lemma5 : Tautology ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 lemma5 = {!!}
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187