证明拼接两个递增列表的结果仍为递增列表

Let's start by restating the Increasing predicate definition you provided—this is our foundation for the proof:

mutual
  data Increasing : List a -> Type where
    SingleIncreasing : (x : a) -> Increasing [x]
    RecIncreasing : Ord a => (x : a) -> (rest : Increasing xs) -> (let prf = increasingIsNonEmpty rest in x <= head xs = True) -> Increasing (x :: xs)
  %name Increasing xsi, ysi, zsi

increasingIsNonEmpty : Increasing xs -> NonEmpty xs
increasingIsNonEmpty (SingleIncreasing x) = IsNonEmpty
increasingIsNonEmpty (RecIncreasing x rest _) = IsNonEmpty -- rest is non-empty, so x::rest is too

First, a critical note: to guarantee the concatenated list is increasing, we need an extra condition the last element of the first list must be less than or equal to the first element of the second list. Without this, you could have valid increasing lists like [1,3] and [2,4] that concatenate to [1,3,2,4]—which isn't increasing. Our theorem will include this necessary constraint.

Step 1: Add Helper Functions #

We need two small helpers to simplify the proof:

-- Get the last element of an increasing list (all such lists are non-empty by definition)
lastIncreasing : Increasing xs -> a
lastIncreasing (SingleIncreasing x) = x
lastIncreasing (RecIncreasing x rest _) = lastIncreasing rest

-- Lemma: The last element of x::xs equals the last element of xs (when xs is non-empty)
lastCons : (x : a) -> (xs : List a) -> NonEmpty xs -> last (x :: xs) = last xs
lastCons x (y :: ys) IsNonEmpty = Refl

Step 2: Prove the Concatenation Theorem #

We'll prove this by induction on the structure of the first Increasing list:

concatIncreasing : Ord a => (xsi : Increasing xs) -> (ysi : Increasing ys) -> (lastIncreasing xsi <= head ys = True) -> Increasing (xs ++ ys)
-- Case 1: First list is a single element
concatIncreasing (SingleIncreasing x) ysi prf =
  RecIncreasing x ysi prf
-- Case 2: First list is a recursive cons
concatIncreasing (RecIncreasing x rest_xsi prf_x) ysi prf_last =
  let
    -- Rewrite our premise using the lastCons lemma: last(x::rest) = last rest
    prf_rest = rewrite lastCons x rest (increasingIsNonEmpty rest_xsi) in prf_last
    -- Recursively prove rest ++ ys is increasing
    rest_ys_inc = concatIncreasing rest_xsi ysi prf_rest
  in
    -- Build the final proof for x :: (rest ++ ys)
    RecIncreasing x rest_ys_inc prf_x

Let's Break Down the Proof #

• Single element case: When the first list is just [x], concatenating gives x :: ys. We already know ys is increasing, and our premise confirms x <= head ys is true—so we can directly use RecIncreasing to construct the proof.
• Recursive case: For x :: rest, concatenating gives x :: (rest ++ ys). We first use lastCons to adjust our premise (since last(x::rest) is the same as last rest) to meet the recursive call's requirement. Then we recursively prove rest ++ ys is increasing, and finally use RecIncreasing again—reusing the original proof that x <= head rest holds, which is still valid because we're prepending x to an already-proven-increasing list.

This covers all possible cases, giving us a valid proof that the concatenated list maintains the Increasing property!

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