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