PROSAGA码农传奇-精益-如何在精益模式匹配时传播假设

<div class =“post-text”itemprop =“text”>
  <P>
    在精益中，您需要明确无法访问的术语：
  </p>
   <pre>
    <code>
      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 := _

</code>
  </pre>
  <P>
    有关无法访问的术语的更多信息，请参阅第8.5章
    <a href="https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf" rel="nofollow noreferrer">
      https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf
    </A>
    。
  </p>
  <P>
    请注意，Lean会自动为隐式参数使用不可访问的术语：
  </p>
   <pre>
    <code>
      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 := _

</code>
  </pre>
</DIV>