如何在精益模式匹配时提出假设

Question

我试图在Lean中证明，如果一项小于排序列表的头部，则它不是列表的成员。

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 _

在匹配列表尾部的t之后，作为(y::ys)，我预计假设Hs: is_sorted (h::t)会被传播，添加is_sorted (y::ys)作为假设(我发现Idris就是这样做的)，但在精益中似乎不是这样。此外，等式t = (y::ys)不会被传播，所以我不确定如何证明is_sorted (y::ys)。

当模式匹配传播这个假设时，我需要做什么额外的事情吗？

我将is_sorted定义为：

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)

上下文中作为_占位符的假设为：

α : 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

作为参考，Idris定义了is_sorted，它在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)

而Idris证明：

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)

我还尝试定义了更接近Idris定义的精益一号，将:向左移动以允许模式匹配：

 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 := _

但在这种情况下，Lean抱怨invalid pattern, 'x' already appeared in this pattern (也适用于h、y和ys)。例如，如果我将h重命名为h1，则它会报告given argument 'h1', expected argument 'h'。我发现实际上似乎可以通过将x、y和ys参数隐式地设置为is_sorted_many来解决这个问题，所以它们不需要匹配，但这似乎有点老生常谈。

Answer 1

在精益项目中，您需要明确表示不可访问的术语：

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 := _

有关不可访问术语的更多信息，请参阅https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf的第8.5章。

请注意，Lean会自动为隐式参数使用不可访问的术语：

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 := _