將參數應用於Coq中的等同函數

Question

假設我有兩個函數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. 

Answer 1

我想我不能正確地推斷出你有的一般問題，給出你的描述和例子。

如果你已經知道H : f = g，你可以不管你想展示一些關於f和g，或者只是elim H在一次改寫一切用它來rewrite H。你不需要assert輔助定理，如果你這樣做，你顯然需要類似assert或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. 

（即符號是有點鬆散的大炮，並在錯誤的地方可能改寫不要依賴如果出現異常，請手動執行pattern和rewrite。）

Answer 2

我沒有很多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.