/
06-Induction.agda
150 lines (116 loc) · 3.87 KB
/
06-Induction.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
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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
module 06-Induction where
open import Data.Nat
open import Data.List
open import Data.List.Properties
open import Data.Empty
open import Data.Sum
using (_⊎_; inj₁; inj₂)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function
import Function.Related as Related
indℕ : (P : ℕ → Set) → P zero → (∀ n → P n → P (suc n)) →
∀ n → P n
indℕ P base step zero = {!!}
indℕ P base step (suc n) = {!-l!}
indℕ₁ : (P : ℕ → Set) → P zero → (∀ n → P n → P (suc n)) →
∀ n → P n
indℕ₁ P base step zero = {!!}
indℕ₁ P base step (suc n) = {!-l!}
+-suc : ∀ n m → n + suc m ≡ suc (n + m)
+-suc n m = {!!}
+-suc₁ : ∀ m n → n + suc m ≡ suc (n + m)
+-suc₁ m = indℕ (λ n → n + suc m ≡ suc (n + m)) {!!} {!!}
mutual
data Even : ℕ → Set where
even0 : Even zero
even1 : ∀ {n} → (odd-n : Odd n) → Even (suc n)
data Odd : ℕ → Set where
odd1 : ∀ {n} → (even-n : Even n) → Odd (suc n)
even3 : Even 2
even3 = {!!}
odd4 : Odd 3
odd4 = {!!}
even2n : ∀ n → Even (n + n)
even2n zero = even0
even2n (suc n) = {!!}
even2n′ : ∀ n → Even (n + n)
even2n′ zero = even0
even2n′ (suc n) = step (even2n′ n)
where
open Related.EquationalReasoning renaming (sym to ∼sym)
step : Even (n + n) → Even (suc n + suc n)
step = Even (n + n)
∼⟨ {!!} ⟩
Odd (suc (n + n))
∼⟨ {!!} ⟩
Even (suc (suc (n + n)))
∼⟨ {!!} ⟩
Even (suc (n + suc n))
∼⟨ {!!} ⟩
Even (suc n + suc n) ∎
even⊎odd : ∀ n → Even n ⊎ Odd n
even⊎odd zero = inj₁ even0
even⊎odd (suc n) with even⊎odd n
... | r = {!!}
-- even⊎odd (suc n) = [ inj₂ ∘ odd1 , inj₁ ∘ even1 ]′ (even-odd n)
odd→¬even : ∀ {n} → Odd n → ¬ Even n
odd→¬even odd-n even-n = {!!}
even? : ∀ n → Dec (Even n)
even? n with even⊎odd n
even? n | r = {!!}
-- Trees
data Tree (A : Set) : Set where
leaf : (a : A) → Tree A
node : (t₁ t₂ : Tree A) → Tree A
tree-ind : ∀ {A : Set} (P : Tree A → Set) →
(∀ a → P (leaf a)) →
(∀ (t₁ t₂ : Tree A) → P t₁ → P t₂ → P (node t₁ t₂)) →
∀ t → P t
tree-ind P base step (leaf a) = {!!}
tree-ind P base step (node t₁ t₂) =
{!!}
flatten : {A : Set} → Tree A → List A
flatten (leaf a) = a ∷ []
flatten (node t₁ t₂) = flatten t₁ ++ flatten t₂
append : {A : Set} → Tree A → List A → List A
append (leaf a) as = a ∷ as
append (node t₁ t₂) as = append t₁ (append t₂ as)
module Test-flatten {A : Set} (a b c : A) where
t1 : flatten (leaf a) ≡ a ∷ []
t1 = refl
t2 : flatten (node (node (leaf a) (leaf b)) (leaf c)) ≡ a ∷ b ∷ c ∷ []
t2 = refl
t3 : append (leaf a) [] ≡ a ∷ []
t3 = refl
t4 : append (node (node (leaf a) (leaf b)) (leaf c)) [] ≡ a ∷ b ∷ c ∷ []
t4 = refl
++-[] : {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-[] [] = refl
++-[] (x ∷ xs) = cong (_∷_ x) (++-[] xs)
++-assoc : {A : Set} (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)
append-correct′ : {A : Set} (t : Tree A) (xs : List A) →
flatten t ++ xs ≡ append t xs
append-correct′ (leaf a) xs = {!!}
append-correct′ (node t₁ t₂) xs = begin
(flatten t₁ ++ flatten t₂) ++ xs
≡⟨ {!!} ⟩
flatten t₁ ++ (flatten t₂ ++ xs)
≡⟨ {!!} ⟩
flatten t₁ ++ (append t₂ xs)
≡⟨ {!!} ⟩
append t₁ (append t₂ xs)
∎
where open ≡-Reasoning
append-correct : {A : Set} (t : Tree A) →
flatten t ≡ append t []
append-correct t =
flatten t
≡⟨ {!!} ⟩
flatten t ++ []
≡⟨ {!!} ⟩
append t []
∎
where open ≡-Reasoning