将引理应用于绑定变量

Question

我可以证明以下引理：

lemma lem1: assumes "(a::real) ≤ b / c" and "c > 0" shows "a * c ≤ b"
using assms
using pos_le_divide_eq[of "c" "a" "b"] by auto

但是，如果我使用绑定变量，则证明不起作用。

lemma lem2: assumes "∀a b c. (a::real) ≤ b / c" and "∀c. c > 0" shows "∀a b c. a * c ≤ b"
using assms
using pos_le_divide_eq[of "c" "a" "b"]

将 ∀ 量词插入 pos_le_divide_eq 会更改数据类型，因此这是不可能的。我怎样才能解决lem2？

Answer 1

目前阅读lem2第一个和最后一个假设讲的是不同的c，即∀c. c > 0也可以写成∀d. d > 0，而在lem1 两个 c 指的是同一个变量。

因此，如果第一个公式中的 c 始终为正，则应该只有一个假设 ∀a b c. (a::real) ≤ b / c ∧ c > 0。或者，如果任何值预期为正，则第二个假设需要阐明 c 的类型，类似于第一个假设中指定的方式：∀c. (c :: real) > 0.

应用任一更改后 lem2 可以通过 auto 证明而无需 using pos_le_divide_eq[of "c" "a" "b"]。

Apply lemmas to bound variables