module automaton-text where

-- open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Maybe
-- open import Data.Bool using ( Bool ; true ; false ; _∧_ )
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import logic
-- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )

open import automaton

open Automaton


lemma4 : {i n : ℕ } → i < n → i < suc n
lemma4 {0} {0} ()
lemma4 {0} {suc n} lt = s≤s z≤n
lemma4 {suc i} {0} ()
lemma4 {suc i} {suc n} (s≤s lt) =  s≤s (lemma4 lt)

lemma5 : {n : ℕ } → n < suc n
lemma5 {zero} = s≤s z≤n
lemma5 {suc n} =  s≤s lemma5

record accept-n { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (astart : Q ) (n : ℕ ) (s : {i : ℕ } → (i < n)  → Σ ) : Set where
   field
      r : (i : ℕ ) → i < suc n  → Q
      accept-1 : r 0 (s≤s z≤n)  ≡ astart
      accept-2 : (i : ℕ ) → (i<n : i < n ) → δ M (r i (lemma4 i<n)) (s i<n) ≡ r (suc i) (s≤s i<n)
      accept-3 : aend M (r n lemma5 ) ≡ true

get : { Σ : Set  } →  (x : List Σ ) → { i : ℕ } → i < length x  → Σ
get [] ()
get (h ∷ t) {0} (s≤s lt) = h
get (h ∷ t) {suc i} (s≤s lt) = get t lt

lemma7 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ) → (t : List Σ ) → accept M q (h ∷ t) ≡ true →  accept M (δ M q h) t ≡ true
lemma7 M q h t eq with accept M (δ M q h) t
lemma7 M q h t refl | true = refl
lemma7 M q h t () | false 

open accept-n

lemma→ :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept M q x ≡ true → accept-n M q (length x) (get x )
lemma→ {Q} {Σ} M q [] eq = record { r = λ i lt → get [ q ] {i} lt ; accept-1 = refl ; accept-2 = λ _ () ; accept-3 = eq  } 
lemma→ {Q} {Σ} M q (h ∷ t) eq with lemma→ M (δ M q h) t (lemma7 M q h t eq) 
... | an = record { r = seq ; accept-1 = refl ; accept-2 = acc2 ; accept-3 = accept-3 an } where
    seq : (i : ℕ) → i < suc (suc (foldr (λ _ → suc) 0 t)) → Q
    seq 0 lt = q
    seq (suc i) (s≤s lt) = r an i lt
    acc2 : (i : ℕ) (i<n : i < suc (foldr (λ _ → suc) 0 t)) → δ M (seq i (lemma4 i<n)) (get (h ∷ t) i<n) ≡ seq (suc i) (s≤s i<n)
    acc2 zero (s≤s z≤n) = begin
         δ M (seq zero (lemma4 (s≤s z≤n))) (get (h ∷ t) (s≤s z≤n))
       ≡⟨⟩
         δ M q h
       ≡⟨ sym ( accept-1 an)  ⟩
         seq 1 (s≤s (s≤s z≤n))
       ∎ where open ≡-Reasoning
    acc2 (suc i)  (s≤s lt) = accept-2 an i lt

an-1 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ ) → (t : List Σ )
    → accept-n M q (length (h ∷ t)) (get (h ∷ t) ) 
    → accept-n M (δ M q h) (length t) (get t )
an-1 {Q} {Σ} M q h t an = record {
      r = seq
    ; accept-1 = acc1
    ; accept-2 = acc2
    ; accept-3 = accept-3 an
   } where
       seq : (i : ℕ) → i < suc (length t) → Q
       seq i lt = r an (suc i) ( s≤s lt)
       acc1 : seq 0 (s≤s z≤n) ≡ δ M q h
       acc1 = begin
              seq 0 (s≤s z≤n)
           ≡⟨⟩
              r an 1 (s≤s (s≤s z≤n))
           ≡⟨ sym (accept-2 an 0 (s≤s z≤n)) ⟩
              δ M (r an 0 (s≤s z≤n)) h
           ≡⟨ cong (λ k → δ M k h) (accept-1 an)  ⟩
              δ M q h
           ∎ where open ≡-Reasoning
       acc2 : (i : ℕ) (i<n : i < length t) → δ M (seq i (lemma4 i<n)) (get t i<n) ≡ seq (suc i) (s≤s i<n)
       acc2 i lt = accept-2 an (suc i) (s≤s lt)

lemma← :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept-n M q (length x) (get x ) → accept M q x ≡ true 
lemma← {Q} {Σ} M q [] an with accept-1 an | accept-3 an
... | eq1 | eq3 = begin
         aend M q
       ≡⟨ cong ( λ k → aend M k ) (sym (accept-1 an))  ⟩
         aend M (r an 0 lemma5)
       ≡⟨ accept-3 an  ⟩
         true
       ∎ where open ≡-Reasoning
lemma← {Q} {Σ} M q (h ∷ t) an = lemma← M (δ M q h) t ( an-1 M q h t an )