如何在精益模式匹配时传播假设

Question

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

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

作为参考，is_sorted 的 Idris 定义在 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'。我发现实际上似乎可以通过使 is_sorted_many 的 x、y 和 ys 参数隐式化来解决这个问题，因此它们不必匹配上，但这似乎有点老套。

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 章。

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

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

如何在精益模式匹配时传播假设

How to propogate an assumption when pattern matching in Lean

dependent-type

idris

type-theory

lean