blob: 3aab789baaf317dc573a6ee01b57ca81fb5b7627 (
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
|
{-# OPTIONS --safe #-}
module Problem1 where
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
data 𝔹 : Set where
T F : 𝔹
iterate : (n : ℕ) (f : 𝔹 → 𝔹) (x : 𝔹) → 𝔹
iterate zero f x = x
iterate (suc n) f x = f (iterate n f x)
twice = iterate (suc (suc zero))
-- There are exactly four functions 𝔹 → 𝔹: the two constant functions, the
-- identiy and the inversion.
--
-- We can decide (extensionally) which function we have.
data OneOf (f : 𝔹 → 𝔹) : Set where
is-const : (∀ x y → f x ≡ f y) → OneOf f
is-id : (∀ x → f x ≡ x) → OneOf f
is-not : f T ≡ F → f F ≡ T → OneOf f
which-one? : (f : 𝔹 → 𝔹) → OneOf f
which-one? f with f T in prfT | f F in prfF
... | T | T = is-const λ
{ T T → refl
; T F → begin
f T ≡⟨ prfT ⟩
T ≡⟨ sym prfF ⟩
f F ∎
; F T → begin
f F ≡⟨ prfF ⟩
T ≡⟨ sym prfT ⟩
f T ∎
; F F → refl
}
... | T | F = is-id λ { T → prfT ; F → prfF }
... | F | T = is-not prfT prfF
... | F | F = is-const λ
{ T T → refl
; T F → begin
f T ≡⟨ prfT ⟩
F ≡⟨ sym prfF ⟩
f F ∎
; F T → begin
f F ≡⟨ prfF ⟩
F ≡⟨ sym prfT ⟩
f T ∎
; F F → refl
}
-- First, we show that applying a function thrice is equal to a single
-- application. We do this by splitting on the exact function.
thrice-is-once : (f : 𝔹 → 𝔹) → iterate 3 f ≗ f
thrice-is-once f with which-one? f
... | is-const prf = λ b → prf (f (f b)) b
... | is-id prf = λ b →
begin
f (f (f b)) ≡⟨ prf (f (f b)) ⟩
f (f b) ≡⟨ prf (f b) ⟩
f b ∎
... | is-not prfT prfF = λ
{ T → begin
f (f (f T)) ≡⟨ cong (twice f) prfT ⟩
f (f F) ≡⟨ cong f prfF ⟩
f T ∎
; F → begin
f (f (f F)) ≡⟨ cong (twice f) prfF ⟩
f (f T) ≡⟨ cong f prfT ⟩
f F ∎
}
-- We prove the theorem by induction on n.
goal : ∀ (f : 𝔹 → 𝔹) (b : 𝔹) (n : ℕ) → iterate n (twice f) (f b) ≡ f b
goal f b zero = refl
goal f b (suc n) = begin
f (f (iterate n (twice f) (f b))) ≡⟨ cong (twice f) (goal f b n) ⟩
f (f (f b)) ≡⟨ thrice-is-once f b ⟩
f b ∎
|
