Mercurial > hg > Members > ryokka > HoareLogic
annotate whileTestGears.agda @ 97:1b2d58c5d75b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 08 Apr 2023 07:52:36 +0900 |
| parents | e152d7afbb58 |
| children |
| rev | line source |
|---|---|
| 93 | 1 module whileTestGears where |
| 4 | 2 |
| 3 open import Function | |
| 89 | 4 open import Data.Nat renaming ( _∸_ to _-_) |
| 88 | 5 open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_ ) |
| 4 | 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 | 10 open import utilities |
| 11 open _/\_ | |
| 4 | 12 |
| 6 | 13 record Env : Set where |
| 14 field | |
| 15 varn : ℕ | |
| 16 vari : ℕ | |
| 17 open Env | |
| 18 | |
| 87 | 19 whileTestS : { m : Level} → (c10 : ℕ) → (Code : Env → Set m) → Set m |
| 85 | 20 whileTestS c10 next = next (record {varn = c10 ; vari = 0} ) |
| 21 | |
| 22 whileTestS1 : (c10 : ℕ) → whileTestS c10 (λ e → ((varn e ≡ c10) /\ (vari e ≡ 0 )) ) | |
| 23 whileTestS1 c10 = record { pi1 = refl ; pi2 = refl } | |
| 24 | |
| 25 | |
| 87 | 26 whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t |
| 14 | 27 whileTest c10 next = next (record {varn = c10 ; vari = 0} ) |
| 4 | 28 |
| 29 {-# TERMINATING #-} | |
| 87 | 30 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t |
| 4 | 31 whileLoop env next with lt 0 (varn env) |
| 32 whileLoop env next | false = next env | |
| 33 whileLoop env next | true = | |
| 34 whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next | |
| 35 | |
| 36 test1 : Env | |
| 14 | 37 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) |
| 4 | 38 |
| 39 | |
| 14 | 40 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) |
| 4 | 41 proof1 = refl |
| 42 | |
| 16 | 43 -- ↓PostCondition |
| 87 | 44 whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t |
| 14 | 45 whileTest' {_} {_} {c10} next = next env proof2 |
| 4 | 46 where |
| 47 env : Env | |
| 14 | 48 env = record {vari = 0 ; varn = c10} |
| 16 | 49 proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition |
| 4 | 50 proof2 = record {pi1 = refl ; pi2 = refl} |
| 11 | 51 |
| 52 open import Data.Empty | |
| 53 open import Data.Nat.Properties | |
| 54 | |
| 87 | 55 lemma1 : {i : ℕ} → ¬ 1 ≤ i → i ≡ 0 |
| 56 lemma1 {zero} not = refl | |
| 57 lemma1 {suc i} not = ⊥-elim ( not (s≤s z≤n) ) | |
| 11 | 58 |
| 16 | 59 -- Condition to Invaliant |
| 87 | 60 conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) |
| 61 → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t | |
| 62 conversion1 env {c10} p1 next = next env proof4 where | |
| 14 | 63 proof4 : varn env + vari env ≡ c10 |
| 87 | 64 proof4 = let open ≡-Reasoning in begin |
| 65 varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ | |
| 66 c10 + vari env ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ | |
| 67 c10 + 0 ≡⟨ +-sym {c10} {0} ⟩ | |
| 14 | 68 c10 |
| 6 | 69 ∎ |
| 4 | 70 |
| 87 | 71 open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) |
| 9 | 72 |
| 86 | 73 whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ |
| 74 whileTestSpec1 _ _ x = tt | |
| 17 | 75 |
| 87 | 76 whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) |
| 96 | 77 → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) -- next with PostCondition |
| 87 | 78 → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t |
| 79 whileLoopSeg env proof next exit with ( suc zero ≤? (varn env) ) | |
| 80 whileLoopSeg {_} {_} {c10} env proof next exit | no p = exit env ( begin | |
| 81 vari env ≡⟨ refl ⟩ | |
| 82 0 + vari env ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩ | |
| 83 varn env + vari env ≡⟨ proof ⟩ | |
| 84 c10 ∎ ) where open ≡-Reasoning | |
| 89 | 85 whileLoopSeg {_} {_} {c10} env proof next exit | yes p = next env1 (proof3 p ) (proof4 (varn env) p) where |
| 87 | 86 env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} |
| 87 1<0 : 1 ≤ zero → ⊥ | |
| 88 1<0 () | |
| 89 | 89 proof4 : (i : ℕ) → 1 ≤ i → i - 1 < i |
| 90 proof4 zero () | |
| 91 proof4 (suc i) lt = begin | |
| 92 suc (suc i - 1 ) ≤⟨ ≤-refl ⟩ | |
| 93 suc i ∎ where open ≤-Reasoning | |
| 87 | 94 proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10 |
| 95 proof3 (s≤s lt) with varn env | |
| 96 proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) | |
| 97 proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in begin | |
| 98 n' + (vari env + 1) ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ | |
| 99 n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ | |
| 100 (n' + 1) + vari env ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ | |
| 101 (suc n' ) + vari env ≡⟨⟩ | |
| 102 varn env + vari env ≡⟨ proof ⟩ | |
| 103 c10 | |
| 104 ∎ | |
| 17 | 105 |
| 88 | 106 open import Relation.Binary.Definitions |
| 107 | |
| 108 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ | |
| 109 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x | |
| 89 | 110 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ |
| 111 lemma3 refl () | |
| 90 | 112 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ |
| 113 lemma5 (s≤s z≤n) () | |
| 88 | 114 |
| 94 | 115 TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ) |
| 116 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) | |
| 117 → (r : Index) → (p : Invraiant r) → t | |
| 118 TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) | |
| 119 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) | |
| 120 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where | |
|
92
9c91d23c2836
Abstract Termination done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
121 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t |
| 94 | 122 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) |
|
92
9c91d23c2836
Abstract Termination done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
123 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) |
|
9c91d23c2836
Abstract Termination done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
124 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt |
| 95 | 125 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) |
| 91 | 126 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) |
| 88 | 127 |
|
92
9c91d23c2836
Abstract Termination done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
128 proofGearsTermS : {c10 : ℕ } → ⊤ |
|
9c91d23c2836
Abstract Termination done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
129 proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → |
| 94 | 130 TerminatingLoopS Env (λ env → varn env) |
| 131 (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) | |
| 91 | 132 |
| 133 | |
| 134 | |
| 135 | |
| 136 | |
| 137 | |
|
92
9c91d23c2836
Abstract Termination done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
138 |
|
9c91d23c2836
Abstract Termination done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
91
diff
changeset
|
139 |