task18.v

Require Import Arith.
 
Definition Nat : Type :=
  forall A : Type, (A -> A) -> (A -> A).
 
Definition NatPlus(n m : Nat) : Nat :=
  fun (A:Type)(f:A->A)(x:A) => ((n A) f)(((m A) f) x).
 
Definition nat2Nat : nat -> Nat := nat_iter.
 
Definition Nat2nat(n : Nat) : nat := n _ S O.
 
Lemma NatPlus_plus :
  forall n m, Nat2nat (NatPlus (nat2Nat n) (nat2Nat m)) = n + m.
Proof.
  intros.
  unfold nat2Nat.
  unfold NatPlus.
  unfold Nat2nat.
  assert (nat_iter m S 0 = m).
  induction m.
  simpl.
  reflexivity.
  simpl.
  rewrite IHm.
  reflexivity.
  rewrite H.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

task19.v

Parameter A : Set.

Definition Eq : A -> A -> Prop :=
  fun (a b:A) => forall (P:A->Prop) , P a -> P b.

Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
  intros.
  apply (iff_to_and (Eq x y) (x = y)).
  split.
  intros.
  apply H.
  auto.
  intros.
  rewrite H.
  unfold Eq.
  auto.
Qed.

task21-1.v

Require Import Coq.Logic.Classical_Prop. 

Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
  unfold iff.
  intros.
  split.
  intros.
  destruct H.
  split.
  split.
  intros.
  apply H.
  split.
  intros.
  apply H2.
  intros.
  apply H1.
  intros.
  assert( (A -> B) /\ (B -> A) ).
  apply H0.
  apply H2.
  destruct H3.
  apply H3.
  apply H1.
  intros.
  destruct H1.
  assert( B \/ ~B ).
  apply classic.
  case H3.
  intros.
  assert C.
  apply H1.
  apply H4.
  assert ( (A->B)/\(B->A) ).
  apply H0.
  apply H5.
  destruct H6.
  apply H7.
  apply H4.
  intros.
  assert (~B -> ~C ).
  unfold not.
  intros.
  assert B.
  apply H2.
  apply H6.
  contradiction.
  assert (~C).
  apply H5.
  apply H4.
  assert ((~C) -> ~((A->B)/\(B->A))).
  unfold not.
  intros.
  assert C.
  apply H.
  apply H8.
  apply H7.
  apply H9.
  assert (~((A->B)/\(B->A))).
  apply H7.
  apply H6.
  unfold not in H8.
  assert ( A \/ ~A ).
  apply classic.
  case H9.
  auto.
  intros.
  apply False_ind.
  apply H8.
  split.
  intros.
  contradiction.
  intros.
  contradiction.
  intros.
  destruct H.
  split.
  intros.
  destruct H1.
  assert (B\/~B).
  apply classic.
  case H3.
  intros.
  assert A.
  apply H2.
  apply H4.
  assert ((B->C)/\(C->B)).
  apply H.
  apply H5.
  destruct H6.
  apply H6.
  apply H4.
  intros.
  assert (~B -> ~A).
  unfold not.
  intros.
  apply H5.
  apply H1.
  apply H6.
  assert (~A).
  apply H5.
  apply H4.
  assert ((~A) -> (~((B->C)/\(C->B)))).
  unfold not.
  intros.
  apply H7.
  apply H0.
  apply H8.
  assert (~((B->C)/\(C->B))).
  apply H7.
  apply H6.
  unfold not in H8.
  assert (C \/ ~C).
  apply classic.
  case H9.
  auto.
  intros.
  apply False_ind.
  apply H8.
  split.
  intros.
  contradiction.
  intros.
  contradiction.
  intros.
  split.
  intros.
  assert ((B->C)/\(C->B)).
  apply H.
  apply H2.
  destruct H3.
  apply H4.
  apply H1.
  intros.
  apply H0.
  split.
  auto.
  auto.
Qed.

task21-2.v

Require Import Coq.Logic.Classical_Prop.

Goal
  forall P Q R : Prop,
  (IF P then Q else R) ->
  exists b : bool,
  (if b then Q else R).
Proof.
  unfold IF_then_else.
  intros.
  assert( P \/ ~P ).
  apply classic.
  case H0.
  intros.
  exists true.
  case H.
  intros.
  apply H2.
  intros.
  assert (~P).
  apply H2.
  contradiction.
  intros.
  exists false.
  case H.
  intros.
  assert P.
  apply H2.
  contradiction.
  intros.
  apply H2.
Qed.

task21-3.v

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 (n:nat) => if excluded_middle_informative (P n) then true else false ).
  intros.
  assert( forall n:nat , (P n ) \/ ~(P n) ).
  intros.
  apply classic.
  destruct (H0 n).
  destruct excluded_middle_informative.
  unfold IF_then_else in H.
  case (H n).
  intros.
  destruct H2.
  apply H3.
  intros.
  destruct H2.
  contradiction.
  unfold IF_then_else in H.
  case (H n).
  intros.
  destruct H2.
  contradiction.
  intros.
  destruct H2.
  apply H3.
  destruct excluded_middle_informative.
  unfold IF_then_else in H.
  case (H n).
  intros.
  destruct H2.
  apply H3.
  intros.
  destruct H2.
  contradiction.
  case (H n).
  intros.
  destruct H2.
  contradiction.
  intros.
  destruct H2.
  apply H3.
Qed.