|
138
|
1 {-# OPTIONS --guardedness #-}
|
|
|
2 module induction-ex where
|
|
|
3
|
|
|
4 open import Relation.Binary.PropositionalEquality
|
|
|
5 open import Size
|
|
|
6 open import Data.Bool
|
|
|
7
|
|
|
8 data List (A : Set ) : Set where
|
|
|
9 [] : List A
|
|
|
10 _∷_ : A → List A → List A
|
|
|
11
|
|
|
12 data Nat : Set where
|
|
|
13 zero : Nat
|
|
|
14 suc : Nat → Nat
|
|
|
15
|
|
|
16 add : Nat → Nat → Nat
|
|
|
17 add zero x = x
|
|
|
18 add (suc x) y = suc ( add x y )
|
|
|
19
|
|
|
20 _++_ : {A : Set} → List A → List A → List A
|
|
|
21 [] ++ y = y
|
|
|
22 (x ∷ t) ++ y = x ∷ ( t ++ y )
|
|
|
23
|
|
|
24 test1 = (zero ∷ []) ++ (zero ∷ [])
|
|
|
25
|
|
|
26 length : {A : Set } → List A → Nat
|
|
|
27 length [] = zero
|
|
|
28 length (_ ∷ t) = suc ( length t )
|
|
|
29
|
|
|
30 lemma1 : {A : Set} → (x y : List A ) → length ( x ++ y ) ≡ add (length x) (length y)
|
|
|
31 lemma1 [] y = refl
|
|
|
32 lemma1 (x ∷ t) y = cong ( λ k → suc k ) lemma2 where
|
|
|
33 lemma2 : length (t ++ y) ≡ add (length t) (length y)
|
|
|
34 lemma2 = lemma1 t y
|
|
|
35
|
|
|
36 -- record List1 ( A : Set ) : Set where
|
|
|
37 -- inductive
|
|
|
38 -- field
|
|
|
39 -- nil : List1 A
|
|
|
40 -- cons : A → List1 A → List1 A
|
|
|
41 --
|
|
|
42 -- record List2 ( A : Set ) : Set where
|
|
|
43 -- coinductive
|
|
|
44 -- field
|
|
|
45 -- nil : List2 A
|
|
|
46 -- cons : A → List2 A → List2 A
|
|
|
47
|
|
|
48 data SList (i : Size) (A : Set) : Set where
|
|
|
49 []' : SList i A
|
|
|
50 _∷'_ : {j : Size< i} (x : A) (xs : SList j A) → SList i A
|
|
|
51
|
|
|
52
|
|
|
53 map : ∀{i A B} → (A → B) → SList i A → SList i B
|
|
|
54 map f []' = []'
|
|
|
55 map f ( x ∷' xs)= f x ∷' map f xs
|
|
|
56
|
|
|
57 foldr : ∀{i} {A B : Set} → (A → B → B) → B → SList i A → B
|
|
|
58 foldr c n []' = n
|
|
|
59 foldr c n (x ∷' xs) = c x (foldr c n xs)
|
|
|
60
|
|
|
61 any : ∀{i A} → (A → Bool) → SList i A → Bool
|
|
|
62 any p xs = foldr _∨_ false (map p xs)
|
|
|
63
|
|
|
64 -- Sappend : {A : Set } {i j : Size } → SList i A → SList j A → SList {!!} A
|
|
|
65 -- Sappend []' y = y
|
|
|
66 -- Sappend (x ∷' x₁) y = _∷'_ {?} x (Sappend x₁ y)
|
|
|
67
|
|
|
68 language : { Σ : Set } → Set
|
|
|
69 language {Σ} = List Σ → Bool
|
|
|
70
|
|
|
71 record Lang (i : Size) (A : Set) : Set where
|
|
|
72 coinductive
|
|
|
73 field
|
|
|
74 ν : Bool
|
|
|
75 δ : ∀{j : Size< i} → A → Lang j A
|
|
|
76
|
|
|
77 open Lang
|
|
|
78
|
|
|
79 ∅ : ∀ {i A} → Lang i A
|
|
|
80 ν ∅ = false
|
|
|
81 δ ∅ _ = ∅
|
|
|
82
|
|
|
83 ∅' : {i : Size } { A : Set } → Lang i A
|
|
|
84 ∅' {i} {A} = record { ν = false ; δ = lemma3 } where
|
|
|
85 lemma3 : {j : Size< i} → A → Lang j A
|
|
|
86 lemma3 {j} _ = {!!}
|
|
|
87
|
|
|
88 ∅l : {A : Set } → language {A}
|
|
|
89 ∅l _ = false
|
|
|
90
|
|
|
91 ε : ∀ {i A} → Lang i A
|
|
|
92 ν ε = true
|
|
|
93 δ ε _ = ∅
|
|
|
94
|
|
|
95 εl : {A : Set } → language {A}
|
|
|
96 εl [] = true
|
|
|
97 εl (_ ∷ _) = false
|
|
|
98
|
|
|
99 _+_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
|
|
|
100 ν (a + b) = ν a ∨ ν b
|
|
|
101 δ (a + b) x = δ a x + δ b x
|
|
|
102
|
|
|
103 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
104 Union {Σ} A B x = (A x ) ∨ (B x)
|
|
|
105
|
|
|
106 _·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
|
|
|
107 ν (a · b) = ν a ∧ ν b
|
|
|
108 δ (a · b) x = if (ν a) then ((δ a x · b ) + (δ b x )) else ( δ a x · b )
|
|
|
109
|
|
|
110 split : {Σ : Set} → (List Σ → Bool)
|
|
|
111 → ( List Σ → Bool) → List Σ → Bool
|
|
|
112 split x y [] = x [] ∨ y []
|
|
|
113 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
114 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
115
|
|
|
116 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
117 Concat {Σ} A B = split A B
|
|
|
118
|
