Don't repeat a proof branch with a single different name

Stream: general

[nrs]

  def getMatchLocsFromBack [DecidableEq α] [Inhabited α] : Array α -> Array α -> Array Nat
  | ara, arb =>
    let rec counter : Array α -> Array α -> Nat -> Array Nat
      | ara', arb', count =>
        if hh : ara'.isEmpty || arb'.isEmpty then #[]
        else
          if ara'.back! = arb'.back!
          then Array.singleton count ++ counter ara'.pop arb'.pop count.succ
          else counter ara' arb'.pop count.succ
    termination_by _ arb' _ => arb'.size
    decreasing_by
      all_goals
        simp_all [@List.length_pos_iff_ne_nil]
    counter ara arb 0

  theorem counterMonotonicityPart1 [DecidableEq α] [Inhabited α] {ara arb : Array α} {n : Nat} : getMatchLocsFromBack.counter ara arb n = Array.singleton n ++ (getMatchLocsFromBack.counter ara.pop arb.pop n.succ) ∨ getMatchLocsFromBack.counter ara arb n =  getMatchLocsFromBack.counter ara arb.pop n.succ := by
    rw [getMatchLocsFromBack.counter]
    split
    · simp_all
      rename_i h
      cases h
      · rename_i h
        rw [getMatchLocsFromBack.counter]
        match ara with
        | Array.mk artolist =>
          simp_all [getMatchLocsFromBack.counter]
      · rename_i h
        rw [getMatchLocsFromBack.counter]
        match arb with
        | Array.mk artolist =>
          simp_all [getMatchLocsFromBack.counter]
    · split
      all_goals
        simp_all

I'm working towards proving monotonicity wrt. argument size for the first argument of getMatchLocsFromBack, which is a function that returns an array that contains all the positions where two arrays match, beginning from the back.

In the counterMonotonicityPart1, the two branches resulting from cases h are nearly the same with the sole exception of ara and arb. How could I prove them both at the same time? (general style/writing tips are also welcome)

      cases h
      · rename_i h
        rw [getMatchLocsFromBack.counter]
        match ara with
        | Array.mk artolist =>
          simp_all [getMatchLocsFromBack.counter]
      · rename_i h
        rw [getMatchLocsFromBack.counter]
        match arb with
        | Array.mk artolist =>
          simp_all [getMatchLocsFromBack.counter]

[nrs]

Using rcases works for this purpose in this case:

  theorem counterMonotonicity1' [DecidableEq α] [Inhabited α] {ara arb : Array α} {n : Nat} : getMatchLocsFromBack.counter ara arb n = Array.singleton n ++ (getMatchLocsFromBack.counter ara.pop arb.pop n.succ) ∨ getMatchLocsFromBack.counter ara arb n =  getMatchLocsFromBack.counter ara arb.pop n.succ := by
  rw [getMatchLocsFromBack.counter]
  split
  · simp_all
    rename_i h
    cases h
    all_goals
      rename_i h
      rw [getMatchLocsFromBack.counter]
      rcases ara
      rcases arb
      simp_all [getMatchLocsFromBack.counter]
  · split
    all_goals
      simp_all

[Marcus Rossel]

Here's another shorter version:

import Mathlib

variable [DecidableEq α] [Inhabited α]

def getMatchLocsFromBack (ara arb : Array α) : Array Nat :=
  counter ara arb 0
where
  counter (ara arb count) : Array Nat :=
    if ara.isEmpty || arb.isEmpty then
      #[]
    else if ara.back! = arb.back! then
      #[count] ++ counter ara.pop arb.pop (count + 1)
    else
      counter ara arb.pop (count + 1)
  termination_by arb.size
  decreasing_by all_goals simp_all [List.length_pos_iff_ne_nil]

theorem counterMonotonicityPart1 {ara arb : Array α} :
    getMatchLocsFromBack.counter ara arb n = #[n] ++ getMatchLocsFromBack.counter ara.pop arb.pop (n + 1) ∨
    getMatchLocsFromBack.counter ara arb n = getMatchLocsFromBack.counter ara arb.pop (n + 1) := by
  rw [getMatchLocsFromBack.counter]
  split_ifs <;> simp_all
  cases ara; cases arb; cases ‹_ ∨ _› <;> simp_all [getMatchLocsFromBack.counter]

[nrs]

Marcus Rossel said:

Here's another shorter version:

import Mathlib

variable [DecidableEq α] [Inhabited α]

def getMatchLocsFromBack (ara arb : Array α) : Array Nat :=
  counter ara arb 0
where
  counter (ara arb count) : Array Nat :=
    if ara.isEmpty || arb.isEmpty then
      #[]
    else if ara.back! = arb.back! then
      #[count] ++ counter ara.pop arb.pop (count + 1)
    else
      counter ara arb.pop (count + 1)
  termination_by arb.size
  decreasing_by all_goals simp_all [List.length_pos_iff_ne_nil]

theorem counterMonotonicityPart1 {ara arb : Array α} :
    getMatchLocsFromBack.counter ara arb n = #[n] ++ getMatchLocsFromBack.counter ara.pop arb.pop (n + 1) ∨
    getMatchLocsFromBack.counter ara arb n = getMatchLocsFromBack.counter ara arb.pop (n + 1) := by
  rw [getMatchLocsFromBack.counter]
  split_ifs <;> simp_all
  cases ara; cases arb; cases ‹_ ∨ _› <;> simp_all [getMatchLocsFromBack.counter]

woah very cool! thank you very much, I've learned a lot from reading your version!!