forked from jonsterling/agda-calf
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Spec.agda
70 lines (59 loc) · 3.02 KB
/
Spec.agda
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
{-# OPTIONS --prop --rewriting #-}
module Examples.Gcd.Spec where
open import Calf.CostMonoid
import Calf.CostMonoids as CM
open import Calf CM.ℕ-CostMonoid
open import Calf.Types.Nat
open import Examples.Gcd.Euclid
open import Examples.Gcd.Clocked
open import Data.Nat.DivMod
open import Data.Nat
open import Relation.Binary.PropositionalEquality as P
open import Data.Nat.Properties
open import Data.Product
gcd/clocked≡spec/zero : ∀ k x h → k ≥ gcd/depth (x , ℕ.zero , h) →
◯ (gcd/clocked k (x , ℕ.zero , h) ≡ ret {nat} x)
gcd/clocked≡spec/zero ℕ.zero x h h1 u = refl
gcd/clocked≡spec/zero (suc k) x h h1 u = refl
suc-cancel-≤ : ∀ {m n} → suc m ≤ suc n → m ≤ n
suc-cancel-≤ (s≤s h) = h
gcd/clocked/mono : ∀ k x y h → k ≥ gcd/depth (x , y , h) →
gcd/clocked k (x , y , h) ≡ gcd/clocked (suc k) (x , y , h)
gcd/clocked/mono ℕ.zero x ℕ.zero h h1 = refl
gcd/clocked/mono (suc k) x ℕ.zero h h1 = refl
gcd/clocked/mono (suc k) x (suc y) h h1 =
begin
gcd/clocked (suc k) (x , suc y , h) ≡⟨ refl ⟩
step (F nat) 1 (gcd/clocked k (suc y , x % suc y , m%n<n x y)) ≡⟨
P.cong (step (F nat) 1)
(gcd/clocked/mono k (suc y) (x % suc y) (m%n<n x y)
(suc-cancel-≤ (P.subst (λ r → suc k ≥ r) (gcd/depth-unfold-suc {x} {y} {h}) h1))) ⟩
step (F nat) 1 (gcd/clocked (suc k) (suc y , x % suc y , m%n<n x y))
∎
where open ≡-Reasoning
gcd/clocked≡spec/suc : ∀ k x y h → k ≥ gcd/depth (x , suc y , h) →
◯ (gcd/clocked k (x , suc y , h) ≡ gcd/clocked k (suc y , x % suc y , m%n<n x y))
gcd/clocked≡spec/suc (suc k) x y h h1 u =
begin
gcd/clocked (suc k) (x , suc y , h) ≡⟨ refl ⟩
step (F nat) 1 (gcd/clocked k (suc y , x % suc y , m%n<n x y)) ≡⟨ step/ext (F nat) ((gcd/clocked k (suc y , x % suc y , m%n<n x y))) 1 u ⟩
gcd/clocked k (suc y , x % suc y , m%n<n x y) ≡⟨ gcd/clocked/mono k (suc y) (x % suc y) (m%n<n x y)
(suc-cancel-≤ (P.subst (λ r → suc k ≥ r) (gcd/depth-unfold-suc {x} {y} {h}) h1)) ⟩
gcd/clocked (suc k) (suc y , x % suc y , m%n<n x y)
∎
where open ≡-Reasoning
gcd≡spec/zero : ∀ x h → ◯ (gcd (x , 0 , h) ≡ ret {nat} x)
gcd≡spec/zero x h = gcd/clocked≡spec/zero (gcd/depth (x , 0 , h)) x h ≤-refl
gcd≡spec/suc : ∀ x y h → ◯ (gcd (x , suc y , h) ≡ gcd (suc y , x % suc y , m%n<n x y))
gcd≡spec/suc x y h u =
begin
gcd (x , suc y , h) ≡⟨ gcd/clocked≡spec/suc (gcd/depth (x , suc y , h)) x y h ≤-refl u ⟩
gcd/clocked (gcd/depth (x , suc y , h)) (suc y , x % suc y , m%n<n x y) ≡⟨
cong (λ k → gcd/clocked k (suc y , x % suc y , m%n<n x y))
(gcd/depth-unfold-suc {x} {y} {h}) ⟩
gcd/clocked (suc (gcd/depth (suc y , x % suc y , m%n<n x y))) (suc y , x % suc y , m%n<n x y) ≡⟨
sym (gcd/clocked/mono
(gcd/depth (suc y , x % suc y , m%n<n x y)) (suc y) (x % suc y) (m%n<n x y) ≤-refl) ⟩
gcd/clocked (gcd/depth (suc y , x % suc y , m%n<n x y)) (suc y , x % suc y , m%n<n x y)
∎
where open ≡-Reasoning