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

[pandaman]

In my real code, I have a few fixed parameters I want to exclude from the motive, but it seems the auto-generated .fun_cases treat all arguments as indices. I tried to create a custom .fun_cases, but I couldn't use it with the cases tactic. Is my lemma malformed somehow?

set_option autoImplicit false

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

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

#check pushNext.fun_cases -- gives `motive : Nat → Node → List Nat → Prop`

theorem pushNext.fun_cases' (param : Nat) (motive : Node → List Nat → Prop)
  (done : ∀ (stack : List Nat), motive Node.done stack)
  (epsilon_pos : ∀ (stack : List Nat) (next : Nat), next < param → motive (Node.epsilon next) stack)
  (epsilon_neg : ∀ (stack : List Nat) (next : Nat), ¬next < param → motive (Node.epsilon next) stack) :
  ∀ (n : Node) (stack : List Nat), motive n stack := by
  intro n stack
  match n with
  | .done => exact done stack
  | .epsilon next =>
    if lt : next < param then
      exact epsilon_pos stack next lt
    else
      exact epsilon_neg stack next lt

example (n : Node) (stack : List Nat) (h : ∀ i ∈ stack, i < 10) : ∀ i ∈ pushNext 10 n stack, i < 10 := by
  -- invalid number of targets #2, motive expects #0
  cases n, stack using pushNext.fun_cases' 10
  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

example (n : Node) (stack : List Nat) (h : ∀ i ∈ stack, i < 10) : ∀ i ∈ pushNext 10 n stack, i < 10 := by
  -- Need to manually revert
  revert n stack
  apply pushNext.fun_cases' 10
  -- Cannot introduce variables in `case done =>` due to "too many variable names provided"
  case done =>
    intro stack h i mem
    simp [pushNext] at mem
    exact h i mem
  case epsilon_pos =>
    intro stack next lt h i mem
    simp [pushNext, lt] at mem
    cases mem with
    | inl eq => simp [eq, lt]
    | inr mem => exact h i mem
  case epsilon_neg =>
    intro stack next nlt h i mem
    simp [pushNext, nlt] at mem
    exact h i mem

[pandaman]

Hmm. I could do this. The real example would have 5 parameters so it might look ugly, but it may work.

example (n : Node) (stack : List Nat) (h : ∀ i ∈ stack, i < 10) : ∀ i ∈ pushNext 10 n stack, i < 10 := by
  cases h : 10, n, stack using pushNext.fun_cases
  case case1 param =>
    -- h: 10 = param
    sorry
  case case2 param next lt =>
    sorry
  case case3 param next nlt =>
    sorry

[pandaman]

It couldn't type check in more involved cases like this :cry:

set_option autoImplicit false

structure Params where
  T : Type
  limit : Nat
  ofNat : Nat → T

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

def pushNext (params : Params) (n : Node) (stack : List (params.T × Nat)) : List (params.T × Nat) :=
  match n with
  | .done => stack
  | .epsilon next =>
    if next < params.limit then
      (params.ofNat next, next) :: stack
    else
      stack

#check pushNext.fun_cases -- gives `motive : Nat → Node → List Nat → Prop`

def P1 : Params := {
  T := Nat
  limit := 10
  ofNat := id
}

example (n : Node) (stack : List (Nat × Nat)) (h : ∀ p ∈ stack, p.2 < 10) : ∀ p ∈ pushNext P1 n stack, p.2 < 10 := by
  --tactic 'generalize' failed, result is not type correct
  -- ∀ (x : Params) (p : x.T × Nat), p ∈ pushNext x n stack → p.snd < 10
  cases h : P1, n, stack using pushNext.fun_cases
  case case1 param =>
    -- h: 10 = param
    sorry
  case case2 param next lt =>
    sorry
  case case3 param next nlt =>
    sorry

[pandaman]

We can make it work if we treat Params as a parameter, so it would be really great if we can make the following fun_cases' work with cases.

-- push params to parameter
theorem pushNext.fun_cases' (params : Params) (motive : Node → List (params.T × Nat) → Prop)
  (done : ∀ (stack : List (params.T × Nat)), motive Node.done stack)
  (epsilon_pos : ∀ (stack : List (params.T × Nat)) (next : Nat), next < params.limit → motive (Node.epsilon next) stack)
  (epsilon_neg : ∀ (stack : List (params.T × Nat)) (next : Nat), ¬next < params.limit → motive (Node.epsilon next) stack) :
  ∀ (n : Node) (stack : List (params.T × Nat)), motive n stack := by
  intro n stack
  match n with
  | .done => exact done stack
  | .epsilon next =>
    if lt : next < params.limit then
      exact epsilon_pos stack next lt
    else
      exact epsilon_neg stack next lt

example (n : Node) (stack : List (P1.T × Nat)) (h : ∀ p ∈ stack, p.2 < 10) : ∀ p ∈ pushNext P1 n stack, p.2 < 10 := by
  -- invalid number of targets #2, motive expects #0
  cases n, stack using pushNext.fun_cases' P1
  sorry

example (n : Node) (stack : List (P1.T × Nat)) (h : ∀ p ∈ stack, p.2 < 10) : ∀ p ∈ pushNext P1 n stack, p.2 < 10 := by
  -- Need to manually revert
  revert n stack
  apply pushNext.fun_cases' P1
  -- Cannot introduce variables in `case done =>` due to "too many variable names provided"
  case done =>
    intro stack h i mem
    simp [pushNext] at mem
    exact h i mem
  case epsilon_pos =>
    intro stack next lt h i mem
    simp [pushNext, lt] at mem
    cases mem with
    | inl eq =>
      simp [P1] at lt
      simp [eq, lt]
    | inr mem => exact h i mem
  case epsilon_neg =>
    intro stack next nlt h i mem
    simp [pushNext, nlt] at mem
    exact h i mem

[Robin Arnez]

induction seems to work in your original example, not sure what's wrong with cases. This seems like a bug though.

[Robin Arnez]

Actually, you need to make motive implicit and then cases works as well

[pandaman]

Actually, you need to make motive implicit and then cases works as well

Interesting, thanks!