td1_sol

(* Tautologies and propositional calculus *)

Parameter A B C D : Prop.

(* A now exists in the context *)
Check A.

(* Let's move hypotheses around  *)

Lemma stupid : A -> (B -> C).
Proof.
intros a.
intros b.

Restart.

intros a b.
Undo.

Abort.

Lemma l1 : A -> B -> A.
Proof.
intros a b.
exact a. (* this time we are done  *)

(* or equivalently *)
Undo.
assumption.

(* or also *)
Undo.
trivial.

(* in any cases, we finish by saving the proof  *)
Qed.

(* to use an  implication :  "apply" *)
Lemma foo : (B -> A) -> A.
Proof.
intros a.
apply a.

Abort.

(* You turn *)

Lemma ex0 : A -> A.
  intros a; exact a.
Qed.

Lemma ex1 : forall A : Prop, A -> A.
intros A a; exact a.
Qed.

Lemma ex2 : (A -> B) -> (B -> C) -> A -> C.
  intros b c a; apply c; apply b; assumption.
Qed.

Lemma ex3 : (A -> B -> C) -> (B -> A) -> B -> C.
intros c a b; apply c; try apply a; apply b.
Qed.

(* With conjonctions *)

(* example *)

Lemma demo2 : (A/\B) -> A.
Proof.
intros h.
destruct h as [a b]. (* a proof of A/\B can be broken in two *)
exact a.

Restart. (* alternatively *)
intros [a b].
exact a.
Qed.

Lemma demo3 : A -> B -> A/\B.
Proof.
intros a b.
split. (* tactic to prove a conjonction *)
 trivial.
trivial.

Undo. (* or shorter *)
Undo.
Undo.
split; trivial. (* the trivial tactic is applied *)
                (* to both branches *)
Qed.

(* your turn *)

Lemma ex4: A /\ B <-> B /\ A.
split ; intros [x y]; split; trivial.
Qed.

(* Disjonctions *)

Lemma demo4 : A -> A\/B.
intros a.
left.
trivial.
Qed.

Lemma demo5 : B -> A\/B.
intros b.
right.
trivial.
Qed.

Lemma foo : A\/B -> C.
intros [a | b]. (* gives two subgoals *)

Abort.

(* Your turn *)

Lemma ex5 : A \/ B <-> B \/ A.
  split; intros [x|y]; try (left; assumption); right; assumption.
  Qed.

Lemma ex6 : A/\B -> A\/B.
intros [a b]; left; trivial.
Qed.

(* With negation *)
Print not.

Check (not A). (* written ~A   *)

Lemma ex7 : A -> ~~A.
  intros a na; apply na; exact a.
Qed.

Lemma ex8 : (A -> B) -> ~B -> ~A.
intros ab nb a; apply nb; apply ab; assumption.
Qed.

Lemma ex9 : ~~(A \/ ~A).
intros naa; apply naa; right; intros a.
apply naa; left; assumption.
Qed.

Lemma ex10 : (A \/ B) /\ C <-> (A /\ C) \/ (B /\ C).
split.
intros [[a|b] c].
 left; split; assumption.
 right; split; assumption.
intros [[a c]| [b c]]; split; try assumption.
left; assumption.
right; assumption.
Qed.

 Lemma ex11 : (A /\ B) \/ C <-> (A \/ C) /\ (B \/ C).
split.
intros [[a b] | c].
split; left; assumption.
split; right; assumption.

intros [[a|c][b|c']].
left; split; assumption.
right; assumption.
right; assumption.
right; assumption.
Qed.

(* Predicate Calculus *)

  (* We have types. *)

  Check 0.
  Check S.

  (* pretty-printing *)
  Check (S (S 0)).

  Check 0=0.
  Check 0=1.

  (* a predicate is typed as a function *)
  Parameter P : nat -> Prop.
  Parameter Q : nat -> Prop.

  (* forall quantifier *)

  Lemma foo : forall n, P n.
intros n.

Abort.


  Axiom PQ : forall n, P n -> Q n.

  Lemma foo: Q 0.
apply PQ.

Abort.

  (* Existential quantifier *)

Lemma foo : exists x, P x.
exists 0.

Abort.

Lemma foo : (exists x, P x) -> A.
  intros ep.
destruct ep as [x p].
(* you can think of a proof of exists x, P x as composed *)
(* by x and the proof of P x   *)

Undo.
Undo.
intros [x p].

Abort.

(* you *)
Lemma q1 : (P 3) -> exists x, Q x.
  intros p; exists 3.
  apply PQ.
assumption.
Qed.

Lemma q2 : (forall x, ~P x) -> ~(exists x, P x).
  intros np [x p]; apply np with x.
  assumption.
Qed.

Lemma q3 : ~(exists x, P x) -> forall x, ~P x.
intros np x p.
apply np.
exists x; assumption.
Qed.