Как доказать (p -> q) -> (~ p \ / q) в Coq

Question

Я пытаюсь доказать (p -> q) -> (~ p / q) в Coq, используя Аксиому:

Axiom tautology : forall P:Prop, P \/ ~ P.

Я пытаюсь преобразовать ~ p / q в ~ p / p, применяя p -> q. Так что сделайте что-то вроде этого:

Theorem Conversion: forall (p q: Prop),(p -> q) -> (~ p \/ q).
Proof.
  intros p q.
  intros p_implies_q.
  (do something here, change ~p\/q into ~p\/p)
  apply tautology...

Но я не знаю, как я могу это сделать. И если есть лучший способ сделать это, пожалуйста, скажите мне. Спасибо!.

Answer 1

Один из способов использования tautology - тактика destruct.Это позволяет свести к случаям, когда p истинно, а p неверно.

Axiom tautology : forall P:Prop, P \/ ~ P.

Theorem Conversion: forall (p q: Prop),(p -> q) -> (~ p \/ q).
Proof.
  intros p q.
  intros p_implies_q.
  destruct (tautology p) as [p_true | p_not_true].
  - (* prove ~p \/ q using p *)
  - (* prove ~p \/ q using ~p *)
Qed.

Можете ли вы увидеть, как доказать ~p \/ q в каждом из этих случаев?