I'm trying to prove in Lean that if an item is less than the head of a sorted list, it's not a member of the list.
theorem not_in_greater {α: Type} [d: decidable_linear_order α] {x h: α} (t: list α) (Hs: is_sorted (h::t)) (Hlt: x < h) : x ∉ (h::t) :=
match t with
| [] := not_eq_not_in (ne_of_lt Hlt)
| (y::ys) :=
have x_neq_h: x ≠ h, from ne_of_lt Hlt,
have sorted_tail: is_sorted (y::ys), from _
After matching on t, the tail of the list, as (y::ys), I expected the assumption Hs: is_sorted (h::t) to be propagated, adding is_sorted (y::ys) as an assumption (and I've found Idris does exactly this), but this seems not to be the case in Lean. Moreover the equality t = (y::ys) isn't propagated, so I'm not sure how to prove that is_sorted (y::ys).
Is there something extra I need to do when pattern matching to propagate this assumption?
I've defined is_sorted as:
inductive is_sorted {α: Type} [d: decidable_linear_order α] : list α -> Type
| is_sorted_zero : is_sorted []
| is_sorted_one : Π (x: α), is_sorted [x]
| is_sorted_many : Π (x y: α) (ys: list α), x < y -> is_sorted (y::ys) -> is_sorted (x::y::ys)
The assumptions in the context as the _ placeholder are:
α : Type,
d : decidable_linear_order α,
x h : α,
t : list α,
Hs : is_sorted (h :: t),
Hlt : x < h,
_match : ∀ (_a : list α), x ∉ h :: _a,
y : α,
ys : list α,
x_neq_h : x ≠ h
For reference, the Idris definition of is_sorted, which produces the desired behaviour in Idris:
data IsSorted : {a: Type} -> (ltRel: (a -> a -> Type)) -> List a -> Type where
IsSortedZero : IsSorted {a=a} ltRel Nil
IsSortedOne : (x: a) -> IsSorted ltRel [x]
IsSortedMany : (x: a) -> (y: a) -> .IsSorted rel (y::ys) -> .(rel x y) -> IsSorted rel (x::y::ys)
And the Idris proof:
notInGreater : .{so: SensibleOrdering a eqRel ltRel} -> (x: a) -> (h: a) -> (t: List a) ->
.IsSorted ltRel (h::t) -> ltRel x h -> Not (Elem x (h::t))
notInGreater {so} x h [] _ xLtH = let xNeqH = (ltNe so) xLtH in notEqNotIn x h (xNeqH)
notInGreater {so} x h (y::ys) (IsSortedMany h y yYsSorted hLtY) xLtH = elemAbsurd
where
xNeqH : Not (x = h)
xNeqH = (ltNe so) xLtH
elemAbsurd : Elem x (h::y::ys) -> a
elemAbsurd xElemAll = case xElemAll of
Here {x=y} => absurd $ ((ltNe so) xLtH) Refl
There inRest => let notInRest = notInGreater {so} x y ys yYsSorted ((ltTrans so) xLtH hLtY)
in absurd (notInRest inRest)
I've also tried defining the Lean one closer to the Idris definition, moving the : left to allow pattern matching:
theorem not_in_greater2 {α: Type} [d: decidable_linear_order α] : Π (x h: α) (t: list α), is_sorted (h::t) -> x < h -> ¬ list.mem x (h::t)
| x h [] _ x_lt_h := not_eq_not_in (ne_of_lt x_lt_h)
| x h (y::ys) (is_sorted.is_sorted_many x h (y::ys) h_lt_y rest_sorted) x_lt_h := _
But in this case Lean complains that invalid pattern, 'x' already appeared in this pattern (also for h, y and ys). And if I e.g. rename h to h1, then it complains that given argument 'h1', expected argument 'h'. I've found it actually seems possible to work around this by making the x, y and ys arguments to is_sorted_many implicit, so they don't have to be matched upon, but that seems a bit hacky.
In Lean, you need to be explicit about inaccessible terms:
theorem not_in_greater2 {α: Type} [d: decidable_linear_order α] : Π (x h: α) (t: list α), is_sorted (h::t) → x < h → ¬ list.mem x (h::t)
| x h [] _ x_lt_h := _
| x h (y::ys) (is_sorted.is_sorted_many ._ ._ ._ h_lt_y rest_sorted) x_lt_h := _
For more information about inaccessible terms, see chapter 8.5 of https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf.
Note that Lean uses inaccessible terms automatically for implicit arguments:
inductive is_sorted {α : Type} [decidable_linear_order α] : list α → Type
| zero : is_sorted []
| one (x : α) : is_sorted [x]
| many {x y : α} {ys : list α} : x < y → is_sorted (y::ys) → is_sorted (x::y::ys)
theorem not_in_greater2 {α : Type} [decidable_linear_order α] : Π (x h : α) (t : list α), is_sorted (h::t) → x < h → ¬ list.mem x (h::t)
| x h [] _ x_lt_h := not_eq_not_in (ne_of_lt x_lt_h)
| x h (y::ys) (is_sorted.many h_lt_y rest_sorted) x_lt_h := _