0

と と の 2 つの関数がある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使用したり、一度にすべてを書き直したりすることができます。ヘルパー定理は必要ありません。必要な場合は、明らかにorのようなものが必要になります。rewrite Hfgelim Hassertassertpose proof

あなたの例のように、その等式が一部の eta-expansion の下に隠されている場合は、そのレイヤーを削除してから、上記のように進みます。これを行うための (多くの) 2 つの方法を次に示します。

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

assertこれは、等式を調べてから書き直すことで、例の証明を解決します。もう 1 つの可能性は、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 に答える