0

假设我有两个函数f，g并且我知道f = g. 是否有一种向前推理的“功能应用”策略，可以让我为他们共同领域f a = g a中的一些人添加上下文？a在这个人为的示例中，我可以使用assert (f a = g a)后跟f_equal. 但我想在更复杂的情况下做这样的事情；例如，

Lemma fapp : forall (A B : Type) (P Q : A -> B) (a : A), 
               (fun (a : A) => P a) = (fun (a : A) => Q a) -> 
               P a = Q a.
4

2 回答 2

1

我对 Coq 或其策略没有太多经验，但为什么不直接使用辅助定理呢？

Theorem fapp': forall (t0 t1: Type) (f0 f1: t0 -> t1),
  f0 = f1 -> forall (x0: t0), f0 x0 = f1 x0.
Proof.
intros.
rewrite H.
trivial.
Qed.

Lemma fapp : forall (A B : Type) (P Q : A -> B) (a : A), 
               (fun (a : A) => P a) = (fun (a : A) => Q a) -> 
               P a = Q a.
Proof.
intros.
apply fapp' with (x0 := a) in H.
trivial.
Qed.
于 2012-07-22T15:18:10.190 回答
1

鉴于您的描述和示例，我认为我无法正确推断出您遇到的一般问题。

如果您已经知道H : f = g，您可以将它用于rewrite H任何您想展示和的东西f，g或者只是elim H一次重写所有内容。你不需要assert辅助定理，如果你这样做，你显然需要类似assertor的东西pose proof。

如果该相等性隐藏在某些 eta 扩展下方，例如在您的示例中，请删除该层，然后按上述方法进行操作。以下是两种（多种）可能的方法：

intros A B P Q a H. assert (P = Q) as H0 by apply H. rewrite H0; reflexivity.

assert这通过设置相等性然后重写来解决您的示例证明。另一种可能性是定义 eta 减少助手（还没有找到预定义的）并使用它们。这将更加冗长，但可能适用于更复杂的情况。

如果你定义

Lemma eta_reduce : forall (A B : Type) (f : A -> B),
    (fun x => f x) = f.
  intros. reflexivity.
Defined.

Tactic Notation "eta" constr(f) "in" ident(H) :=
  pattern (fun x => f x) in H;
  rewrite -> eta_reduce in H.

您可以执行以下操作：

intros A B P Q a H. eta P in H. eta Q in H. rewrite H; reflexivity.

（这种表示法有点松散，可能会在错误的地方重写。不要依赖它，如果出现异常，请手动执行patternand 。）rewrite

于 2012-07-22T20:45:05.403 回答