blob: 9bc5a6178946c7effbd355cb91ee18ce46801512 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
{-# OPTIONS --safe #-}
module Problem9 where
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Relation.Nullary
open import Data.List
open import Data.Nat.Properties using (suc-injective)
open import Data.List.Properties using (++-identityʳ;length-++; ++-assoc;unfold-reverse; length-reverse)
open ≡-Reasoning
variable A : Set
record Queue A : Set where
constructor Q
field
size-front : ℕ
size-back : ℕ
front : List A
back : List A
invariant : size-back ≤ size-front
size-inv₁ : length front ≡ size-front
size-inv₂ : length back ≡ size-back
open Queue
record CorrectQueue (Q : Set → Set) : Set₁ where
field
abstraction : Q A → List A
enqueue : A → Q A → Q A
dequeue : Q A → Maybe (Q A)
first : Q A → Maybe A
size : Q A → ℕ
empty : Q A
emptyᵣ : abstraction (empty {A}) ≡ []
sizeᵣ : ∀ (q : Q A) → size q ≡ length (abstraction q)
firstᵣ : ∀ (q : Q A) → first q ≡ head (abstraction q)
dequeueᵣ : ∀ (q : Q A) → Maybe.map abstraction (dequeue q) ≡ tail (abstraction q)
enqueueᵣ : ∀ (q : Q A) x → abstraction (enqueue x q) ≡ abstraction q ∷ʳ x
enqueueQ : A → Queue A → Queue A
enqueueQ x q with suc (size-back q) ≤? size-front q
... | yes p = Q (size-front q) (suc (size-back q)) (front q) (x ∷ back q) p (size-inv₁ q) (cong suc (size-inv₂ q))
... | no p = Q (size-front q + suc (size-back q)) 0 (front q ++ reverse (x ∷ back q)) [] z≤n (trans (length-++ (front q)) (cong₂ _+_ (size-inv₁ q) (trans (length-reverse (x ∷ back q) ) (cong suc (size-inv₂ q))))) refl
dequeueQ : Queue A → Maybe (Queue A)
dequeueQ (Q _ _ [] [] z≤n refl refl) = nothing
dequeueQ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) with size-back₁ ≤? size-front₁
... | yes p = just (Q size-front₁ size-back₁ front₁ back₁ p (suc-injective size-inv₃) size-inv₄)
... | no p = just (Q (size-front₁ + size-back₁) 0 (front₁ ++ reverse back₁) [] z≤n (trans (length-++ front₁) (cong₂ _+_ (suc-injective size-inv₃) (trans (length-reverse back₁) size-inv₄))) refl)
firstQ : Queue A → Maybe A
firstQ (Q size-front₁ size-back₁ [] back₁ invariant₁ size-inv₃ size-inv₄) = nothing
firstQ (Q size-front₁ size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) = just x
sizeQ : Queue A → ℕ
sizeQ q = size-front q + size-back q
emptyQ : Queue A
emptyQ = Q 0 0 [] [] z≤n refl refl
open CorrectQueue
goal : CorrectQueue Queue
-- Data portion of goal
goal .abstraction q = front q ++ reverse (back q)
goal .enqueue x q = enqueueQ x q
goal .dequeue q = dequeueQ q
goal .first q = firstQ q
goal .size q = sizeQ q
goal .empty = emptyQ
-- Correctness portion of goal
goal .emptyᵣ = refl
goal .sizeᵣ q = begin
sizeQ q ≡⟨⟩
size-front q + size-back q ≡˘⟨ cong₂ _+_ (size-inv₁ q) (size-inv₂ q) ⟩
length (front q) + length (back q) ≡˘⟨ cong (length (front q) +_) (length-reverse (back q)) ⟩
length (front q) + length (reverse (back q)) ≡˘⟨ length-++ (front q) ⟩
length (front q ++ reverse (back q)) ∎
goal .firstᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
goal .firstᵣ (Q _ _ (x ∷ front₁) back₁ _ _ _) = refl
goal .dequeueᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
goal .dequeueᵣ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄)
with size-back₁ ≤? size-front₁
... | yes p = refl
... | no p = cong just (++-identityʳ (front₁ ++ reverse back₁))
goal .enqueueᵣ q x with suc (size-back q) ≤? size-front q
... | yes p = begin
front q ++ reverse (x ∷ back q) ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
front q ++ reverse (back q) ++ x ∷ [] ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
(front q ++ reverse (back q)) ++ x ∷ [] ∎
... | no p = begin
(front q ++ reverse (x ∷ back q)) ++ [] ≡⟨ ++-identityʳ (front q ++ reverse (x ∷ back q)) ⟩
front q ++ reverse (x ∷ back q) ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
front q ++ reverse (back q) ++ x ∷ [] ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
(front q ++ reverse (back q)) ++ x ∷ [] ∎
|
