|
4
|
1 module whileTestGears where
|
|
|
2
|
|
|
3 open import Function
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.Bool hiding ( _≟_ ; _∧_)
|
|
|
6 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
7 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9
|
|
|
10
|
|
6
|
11 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
|
|
4
|
12 field
|
|
6
|
13 pi1 : a
|
|
|
14 pi2 : b
|
|
|
15
|
|
|
16 open _∧_
|
|
4
|
17
|
|
|
18 _-_ : ℕ -> ℕ -> ℕ
|
|
|
19 x - zero = x
|
|
|
20 zero - _ = zero
|
|
|
21 (suc x) - (suc y) = x - y
|
|
|
22
|
|
6
|
23 sym1 : { y : ℕ } -> y + zero ≡ y
|
|
|
24 sym1 {zero} = refl
|
|
|
25 sym1 {suc y} = cong ( λ x → suc x ) ( sym1 {y} )
|
|
|
26
|
|
|
27 +-sym : { x y : ℕ } -> x + y ≡ y + x
|
|
|
28 +-sym {zero} {zero} = refl
|
|
|
29 +-sym {zero} {suc y} = let open ≡-Reasoning in
|
|
|
30 begin
|
|
|
31 zero + suc y
|
|
|
32 ≡⟨⟩
|
|
|
33 suc y
|
|
|
34 ≡⟨ sym sym1 ⟩
|
|
|
35 suc y + zero
|
|
|
36 ∎
|
|
|
37 +-sym {suc x} {zero} = let open ≡-Reasoning in
|
|
|
38 begin
|
|
|
39 suc x + zero
|
|
|
40 ≡⟨ sym1 ⟩
|
|
|
41 suc x
|
|
|
42 ≡⟨⟩
|
|
|
43 zero + suc x
|
|
|
44 ∎
|
|
|
45 +-sym {suc x} {suc y} = cong ( λ z → suc z ) ( let open ≡-Reasoning in
|
|
|
46 begin
|
|
|
47 x + suc y
|
|
|
48 ≡⟨ +-sym {x} {suc y} ⟩
|
|
|
49 suc (y + x)
|
|
|
50 ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩
|
|
|
51 suc (x + y)
|
|
|
52 ≡⟨ sym ( +-sym {y} {suc x}) ⟩
|
|
|
53 y + suc x
|
|
|
54 ∎ )
|
|
|
55
|
|
|
56 minus-plus : { x y : ℕ } -> (suc x - 1) + (y + 1) ≡ suc x + y
|
|
|
57 minus-plus {zero} {y} = +-sym {y} {1}
|
|
|
58 minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y})
|
|
4
|
59
|
|
|
60 lt : ℕ -> ℕ -> Bool
|
|
|
61 lt x y with (suc x ) ≤? y
|
|
|
62 lt x y | yes p = true
|
|
|
63 lt x y | no ¬p = false
|
|
|
64
|
|
|
65 Equal : ℕ -> ℕ -> Bool
|
|
|
66 Equal x y with x ≟ y
|
|
|
67 Equal x y | yes p = true
|
|
|
68 Equal x y | no ¬p = false
|
|
|
69
|
|
6
|
70 record Env : Set where
|
|
|
71 field
|
|
|
72 varn : ℕ
|
|
|
73 vari : ℕ
|
|
|
74 open Env
|
|
|
75
|
|
4
|
76 whileTest : {l : Level} {t : Set l} -> (Code : Env -> t) -> t
|
|
|
77 whileTest next = next (record {varn = 10 ; vari = 0} )
|
|
|
78
|
|
|
79 {-# TERMINATING #-}
|
|
|
80 whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t
|
|
|
81 whileLoop env next with lt 0 (varn env)
|
|
|
82 whileLoop env next | false = next env
|
|
|
83 whileLoop env next | true =
|
|
|
84 whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
|
85
|
|
|
86 test1 : Env
|
|
|
87 test1 = whileTest (λ env → whileLoop env (λ env1 → env1 ))
|
|
|
88
|
|
|
89
|
|
|
90 proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
|
|
|
91 proof1 = refl
|
|
|
92
|
|
|
93
|
|
|
94
|
|
|
95 -- stmt2Cond : {l : Level} → EnvWithCond {l} →
|
|
|
96 -- stmt2Cond env = (Equal (varn' env) 10) ∧ (Equal (vari' env) 0)
|
|
|
97
|
|
5
|
98 whileTest' : {l : Level} {t : Set l} -> (Code : (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) -> t) -> t
|
|
4
|
99 whileTest' next = next env proof2
|
|
|
100 where
|
|
|
101 env : Env
|
|
|
102 env = record {vari = 0 ; varn = 10}
|
|
|
103 proof2 : ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
|
|
|
104 proof2 = record {pi1 = refl ; pi2 = refl}
|
|
|
105
|
|
|
106 {-# TERMINATING #-}
|
|
5
|
107 whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> ((varn env) + (vari env) ≡ 10) -> (Code : Env -> t) -> t
|
|
4
|
108 whileLoop' env proof next with lt 0 (varn env)
|
|
|
109 whileLoop' env proof next | false = next env
|
|
|
110 whileLoop' env proof next | true = whileLoop' env1 proof3 next
|
|
|
111 where
|
|
|
112 env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1}
|
|
5
|
113 proof3 : varn env1 + vari env1 ≡ 10
|
|
6
|
114 proof3 = let open ≡-Reasoning in
|
|
|
115 begin
|
|
|
116 varn env1 + vari env1
|
|
|
117 ≡⟨⟩
|
|
|
118 (varn env - 1) + (vari env + 1)
|
|
|
119 ≡⟨ {!!} ⟩
|
|
|
120 10
|
|
|
121 ∎
|
|
|
122
|
|
4
|
123
|
|
5
|
124 conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
|
|
|
125 -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ 10) -> t) -> t
|
|
6
|
126 conversion1 env p1 next = next env proof4
|
|
|
127 where
|
|
|
128 proof4 : varn env + vari env ≡ 10
|
|
|
129 proof4 = let open ≡-Reasoning in
|
|
|
130 begin
|
|
|
131 varn env + vari env
|
|
|
132 ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
|
|
|
133 10 + vari env
|
|
|
134 ≡⟨ cong ( λ n → 10 + n ) (pi1 p1 ) ⟩
|
|
|
135 10 + 0
|
|
|
136 ≡⟨⟩
|
|
|
137 10
|
|
|
138 ∎
|
|
4
|
139
|
|
6
|
140
|
|
|
141 proofGears : Set
|
|
|
142 proofGears = whileTest' (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ 10 ))))
|
