# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484372776 0
# Node ID 44d448a978d36d7902f124f36f79b1ee1c773d55
# Parent  c3afde46a41d9e31fa234d51a2f6644dff724768
Trying define n-push/n-pop equiv

diff -r c3afde46a41d -r 44d448a978d3 cbc/stack-subtype-sample.agda
--- a/cbc/stack-subtype-sample.agda	Sat Jan 14 02:35:33 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sat Jan 14 05:46:16 2017 +0000
@@ -1,11 +1,12 @@
 module stack-subtype-sample where
 
+open import Level renaming (suc to S ; zero to O)
 open import Function
 open import Data.Nat
 open import Data.Maybe
 open import Relation.Binary.PropositionalEquality
 
-open import stack-subtype ℕ  as S
+open import stack-subtype ℕ 
 open import subtype Context  as N
 open import subtype Meta     as M
 
@@ -85,37 +86,37 @@
 pushOnce m = M.exec pushSingleLinkedStackCS m
 
 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
-n-push {{mm}} (zero)  = M.cs {{mm}} {{mm}} pushOnce
-n-push {m} {{mm}} (suc n)        = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce)
+n-push {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-push {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce)
 
 popOnce : Meta -> Meta
 popOnce m = M.exec popSingleLinkedStackCS m
 
 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
-n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} popOnce
+n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
 n-pop {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-pop {m} {{mm}} n) (M.cs {{mm}} {{mm}} popOnce)
 
 
 
 
-initMeta : ℕ -> N.CodeSegment Context Context -> Meta
-initMeta n code = record { context = record { n = n ; element = nothing}
+initMeta : ℕ  -> Maybe ℕ -> N.CodeSegment Context Context -> Meta
+initMeta n mn code = record { context = record { n = n ; element = mn}
                          ; stack   = emptySingleLinkedStack
                          ; nextCS  = code
                          }
 
-n-push-cs-exec = M.exec (n-push {meta} 2) meta
+n-push-cs-exec = M.exec (n-push {meta} 3) meta
   where
-    meta = (initMeta 5 pushNum)
+    meta = (initMeta 5 (just 9) pushNum)
 
 
 n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS  = pushNum
                                                 ; context = record {n = 2 ; element = just 3}
-                                                ; stack   = record {top = just (cons 4 (just (cons 5 nothing)))}}
+                                                ; stack   = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}}
 n-push-cs-exec-equiv = refl
 
 
-n-pop-cs-exec = M.exec (n-pop {meta} 3) meta
+n-pop-cs-exec = M.exec (n-pop {meta} 4) meta
   where
     meta = record { nextCS  = N.cs id
                   ; context = record { n = 0 ; element = nothing}
@@ -128,3 +129,108 @@
                                               }
 
 n-pop-cs-exec-equiv = refl
