Mercurial > hg > Papers > 2019 > oshiro-thesis

comparison final_main/src/AgdaTreeProof.agda @ 0:83f997abf3b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
first commit
author e155702
date Thu, 14 Feb 2019 16:51:50 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:83f997abf3b5
1 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
2 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
3
4 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
5 -> (k : ℕ) (x : ℕ)
6 -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
7 (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x ≡ True))
8 putTest1 n k x with n
9 ... | Just n1 = lemma2 ( record { top = Nothing } )
10 where
11 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
12 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
13 lemma2 s with compare2 k (key n1)
14 ... | EQ = lemma3 {!!}
15 where
16 lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {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 = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ 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 {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
29 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
30 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k
31 ( \ t x1 -> check2 x1 x ≡ True)
32 lemma1 with compare2 k k | putTest1Lemma2 k
33 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
34 ... | EQ | refl = refl