lean - 如何删除精益中的通用量词？

Question

我正在处理两个二元关系：g_o 和 pw_o，并且我在下面定义了 pw_o：

constants {A : Type} (g_o : A → A → Prop)

def pw_o (x y : A) : Prop := ∀ w : A, (g_o w x → g_o w y) ∧ (g_o y w → g_o x w)

我需要证明以下几点：

theorem prelim: ∀ x y z : A, g_o x y ∧ pw_o y z → g_o x z :=

我从这些策略开始：

begin

   intros,

   cases a with h1 h2,

end

我有这个：

x y z : A,
h1 : g_o x y,
h2 : pw_o y z
⊢ g_o x z

由于 pw_o 是用通用量词定义的，所以我想用 x 替换 w，那么我将有 (g_o xy → g_o xz) ∧ (g_o zx → g_o yx)。在用“cases”策略分离出第一个连词之后，我可以在第一个连词和 h1 上使用 modus ponens。

如何告诉 Lean 将 pw_o 定义中的 w 替换为 x 并将 pw_o 定义中的 x 和 y 分别替换为 y 和 z？

score 1 · Accepted Answer

全称量词的消除基本上只是应用，所以用 x 替换 w，只需将 x 应用于 pw_o y z 的实例 h2。

theorem prelim': ∀ x y z : A, g_o x y ∧ pw_o y z → g_o x z :=
begin

   intros,

   cases a with h1 h2,
   cases h2 x with h3 _,
   sorry
end

1 回答 1