Mercurial > hg > Members > atton > agda-proofs

changeset 67:ee2659635734

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying prove n-push/n-pop ...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 15 Jan 2017 02:55:38 +0000
parents 211fde284b7e
children f3ad255e3b50
files cbc/stack-subtype-sample.agda
diffstat 1 files changed, 5 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/cbc/stack-subtype-sample.agda	Sun Jan 15 02:33:47 2017 +0000
+++ b/cbc/stack-subtype-sample.agda	Sun Jan 15 02:55:38 2017 +0000
@@ -231,15 +231,11 @@
   ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
   M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
   ≡⟨ refl ⟩
-  M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (record { nextCS  = (N.cs id) ;
-                                                           context = record {n = cn ; element = just ce} ;
-                                                           stack   = record {top = just (cons ce (SingleLinkedStack.top s)) }
-                                                         }))
-  ≡⟨ {!!} ⟩
-  M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) ?
-  ≡⟨ {!!} ⟩
-  M.exec (n-push n) (record { nextCS  = (N.cs id) ; context = record {n = cn ; element = just ce} ;
-                              stack   = record {top = just (cons ce (SingleLinkedStack.top s))}})
+  M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
+  ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩
+  M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ pop-n-push {!!} cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩
+  M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
   ≡⟨ refl ⟩
   M.exec (n-push n) (pushOnce (id-meta cn ce s))
   ≡⟨ refl ⟩