|
138
|
1 module list where
|
|
|
2
|
|
|
3 postulate A : Set
|
|
|
4
|
|
|
5 postulate a : A
|
|
|
6 postulate b : A
|
|
|
7 postulate c : A
|
|
|
8
|
|
|
9
|
|
|
10 infixr 40 _::_
|
|
|
11 data List (A : Set ) : Set where
|
|
|
12 [] : List A
|
|
266
|
13 _::_ : A → List A → List A
|
|
138
|
14
|
|
266
|
15 --
|
|
|
16 -- A List A
|
|
|
17 -- -------------- [] ---------------- _::_
|
|
|
18 -- List A List A
|
|
|
19 --
|
|
138
|
20
|
|
|
21 infixl 30 _++_
|
|
|
22 _++_ : {A : Set } → List A → List A → List A
|
|
266
|
23 [] ++ y = y
|
|
|
24 (x :: x₁) ++ y = x :: (x₁ ++ y )
|
|
138
|
25
|
|
|
26 l1 = a :: []
|
|
266
|
27 l2 = a :: b :: a :: c :: []
|
|
138
|
28
|
|
|
29 l3 = l1 ++ l2
|
|
|
30
|
|
|
31 data Node ( A : Set ) : Set where
|
|
|
32 leaf : A → Node A
|
|
|
33 node : Node A → Node A → Node A
|
|
|
34
|
|
|
35 flatten : { A : Set } → Node A → List A
|
|
|
36 flatten ( leaf a ) = a :: []
|
|
|
37 flatten ( node a b ) = flatten a ++ flatten b
|
|
|
38
|
|
|
39 n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c ))
|
|
|
40
|
|
|
41 open import Relation.Binary.PropositionalEquality
|
|
|
42
|
|
|
43 ++-assoc : (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
|
|
|
44 ++-assoc A [] ys zs = let open ≡-Reasoning in
|
|
|
45 begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs)
|
|
|
46 ( [] ++ ys ) ++ zs
|
|
|
47 ≡⟨ refl ⟩
|
|
|
48 ys ++ zs
|
|
|
49 ≡⟨⟩
|
|
|
50 [] ++ ( ys ++ zs )
|
|
|
51 ∎
|
|
|
52
|
|
|
53 ++-assoc A (x :: xs) ys zs = let open ≡-Reasoning in
|
|
|
54 begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
|
|
|
55 ((x :: xs) ++ ys) ++ zs
|
|
|
56 ≡⟨ refl ⟩
|
|
|
57 (x :: (xs ++ ys)) ++ zs
|
|
|
58 ≡⟨ refl ⟩
|
|
|
59 x :: ((xs ++ ys) ++ zs)
|
|
|
60 ≡⟨ cong (_::_ x) (++-assoc A xs ys zs) ⟩
|
|
|
61 x :: (xs ++ (ys ++ zs))
|
|
|
62 ≡⟨ refl ⟩
|
|
|
63 (x :: xs) ++ (ys ++ zs)
|
|
|
64 ∎
|
|
|
65
|
|
266
|
66 -- open import Data.Nat
|
|
|
67
|
|
|
68 data Nat : Set where
|
|
|
69 zero : Nat
|
|
|
70 suc : Nat → Nat
|
|
|
71
|
|
|
72 _+_ : Nat → Nat → Nat
|
|
|
73 zero + y = y
|
|
|
74 suc x + y = suc (x + y)
|
|
|
75
|
|
|
76 sym1 : {A : Set} → {a b : A} → a ≡ b → b ≡ a
|
|
|
77 sym1 {_} {a} {.a} refl = refl
|
|
|
78
|
|
|
79 trans1 : {A : Set} → {a b c : A} → a ≡ b → b ≡ c → a ≡ c
|
|
|
80 trans1 {_} {a} {b} {.a} refl refl = refl
|
|
|
81
|
|
|
82 cong1 : {A B : Set} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
|
|
|
83 cong1 f refl = refl
|
|
|
84
|
|
|
85 induction : (P : (x : Nat) → Set) → (initial : P zero ) → (induction-setp : ((x : Nat) → P x → P (suc x))) → (x : Nat) → P x
|
|
|
86 induction P initial induction-setp zero = initial
|
|
|
87 induction P initial induction-setp (suc x) = induction-setp x ( induction P initial induction-setp x)
|
|
138
|
88
|
|
266
|
89 induction' : (P : (x : Nat) → Set) → (initial : P zero ) → (induction-setp : ((x : Nat) → P x → P (suc x))) → (x : Nat) → P x
|
|
|
90 induction' P initial induction-setp x = {!!} where
|
|
|
91 ind1 : {!!} → P x
|
|
|
92 ind1 = {!!}
|
|
|
93
|
|
|
94 +-comm : {x y : Nat} → x + y ≡ y + x
|
|
|
95 +-comm {zero} {y} = sym1 lemma01 where
|
|
|
96 lemma01 : {y : Nat} → y + zero ≡ y
|
|
|
97 lemma01 {zero} = refl -- (zero + zero ) → zero → zero + zero ≡ zero
|
|
|
98 lemma01 {suc y} = cong1 (λ x → suc x) (lemma01 {y}) --- (suc y + zero) ≡ suc y
|
|
|
99 -- suc (y + zero) ≡ suc y ← y + zero ≡ y
|
|
|
100 +-comm {suc x} {y} = {!!}
|
|
|
101
|
|
|
102 _*_ : Nat → Nat → Nat
|
|
|
103 zero * y = zero
|
|
|
104 suc x * y = y + (x * y)
|
|
|
105
|
|
|
106 --
|
|
|
107 -- * * * * *
|
|
|
108 -- * * * ≡ * *
|
|
|
109 -- * *
|
|
|
110
|
|
|
111 *-comm : {x y : Nat} → x * y ≡ y * x
|
|
|
112 *-comm = {!!}
|
|
|
113
|
|
|
114 length : {L : Set} → List L → Nat
|
|
138
|
115 length [] = zero
|
|
|
116 length (_ :: T ) = suc ( length T )
|
|
|
117
|
|
|
118 lemma : {L : Set} → (x y : List L ) → ( length x + length y ) ≡ length ( x ++ y )
|
|
|
119 lemma [] [] = refl
|
|
|
120 lemma [] (_ :: _) = refl
|
|
|
121 lemma (H :: T) L = let open ≡-Reasoning in
|
|
|
122 begin
|
|
266
|
123 {!!}
|
|
|
124 ≡⟨ {!!} ⟩
|
|
|
125 {!!}
|
|
138
|
126 ∎
|
|
|
127
|
