Possible to eliminate impossible cases? without proofs?

Stream: new members

[aron]

I have defined an inductive type BoundedList t (min : Nat) (max : Nat) whose constructors should make it impossible for min to ever be larger than max.

When I match on a BoundedList t 0 2 Lean can indeed eliminate a lot of patterns as impossible, where the matched pattern would result in a straightforward type contradiction. But it can't seem to figure out a slightly subtler invariant of my type: that there would be no way to construct a value in whose type min > max.

Is there any way to tell Lean that those patterns are impossible? Ideally without having to construct a proof for it?

(the commented out patterns are where Lean has correctly eliminated those patterns as impossible)

set_option linter.unusedVariables false

inductive BoundedList (t : Type u) : (min : Nat) → (max : Nat) → Type u where
  | nil : BoundedList t 0 0
  | cons {min max : Nat} : (item : t) → BoundedList t min max → BoundedList t (.succ min) (.succ max)
  /-- Raises the upper bound by one. --/
  | raise {min max : Nat} : BoundedList t min max → BoundedList t min (.succ max)
  /-- Lowers the lower bound by one. --/
  | lower {min max : Nat} : BoundedList t (.succ min) (.succ max) → BoundedList t min (.succ max)


example : BoundedList t 0 2 → Unit
  -- | .nil => ()
  -- | .cons _ _ => ()
  | .raise l =>
    match h : l with
    -- | .nil => ()
    -- | .cons _ _ => ()
    | .raise .nil => ()
    | .lower l' =>
      match h' : l' with
      -- | .nil => ()
      | .cons _ .nil => ()
      | .raise l'' => () -- this should be impossible – there's no way to make a BL with a min bound that's higher than its max bound
      | .lower l'' => () -- this should be impossible

  | .lower l =>
    match h : l with
    -- | .nil => ()
    | .cons _ l' =>
      match h' : l' with
      -- | .nil => ()
      -- | .cons _ _ => ()
      | .raise .nil => ()
      | .lower l'' =>
        match h'' : l'' with
        -- | .nil => ()
        | .cons _ .nil => ()
        | .raise l''' => () -- this should be impossible
        | .lower l''' => () -- this should be impossible

    | .raise l' =>
      match h' : l' with
      -- | .nil => ()
      | .cons _ .nil => ()
      | .raise l'' => () -- this should be impossible
      | .lower l'' => () -- this should be impossible

    | .lower l' =>
      match h' : l' with
      -- | .nil => ()
      | .cons _ l'' =>
        match h'' : l'' with
        -- | .nil => ()
        | .cons _ .nil => ()
        | .raise l''' => () -- this should be impossible
        | .lower l''' => () -- this should be impossible

      | .raise l'' => () -- this should be impossible
      | .lower l'' => () -- this should be impossible

[Robin Arnez]

I have been able to do this:

theorem BoundedList.le {t : Type u} {min max : Nat} (x : BoundedList t min max) : min ≤ max := by
  induction x with
  | nil => exact Nat.le_refl _
  | cons _ l ih => exact Nat.succ_le_succ ih
  | raise _ ih => exact Nat.le_succ_of_le ih
  | lower _ ih => exact Nat.le_of_succ_le ih

example (x : BoundedList t 0 2) : Unit :=
  have : BoundedList t 2 1 → False := (by decide) ∘ BoundedList.le
  have this' : BoundedList t 3 2 → False := (by decide) ∘ BoundedList.le
  match x with
  | .raise l =>
    match l with
    | .raise .nil => ()
    | .lower l' =>
      match l', this with
      | .cons _ .nil, _ => ()
  | .lower l =>
    match l with
    | .cons _ l' =>
      match l' with
      | .raise .nil => ()
      | .lower l'' =>
        match l'', this with
        | .cons _ .nil, _ => ()
    | .raise l' =>
      match l', this with
      | .cons _ .nil, _ => ()
    | .lower l' =>
      match l', this, this' with
      | .cons _ l'', _, _ =>
        match l'', this with
        | .cons _ .nil, _ => ()

The trick is to give match more helpers to work with.