Mercurial > hg > Members > kono > Proof > automaton

comparison agda/induction-ex.agda @ 138:7a0634a7c25a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 18 Dec 2019 17:34:15 +0900
parents
children
comparison
equal deleted inserted replaced
137:08e2af685c69 138:7a0634a7c25a
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