Mercurial > hg > Members > ryokka > HoareLogic
comparison whileTestGears.agda @ 59:5c2cdcee9971
restore bad proof
| author | ryokka |
|---|---|
| date | Sat, 21 Dec 2019 17:49:15 +0900 |
| parents | 7523d5cd670b |
| children | ad83c2d5e869 |
comparison
equal
deleted
inserted
replaced
| 58:7523d5cd670b | 59:5c2cdcee9971 |
|---|---|
| 181 whileTestPCallwP : (c : ℕ ) → Set | 181 whileTestPCallwP : (c : ℕ ) → Set |
| 182 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where | 182 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where |
| 183 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env | 183 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env |
| 184 conv e record { pi1 = refl ; pi2 = refl } = +zero | 184 conv e record { pi1 = refl ; pi2 = refl } = +zero |
| 185 | 185 |
| 186 | |
| 187 conv1 : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env | |
| 188 conv1 e record { pi1 = refl ; pi2 = refl } = +zero | |
| 189 | |
| 190 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!})) | |
| 191 | |
| 186 {-# TERMINATING #-} | 192 {-# TERMINATING #-} |
| 187 Proof : (c : ℕ ) → whileTestPCallwP c | 193 Proof : (c : ℕ ) → whileTestPCallwP c |
| 188 Proof c = Proof c | 194 Proof zero = whileTestPwP {_} {_} zero ( λ env s → loopPwP env (conv env s) ( λ env s → refl) ) |
| 195 where | |
| 196 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env | |
| 197 conv e record { pi1 = refl ; pi2 = refl } = +zero | |
| 198 Proof (suc c) = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → lem )) | |
| 199 where | |
| 200 lem : whileLoopPwP (record { c10 = suc c ; varn = c ; vari = 0 + 1 }) ({!!}) | |
| 201 (λ env s → loopPwP env s (λ env₁ s₁ → vari env₁ ≡ suc c)) (λ env s3 → {!!}) | |
| 202 lem = {!!} | |
| 203 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env | |
| 204 conv e record { pi1 = refl ; pi2 = refl } = +zero | |
| 205 | |
| 206 | |
| 207 {-- | |
| 208 -- whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env | |
| 209 -- → (next : (env : Envc ) → whileTestStateP s2 env → t) | |
| 210 -- → (exit : (env : Envc ) → whileTestStateP sf env → t) → t | |
| 211 | |
| 212 next : (whileTestGears.proof5 | |
| 213 (record { c10 = suc c ; varn = suc c ; vari = 0 }) | |
| 214 (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt) | |
| 215 (λ x → | |
| 216 Relation.Nullary.Reflects.invert (ofⁿ (λ ())) (≡⇒≡ᵇ 0 (suc c) x)) | |
| 217 (<⇒≯ (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt)) | |
| 218 (whileTestGears.conv (suc c) (whileTestP (suc c) (λ env₁ → env₁)) | |
| 219 (record { pi1 = refl ; pi2 = refl })) | |
| 220 (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c)) | |
| 221 (λ env₁ s₁ → vari env₁ ≡ suc c) | |
| 222 (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt)) | |
| 223 | |
| 224 exit : (whileTestGears.conv (suc c) (whileTestP (suc c) (λ env₁ → env₁)) | |
| 225 (record { pi1 = refl ; pi2 = refl })) | |
| 226 (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c)) | |
| 227 (λ env₁ s₁ → vari env₁ ≡ suc c) | |
| 228 (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt)) | |
| 229 (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c)) | |
| 230 (λ env₁ s₁ → vari env₁ ≡ suc c) | |
| 231 | |
| 232 | (<-cmp 0 c | |
| 233 | Relation.Nullary.Decidable.Core.map′ (≡ᵇ⇒≡ 0 c) (≡⇒≡ᵇ 0 c) | |
| 234 (Data.Bool.Properties.T? (0 ≡ᵇ c)) | |
| 235 | Data.Bool.Properties.T? (0 <ᵇ c)) | |
| 236 | |
| 237 --} |