Idris中已知index+1在列表范围内，如何简洁证明index合法？

Great question! Let's break this down into two parts: first proving the general logical implication, then applying it cleanly in your specific scenario.

Proving the General Implication #

First, let's ground this in the typical definition of InBounds (aligned with Idris' standard library logic)—it hinges on a number being less than the list's length:

data InBounds : Nat -> List a -> Type where
  MkInBounds : (prf : n < length xs) -> InBounds n xs

You want to prove: If index + 1 is in bounds for a list, then index must also be in bounds. Translating this to an Idris type gives us a reusable lemma:

inBoundsSuccImpliesPred : InBounds (S n) xs -> InBounds n xs

This proof relies on two basic properties of natural number ordering:

1. For any natural number n, n < S n (provided by the standard library's LT.ltSucc).
2. The transitivity of the < relation (LT.trans), which lets us chain inequalities.

Putting it all together:

inBoundsSuccImpliesPred : InBounds (S n) xs -> InBounds n xs
inBoundsSuccImpliesPred (MkInBounds prf) = 
  MkInBounds (LT.trans (LT.ltSucc n) prf)

Here, LT.ltSucc n gives us n < S n, and LT.trans chains that with our existing proof prf (which confirms S n < length xs) to get n < length xs—exactly what we need for InBounds n xs.

Clean Usage in Your Scenario #

Your specific case: you have prf : InBounds 1 list (proving the second element exists) and need to safely access the first element (requires InBounds 0 list). Here are the two most idiomatic, concise approaches:

1. Explicitly Call the Reusable Lemma #

Since 1 = S 0, our inBoundsSuccImpliesPred lemma directly converts the proof for index 1 to a proof for index 0. Use it inline when accessing the first element:

useFirstTwo : List a -> Maybe (a, a)
useFirstTwo list with (isInBounds 1 list)
  useFirstTwo list | Yes prf = 
    Just (index 0 list (inBoundsSuccImpliesPred prf), index 1 list prf)
  useFirstTwo list | No _ = Nothing

2. Auto-Fill Proofs with Hints #

If you'll need this implication often, mark the lemma as a %hint so Idris' auto-prover can automatically find and apply it. This lets you avoid explicit calls entirely:

%hint
inBoundsSuccImpliesPred : InBounds (S n) xs -> InBounds n xs
inBoundsSuccImpliesPred (MkInBounds prf) = 
  MkInBounds (LT.trans (LT.ltSucc n) prf)

useFirstTwo : List a -> Maybe (a, a)
useFirstTwo list with (isInBounds 1 list)
  useFirstTwo list | Yes prf = 
    Just (index 0 list auto, index 1 list prf)
  useFirstTwo list | No _ = Nothing

Idris will scan registered hints, recognize that inBoundsSuccImpliesPred can derive the required InBounds 0 list proof from prf, and fill it in automatically.

Note on the Standard Library #

If you're using Idris' built-in Data.List.InBounds, the core logic is identical—you just need to adapt the lemma to match the standard library's constructor (which still relies on n < length xs). The natural number ordering reasoning stays the same.

内容的提问来源于stack exchange，提问作者0xd34df00d