open import Relation.Nullary open import Relation.Binary.PropositionalEquality module flcagl (A : Set) ( _≟_ : (a b : A) → Dec ( a ≡ b ) ) where open import Data.Bool hiding ( _≟_ ) -- open import Data.Maybe open import Level renaming ( zero to Zero ; suc to succ ) open import Size module List where data List (i : Size) (A : Set) : Set where [] : List i A _∷_ : {j : Size< i} (x : A) (xs : List j A) → List i A map : ∀{i A B} → (A → B) → List i A → List i B map f [] = [] map f ( x ∷ xs)= f x ∷ map f xs foldr : ∀{i} {A B : Set} → (A → B → B) → B → List i A → B foldr c n [] = n foldr c n (x ∷ xs) = c x (foldr c n xs) any : ∀{i A} → (A → Bool) → List i A → Bool any p xs = foldr _∨_ false (map p xs) module Lang where open List record Lang (i : Size) : Set where coinductive field ν : Bool δ : ∀{j : Size< i} → A → Lang j open Lang _∋_ : ∀{i} → Lang i → List i A → Bool l ∋ [] = ν l l ∋ ( a ∷ as ) = δ l a ∋ as trie : ∀{i} (f : List i A → Bool) → Lang i ν (trie f) = f [] δ (trie f) a = trie (λ as → f (a ∷ as)) ∅ : ∀{i} → Lang i ν ∅ = false δ ∅ x = ∅ ε : ∀{i} → Lang i ν ε = true δ ε x = ∅ open import Relation.Nullary.Decidable char : ∀{i} (a : A) → Lang i ν (char a) = false δ (char a) x = if ⌊ a ≟ x ⌋ then ε else ∅ compl : ∀{i} (l : Lang i) → Lang i ν (compl l) = not (ν l) δ (compl l) x = compl (δ l x) _∪_ : ∀{i} (k l : Lang i) → Lang i ν (k ∪ l) = ν k ∨ ν l δ (k ∪ l) x = δ k x ∪ δ l x _·'_ : ∀{i} (k l : Lang i) → Lang i ν (k ·' l) = ν k ∧ ν l δ (k ·' l) x = let k′l = δ k x ·' l in if ν k then k′l ∪ δ l x else k′l _·_ : ∀{i} (k l : Lang i ) → Lang i ν (k · l) = ν k ∧ ν l δ (_·_ {i} k l) {j} x = let k′l : Lang j k′l = _·_ {j} (δ k {j} x) l in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l _* : ∀{i} (l : Lang i) → Lang i ν (l *) = true δ (l *) x = δ l x · (l *) record _≅⟨_⟩≅_ (l : Lang ∞ ) i (k : Lang ∞) : Set where coinductive field ≅ν : ν l ≡ ν k ≅δ : ∀ {j : Size< i } (a : A ) → δ l a ≅⟨ j ⟩≅ δ k a open _≅⟨_⟩≅_ ≅refl : ∀{i} {l : Lang ∞} → l ≅⟨ i ⟩≅ l ≅ν ≅refl = refl ≅δ ≅refl a = ≅refl ≅sym : ∀{i} {k l : Lang ∞} (p : l ≅⟨ i ⟩≅ k) → k ≅⟨ i ⟩≅ l ≅ν (≅sym p) = sym (≅ν p) ≅δ (≅sym p) a = ≅sym (≅δ p a) ≅trans : ∀{i} {k l m : Lang ∞} ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m ≅ν (≅trans p q) = trans (≅ν p) (≅ν q) ≅δ (≅trans p q) a = ≅trans (≅δ p a) (≅δ q a) open import Relation.Binary ≅isEquivalence : ∀(i : Size) → IsEquivalence _≅⟨ i ⟩≅_ ≅isEquivalence i = record { refl = ≅refl; sym = ≅sym; trans = ≅trans } Bis : ∀(i : Size) → Setoid _ _ Setoid.Carrier (Bis i) = Lang ∞ Setoid._≈_ (Bis i) = _≅⟨ i ⟩≅_ Setoid.isEquivalence (Bis i) = ≅isEquivalence i import Relation.Binary.EqReasoning as EqR ≅trans′ : ∀ i (k l m : Lang ∞) ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m ≅trans′ i k l m p q = begin k ≈⟨ p ⟩ l ≈⟨ q ⟩ m ∎ where open EqR (Bis i) open import Data.Bool.Properties union-assoc : ∀{i} (k {l m} : Lang ∞) → ((k ∪ l) ∪ m ) ≅⟨ i ⟩≅ ( k ∪ (l ∪ m) ) ≅ν (union-assoc k) = ∨-assoc (ν k) _ _ ≅δ (union-assoc k) a = union-assoc (δ k a) union-comm : ∀{i} (l k : Lang ∞) → (l ∪ k ) ≅⟨ i ⟩≅ ( k ∪ l ) ≅ν (union-comm l k) = ∨-comm (ν l) _ ≅δ (union-comm l k) a = union-comm (δ l a) (δ k a) union-idem : ∀{i} (l : Lang ∞) → (l ∪ l ) ≅⟨ i ⟩≅ l ≅ν (union-idem l) = ∨-idem _ ≅δ (union-idem l) a = union-idem (δ l a) union-emptyl : ∀{i}{l : Lang ∞} → (∅ ∪ l ) ≅⟨ i ⟩≅ l ≅ν union-emptyl = refl ≅δ union-emptyl a = union-emptyl union-cong : ∀{i}{k k′ l l′ : Lang ∞} (p : k ≅⟨ i ⟩≅ k′)(q : l ≅⟨ i ⟩≅ l′ ) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l′ ) ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q) ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a) -- union-union-distr : ∀{i} (k {l m} : Lang ∞) → ( ( k ∪ l ) ∪ m ) ≅⟨ i ⟩≅ ( ( k ∪ m ) ∪ ( l ∪ m ) ) -- ≅ν (union-union-distr k) = {!!} -- ≅δ (union-union-distr k) a = {!!} withExample : (P : Bool → Set) (p : P true) (q : P false) → {A : Set} (g : A → Bool) (x : A) → P (g x) withExample P p q g x with g x ... | true = p ... | false = q rewriteExample : {A : Set} {P : A → Set} {x : A} (p : P x) {g : A → A} (e : g x ≡ x) → P (g x) rewriteExample p e rewrite e = p infixr 6 _∪_ infixr 7 _·_ infix 5 _≅⟨_⟩≅_ postulate concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m ) union-swap24 : {!!} union-swap24 = {!!} concat-union-distribr : ∀{i} (k {l m} : Lang ∞) → k · ( l ∪ m ) ≅⟨ i ⟩≅ ( k · l ) ∪ ( k · m ) ≅ν (concat-union-distribr k) = {!!} -- ∧-distribʳ-∨ (ν k) _ _ ≅δ (concat-union-distribr k) a with ν k ≅δ (concat-union-distribr k {l} {m}) a | true = begin δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a) -- ≈⟨ union-cong (concat-union-distribr (δ k a)) ⟩ ≈⟨ {!!} ⟩ (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a) ≈⟨ {!!} ⟩ (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a) ∎ where open EqR (Bis _) ≅δ (concat-union-distribr k) a | false = concat-union-distribr (δ k a) postulate concat-congl : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → l · m ≅⟨ i ⟩≅ k · m concat-congr : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → m · l ≅⟨ i ⟩≅ m · k concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m) concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅ concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅ concat-unitl : ∀{i} l → ε · l ≅⟨ i ⟩≅ l concat-unitr : ∀{i} l → l · ε ≅⟨ i ⟩≅ l star-empty : ∀{i} → ∅ * ≅⟨ i ⟩≅ ε star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l * ≅ν (star-concat-idem l) = refl ≅δ (star-concat-idem l) a = begin δ ((l *) · (l *)) a ≈⟨ union-cong (concat-assoc _) ≅refl ⟩ δ l a · (l * · l *) ∪ δ l a · l * ≈⟨ union-cong (concat-congr (star-concat-idem _)) ≅refl ⟩ δ l a · l * ∪ δ l a · l * ≈⟨ union-idem _ ⟩ δ (l *) a ∎ where open EqR (Bis _) star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l * ≅ν (star-idem l) = refl ≅δ (star-idem l) a = begin δ ((l *) *) a ≈⟨ concat-assoc (δ l a) ⟩ δ l a · (l *) · ((l *) *) ≈⟨ {!!} ⟩ δ l a · l * · l * ≈⟨ {!!} ⟩ δ l a · ((l *) *) ≈⟨ concat-congr (star-idem l) ⟩ δ l a · l * ∎ where open EqR (Bis _) postulate star-rec : ∀{i} (l : Lang ∞) → l * ≅⟨ i ⟩≅ ε ∪ (l · l *) star-from-rec : ∀{i} (k {l m} : Lang ∞) → ν k ≡ false → l ≅⟨ i ⟩≅ k · l ∪ m → l ≅⟨ i ⟩≅ k * · m ≅ν (star-from-rec k n p) with ≅ν p ... | b rewrite n = b ≅δ (star-from-rec k {l} {m} n p) a with ≅δ p a ... | q rewrite n = begin (δ l a) ≈⟨ q ⟩ δ k a · l ∪ δ m a ≈⟨ union-cong (concat-congr (star-from-rec k {l} {m} n p)) ≅refl ⟩ (δ k a · (k * · m) ∪ δ m a) ≈⟨ union-cong (≅sym (concat-assoc (δ k a))) ≅refl ⟩ (δ k a · (k *)) · m ∪ δ m a ∎ where open EqR (Bis _) open List record DA (S : Set) : Set where field ν : (s : S) → Bool δ : (s : S)(a : A) → S νs : ∀{i} (ss : List.List i S) → Bool νs ss = List.any ν ss δs : ∀{i} (ss : List.List i S) (a : A) → List.List i S δs ss a = List.map (λ s → δ s a) ss open Lang lang : ∀{i} {S} (da : DA S) (s : S) → Lang i Lang.ν (lang da s) = DA.ν da s Lang.δ (lang da s) a = lang da (DA.δ da s a) open import Data.Unit hiding ( _≟_ ) open DA ∅A : DA ⊤ ν ∅A s = false δ ∅A s a = s εA : DA Bool ν εA b = b δ εA b a = false open import Relation.Nullary.Decidable data 3States : Set where init acc err : 3States charA : (a : A) → DA 3States ν (charA a) init = false ν (charA a) acc = true ν (charA a) err = false δ (charA a) init x = if ⌊ a ≟ x ⌋ then acc else err δ (charA a) acc x = err δ (charA a) err x = err complA : ∀{S} (da : DA S) → DA S ν (complA da) s = not (ν da s) δ (complA da) s a = δ da s a open import Data.Product _⊕_ : ∀{S1 S2} (da1 : DA S1) (da2 : DA S2) → DA (S1 × S2) ν (da1 ⊕ da2) (s1 , s2) = ν da1 s1 ∨ ν da2 s2 δ (da1 ⊕ da2) (s1 , s2) a = δ da1 s1 a , δ da2 s2 a powA : ∀{S} (da : DA S) → DA (List ∞ S) ν (powA da) ss = νs da ss δ (powA da) ss a = δs da ss a open _≅⟨_⟩≅_ powA-nil : ∀{i S} (da : DA S) → lang (powA da) [] ≅⟨ i ⟩≅ ∅ ≅ν (powA-nil da) = refl ≅δ (powA-nil da) a = powA-nil da powA-cons : ∀{i S} (da : DA S) {s : S} {ss : List ∞ S} → lang (powA da) (s ∷ ss) ≅⟨ i ⟩≅ lang da s ∪ lang (powA da) ss ≅ν (powA-cons da) = refl ≅δ (powA-cons da) a = powA-cons da composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × List ∞ S2) ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ νs da2 ss2 δ (composeA da1 s2 da2) (s1 , ss2) a = δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a import Relation.Binary.EqReasoning as EqR composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) → lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss ≅ν (composeA-gen da1 da2 s1 s2 ss) = refl ≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1 ... | false = composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 ss a) ... | true = begin lang (composeA da1 s2 da2) (δ da1 s1 a , δ da2 s2 a ∷ δs da2 ss a) ≈⟨ composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 (s2 ∷ ss) a) ⟩ lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang (powA da2) (δs da2 (s2 ∷ ss) a) ≈⟨ {!!} ⟩ (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a)) ≈⟨ ≅sym {!!} ⟩ (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a) ∎ where open EqR (Bis _) postulate composeA-correct : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) s1 s2 → lang (composeA da1 s2 da2) (s1 , []) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 open import Data.Maybe acceptingInitial : ∀{S} (s0 : S) (da : DA S) → DA (Maybe S) ν (acceptingInitial s0 da) (just s) = ν da s δ (acceptingInitial s0 da) (just s) a = just (δ da s a) ν (acceptingInitial s0 da) nothing = true δ (acceptingInitial s0 da) nothing a = just (δ da s0 a) finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (List ∞ (Maybe S)) ν (finalToInitial da) ss = νs da ss δ (finalToInitial da) ss a = let ss′ = δs da ss a in if νs da ss then δ da nothing a ∷ ss′ else ss′ starA : ∀{S}(s0 : S)(da : DA S) → DA (List ∞(Maybe S)) starA s0 da = finalToInitial (acceptingInitial s0 da) postulate acceptingInitial-just : ∀{i S} (s0 : S) (da : DA S) {s : S} → lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) → lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0 starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→ lang (starA s0 da) ss ≅⟨ i ⟩≅ lang (powA (acceptingInitial s0 da)) ss · (lang da s0) * starA-correct : ∀{i S} (da : DA S) (s0 : S) → lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *