Creating a case analysis lemma for a function

Stream: new members

[pandaman]

Hi! I'd like to create a lemma to abstract the case analysis of a (non-recursive) function so that I can easily perform the same case analysis in different results (ideally using the cases tactic). For recursive functions, we now have auto-generated .induct, so mimicking the signature allowed me to use the induction tactic with my own induction principle. However, I'm lost how to do something like this for a non-recursive function. Any advice are welcome!

set_option autoImplicit false

inductive Node where
  | done
  | epsilon (next : Nat)

def pushNext (n : Node) (stack : List Nat) : List Nat :=
  match n with
  | .done => stack
  | .epsilon next =>
    if next < 10 then
      next :: stack
    else
      stack

-- A case analysis lemma
theorem pushNext.cases (n : Node) (stack : List Nat)
  (motive : List Nat → Prop)
  (done : n = .done → motive stack)
  (epsilon_pos : ∀ (next : Nat), n = .epsilon next → next < 10 → motive (next :: stack))
  (epsilon_neg : ∀ (next : Nat), n = .epsilon next → ¬next < 10 → motive stack) :
  motive (pushNext n stack) := by
  unfold pushNext
  split
  next n => exact done rfl
  next n next =>
    split
    next lt => exact epsilon_pos next rfl lt
    next nlt => exact epsilon_neg next rfl nlt

example (n : Node) (stack : List Nat) (h : ∀ i ∈ stack, i < 10) : ∀ i ∈ pushNext n stack, i < 10 := by
  apply pushNext.cases (motive := fun stack => ∀ i ∈ stack, i < 10)
  -- Cannot introduce variables due to "too many variable names provided"
  case done /-h-/ => sorry
  case epsilon_pos /-next hn lt-/ => sorry
  case epsilon_neg /-next hn nlt-/ => sorry

example (n : Node) (stack : List Nat) (h : ∀ i ∈ stack, i < 10) : ∀ i ∈ pushNext n stack, i < 10 := by
  -- How can I use `cases` here?
  -- cases n, stack using pushNext.cases
  sorry

[Yaël Dillies]

You should do induction on n : Node, not on pushNext n stack

[pandaman]

That means I need to add if h : next < 10 to the epsilon case every time, which I want to avoid.

[pandaman]

Functional induction does case analysis (along the branching of a function) + induction. I want the former for non-recursive functions.

[Markus Himmel]

Are you aware of the fun_cases tactic, i.e., fun_cases pushNext n stack?

[Markus Himmel]

Your pushNext.cases lemma is quite similar to the autogenerated pushNext.fun_cases (which is created by the same machinery as the .induct lemmas for recursive functions). The fun_cases tactic applies that lemma for you (just like the fun_induction tactic applies the .induct lemma for you).

[pandaman]

I'll try it. Thank you!

[pandaman]

It worked perfectly. Thank you! I missed we have .fun_cases (I tried .cases and .casesOn and assumed it's not implemented :sweat_smile: )

[pandaman]

Now I have something like this

set_option autoImplicit false

inductive Node where
  | done
  | epsilon (next : Nat)

def pushNext (n : Node) (stack : List Nat) : List Nat :=
  match n with
  | .done => stack
  | .epsilon next =>
    if next < 10 then
      next :: stack
    else
      stack

-- Renaming branches
theorem pushNext.fun_cases' (motive : Node → List Nat → Prop)
  (done : ∀ (stack : List Nat), motive Node.done stack)
  (epsilon_pos : ∀ (stack : List Nat) (next : Nat), next < 10 → motive (Node.epsilon next) stack)
  (epsilon_neg : ∀ (stack : List Nat) (next : Nat), ¬next < 10 → motive (Node.epsilon next) stack) :
  ∀ (n : Node) (stack : List Nat), motive n stack :=
  pushNext.fun_cases motive done epsilon_pos epsilon_neg

example (n : Node) (stack : List Nat) (h : ∀ i ∈ stack, i < 10) : ∀ i ∈ pushNext n stack, i < 10 := by
  cases n, stack using pushNext.fun_cases'
  case done =>
    simpa [pushNext] using h
  case epsilon_pos next lt =>
    simpa [pushNext, lt] using h
  case epsilon_neg next nlt =>
    simpa [pushNext, nlt] using h