Leanでのパターンマッチングの仮定を推進する方法

Question

私は、項目がソートされたリストの先頭よりも小さい場合、それがリストのメンバーではないことをLeanで証明しようとしています。 tにマッチングした後、リストの末尾には、(y::ys)として、私は前提としてis_sorted (y::ys)を追加する、という仮定Hs: is_sorted (h::t)が伝播することが期待される（と私はイドリスはまさにこれを行い見つけた）

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)は伝播されないので、そのことを証明する方法がわかりませんis_sorted (y::ys)。

この仮説を伝播するためにパターンマッチングを行う必要がありますか？

Iのように並べ替え済み定義した：_プレースホルダであるよう

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の：

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) 

私も:を動かし、イドリスの定義に近いリーン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 := 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、およびy）。たとえば、 hをh1に変更した場合は、given argument 'h1', expected argument 'h'と表示されます。私は実際には、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を参照してください。暗黙の引数に自動的にアクセスできない用語を使用していますリーン

注：

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