Coq演習

21.v

Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
Require Import Classical. 
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 P Q R H.
destruct H.
+ exists true; tauto.
+ exists false; tauto.
Qed.

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 P Q R H.
Require Import Coq.Logic.ClassicalDescription.
exists (fun n => if excluded_middle_informative (P n) then true else false).
intro n.
destruct (H n);destruct (excluded_middle_informative (P n));tauto.
Qed.