Require Import CoqTypesTheory.
Require Import Classical.
Section Simple.
Variable U : Type.
Variable A B C : Predicate U.
(* Prove that AuB \ C = A\C u B\C *)
Goal(A u B) \ C = (A \ C) u (B \ C).
apply ax_pred_ext.
intro.
split.
intro.
destruct H.
destruct H.
unfold In; unfold Sum.
left.
unfold In; unfold Minus.
split.
info assumption.
info assumption.
unfold In; unfold Sum.
right.
unfold In; unfold Minus.
split.
info assumption.
info assumption.
intro.
unfold In; unfold Minus.
split.
destruct H.
destruct H.
unfold In; unfold Sum.
left.
info assumption.
destruct H.
unfold In; unfold Sum.
right.
info assumption.
destruct H.
destruct H.
info assumption.
destruct H.
info assumption.
Save.
(* simple solution: unfold Sum; unfold Minus; info tauto,
;)
*)
(* Prove that A\(B\C) = (A\B) u (AnC) *)
Goal Minus A (Minus B C) = Sum (Minus A B) (Intersection A C).
apply ax_pred_ext.
intro.
split.
unfold Sum in *.
unfold Minus in *.
unfold Intersection in *.
intro.
unfold In.
apply lem_classic_disj_2.
intro.
split.
destruct H.
info assumption.
unfold not in *.
intro.
destruct H0.
split.
destruct H.
info assumption.
destruct H.
info classic_contr.
destruct H0.
split.
info assumption.
info assumption.
(* not the simplest way, but leads to the solution *)
unfold Minus in *.
unfold Sum in *. (* may-be they should be proposed automatically? *)
unfold Intersection in *.
intro.
split.
destruct H. (* right-click assumptions and select "Use" *)
destruct H. (* and so on... *)
info assumption.
destruct H.
info assumption.
unfold not in *.
intro.
destruct H.
destruct H.
destruct H1.
destruct H0.
info assumption.
destruct H0.
destruct H1.
destruct H.
info assumption.
Save Z1_2b.
End Simple.