How would you complete this inductive proof?

Stream: new members

[Agnishom Chattopadhyay]

I am trying to do some very simple constructions and proofs using the computability libraries.

How would you complete this proof?

import computability.regular_expressions
import computability.NFA
import computability.epsilon_NFA
import computability.language

universes u v

variables {α : Type u} {σ σ' : Type v}

def choice (M : ε_NFA α σ) (N : ε_NFA α σ') : (ε_NFA α (σ ⊕ σ')) :=
  { start := (sum.inl <$> M.start) ∪ (sum.inr <$> N.start),
    accept := (sum.inl <$> M.accept) ∪ (sum.inr <$> N.accept),
    step :=
      λ s a,
        match s with
        | sum.inl s := sum.inl <$> M.step s a
        | sum.inr s := sum.inr <$> N.step s a
        end }

lemma choice_eval (M : ε_NFA α σ) (N : ε_NFA α σ') (w : list α) (x : σ) :
  x ∈ M.eval w → sum.inl x ∈ (choice M N).eval w :=
begin
  intro h,
  induction w with a w ih generalizing x,
  { simp at h,
    simp,
    cases h,
    { apply ε_NFA.subset_ε_closure,
      fconstructor,
      finish,
    },
    {
      apply ε_NFA.ε_closure.step,
      { -- ?? refine (sum.inl h_s),

      }


    }
  },
end

Any hints would be helpful. I am not sure I understand how the ε_NFA.ε_closure inductive proposition can be used.

[Eric Rodriguez]

it'll probably make it easier if you make some API for your definition, such as what the eps_closure of choice is (for specific inl/inr)

[Eric Rodriguez]

also, I think people are generally more likely to help if there's no autogenerated names in your code; it makes it hard to read and use

[Agnishom Chattopadhyay]

thanks, that is probably a good idea.

[Joanna Choules]

You can avoid having to supply sum.inl h_s in a separate step by currying it into ε_NFA.ε_closure.step and applying that:

apply ε_NFA.ε_closure.step (sum.inl h_s),

That way you're just left with two metavariable-free subgoals.

The constructor family of tactics all seem to do broadly the same thing, which is to try and apply each constructor of the goal type in turn until they find one that works. In this case fconstructor applies or.inl, which happens to be the correct constructor to let you complete the proof – or.inr is also applicable here, though, and if fconstructor had applied that instead then you'd be stuck with an unprovable goal.

[Joanna Choules]

So I had a go at finishing this proof myself (very happy to share the code if you'd like) and one of the tricky parts is that the default induction principle for list sends you down the wrong path. ε_NFA.eval works with input strings that accumulate new elements at the end, whereas lists, definitionally speaking, accumulate from the front. The solution is to tell the induction tactic to use a different principle:

induction w using list.reverse_rec_on generalizing x,

[Agnishom Chattopadhyay]

Thanks, that is interesting to note. I have not looked back at this in a while, but I will try to give it another try soon.

By the way, how does Lean know that the lemma list.reverse_rec_on can be used as an induction principle?

[Joanna Choules]

It does it by inspecting the result type. From docs#tactic_doc.tactic.induction:

induction e using r allows the user to specify the principle of induction that should be used. Here r should be a theorem whose result type must be of the form C t, where C is a bound variable and t is a (possibly empty) sequence of bound variables