Mercurial > hg > Members > soto > experimental
comparison WhileTest.agda @ 13:724766af8b12
add impl
author | soto |
---|---|
date | Thu, 11 Feb 2021 19:33:35 +0900 |
parents | 77f0530f2eff |
children |
comparison
equal
deleted
inserted
replaced
12:77f0530f2eff | 13:724766af8b12 |
---|---|
7 open import Data.Maybe | 7 open import Data.Maybe |
8 open import Data.List | 8 open import Data.List |
9 open import Function | 9 open import Function |
10 open import logic | 10 open import logic |
11 | 11 |
12 --open import Data.Bool hiding ( _≟_ ) -- ; _≤?_ ; _≤_ ; _<_) | 12 open import Data.Bool hiding ( _∧_ ; _≟_ ) -- ; _∧_ ; _≤_ ; _<_) |
13 --open import Relation.Binary.PropositionalEquality | 13 open import Data.Product |
14 open import Agda.Builtin.Unit | 14 open import Agda.Builtin.Unit |
15 open import Relation.Nullary using (¬_; Dec; yes; no) | |
16 | |
17 open import Data.Empty | |
18 open import Data.Nat.Properties | |
19 | |
20 -- logicへ | |
21 +zero : { y : ℕ } → y + zero ≡ y | |
22 +zero {zero} = refl | |
23 +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) | |
24 | |
25 -- utilへ | |
26 _-_ : ℕ → ℕ → ℕ | |
27 x - zero = x | |
28 zero - _ = zero | |
29 (suc x) - (suc y) = x - y | |
15 | 30 |
16 record Env : Set (Suc Zero) where | 31 record Env : Set (Suc Zero) where |
17 field | 32 field |
33 c10 : ℕ | |
18 varn : ℕ | 34 varn : ℕ |
19 vari : ℕ | 35 vari : ℕ |
20 open Env | 36 open Env |
21 | 37 |
22 data _implies_ (A B : Set ) : Set (Suc Zero) where | 38 data _implies_ (A B : Set ) : Set (Suc Zero) where |
23 proof : ( A → B ) → A implies B | 39 proof : ( A → B ) → A implies B |
24 | 40 |
41 implies2p : {A B : Set } → A implies B → A → B | |
42 implies2p (proof x) = x | |
43 | |
25 data whileTestState : Set where | 44 data whileTestState : Set where |
26 s1 : whileTestState | 45 s1 : whileTestState |
27 s2 : whileTestState | 46 s2 : whileTestState |
28 sf : whileTestState | 47 sf : whileTestState |
29 | 48 |
30 whileTestStateP : whileTestState → Env → ℕ → Set | 49 whileTestStateP : whileTestState → Env → Set |
31 whileTestStateP s1 env c10 = (vari env ≡ 0) ∧ (varn env ≡ c10) | 50 whileTestStateP s1 env = (vari env ≡ 0) ∧ (varn env ≡ c10 env) |
32 whileTestStateP s2 env c10 = (varn env + vari env ≡ c10 ) | 51 whileTestStateP s2 env = (varn env + vari env ≡ c10 env) |
33 whileTestStateP sf env c10 = (vari env ≡ c10) | 52 whileTestStateP sf env = (vari env ≡ c10 env) |
34 | 53 |
35 record WhileTest {m : Level } {t : Set m } : Set (Suc m) where | 54 record WhileTest {m : Level } {t : Set m } : Set (Suc m) where |
36 field | 55 field |
37 env : Env | 56 env : Env |
38 whileInit : {m : Level } {t : Set m } → (c10 : ℕ) → (Env → t) → t | 57 whileInit : {m : Level } {t : Set m } → (c10 : ℕ) → (Env → t) → t |
39 whileInit c10 next = next (record {varn = c10 ; vari = 0 } ) | 58 whileInit c10 next = next (record {c10 = c10 ; varn = c10 ; vari = 0 } ) |
40 whileInit-impl : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env c10) ) | |
41 whileInit-impl c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } ) | |
42 whileLoop : Env → (Code : Env → t) → t | 59 whileLoop : Env → (Code : Env → t) → t |
43 whileLoop env next = whileLoop1 (varn env) env where | 60 whileLoop env next = whileLoop1 (varn env) env where |
44 whileLoop1 : ℕ → Env → t | 61 whileLoop1 : ℕ → Env → t |
45 whileLoop1 zero env = next env | 62 whileLoop1 zero env = next env |
46 whileLoop1 (suc t ) env = whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) | 63 whileLoop1 (suc t ) env = whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) |
47 whileTest : (c10 : ℕ) → (Env → t) → t | 64 whileTest : (c10 : ℕ) → (Env → t) → t |
48 whileTest c10 next = whileInit c10 $ λ env → whileLoop env next | 65 whileTest c10 next = whileInit c10 $ λ env → whileLoop env next |
49 | 66 |
67 loopPP : (n : ℕ) → (input : Env ) → (n ≡ varn input) → Env | |
68 loopPP zero input refl = input | |
69 loopPP (suc n) input refl = loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl | |
70 | |
71 -- init | |
72 whileInit-impl : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env) ) | |
73 whileInit-impl c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } ) | |
74 whileTestPSemSound : (c : ℕ ) (output : Env ) → output ≡ whileInit c (λ e → e) → ⊤ implies ((vari output ≡ 0) ∧ (varn output ≡ c)) | |
75 whileTestPSemSound c output refl = whileInit-impl c | |
76 -- init → loop | |
77 whileConvPSemSound : {l : Level} → (input : Env) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input) | |
78 whileConvPSemSound input = proof λ x → (conv input x) where | |
79 conv : (env : Env ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env ) → varn env + vari env ≡ c10 env | |
80 conv e record { proj1 = refl ; proj2 = refl } = +zero | |
81 -- loop → loop | |
82 whileLoopPSem : {l : Level} {t : Set l} → (input : Env ) → whileTestStateP s2 input | |
83 → (next : (output : Env ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) | |
84 → (exit : (output : Env ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t | |
85 whileLoopPSem env s next exit with varn env | s | |
86 ... | zero | _ = exit env (proof (λ z → z)) | |
87 ... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) ) | |
88 -- loop → fin | |
89 | |
90 loopPPSem : (input output : Env ) → output ≡ loopPP (varn input) input refl | |
91 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) | |
92 loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p | |
93 where | |
94 lem : (n : ℕ) → (env : Env) → n + suc (vari env) ≡ suc (n + vari env) | |
95 lem n env = +-suc (n) (vari env) | |
96 loopPPSemInduct : (n : ℕ) → (current : Env) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq) | |
97 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) | |
98 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) | |
99 loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = | |
100 whileLoopPSem current refl | |
101 (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) | |
102 (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) | |
103 | |
104 | |
105 whileLoopPSemSound : {l : Level} → (input output : Env ) | |
106 → whileTestStateP s2 input | |
107 → output ≡ loopPP (varn input) input refl | |
108 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) | |
109 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre | |
110 | |
111 whileTestSound : {l : Level} (c : ℕ) → (output : Env) → ⊤ → whileTestStateP sf output | |
112 whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top = | |
113 implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!}) (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileInit c (λ e → e)) refl) top)) | |
114 | |
50 open WhileTest | 115 open WhileTest |
51 | 116 |
52 createWhileTest : {m : Level} {t : Set m } → WhileTest {m} {t} | 117 createWhileTest : {m : Level} {t : Set m } → WhileTest {m} {t} |
53 createWhileTest = record { env = record { varn = 0; vari = 0 } } | 118 createWhileTest = record { env = record { c10 = 0; varn = 0; vari = 0 } } |
54 | 119 |
55 test2 : ℕ | 120 test2 : ℕ |
56 test2 = whileTest createWhileTest 10 $ λ e → vari e | 121 test2 = whileTest createWhileTest 10 $ λ e → vari e |
57 | 122 |
58 --- | 123 --- |