coq_practice_21.v

(* 必要な公理を入れる*)
Require Import Coq.Logic.Classical.
Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
  intros.
  tauto.
Qed.

(* 必要な公理を入れる *)

Goal
  forall P Q R : Prop,
  (IF P then Q else R) ->
  exists b : bool,
  (if b then Q else R).
Proof.
  intros.
  destruct H.
    exists true.
    destruct H.
    apply H0.
  
    exists false.
    destruct H.
    apply H0.
Qed.

(* 必要な公理を入れる *)

Require Import Coq.Logic.ClassicalDescription.


Goal
  forall P Q R : nat -> Prop,
  (forall n, IF P n then Q n else R n) ->
  exists f : nat -> bool,
  (forall n, if f n then Q n else R n).
Proof.
  intros.
  exists (fun (p:nat) => if (excluded_middle_informative (P p)) then true else false ).
  intros.

  assert (IF P n then Q n else R n).
    apply H.

  destruct excluded_middle_informative.
    destruct H0.
      destruct H0.
      apply H1.
      destruct H0.
      contradiction.
    destruct H0.
      destruct H0.
      contradiction.
      destruct H0.
      apply H1.
Qed.