# HG changeset patch
# User ryokka
# Date 1577883038 -32400
# Node ID 148feaa1e346e73708b1da2167b4031906318d19
# Parent  52d957db02229b2b0c71a7b8132858baf39b5dc1
write loopPPSemInduct

diff -r 52d957db0222 -r 148feaa1e346 whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 30 20:53:00 2019 +0900
+++ b/whileTestGears.agda	Wed Jan 01 21:50:38 2020 +0900
@@ -214,7 +214,7 @@
   → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
   → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)  → t) → t
 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s _ exit = exit env (proof (λ z → z))
-whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next _ =
+whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next exit =
   next (record env {c10 = c10 ; varn = varn ; vari = suc vari }) (proof λ x → +-suc varn vari)
 
 
@@ -228,6 +228,7 @@
 loopPP (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP input (λ x → loopPP n (record x { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl) λ x → x -- ?
 
 loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
+
 loopPP' zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
 loopPP' (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = loopPP' n (record { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl -- ?
 
@@ -239,18 +240,14 @@
     -- lem output eq with <-cmp 0 (Envc.varn input)
     -- lem output refl | tri< a ¬b ¬c rewrite s2p = {!!}
     -- lem output refl | tri≈ ¬a refl ¬c = s2p
+    lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
+    lem n env = +-suc (n) (vari env)
     loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  (loopeq : output ≡ loopPP' n current eq)
       → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
     loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) -- loopeq には output ≡ loopPP zero current (zero = varn current)
 
     -- n を減らして loop を回しつつ証明したい
-    loopPPSemInduct (suc n) current refl loopeq refl = whileLoopPSem' current refl (λ output x → loopPPSemInduct (suc n) current {!!} {!!} {!!}) {!!}  -- why we can't write loopPPSemInduct n (record { c10 = suc (n + vari current) ; varn = n ; vari = suc (vari current) }) hogefuga
-    -- loopPPSemInduct zero (record { c10 = vari current ; varn = zero ; vari = vari current }) {!!} {!!} refl) {!!}
-
-    loopPPSemInduct2 : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  (loopeq : output ≡ loopPP n  current eq)
-      → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
-    loopPPSemInduct2 .0 record { c10 = .vari₁ ; varn = zero ; vari = vari₁ } refl loopeq refl rewrite loopeq = proof (λ x → refl)
-    loopPPSemInduct2 .(suc varn₁) record { c10 = .(suc (varn₁ + vari₁)) ; varn = (suc varn₁) ; vari = vari₁ } refl loopeq refl rewrite loopeq = whileLoopPSem' (record { c10 = (suc (varn₁ + vari₁)) ; varn = (suc varn₁) ; vari = vari₁ }) refl (λ output x → {!!}) λ exit x → {!!}
+    loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = whileLoopPSem' current refl (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)  (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
 
 -- -- whileLoopPSem' current refl (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl)
 
@@ -280,34 +277,34 @@
 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
 
 
-data GComm : Set (succ Zero) where
-  Skip  : GComm
-  Abort : GComm
-  PComm : Set → GComm
-  -- Seq   : GComm → GComm → GComm
-  -- If   : whileTestState → GComm → GComm → GComm
-  while : whileTestState → GComm → GComm
+-- data GComm : Set (succ Zero) where
+--   Skip  : GComm
+--   Abort : GComm
+--   PComm : Set → GComm
+--   -- Seq   : GComm → GComm → GComm
+--   -- If   : whileTestState → GComm → GComm → GComm
+--   while : whileTestState → GComm → GComm
 
-gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set
-gearsSem pre post = {!!}
+-- gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set
+-- gearsSem pre post = {!!}
 
-unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l
-unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
+-- unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l
+-- unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
 
-comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l)
-comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b)
+-- comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l)
+-- comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b)
 
--- repeat : ℕ -> rel set zero -> rel set zero
--- repeat ℕ.zero r = λ x x₁ → ⊤
--- repeat (ℕ.suc m) r = comp (repeat m r) r
+-- -- repeat : ℕ -> rel set zero -> rel set zero
+-- -- repeat ℕ.zero r = λ x x₁ → ⊤
+-- -- repeat (ℕ.suc m) r = comp (repeat m r) r
 
-GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero)
-GSemComm Skip = λ x x₁ → ⊤
-GSemComm Abort = λ x x₁ → ⊥
-GSemComm (PComm x) = λ x₁ x₂ → x
--- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!}
--- GSemComm (If x con con₁) = {!!}
-GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) →  {!!}) {!!} {!!}
+-- GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero)
+-- GSemComm Skip = λ x x₁ → ⊤
+-- GSemComm Abort = λ x x₁ → ⊥
+-- GSemComm (PComm x) = λ x₁ x₂ → x
+-- -- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!}
+-- -- GSemComm (If x con con₁) = {!!}
+-- GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) →  {!!}) {!!} {!!}
 
 ProofConnect : {l : Level} {t : Set l}
   → (pr1 : Envc → Set → Set)