リーンでパターンマッチングを行うときに仮定を伝播する方法

アイテムがソートされたリストの先頭よりも小さい場合、それはリストのメンバーではないことをリーンで証明しようとしています。

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がこれを正確に実行することがわかりました）が、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の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 := _

しかし、この場合、リーンはそれを不平を言います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暗黙的にすることでこれを回避することが実際に可能であるように思われるので、それらを一致させる必要はありませんが、それは少しハックなようです。