如何执行多个共享一个多变量普遍量化假设的存在消除？

Question

精益文档显示了以下两个仅包含一个变量的示例：

来自 Theorem Proving in Lean: Existential Quantifiers：

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⟩)

来自 Logic and Proof: Using the Existential Quantifier ***：

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 form a pair of even numbers".

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 ...)) 似乎不起作用。

Answer 1

这对我有用

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

如何执行多个共享一个多变量普遍量化假设的存在消除？

How to perform multiple exists-eliminations that all share a single multivariate universally-quantified hypothesis?

theorem-proving

lean