# HG changeset patch
# User ryokka
# Date 1575883971 -32400
# Node ID cc6db47d6882251f25009263be7a8de0ae35b03d
# Parent  23cce74379180aea764be54d87da81844c68941d
add whileTestCondition

diff -r 23cce7437918 -r cc6db47d6882 utilities.agda
--- a/utilities.agda	Sun Dec 16 19:31:36 2018 +0900
+++ b/utilities.agda	Mon Dec 09 18:32:51 2019 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module utilities where
 
 open import Function
@@ -63,7 +65,7 @@
 +1≡suc {suc x} = cong ( λ z → suc z ) ( +1≡suc {x} )
 
 lt : ℕ → ℕ → Bool
-lt x y with (suc x ) ≤? y
+lt x y with (suc x ) Data.Nat.≤? y
 lt x y | yes p = true
 lt x y | no ¬p = false
 
@@ -149,8 +151,8 @@
 
 Equal+1 : { x y : ℕ } →  Equal x y ≡ Equal (suc x) (suc y)
 Equal+1 {x} {y} with  x ≟ y
-Equal+1 {x} {.x} | yes refl = refl
-Equal+1 {x} {y} | no ¬p = refl
+Equal+1 {x} {.x} | yes refl = {!!}
+Equal+1 {x} {y} | no ¬p = {!!}
 
 open import Data.Empty 
 
diff -r 23cce7437918 -r cc6db47d6882 whileTestGears.agda
--- a/whileTestGears.agda	Sun Dec 16 19:31:36 2018 +0900
+++ b/whileTestGears.agda	Mon Dec 09 18:32:51 2019 +0900
@@ -8,6 +8,7 @@
 open import Relation.Binary.PropositionalEquality
 
 open import utilities
+
 open  _/\_
 
 record Env  : Set where
@@ -29,7 +30,6 @@
 test1 : Env
 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
 
-
 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 = refl
 
@@ -48,14 +48,14 @@
 
 {-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
 whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) -> (Code : Env -> t) -> t
-whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
+whileLoop' env proof next with  ( suc zero  Data.Nat.≤? (varn  env) )
 whileLoop' env proof next | no p = next env 
 whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
     where
       env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
-      1<0 : 1 ≤ zero → ⊥
+      1<0 : 1 Data.Nat.≤ zero → ⊥
       1<0 ()
-      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
+      proof3 : (suc zero  Data.Nat.≤ (varn  env))  → varn env1 + vari env1 ≡ c10
       proof3 (s≤s lt) with varn  env
       proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
       proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
@@ -96,3 +96,30 @@
 
 proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 proofGearsMeta {c10} = {!!}
+
+data whileTestState : Set where
+  
+  state1 : whileTestState
+  state2 : whileTestState
+
+
+record whileTestCondition  (c10 : ℕ)  (t : whileTestState)  : Set where
+  inductive
+  field
+    case1 : (env : Env)  → (t ≡ state1) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestCondition c10 state2
+    case2 : (env : Env) → (t ≡ state2)  → (varn env + vari env ≡ c10) → whileTestCondition c10 state2
+
+open whileTestCondition
+
+test2 : (c10 : ℕ) → whileTestCondition c10 state1 → whileTestCondition c10 state2 
+test2 c10 cond1 = whileTest 10 (λ env  → whileLoop env (λ env1 → proof3 env1 cond1 ))
+  where    
+    whileLoopCond : (e env1 : Env) → varn env1 + vari env1 ≡ c10 → varn e + vari e ≡ c10 → whileTestCondition c10 state2
+    whileLoopCond = {!!}
+    proof2 : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
+    proof2 env = record {pi1 = {!!} ; pi2 = {!!}}
+    proof3 : (env : Env) → whileTestCondition c10 state1 → whileTestCondition c10 state2
+    proof3 env cond1 = record {
+                          case1 = λ e ()
+                          ; case2 = λ e refl → conversion1 e {c10} (record { pi1 = {!!} ; pi2 = {!!} }) {!!}
+                          }
diff -r 23cce7437918 -r cc6db47d6882 whileTestPrim.agda
--- a/whileTestPrim.agda	Sun Dec 16 19:31:36 2018 +0900
+++ b/whileTestPrim.agda	Mon Dec 09 18:32:51 2019 +0900
@@ -145,6 +145,8 @@
     true
   ∎ )
 
+
+
 proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10})
 proofs c10 =
       SeqRule {initCond} ( PrimRule (init-case {c10} ))