如何用超出范围的变量实例化假设

Question

我试图证明以下关于自然数上函数的引理

Lemma nat_funcs : 
forall (f : nat -> nat -> nat) (P : (nat -> nat) -> Prop), 
(forall n, P (fun m => (f n m))) -> P (fun m => f (m + 1) m).

当我继续并将变量引入上下文时，我最终得出了一个假设：

H : forall n, P (fun m => (f n m))

我的目标是：

P (fun m => f (m + 1) m)

我想应用H并用m+1实例化n，但问题是，m超出了范围，有办法做到这一点吗？

Answer 1

这不是真的。一个简单的反例是f x _ := x(常函数族(和P f := exists u, forall x, f x = u(检测常函数(。假设nat_funcs中的f n创建了一个常数函数，该函数通过P。在结论中，fun m => f (m + 1) m只是S，它不是一个常数函数。

Example nat_funcs_contra
: exists (f : nat -> nat -> nat) (P : (nat -> nat) -> Prop),
(forall n, P (f n)) / ~P (fun m => f (m + 1) m).
Proof.
exists (fun x _ => x), (fun f => exists u, forall x, f x = u).
split.
- intros n.
exists n.
reflexivity.
- intros [u no].
specialize (no u).
induction u as [ | u rec].
+ discriminate.
+ injection no.
apply rec.
Defined.

"需要"；脱离其范围的变量通常是某个地方出现严重错误的坏迹象。

(* Explicit negative proof *)
Theorem nat_funcs_no
: ~forall (f : nat -> nat -> nat) (P : (nat -> nat) -> Prop), 
(forall n, P (fun m => (f n m))) -> P (fun m => f (m + 1) m).
Proof.
destruct nat_funcs_contra as (f & P & hyp & prf).
intros no.
apply prf, no, hyp.
Qed.

也许你需要对所涉及的变量添加更多的约束/重新思考你试图用这个引理解决的问题。现在，这种说法过于笼统，不可能是真的。