Comment propager une hypothèse lors de l'appariement de formes dans Lean

Question

J'essaie de prouver dans Lean que si un élément est inférieur à la tête d'une liste triée, ce n'est pas un membre de la liste.

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 _ 

Après avoir établi le t, la queue de la liste, comme (y::ys), je me attendais à l'hypothèse Hs: is_sorted (h::t) à être reproduit, en ajoutant is_sorted (y::ys) comme hypothèse (et je l'ai trouvé Idris fait exactement cela), mais cela semble ne pas être le cas dans Lean. De plus l'égalité t = (y::ys) n'est pas propagée, donc je ne suis pas sûr de savoir comment le prouver is_sorted (y::ys).

Y a-t-il quelque chose de plus que je dois faire quand la correspondance de modèle pour propager cette hypothèse?

J'ai défini is_sorted comme:

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) 

Les hypothèses dans le contexte que l'espace réservé _ sont:

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

Pour référence, la définition de Idris is_sorted, qui produit le comportement souhaité dans 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) 

Et la preuve 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) 

J'ai aussi essayé de définir le Lean on se rapproche de la définition Idris, le déplacement du : gauche pour permettre correspondance de motif:

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

Mais dans ce cas Lean se plaint que invalid pattern, 'x' already appeared in this pattern (aussi h, y et ys). Et si par exemple je renommer h en h1, alors il se plaint que given argument 'h1', expected argument 'h'. J'ai trouvé qu'il semble effectivement possible de contourner ce problème en rendant les arguments , y et ys à is_sorted_many implicites, de sorte qu'ils n'ont pas à être appariés, mais cela semble un peu hacky.

Answer 1

Lean, vous devez être explicite sur les termes inaccessibles:

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

Pour plus d'informations sur les termes inaccessibles, voir le chapitre 8.5 de https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf.

Notez que Lean utilise des termes inaccessibles automatiquement pour les arguments implicites:

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