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

diff -r 44d448a978d3 -r c87e85ffde9a cbc/stack-subtype-sample.agda
--- a/cbc/stack-subtype-sample.agda	Sat Jan 14 05:46:16 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sat Jan 14 05:59:49 2017 +0000
@@ -201,18 +201,39 @@
 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)
+n-push-pop (suc n) record {n = num ; element = nothing} = begin
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta record {n = num ; element = nothing})
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta record {n = num ; element = nothing})
+  ≡⟨ cong (\f -> M.exec f (id-meta record {n = num ; element = nothing})) (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 record {n = num ; element = nothing})
+  ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta record {n = num ; element = nothing})  ⟩
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing}))
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing}))
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (id-meta record {n = num ; element = nothing})
+  ≡⟨ cong (\f -> M.exec f (id-meta record {n = num ; element = nothing})) (M.comp-associative (M.cs pushOnce) (n-push n) (M.cs popOnce)) ⟩
+  M.exec (M.csComp (M.csComp (M.cs popOnce) (n-push n)) (M.cs pushOnce)) (id-meta record {n = num ; element = nothing})
+  ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push n)) (M.cs pushOnce) (id-meta record {n = num ; element = nothing }) ⟩
+  M.exec (M.csComp (M.cs popOnce) (n-push n)) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = nothing}))
   ≡⟨ 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))
+  M.exec (M.csComp (M.cs popOnce) (n-push n)) (id-meta record {n = num ; element = nothing})
+  ≡⟨ {!!} ⟩
+  M.exec (n-push (suc n)) (id-meta record {n = num ; element = nothing})
+  ∎
+n-push-pop (suc n) record {n = num ; element = just x} = begin
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta record {n = num ; element = just x})
   ≡⟨ 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 (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta record {n = num ; element = just x})
+  ≡⟨ cong (\f -> M.exec f (id-meta record {n = num ; element = just x})) (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 record {n = num ; element = just x})
+  ≡⟨ exec-comp (M.csComp (M.cs popOnce) (n-push (suc n))) (M.cs pushOnce) (id-meta record {n = num ; element = just x})  ⟩
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = just x}))
+  ≡⟨ refl ⟩
+  M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push n) (M.cs pushOnce))) (M.exec (M.cs pushOnce) (id-meta record {n = num ; element = just x}))
   ≡⟨ {!!} ⟩
-  M.exec (n-push (suc n)) (id-meta c)
+  M.exec (n-push (suc n)) (id-meta record {n = num ; element = just x})
   ∎