Working with homemade inductive type

Stream: new members

[Matt Kempster]

Hi all. I'm trying to prove the correctness of the definition of the union of two ε-NFAs, but I've gotten stuck. This should be an MWE, if you paste it in the middle of src/computability/epsilon_nfa.lean:

open sum

inductive union_step (M' : ε_NFA α σ') : option (σ ⊕ σ') → option α → set (option (σ ⊕ σ'))
| start (s : σ) (h : s ∈ M.start) : union_step none none (some (inl s))
| start' (s' : σ') (h : s' ∈ M'.start) : union_step none none (some (inr s'))
| step (s t : σ) (a : α) (h : M.step s a t) : union_step (some (inl s)) a (some (inl t))
| step' (s' t' : σ') (a : α) (h : M'.step s' a t') : union_step (some (inr s')) a (some (inr t'))

def union (M' : ε_NFA α σ') : ε_NFA α (option (σ ⊕ σ')) :=
{ step := union_step M M',
  start := {none},
  accept := {(some (inl s)) | s ∈ M.accept} ∪ {(some (inr s')) | s' ∈ M'.accept} }

lemma union_step_once (M' : ε_NFA α σ') (x : list α) :
  (M.union M').step none none = {(some (inl s)) | s ∈ M.start} ∪ {(some (inr s')) | s' ∈ M'.start}
  :=
begin
  rw union,
  simp,
  -- cases union_step, -- here?
  sorry,
end

Within union_step_once we end up with a state like this:

  α : Type u,
  σ σ' : Type v,
  M : ε_NFA α σ,
  M' : ε_NFA α σ',
  x : list α
  ⊢ M.union_step M' none none =
      {_x : option (σ ⊕ σ') | ∃ (s : σ), s ∈ M.start ∧ some (inl s) = _x} ∪
        {_x : option (σ ⊕ σ') | ∃ (s' : σ'), s' ∈ M'.start ∧ some (inr s') = _x}

The #xy is that I want to obtain the fact that M.union_step M' none none must either be (some (inl s)) or (some (inr s')) by the definition of union_step. I would have thought cases or something similar to it would have helped, but no matter what I do, I end up with an error like this:

cases tactic failed, it is not applicable to the given hypothesis
state:
α : Type u,
σ σ' : Type v,
M : ε_NFA α σ,
M' : ε_NFA α σ',
x : list α,
_x : ε_NFA α σ → ε_NFA α σ' → option (σ ⊕ σ') → option α → set (option (σ ⊕ σ'))
⊢ _x M M' none none =
    {_x : option (σ ⊕ σ') | ∃ (s : σ), s ∈ M.start ∧ some (inl s) = _x} ∪
      {_x : option (σ ⊕ σ') | ∃ (s' : σ'), s' ∈ M'.start ∧ some (inr s') = _x}

and I'm not sure why. The cases tactic is apparently not applicable, but the _x substitution you can see in the state looks reasonable. It looks even more reasonable when you do something like cases M.union_step M' none none, but the same error occurs.

How do I prove my #xy, and how do I work with this inductive type in general? In fact, have I even defined it correctly? Thanks :)

[Mario Carneiro]

By the way, #mwe means that you should make it work in a free standing file, which imports computability.epsilon_nfa and has the necessary namespace and variable declarations

[Mario Carneiro]

import computability.epsilon_NFA
open sum
universes u v
variables {α : Type u} {σ σ' : Type v} (M : ε_NFA α σ)

namespace ε_NFA

inductive union_step (M' : ε_NFA α σ') : option (σ ⊕ σ') → option α → set (option (σ ⊕ σ'))
| start (s : σ) (h : s ∈ M.start) : union_step none none (some (inl s))
| start' (s' : σ') (h : s' ∈ M'.start) : union_step none none (some (inr s'))
| step (s t : σ) (a : α) (h : M.step s a t) : union_step (some (inl s)) a (some (inl t))
| step' (s' t' : σ') (a : α) (h : M'.step s' a t') : union_step (some (inr s')) a (some (inr t'))

def union (M' : ε_NFA α σ') : ε_NFA α (option (σ ⊕ σ')) :=
{ step := union_step M M',
  start := {none},
  accept := {(some (inl s)) | s ∈ M.accept} ∪ {(some (inr s')) | s' ∈ M'.accept} }

lemma union_step_once (M' : ε_NFA α σ') (x : list α) :
  (M.union M').step none none = {(some (inl s)) | s ∈ M.start} ∪ {(some (inr s')) | s' ∈ M'.start}
  :=
begin
  rw union,
  simp,
  -- cases union_step, -- here?
  sorry,
end

end ε_NFA

[Mario Carneiro]

You are proving an equality of sets, so you need to apply extensionality and split into the two implication directions. In each case you then get an inductive hypothesis that you can destructure to get the two cases.

lemma union_step_once (M' : ε_NFA α σ') (x : list α) :
  (M.union M').step none none = {(some (inl s)) | s ∈ M.start} ∪ {(some (inr s')) | s' ∈ M'.start}
  :=
begin
  rw union,
  ext x, simp,
  split,
  { rintro (⟨s, h⟩ | _ | ⟨s, h⟩ | _),
    { sorry },
    { sorry } },
  { rintro (⟨s, h, rfl⟩ | ⟨s, h, rfl⟩),
    { sorry },
    { sorry } },
end

[Matt Kempster]

Mario Carneiro said:

You are proving an equality of sets, so you need to apply extensionality and split into the two implication directions. In each case you then get an inductive hypothesis that you can destructure to get the two cases.

Thank you for the reply! However I'm afraid this leaves me with more questions than it answers.

The original question still applies. All the sorries still involve union_step, which is the main point of my post; I don't know how to destructure it.

I spent a bunch of time trying to understand rcases the other day, and although I made some progress, I can't fully claim to understand the line rintro (⟨s, h⟩ | _ | ⟨s, h⟩ | _) here. I hesitate to ask you to explain this, though, because I think I partially understand it, and can generally fake it until I make it when it comes to rcases nowadays.

[Mario Carneiro]

The original question still applies. All the sorries still involve union_step, which is the main point of my post; I don't know how to destructure it.

The version of cases union_step in my code is rintro (⟨s, h⟩ | _ | ⟨s, h⟩ | _),, which you can also write intro h, cases h

[Mario Carneiro]

the point being that you don't case on the type union_step but rather a variable whose type is union_step, in this case h

[Mario Carneiro]

Matt Kempster said:

I spent a bunch of time trying to understand rcases the other day, and although I made some progress, I can't fully claim to understand the line rintro (⟨s, h⟩ | _ | ⟨s, h⟩ | _) here. I hesitate to ask you to explain this, though, because I think I partially understand it, and can generally fake it until I make it when it comes to rcases nowadays.

The rintro line can be expanded as I said to intro H, rcases H with ⟨s, h⟩ | _ | ⟨s, h⟩ | _. The contents of the pattern there correspond to the four constructors of the inductive type union_step. Two of them are impossible due to the parameters, but rcases requires that you put something there anyway so that's the _ cases. The other two need names for the arguments to the constructors, which we are calling s, h here. We are left with two goals for the two non-impossible cases, and s, h are new variables introduced in each of them.

You can do the same thing with plain cases, but the bindings are less structured so it looks like intro H, cases H with s h _ _ s h _ _ or something like that.

[Mario Carneiro]

Actually there is a typo, the two impossible cases are cases 3 and 4, not 2 and 4, so it should actually read rintro (⟨s, h⟩ | ⟨s, h⟩ | _ | _),

[Mario Carneiro]

by the way, I think your NFA has one more state than necessary:

inductive union_step (M' : ε_NFA α σ') : σ ⊕ σ' → option α → set (σ ⊕ σ')
| left (s t : σ) (a : α) (h : M.step s a t) : union_step (inl s) a (inl t)
| right (s' t' : σ') (a : α) (h : M'.step s' a t') : union_step (inr s') a (inr t')

def union (M' : ε_NFA α σ') : ε_NFA α (σ ⊕ σ') :=
{ step := union_step M M',
  start := sum.elim M.start M'.start,
  accept := sum.elim M.accept M'.accept }

[Matt Kempster]

Aha! With the typo explained, I think I am starting to understand this now.

However I still require some hand-holding :persevere: I'm not at all sure how to proceed here:

lemma union_step_once (M' : ε_NFA α σ') (x : list α) :
  (M.union M').step none none = {(some (inl s)) | s ∈ M.start} ∪ {(some (inr s')) | s' ∈ M'.start}
  :=
begin
  ext x, simp,
  split,
  { rintro (⟨s, h⟩ | ⟨s, h⟩ | _ | _),
    { sorry },
    { sorry } },
  { rintro (⟨s, h, rfl⟩ | ⟨s, h, rfl⟩),
    {
      /-
        α : Type u,
        σ σ' : Type v,
        M : ε_NFA α σ,
        M' : ε_NFA α σ',
        x : list α,
        s : σ,
        h : s ∈ M.start
        ⊢ some (inl s) ∈ (M.union M').step none none
      -/
      sorry },
    { sorry } },
end

Once again it is the union_step that is causing me pain. I have tried doing things like let S := (M.union M').step none none and cases S... but I'm hitting the same issue as before. This means I have some sort of conceptual misunderstanding.

Where do I begin on this side of the proof?

[Mario Carneiro]

what you want there is apply union_step.start,, although constructor will magically pick the right constructor to use

[Mario Carneiro]

In order to construct elements of an inductive type we use the constructors

[Mario Carneiro]

In this case we want to prove (M.union M').step none none (some (inl s)) and that's literally the statement of union_step.start, except it needs s ∈ M.start which we have in the context

[Mario Carneiro]

so exact union_step.start _ h works

[Matt Kempster]

Ahhh! This is all starting to make sense here. I don't have much else to add for now other than "it makes sense I think", so thank you!!