Extra argument from `cases` tactic

Stream: lean4

[Leni Aniva]

The Or.casesOn function takes 6 arguments:

#check Or.casesOn
Or.casesOn {a b : Prop} {motive : a ∨ b → Prop} (t : a ∨ b) (inl : ∀ (h : a), motive (_ : a ∨ b))
  (inr : ∀ (h : b), motive (_ : a ∨ b)) : motive t

namely a b motive t inl inr.

Consider the following proof of the commutativity of Or:

theorem or_comm: ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h; rename_i a
  apply Or.inr
  assumption
  apply Or.inl
  assumption

Printing out the value of or_comm shows that despite having two motives, there is an extra argument (Eq.refl h) being applied to the result of Or.casesOn:

fun p q h =>
  Or.casesOn (motive := fun t => h = t → q ∨ p) h (fun h_1 h_2 => Eq.symm h_2 ▸ Or.inr h_1)
    (fun h_1 h_2 => Eq.symm h_2 ▸ Or.inl h_1) (Eq.refl h)

Why does the cases tactic generate this extraneous Eq.refl h and why could it not be bundled into the inl and inr motives?

[Ruben Van de Velde]

I think you should generally not read too much into the exact terms generated by a tactic

[Joachim Breitner]

Why does the cases tactic generate this extraneous Eq.refl h and why could it not be bundled into the inl and inr motives?

This is an extra assumption where it keeps track of the relation between the original value (h) and the concrete value in the branch (inl a resp. inl b). Since these are props it’s not so useful and it hides them from you, but if you case split on value you sometimes care a lot about that equality. It’s what you get when you write match h : x with ….

[Leni Aniva]

Joachim Breitner said:

Why does the cases tactic generate this extraneous Eq.refl h and why could it not be bundled into the inl and inr motives?

This is an extra assumption where it keeps track of the relation between the original value (h) and the concrete value in the branch (inl a resp. inl b). Since these are props it’s not so useful and it hides them from you, but if you case split on value you sometimes care a lot about that equality. It’s what you get when you write match h : x with ….

is there a case where this would be visible? Why not bundle the Eq.refl term into the two branches of the motives? For example maybe we could have

fun p q h =>
  Or.casesOn (motive := fun t => h = t → q ∨ p) h (fun h_1 => Eq.symm (Eq.refl h) ▸ Or.inr h_1)
    (fun h_1 => Eq.symm (Eq.refl h)  ▸ Or.inl h_1)

[Leni Aniva]

I found this in the documentation of CasesOn.lean and this seems to be related to the remaining term?

/--
  Given a `casesOn` application `c` of the form
  ```
  casesOn As (fun is x => motive[i, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
  ```
  and an expression `e : B[is, major]`, construct the term
  ```
  casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining
  ```
  We use `kabstract` to abstract the `is` and `major` from `B[is, major]`.
-/
def CasesOnApp.addArg (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM CasesOnApp := do

[Joachim Breitner]

Does that typecheck? are you pondering a different type signature for casesOn here?

Probably it’s possible to hard-code that feature (providing that equality in the branches) in the casesOn eliminator, but if it can be done using a suitable motive instantiation by the tactic, then that’s more flexible, isn't it?

[Leni Aniva]

Joachim Breitner said:

Does that typecheck? are you pondering a different type signature for casesOn here?

Probably it’s possible to hard-code that feature (providing that equality in the branches) in the casesOn eliminator, but if it can be done using a suitable motive instantiation by the tactic, then that’s more flexible, isn't it?

I think the motive would have to be changed