1

私はCoqが初めてです。これが私の問題です。私は声明を持っています：

H : forall x : term, ~ (exists y : term, P x y /\ ~ P y x)

私はそれが同等であると思います：

forall x y : term, (P x y /\ ~ P y x) -> false

しかし、仮説を変換するためにどの戦術を使用できますか?

4

3 に答える 3

1

not-exists を forall-not に変える戦術は知りませんが、いつでもそれassertを証明できます。(それが繰り返し必要な場合は、それを戦術定義または単純なLtac定理にまとめることができます[1]。)

これを証明する 3 つの方法を次に示します。(このトランスクリプトをコピーして CoqIDE または Emacs/ProofGeneral に貼り付け、コードをステップ実行するだけでよいはずです。)

not_ex_all_not[1] Libraryには補題が存在しますがCoq.Logic.Classical_Pred_Type、それをロードすると古典論理の公理が取り込まれます (ここでは必要ありません)。

(* dummy context to set up H of the correct type, for testing it out *)
Lemma SomeName (term : Type) (P : term -> term -> Prop) :
  (forall x : term, ~ (exists (y : term), P x y /\ ~ P y x)) ->
  True. (* dummy goal *)
Proof.
  intro H.
  (* end dummy context *)

(*これが長いバージョンで、いくつかの説明があります：*)

  (* this states the goal, result will be put into the context as H' *)
  assert (forall (x y : term), (P x y /\ ~ P y x) -> False) as H'.
    (* get rid of unneeded variables in context, get new args *)
    clear - H; intros x y Pxy.
    (* unfolding the not shows the computational structure of this *)
    unfold not at 1 in H.
    (* yay... (x, y, Pxy) will produce False via H *)
    (* specialize to x and apply... *)
    apply (H x).
    (* ...and provide the witness. *)
    exists y.  exact Pxy.
    (* done. *)

  (* let's do it again... *)
  clear H'.

(*単一のステートメントで行うこともできます。*)

  assert (forall x y, (P x y /\ ~ P y x) -> False) as H'
    by (clear -H; intros x y Pxy; apply (H x (ex_intro _ y Pxy))).

  (* and again... *)
  clear H'.

(*このような単純なものは、手書きで書くこともできます:*)

  pose proof (fun x y Pxy => H x (ex_intro _ y Pxy)) as H'; simpl in H'.

(*これで正しいタイプの H' が得られました。オプションで古い H を取り除きます:*)

  clear H; rename H' into H.
于 2014-02-11T01:08:06.443 に答える
0

使用できますunfold not at 1 in H。~ Pは の表記にすぎずnot P、not P = (P -> False)定義上は です。のat 1部分はunfold、 の最初の出現のみが必要であることを意味notし、 の部分は、仮説でin Hのみ必要であることを意味します。unfoldH

于 2014-02-08T14:17:13.723 に答える