1

精益文档显示了以下两个示例，其中只有一个变量：

来自精益中的定理证明：存在量词： 
variables (α : Type) (p q : α → Prop)
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
exists.elim h
  (assume w,
    assume hw : p w ∧ q w, -- this is ∀ w, p w ∧ q w
    show ∃ x, q x ∧ p x, from ⟨w, hw.right, hw.left⟩)
来自逻辑与证明：使用存在量词***： 
variables (U : Type) (P : U → Prop) (Q : Prop)
example (h1 : ∃ x, P x) (h2 : ∀ x, P x → Q) : Q :=
exists.elim h1
  (assume (y : U) (h : P y),
    have h3 : P y → Q, from h2 y,
    show Q, from h3 h)

在这两种情况下，普遍假设（h2在前一个例子中，hw在后一个例子中）只取决于一个变量。

现在假设我们得到（我解释原来的问题）：

variables (U : Type) (P R: U → Prop)(Q : Prop)
example (h1a : ∃ x, P x) (h1b : ∃ x, R x) (h2 : ∀ x y, P x → R y → Q) : Q := sorry

在h2中，想象P和R就像nat.is_even，并且Q就像“x,y 形成一对偶数”。

exists.elim我想，需要的内部推导如下：

  (assume (y z : U) (ha : P y) (hb : R z),
    have h3 : P y → R z → Q, from h2 y z,
    show Q, from h4 h1a h1b)

但我不确定如何将它与存在消除一起使用 - 因为基本上需要一次完成两个消除。exists.elim h1a (exists.elim h1b (assume ... show Q, from ...))似乎不起作用。

4

1 回答 1

3

这对我有用

example (h1a : ∃ x, P x) (h1b : ∃ x, R x) (h2 : ∀ x y, P x → R y → Q) : Q :=
exists.elim h1a (exists.elim h1b (assume (x : U) (hRx : R x) (y : U) (hPy : P y), _))

还有其他方法可以做到这一点。一是使用let

example (h1a : ∃ x, P x) (h1b : ∃ x, R x) (h2 : ∀ x y, P x → R y → Q) : Q :=
let ⟨x, hPx⟩ := h1a in
let ⟨y, hRy⟩ := h1b in
_

另一种方法是cases在战术模式下使用战术

example (h1a : ∃ x, P x) (h1b : ∃ x, R x) (h2 : ∀ x y, P x → R y → Q) : Q :=
begin
  cases h1a with x hPx,
  cases h1b with y hRy,
end
于 2020-02-28T23:57:00.607 回答