2

我试图在精益中证明，如果一个项目小于排序列表的头部，它就不是列表的成员。

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列表的尾部 as(y::ys)之后，我预计该假设Hs: is_sorted (h::t)会被传播，并添加is_sorted (y::ys)为假设（我发现 Idris 正是这样做的），但在 Lean 中似乎并非如此。此外，没有传播相等性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)

伊德里斯证明：

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)

我还尝试将 Lean 定义为更接近 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隐式来解决此问题，因此不必匹配它们，但这似乎有点 hacky。

4

1 回答 1

3

在精益中，您需要明确说明无法访问的术语：

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 := _
于 2017-07-05T15:49:37.510 回答