CoqEx21.v

Require Import Coq.Logic.Classical.
Lemma ABC_iff_iff :
  forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
  intros.
  split.
  intro.
  split.
  intro.
  split.
  intro.
  destruct H.
  apply H.
  split.
  intro.
  apply H1.
  intro.
  apply H0.
  intro.
  destruct H.
  apply H2 in H1.
  destruct H1.
  apply H1.
  apply H0.
  intro.
  destruct H.
  destruct (classic (A <-> B)).
  pose H2.
  apply H in i.
  destruct H2.
  apply H3.
  destruct H0.
  apply H4.
  apply i.
  assert (~C).
  intro.
  apply H1 in H3.
  apply H2.
  apply H3.
  assert (~B).
  intro.
  apply H3.
  destruct H0.
  apply H0.
  apply H4.
  destruct (classic A).
  apply H5.
  apply False_ind.
  apply H2.
  split. 
  intros.
  contradiction.
  intros.
  contradiction.
  intro.
  split.
  intros.
  destruct (classic A).
  destruct H.
  pose H1.
  apply H in a.
  destruct a.
  apply H3.
  destruct H0.
  apply H0.
  apply H1.
  assert (~B).
  intro.
  apply H1.
  destruct H0.
  apply H3.
  apply H2.
  assert (~(B<->C)).
  intro.
  destruct H.
  apply H1.
  apply H4.
  apply H3.
  destruct (classic C).
  apply H4.
  apply False_ind.
  apply H3.
  split.
  intro.
  contradiction.
  intro.
  contradiction.
  intro.
  split.
  intro.
  apply H in H1.
  destruct H1.
  apply H2.
  apply H0.
  intro.
  assert (B <-> C).
  split.
  refine (fun _ => H0).
  refine (fun _ => H1).
  destruct H.
  refine (H3 H2).
  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.
  destruct H.
  exists true.
  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.
  specialize (unique_choice (fun n b => IF is_true b then P n else ~P n)).
  intros.
  assert (forall  x : nat, exists ! y : bool, IF is_true y then P x else ~ P x).
  intros.
  destruct (classic (P x)).
  exists true.
  unfold unique.
  split.
  unfold IF_then_else.
  unfold is_true.
  left.
  split.
  reflexivity.
  apply H1.
  intros.
  unfold IF_then_else in  H2.
  destruct H2.
  destruct H2.
  unfold is_true in H2.
  rewrite H2.
  reflexivity.
  destruct H2.
  contradiction.
  exists false.
  unfold unique.
  split.
  unfold IF_then_else.
  right.
  split.
  intro.
  unfold is_true in H2.
  discriminate.
  apply H1.
  intros.
  unfold IF_then_else in H2.
  destruct H2.
  destruct H2.
  contradiction.
  destruct H2.
  destruct x'.
  apply False_ind.
  apply H2.
  unfold is_true.
  reflexivity.
  reflexivity.
  apply H0 in H1.
  destruct H1.
  exists x.
  intros.
  specialize (H1 n).
  remember (x n).
  destruct b.
  unfold IF_then_else in H1.
  destruct H1.
  destruct H1.
  specialize (H n).
  unfold IF_then_else in H.
  destruct H.
  destruct H.
  apply H3.
  destruct H.
  contradiction.
  destruct H1.
  apply False_ind.
  apply H1.
  unfold is_true.
  reflexivity.
  unfold IF_then_else in H1.
  destruct H1.
  destruct H1.
  unfold is_true in H1.
  discriminate.
  destruct H1.
  specialize (H n).
  destruct H.
  destruct H.
  contradiction.
  destruct H.
  apply H3.
  Qed.