Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i j : ℕ
eq : nfa.pushRegex next r = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
induction r generalizing nfa next with
| empty =>
  apply pushRegex.empty eq
  intro eq
  subst eq
  simp at h₂
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ h₁ h₂
  simp [this, NFA.Node.charStep, NFA.Node.εStep] at step
| epsilon | char c | classes r =>
  try apply pushRegex.epsilon eq
  try apply pushRegex.char eq
  try apply pushRegex.sparse eq
  intro eq
  subst eq
  simp at h₂
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ h₁ h₂
  simp [this, NFA.Node.charStep, NFA.Node.εStep] at step
  try exact .inl step
  try exact .inl (And.right step)
| group _ r ih =>
  apply pushRegex.group eq
  intro nfa' nfa'' nfa''' property _ _ eq₁ eq₂ eq₃ eq
  have get₂ (h : i < nfa''.val.nodes.size) : result.val[i] = nfa''.val[i] := by
    simp [eq, eq₃]
    rw [pushNode_get_lt _ h]
  have get₁ (h : i < nfa'.val.nodes.size) : result.val[i] = nfa'.val[i] := by
    rw [get₂ (Nat.lt_trans h nfa''.property)]
    rw [pushRegex_get_lt eq₂.symm _ h]
  cases Nat.eq_or_lt_of_le h₁ with
  | inl eq =>
    have : i < nfa'.val.nodes.size := eq ▸ nfa'.property
    rw [get₁ this] at step
    simp [eq₁, ←eq, Node.charStep, Node.εStep] at step
    exact .inl step
  | inr gt =>
    cases Nat.lt_or_ge i nfa''.val.nodes.size with
    | inl lt =>
      have : nfa'.val.nodes.size ≤ i := by
        simp [eq₁]
        exact gt
      have ih := ih eq₂.symm this lt (get₂ lt ▸ step)
      apply Or.inr
      cases ih with
      | inl eq =>
        rw [eq, eq₁]
        simp
      | inr ge => exact Nat.le_trans (Nat.le_of_lt nfa'.property) ge
    | inr ge =>
      simp [eq, eq₃] at h₂
      have : i = nfa''.val.nodes.size := Nat.eq_of_le_of_lt_succ ge h₂
      simp [this, eq, eq₃, Node.charStep, Node.εStep] at step
      exact .inr (Nat.le_trans (Nat.le_of_lt nfa'.property) (step ▸ ge_pushRegex_start eq₂.symm))
| alternate r₁ r₂ ih₁ ih₂ =>
  apply pushRegex.alternate eq
  intro nfa₁ start₁ nfa₂ start₂ _ nfa' property eq₁ eq₂ eq₃ eq₄ eq₅ eq
  have get₂ (h : i < nfa₂.val.nodes.size) :
    result.val[i] = nfa₂.val[i] := by
    simp [eq, eq₅]
    rw [pushNode_get_lt _ h]
  have get₁ (h : i < nfa₁.val.nodes.size) :
    result.val[i] = nfa₁.val[i] := by
    rw [get₂ (Nat.lt_trans h nfa₂.property)]
    rw [pushRegex_get_lt eq₃.symm _ h]
  cases Nat.lt_or_ge i nfa₁.val.nodes.size with
  | inl lt =>
    apply ih₁ eq₁.symm h₁ lt
    exact get₁ lt ▸ step
  | inr ge =>
    cases Nat.lt_or_ge i nfa₂.val.nodes.size with
    | inl lt =>
      have ih₂ := ih₂ eq₃.symm ge lt (get₂ lt ▸ step)
      simp at ih₂
      cases ih₂ with
      | inl eq => exact .inl eq
      | inr ge => exact .inr (Nat.le_trans (Nat.le_of_lt nfa₁.property) ge)
    | inr ge =>
      simp [eq, eq₅] at h₂
      have : i = nfa₂.val.nodes.size := Nat.eq_of_le_of_lt_succ ge h₂
      simp [this, eq, eq₅, NFA.Node.charStep, NFA.Node.εStep] at step
      apply Or.inr
      cases step with
      | inl eq =>
        simp [eq, eq₂]
        exact ge_pushRegex_start eq₁.symm
      | inr eq =>
        simp [eq, eq₄]
        exact Nat.le_trans (Nat.le_of_lt nfa₁.property) (ge_pushRegex_start eq₃.symm)
| concat r₁ r₂ ih₁ ih₂ =>
  apply pushRegex.concat eq
  intro nfa₂ nfa₁ property eq₂ eq₁ eq
  have get₂ (h : i < nfa₂.val.nodes.size) :
    result.val[i] = nfa₂.val[i] := by
    simp [eq]
    rw [pushRegex_get_lt eq₁.symm _ h]
  cases Nat.lt_or_ge i nfa₂.val.nodes.size with
  | inl lt =>
    apply ih₂ eq₂.symm h₁ lt
    exact get₂ lt ▸ step
  | inr ge =>
    simp [eq] at h₂ step
    have ih₁ := ih₁ eq₁.symm ge h₂ step
    apply Or.inr
    cases ih₁ with
    | inl eq =>
      simp [eq]
      exact ge_pushRegex_start eq₂.symm
    | inr ge => exact Nat.le_trans (Nat.le_of_lt nfa₂.property) ge
| star r ih =>
  apply pushRegex.star eq
  intro placeholder compiled patched nfa' isLt inBounds property
    eq₁ eq₂ eq₃ eq₄ eq
  cases Nat.lt_or_ge nfa.nodes.size i with
  | inl gt =>
    have lt : i < compiled.val.nodes.size := by
      simp [eq, eq₄, eq₃] at h₂
      exact h₂
    have : result.val[i] = compiled.val[i] := by
      simp [eq, eq₄, get_eq_nodes_get, eq₃]
      rw [Array.get_set_ne]
      simp
      exact Nat.ne_of_lt gt
    simp [this] at step
    have ih := ih eq₂.symm
    simp [eq₁] at ih
    have := ih gt lt step
    cases this with
    | inl eq => simp [eq]
    | inr ge => exact .inr (Nat.le_trans (Nat.le_succ _) ge)
  | inr le =>
    have : i = nfa.nodes.size := Nat.le_antisymm le h₁
    simp [this, eq, eq₄, get_eq_nodes_get, eq₃, NFA.Node.charStep, NFA.Node.εStep] at step
    cases step with
    | inl eq =>
      have := ge_pushRegex_start eq₂.symm
      simp [eq₁] at this
      exact .inr (Nat.le_trans (Nat.le_succ _) (eq ▸ this))
    | inr eq => exact .inl eq
Proof state after:
no goals