Best way to eliminate `match` with a proof?

Stream: new members

[C7X]

Hi!

I have a goal that has a match term in it, and a proof that one of the matched objects has a certain form. What is the recommended way to eliminate the match to simplify my goal? Is split the best option, or is there a better way?

To be more specific, my goal is ⊢ (match bad_root s, br_defined with | some x, x_1 => x) ≤ List.length s, but I have a proof (br_defined) that bad_root s is of the form some x. What should I do to change the goal into something like ⊢ (bad_root s).get ≤ List.length s, with no match term in it?

import Mathlib

set_option linter.unusedVariables false

def PrimitiveSeq : Type := List Nat

def bad_root : PrimitiveSeq → Option Nat
  | [] => none
  | 0 :: s => none
  | Nat.succ x :: s => (Nat.succ x :: s).idxOf x

lemma bad_root_leq_length : (s : PrimitiveSeq) → (br_defined : (bad_root s).isSome) → ((bad_root s).get br_defined ≤ s.length) := by {
  /- The bad root of a PrimitiveSeq, if defined, is less than or equal to its length. -/
  intro s br_defined
  unfold Option.get
  let br : ℕ := (bad_root s).get br_defined
  -- Here the goal has a match in it that I want to remove
}```

[Johannes Tantow]

import Mathlib

set_option linter.unusedVariables false

def PrimitiveSeq : Type := List Nat

def bad_root : PrimitiveSeq → Option Nat
  | [] => none
  | 0 :: s => none
  | Nat.succ x :: s => (Nat.succ x :: s).idxOf x

lemma bad_root_leq_length : (s : PrimitiveSeq) → (br_defined : (bad_root s).isSome) → ((bad_root s).get br_defined ≤ s.length) := by {
  /- The bad root of a PrimitiveSeq, if defined, is less than or equal to its length. -/
  intro s br_defined
  unfold Option.get
  let br : ℕ := (bad_root s).get br_defined
  -- Here the goal has a match in it that I want to remove
  cases s with
  | nil =>
    simp [bad_root] at br_defined
  | cons hd tl =>
    cases hd with
    | zero =>
      simp [bad_root] at br_defined
    | succ n =>
      grind [bad_root]
}

You can do a case distinction and eliminate the branches that are impossible based on the proof.

[Michiel Huttener]

If you are willing to change your proof structure a bit, you may write the following:

import Mathlib

def PrimitiveSeq : Type := List Nat

def bad_root : PrimitiveSeq → Option Nat
  | [] => none
  | 0 :: s => none
  | Nat.succ x :: s => (Nat.succ x :: s).idxOf x

lemma bad_root_leq_length (s : PrimitiveSeq) (br_defined : (bad_root s).isSome) :
    (bad_root s).get br_defined ≤ s.length := by
  dsimp [bad_root]
  split
  . contradiction
  . contradiction
  . apply List.idxOf_le_length

[C7X]

These seem to work alright, thank you both!