Mercurial > hg > Members > Moririn

comparison src/parallel_execution/stack.agda @ 179:b3be97ba0782

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove n-push/n-pop
author atton
date Tue, 06 Dec 2016 08:17:08 +0000
parents bf26f1105862
children d8947747ff3b
comparison
equal deleted inserted replaced
178:5077cf9bf54e 179:b3be97ba0782
1 module stack where 1 module stack where
2 2
3 open import Relation.Binary.PropositionalEquality 3 open import Relation.Binary.PropositionalEquality
4
5 data Nat : Set where
6 zero : Nat
7 suc : Nat -> Nat
4 8
5 data Bool : Set where 9 data Bool : Set where
6 True : Bool 10 True : Bool
7 False : Bool 11 False : Bool
8 12
81 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02 85 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
82 86
83 87
84 lemma : {A : Set} {a : A} -> test03 a ≡ False 88 lemma : {A : Set} {a : A} -> test03 a ≡ False
85 lemma = refl 89 lemma = refl
90
91 id : {A : Set} -> A -> A
92 id a = a
93
94
95 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
96 n-push zero s = s
97 n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s)
98
99 n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
100 n-pop zero s = s
101 n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s)
102
103 open ≡-Reasoning
104
105 push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s
106 push-pop-equiv s = refl
107
108 push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s
109 push-and-n-pop zero s = refl
110 push-and-n-pop {A} {a} (suc n) s = begin
111 n-pop (suc (suc n)) (pushSingleLinkedStack s a id)
112 ≡⟨ refl ⟩
113 popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
114 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩
115 popSingleLinkedStack (n-pop n s) (\s _ -> s)
116 ≡⟨ refl ⟩
117 n-pop (suc n) s
118 ∎
119
120
121 n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s
122 n-push-pop-equiv zero s = refl
123 n-push-pop-equiv {A} {a} (suc n) s = begin
124 n-pop (suc n) (n-push (suc n) s)
125 ≡⟨ refl ⟩
126 n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
127 ≡⟨ push-and-n-pop n (n-push n s) ⟩
128 n-pop n (n-push n s)
129 ≡⟨ n-push-pop-equiv n s\ ⟩
130 s
131 ∎