Mercurial > hg > Papers > 2021 > soto-prosym
comparison Paper/src/AgdaTreeProof.agda.replaced @ 0:c59202657321
init
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 Nov 2021 06:55:58 +0900 |
| parents | |
| children | 339fb67b4375 |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:c59202657321 |
|---|---|
| 1 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@ | |
| 2 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } | |
| 3 | |
| 4 putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)) | |
| 5 @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@) | |
| 6 @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x | |
| 7 (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True)) | |
| 8 putTest1 n k x with n | |
| 9 ... | Just n1 = lemma2 ( record { top = Nothing } ) | |
| 10 where | |
| 11 lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (@$\lambda$@ t @$\rightarrow$@ | |
| 12 GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\_{1}$@ x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) (root t)) | |
| 13 lemma2 s with compare2 k (key n1) | |
| 14 ... | EQ = lemma3 {!!} | |
| 15 where | |
| 16 lemma3 : compare2 k (key n1) @$\equiv$@ EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { | |
| 17 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black | |
| 18 } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) | |
| 19 lemma3 eq with compare2 x x | putTest1Lemma2 x | |
| 20 ... | EQ | refl with compare2 k (key n1) | eq | |
| 21 ... | EQ | refl with compare2 x x | putTest1Lemma2 x | |
| 22 ... | EQ | refl = refl | |
| 23 ... | GT = {!!} | |
| 24 ... | LT = {!!} | |
| 25 | |
| 26 ... | Nothing = lemma1 | |
| 27 where | |
| 28 lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { | |
| 29 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red | |
| 30 } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{1}$@ y } ) k | |
| 31 ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) | |
| 32 lemma1 with compare2 k k | putTest1Lemma2 k | |
| 33 ... | EQ | refl with compare2 x x | putTest1Lemma2 x | |
| 34 ... | EQ | refl = refl |