5

[intros]、[apply]、[assump]、[destruct]、[left]、[right]、[split] というタクティクスでこの補題を証明しようとしましたが、失敗しました。誰か証明の仕方教えてくれませんか?

Lemma a : (P \/ Q) /\ ~P -> Q.
proof.


そして、一般的に、false->P、P/~P などの簡単な命題をどのように証明するのでしょうか?

4

4 に答える 4

5

あなたが見逃している戦術は矛盾です。これは、矛盾する仮説を含む目標を証明するために使用されます。矛盾を使用することは許可されていないため、適用しようとしているレンマはFalseの誘導原理であると思います。その後、否定された命題を適用し、仮定によって分岐を閉じることができます。インストラクターが要求したよりもうまくやることができ、リストされた戦術はどれも使用しないことに注意してください! 選言三段論法の証明用語は、比較的簡単に書くことができます。

Definition dis_syllogism (P Q : Prop) (H : (P ∨ Q) ∧ ¬P) : Q :=
  match H with
    | conj H₁ H₂ =>
      match H₁ with
      | or_introl H₃ => False_ind Q (H₂ H₃)
      | or_intror H₃ => H₃
      end
  end.
于 2012-10-08T02:00:41.617 に答える
3 
Section Example.

  (* Introduce some hypotheses.. *)
  Hypothesis P Q : Prop.

  Lemma a : (P \/ Q) /\ ~P -> Q.
    intros.
    inversion H.
    destruct H0.
      contradiction.
      assumption.
  Qed.

End Example.
于 2012-10-04T20:29:39.787 に答える
2

これらすべての簡単なことを証明するために、タクティックtauto、rtauto、intuitionおよびのファミリーがありfirstorderます。

それらはすべて、直観主義的な命題論理の完全な決定手順であるトートよりも強いと思います。

次に、intuition使用するいくつかのヒントと補題を入れることができ、firstorder は 1 次帰納法について推論できます。

もちろん、詳細はドキュメントに記載されていますが、これらはそのような目標で使用したい種類の戦術です.

于 2012-10-03T14:37:33.267 に答える
0

~Pそれは を意味し、仮説P->Falseを反転することで目的が達成されることを思い出してください(コンストラクタがないため)。したがって、本当に必要なのはandだけです。FalseFalseapplyinversion

Lemma a : forall (P Q:Prop), (P \/ Q) /\ ~P -> Q.
Proof.
  intros. 
  inversion H.
  inversion H0.
  - apply H1 in H2.  (* applying ~P on P gives H2: False *)
    inversion H2.
  - apply H2.
Qed.
于 2013-09-17T10:48:11.940 に答える