Theorem: InterpretationPrefix (FOL/NV/Program/PEG.lean)

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
e : PE V_N V_T
xs ys : List V_T
n : ℕ
h1 : Interpretation V_N V_T R (e, xs) (n, some ys)
⊢ ys.IsPrefix xs
Tactic:
induction n using Nat.strongInductionOn generalizing e
State after:
case ind
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
n✝ : ℕ
a✝ : ∀ m < n✝, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
e : PE V_N V_T
h1 : Interpretation V_N V_T R (e, xs) (n✝, some ys)
⊢ ys.IsPrefix xs

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
n : ℕ
ih : ∀ m < n, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
e : PE V_N V_T
h1 : Interpretation V_N V_T R (e, xs) (n, some ys)
⊢ ys.IsPrefix xs
Tactic:
cases h1
State after:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs

case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, a✝ :: xs✝) (m, some [a✝]) → [a✝].IsPrefix (a✝ :: xs✝)
⊢ [a✝].IsPrefix (a✝ :: xs✝)

case nonTerminal
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A✝ : V_N
n✝ : ℕ
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (R A✝, xs) (n✝, some ys)
⊢ ys.IsPrefix xs

case seq_success
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e2✝, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)

case choice_1
V_N V_T : Type
R : V_N → PE V_N V_T
ys : List V_T
e1✝ e2✝ : PE V_N V_T
ys✝ : List V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e1✝, ys ++ ys✝) (n✝, some ys)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, ys ++ ys✝) (m, some ys) → ys.IsPrefix (ys ++ ys✝)
⊢ ys.IsPrefix (ys ++ ys✝)

case choice_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1✝ e2✝ : PE V_N V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs) (n1✝, none)
ih : ∀ m < n1✝ + n2✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (e2✝, xs) (n2✝, some ys)
⊢ ys.IsPrefix xs

case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)

case star_termination
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs

case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs

State before:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs

case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, a✝ :: xs✝) (m, some [a✝]) → [a✝].IsPrefix (a✝ :: xs✝)
⊢ [a✝].IsPrefix (a✝ :: xs✝)

case nonTerminal
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A✝ : V_N
n✝ : ℕ
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (R A✝, xs) (n✝, some ys)
⊢ ys.IsPrefix xs

case seq_success
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e2✝, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)

case choice_1
V_N V_T : Type
R : V_N → PE V_N V_T
ys : List V_T
e1✝ e2✝ : PE V_N V_T
ys✝ : List V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e1✝, ys ++ ys✝) (n✝, some ys)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, ys ++ ys✝) (m, some ys) → ys.IsPrefix (ys ++ ys✝)
⊢ ys.IsPrefix (ys ++ ys✝)

case choice_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1✝ e2✝ : PE V_N V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs) (n1✝, none)
ih : ∀ m < n1✝ + n2✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (e2✝, xs) (n2✝, some ys)
⊢ ys.IsPrefix xs

case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)

case star_termination
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs

case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs
Tactic:
any_goals
  first | apply EmptyStringPrefix | apply CharPrefix | apply PrefixAppend
State after:
case nonTerminal
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A✝ : V_N
n✝ : ℕ
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (R A✝, xs) (n✝, some ys)
⊢ ys.IsPrefix xs

case choice_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1✝ e2✝ : PE V_N V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs) (n1✝, none)
ih : ∀ m < n1✝ + n2✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (e2✝, xs) (n2✝, some ys)
⊢ ys.IsPrefix xs

State before:
case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs
Tactic:
first | apply EmptyStringPrefix | apply CharPrefix | apply PrefixAppend
State after:
no goals

State before:
case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs
Tactic:
apply EmptyStringPrefix
State after:
no goals

State before:
case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, a✝ :: xs✝) (m, some [a✝]) → [a✝].IsPrefix (a✝ :: xs✝)
⊢ [a✝].IsPrefix (a✝ :: xs✝)
Tactic:
apply CharPrefix
State after:
no goals

State before:
case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
Tactic:
apply PrefixAppend
State after:
no goals

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih : ∀ m < n + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
⊢ ys.IsPrefix xs
Tactic:
specialize ih n _ (R A)
State after:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih : ∀ m < n + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
⊢ n < n + 1

V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
ih : Interpretation V_N V_T R (R A, xs) (n, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih : ∀ m < n + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
⊢ n < n + 1
Tactic:
omega
State after:
no goals

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
ih : Interpretation V_N V_T R (R A, xs) (n, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs
Tactic:
exact ih ih_1
State after:
no goals

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih : ∀ m < n1 + n2 + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
⊢ ys.IsPrefix xs
Tactic:
specialize ih n2 _ e2
State after:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih : ∀ m < n1 + n2 + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
⊢ n2 < n1 + n2 + 1

V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
ih : Interpretation V_N V_T R (e2, xs) (n2, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih : ∀ m < n1 + n2 + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
⊢ n2 < n1 + n2 + 1
Tactic:
omega
State after:
no goals

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
ih : Interpretation V_N V_T R (e2, xs) (n2, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs
Tactic:
exact ih ih_2
State after:
no goals