+
+
+open ≡-Reasoning
+
+{-
+comp-id-type : {m : Meta} {{mm : M.DataSegment Meta}} (f : M.CodeSegment Meta Meta) -> Set₁
+comp-id-type {m} {{mm}} f = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} f (M.cs {S O} {S O} {Meta} {Meta} {{mm}}{{mm}} id) ≡ f
+
+comp-id : {m : Meta} (f : M.CodeSegment Meta Meta) -> comp-id-type {m} f
+comp-id (M.cs f) = refl
+
+n-pop-pop-once-n-push :(n : ℕ) (m : Meta) ->
+    M.exec (M.csComp {m} (M.csComp {m} (n-pop {m} n) (M.cs popOnce)) (n-push {m} (suc n))) m
+    ≡
+    M.exec (M.csComp {m} (n-pop {m} n) (n-push {m} n)) m
+n-pop-pop-once-n-push zero m    = begin
+  M.exec (M.csComp {m} (M.csComp {m} (n-pop {m} zero) (M.cs popOnce)) (n-push {m} (suc zero))) m
+  ≡⟨ refl ⟩
+   M.exec (M.csComp {m} (M.csComp {m} (M.cs {S O} {S O} {Meta} {Meta} id) (M.cs popOnce)) (n-push {m} (suc zero))) m
+  ≡⟨ {!!} ⟩
+  M.exec (M.csComp {m} (M.cs popOnce) (n-push {m} (suc zero))) m
+  ≡⟨ {!!} ⟩
+  M.exec (M.csComp {m} (n-pop {m} zero) (n-push {m} zero)) m
+  ∎
+n-pop-pop-once-n-push (suc n) m = {!!} 
+-}
+
+
+
+
+id-meta : Context -> Meta
+id-meta c = record { context = c ; nextCS = (N.cs id) ; stack = record {top = nothing}}
+
+
+push-pop : (c : Context) -> M.exec (M.csComp {id-meta c} (M.cs popOnce) (M.cs pushOnce)) (id-meta c) ≡ id-meta c
+push-pop record { n = n ; element = (just x) } = refl
+push-pop record { n = n ; element = nothing }  = refl
+{-
+n-pop-pop-once-n-push : (n : ℕ) (c : Context) ->
+    M.exec (M.csComp {id-meta c}  (M.csComp {id-meta c} (n-pop {id-meta c} n) (M.cs popOnce)) (n-push {id-meta c} (suc n))) (id-meta c)
+    ≡                                                                                                                
+    M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c)
+n-pop-pop-once-n-push zero    c = begin
+  M.exec (M.csComp {id-meta c} (M.csComp {id-meta c}(n-pop {id-meta c} zero) (M.cs popOnce)) (n-push {id-meta c} (suc zero))) (id-meta c)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp {id-meta c} (M.csComp {id-meta c} (M.cs {S O} {S O} {Meta} {Meta} id) (M.cs popOnce)) (n-push {id-meta c} (suc zero))) (id-meta c)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp {id-meta c} (M.cs popOnce) (n-push {id-meta c} (suc zero))) (id-meta c)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp {id-meta c} (M.cs popOnce) (M.cs pushOnce)) (id-meta c)
+  ≡⟨ push-pop c ⟩
+  id-meta c
+  ≡⟨ refl ⟩
+  M.exec (M.csComp {id-meta c} (n-pop {id-meta c} zero) (n-push {id-meta c} zero)) (id-meta c)
+  ∎
+n-pop-pop-once-n-push (suc n) c = begin
+  M.exec (M.csComp (M.csComp (n-pop (suc n)) (M.cs popOnce)) (n-push (suc (suc n)))) (id-meta c)
+  ≡⟨ cong (\f -> M.exec f (id-meta c)) (sym (M.comp-associative (n-push (suc (suc n))) (M.cs popOnce) (n-pop (suc n)))) ⟩
+  M.exec (M.csComp (n-pop (suc n)) (M.csComp (M.cs popOnce) (n-push (suc (suc n))))) (id-meta c)
+  ≡⟨ {!!} ⟩
+  M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c)
+  ∎
+-}
+
+exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m)
+exec-comp (M.cs x) (M.cs _) m = refl
+
+
+
+n-push-pop :  (n : ℕ) (c : Context) ->
+  (M.exec (M.csComp {id-meta c} (M.cs popOnce) (n-push {id-meta c} (suc n))) (id-meta c)) ≡ M.exec (n-push {id-meta c} n) (id-meta c)
+n-push-pop zero c    = push-pop c
+n-push-pop (suc n) c = begin
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta c)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta c)
+  ≡⟨ cong (\f -> M.exec f (id-meta c)) (M.comp-associative (M.cs pushOnce) (n-push (suc n)) (M.cs popOnce) ) ⟩
+  M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce)) (id-meta c)
+  ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta c)  ⟩
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (M.exec (M.cs pushOnce) (id-meta c))
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (M.exec (M.cs pushOnce) (id-meta c))
+  ≡⟨ {!!} ⟩
+  M.exec (n-push (suc n)) (id-meta c)
+  ∎
+
+
+n-push-pop-equiv : {c : Context} -> (n : ℕ )
+                 -> M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c) ≡ (id-meta c)
+n-push-pop-equiv           zero  = refl
+n-push-pop-equiv {c} (suc n) = begin
+  M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.csComp (n-pop n) (M.cs popOnce)) (n-push (suc n))) (id-meta c)
+  ≡⟨ cong (\f -> M.exec f (id-meta c)) (sym (M.comp-associative (n-push (suc n)) (M.cs popOnce) (n-pop n)))  ⟩
+  M.exec (M.csComp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n)))) (id-meta c)
+  ≡⟨ exec-comp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n)))  (id-meta c) ⟩
+  M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta c))
+  ≡⟨ cong (\x -> M.exec (n-pop n) x) (n-push-pop n c ) ⟩
+  M.exec (n-pop n) (M.exec (n-push {id-meta c} n) (id-meta c))
+  ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta c)) ⟩
+  M.exec (M.csComp (n-pop n) (n-push n)) (id-meta c)
+  ≡⟨ n-push-pop-equiv n ⟩
+  id-meta c
+  ∎
diff -r c3afde46a41d -r 44d448a978d3 cbc/stack-subtype.agda
--- a/cbc/stack-subtype.agda	Sat Jan 14 02:35:33 2017 +0000
+++ b/cbc/stack-subtype.agda	Sat Jan 14 05:46:16 2017 +0000
@@ -96,7 +96,7 @@
     st : Meta -> SingleLinkedStack A
     st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
     st record {stack = record { top = nothing           }} = record {top = nothing}
-    
+