solson

foo

solson

lemma drop_length_eq {α : Type} {n : ℕ} {xs : list α} :
    length (drop n xs) = length xs - n :=
begin
    induction n generalizing xs,
    case nat.zero { refl },
    case nat.succ n' ih_n {
        cases xs,
        case nil { rewrite [drop, length, nat.zero_sub] },
        case cons x' xs' { rewrite [drop, ih_n, length, nat.succ_sub_succ] },
    },

solson

theorem alt_is_regular (L1 L2 : lang α) :
    regular L1 → regular L2 → regular (L1 ∪ L2) :=
assume ⟨r1, h1⟩ ⟨r2, h2⟩, exists.intro (regex.alt r1 r2) (λ w, by {
    rewrite [
        ←mem_lang_of_eq_mem, regex.lang_of, dset.mem_distrib_union,
        dset.mem_distrib_union, h1, h2, mem_lang_of_eq_mem,
        mem_lang_of_eq_mem
    ],
})

solson

@decidable.is_false
  (@Exists.{1}
     (fin
        (nat.succ
           (nat.succ
              (nat.succ
                 (nat.succ
                    (nat.succ
                       (nat.succ
                          (nat.succ

solson

λ (p : ?M_1 → Prop) [_inst_1 : Π (a : ?M_1), decidable (p a)] (l : list ?M_1),
  pprod.rec
    (λ
     (fst :
       decidable
         (∃ (x : ?M_1)
            (H :
              pprod.rec
                (λ (fst : ?M_1 → Prop)
                 (snd :

solson

λ (L1 L2 : list ?M_1 → bool) (w : list ?M_1),
  decidable.rec
    (λ
     (a :
       (∃ (i : ℕ)
          (H :
            pprod.rec
              (λ (fst : ℕ → Prop)
               (snd :
                 list.rec punit (λ (a : ℕ) (a : list ℕ) (ih_1 : Type), pprod (pprod (ℕ → Prop) ih_1) punit)

solson

def concat' (L1 L2 : lang α) : lang α :=
    λ w, ∃ i ∈ range (length w + 1), take i w ∈ L1 ∧ drop i w ∈ L2

solson

def concat (L1 L2 : lang α) : lang α :=
    λ w, any (range (length w + 1)) (λ i, take i w ∈ L1 ∧ drop i w ∈ L2)
    
def concat' (L1 L2 : lang α) : lang α :=
    λ w, ∃ i ∈ range (length w + 1), take i w ∈ L1 ∧ drop i w ∈ L2
    
def concat'''' (L1 L2 : lang α) : lang α :=
    λ w, ∃ i < length w + 1, take i w ∈ L1 ∧ drop i w ∈ L2

solson

lemma bor_assoc (a b c : bool) : a || b || c = a || (b || c) :=
    by cases a; simp

lemma any_cons {α : Type} (p : α → bool) (x : α) (xs : list α) :
    any (x :: xs) p = p x || any xs p :=
begin
    unfold any,
    unfold foldr,
end

solson

instance decidable_ex_lt (p : ℕ → Prop) [decidable_pred p] : ∀ (n : ℕ), decidable (∃ x < n, p x)
| 0     := is_false $ assume ⟨x, h_lt, _⟩, nat.not_lt_zero x h_lt
| (n+1) :=
    if h_pn : p n
    then is_true ⟨n, nat.lt_succ_self n, h_pn⟩
    else match decidable_ex_lt n with
    | is_true h :=
        is_true $ let ⟨x, h_lt, hp⟩ := h in ⟨x, nat.lt_succ_of_lt h_lt, hp⟩
    | is_false h_not := is_false $ assume ⟨x, h_lt, h_px⟩,
        if h_eq : x = n