blob: 6ee5fafa3e6359af3d925a28252beef9776f6c79 (
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
{-# OPTIONS --safe #-}
module Problem23 where
open import Data.List
open import Data.List.Properties
open import Data.Fin using (fromℕ<)
open import Data.Fin.Properties using (fromℕ<-cong)
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open ≡-Reasoning
variable State : Set
variable f : State → State
Assertion : Set → Set₁
Assertion State = State → Set
variable ϕ ϕ′ ψ ψ′ π g : Assertion State
_∧_ : Assertion State → Assertion State → Assertion State
ϕ ∧ ψ = λ σ → ϕ σ × ψ σ
¬'_ : Assertion State → Assertion State
¬' ϕ = λ σ → (ϕ σ → ⊥)
_⇒_ : Assertion State → Assertion State → Set
ϕ ⇒ ψ = ∀ σ → ϕ σ → ψ σ
data Program (State : Set) : Set₁ where
SKIP : Program State
IF_THEN_ELSE_FI : Assertion State → Program State → Program State → Program State
WHILE_DO_OD : Assertion State → Program State → Program State
_∶_ : Program State → Program State → Program State
UPD : (State → State) → Program State
infixl 5 _∶_
variable P Q : Program State
data ⟨_⟩_⟨_⟩ {State : Set} : Assertion State → Program State → Assertion State → Set₁ where
skipₕ : ⟨ ϕ ⟩ SKIP ⟨ ϕ ⟩
ifₕ : ⟨ ϕ ∧ g ⟩ P ⟨ ψ ⟩ → ⟨ ϕ ∧ (¬' g) ⟩ Q ⟨ ψ ⟩ → ⟨ ϕ ⟩ IF g THEN P ELSE Q FI ⟨ ψ ⟩
whileₕ : ⟨ ϕ ∧ g ⟩ P ⟨ ϕ ⟩ → ⟨ ϕ ⟩ WHILE g DO P OD ⟨ ϕ ∧ (¬' g) ⟩
seqₕ : ⟨ ϕ ⟩ P ⟨ π ⟩ → ⟨ π ⟩ Q ⟨ ψ ⟩ → ⟨ ϕ ⟩ P ∶ Q ⟨ ψ ⟩
updₕ : ⟨ ϕ ∘ f ⟩ UPD f ⟨ ϕ ⟩
conseqₕ : ϕ ⇒ ϕ′ → ⟨ ϕ′ ⟩ P ⟨ ψ′ ⟩ → ψ′ ⇒ ψ → ⟨ ϕ ⟩ P ⟨ ψ ⟩
record ListSum : Set where
field
A : List ℕ
s : ℕ
i : ℕ
lookup' : List ℕ → ℕ → ℕ
lookup' V n with n <? length V
... | yes p = lookup V (fromℕ< p)
... | no p = 0
open ListSum
prog : Program ListSum
prog = UPD (λ σ → record σ { s = 0 })
∶ UPD (λ σ → record σ { i = 0 })
∶ WHILE (λ σ → σ .i ≢ length (σ .A)) DO
UPD (λ σ → record σ { s = σ .s + lookup' (σ .A) (σ .i) })
∶ UPD (λ σ → record σ { i = suc (σ .i) })
OD
goal : ∀ A₀ → ⟨ (λ σ → A₀ ≡ σ .A) ⟩ prog ⟨ (λ σ → σ .s ≡ sum A₀) ⟩
goal A₀ =
conseqₕ
(λ σ eq → trans (+-identityʳ (sum (σ .A))) (cong sum (sym eq)) , z≤n)
(seqₕ (seqₕ updₕ updₕ)
(whileₕ {ϕ = λ σ → sum (drop (σ .i) (σ .A)) + σ .s ≡ sum A₀ × σ .i ≤ length (σ .A)}
(conseqₕ
(λ σ ((prf , i≤length) , i≢length) →
let
1+i≤length = ≤∧≢⇒< i≤length i≢length
prf′ = begin
sum (drop (suc (σ .i)) (σ .A)) + (σ .s + lookup' (σ .A) (σ .i)) ≡˘⟨ +-assoc (sum (drop (suc (σ .i)) (σ .A))) _ _ ⟩
sum (drop (suc (σ .i)) (σ .A)) + σ .s + lookup' (σ .A) (σ .i) ≡⟨ +-comm _ (lookup' (σ .A) (σ .i)) ⟩
lookup' (σ .A) (σ .i) + (sum (drop (suc (σ .i)) (σ .A)) + σ .s) ≡˘⟨ +-assoc (lookup' (σ .A) (σ .i)) _ _ ⟩
lookup' (σ .A) (σ .i) + sum (drop (suc (σ .i)) (σ .A)) + σ .s ≡⟨ cong (_+ σ .s) (sum-drop-suc (σ .i) (σ .A) 1+i≤length) ⟩
sum (drop (σ .i) (σ .A)) + σ .s ≡⟨ prf ⟩
sum A₀ ∎
in
prf′ , 1+i≤length)
(seqₕ updₕ updₕ)
(λ σ → id))))
(λ σ ((prf , i≤length) , ¬i≢length) →
let
i≡length : σ .i ≡ length (σ .A)
i≡length = decidable-stable (σ .i ≟ length (σ .A)) ¬i≢length
dropᵢ[A]≡[] : drop (σ .i) (σ .A) ≡ []
dropᵢ[A]≡[] = length⁻¹ (begin
length (drop (σ .i) (σ .A)) ≡⟨ length-drop (σ .i) (σ .A) ⟩
length (σ .A) ∸ σ .i ≡˘⟨ cong (_∸ σ .i) i≡length ⟩
σ .i ∸ σ .i ≡⟨ n∸n≡0 (σ .i) ⟩
0 ∎)
in
begin
σ .s ≡⟨⟩
sum [] + σ .s ≡˘⟨ cong (λ ◌ → sum ◌ + σ .s) dropᵢ[A]≡[] ⟩
sum (drop (σ .i) (σ .A)) + σ .s ≡⟨ prf ⟩
sum A₀ ∎)
where
length⁻¹ : ∀ {xs : List ℕ} → length xs ≡ 0 → xs ≡ []
length⁻¹ {[]} prf = refl
lookup'-suc : (n x : ℕ) (xs : List ℕ) → lookup' (x ∷ xs) (suc n) ≡ lookup' xs n
lookup'-suc n x xs with n <? length xs | suc n <? suc (length xs)
... | yes p₁ | yes p₂ = cong (lookup xs) (fromℕ<-cong n n refl (≤-pred p₂) p₁)
... | yes p₁ | no p₂ = ⊥-elim (p₂ (s≤s p₁))
... | no p₁ | yes p₂ = ⊥-elim (p₁ (≤-pred p₂))
... | no p₁ | no p₂ = refl
sum-drop-suc :
(n : ℕ) (xs : List ℕ) →
.(n < length xs) →
lookup' xs n + sum (drop (suc n) xs) ≡ sum (drop n xs)
sum-drop-suc zero (x ∷ xs) _ = refl
sum-drop-suc (suc n) (x ∷ xs) n<length = begin
lookup' (x ∷ xs) (suc n) + sum (drop (suc n) xs) ≡⟨ cong (_+ sum (drop (suc n) xs)) (lookup'-suc n x xs) ⟩
lookup' xs n + sum (drop (suc n) xs) ≡⟨ sum-drop-suc n xs (≤-pred n<length) ⟩
sum (drop n xs) ∎
|
