Mercurial > hg > Members > soto > while_test
view gearswhile.agda @ 0:f5705a66e9ea default tip
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 13 Oct 2020 18:01:42 +0900 |
parents | |
children |
line wrap: on
line source
module gearswhile where open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Nat open import Relation.Binary.PropositionalEquality open import Data.Nat.Properties open import Relation.Binary.Definitions open import Data.Empty open import utilities open _/\_ record Envc : Set (succ Zero) where field c10 : ℕ varn : ℕ vari : ℕ open Envc data whileTestState : Set where s1 : whileTestState s2 : whileTestState sf : whileTestState whileTestStateP : whileTestState → Envc → Set whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) whileTestStateP s2 env = (varn env + vari env ≡ c10 env) whileTestStateP sf env = (vari env ≡ c10 env) whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (next : (env : Envc ) → whileTestStateP s2 env → t) → (exit : (env : Envc ) → whileTestStateP sf env → t) → t whileLoopPwP env s next exit with <-cmp 0 (varn env) whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s) where lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env lem refl refl = refl whileLoopPwP env s next exit | tri< a ¬b ¬c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a) where 1<0 : 1 ≤ zero → ⊥ 1<0 () proof5 : (suc zero ≤ (varn env)) → (varn env - 1) + (vari env + 1) ≡ c10 env proof5 (s≤s lt) with varn env proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a) proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in begin n' + (vari env + 1) ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ (n' + 1) + vari env ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ (suc n' ) + vari env ≡⟨⟩ varn env + vari env ≡⟨ s ⟩ c10 env ∎