Как выполнить множественные исключения-исключения, которые все разделяют одну многомерную универсально-количественную гипотезу? - PullRequest
Новая
       45

Как выполнить множественные исключения-исключения, которые все разделяют одну многомерную универсально-количественную гипотезу?

0 голосов
/ 28 февраля 2020

Документация Lean показывает следующие два примера только с одной переменной:

из Доказательство теоремы в Lean: экзистенциальные квантификаторы : 
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⟩)
из Logi c и Proof: Using экзистенциальный квантификатор ***: 
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 нуждается, я полагаю, будет go вроде: 

  (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 ...)) не работает, кажется.

1 Ответ

2 голосов
/ 29 февраля 2020

Это работает для меня 

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 tacti c в режиме tacti c 

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
...