Require Import Arith.
Require Import ZArith.

Lemma simple: forall a b: Prop, a /\ b -> a.
(*
  intro. intro. intro. elim H. intros. (*exact H0.*) trivial.
*)
  tauto.
Qed.
Print simple.

Check 0.
Check true.
Check nat.
Check Set.
Check Type.
Check bool.
Check Prop.
Check (fun (n: nat) => n + 1).
Check (nat -> nat).

Inductive tree: Set :=
  | Leaf: tree
  | Node: tree -> tree -> tree.

Check tree_ind.
Print nat.
Check nat_ind.
Print bool.
Print Z.
Print positive.
Print and.
Print and_ind.
Print simple.
Print or.
Print True.
Print False.
Print False_ind.
Lemma inconsistent:
  forall p q: Prop, ~p -> p -> q.
(*
  intros. apply (False_ind q). exact (H H0).
*)
  intros. exact (False_ind q (H H0)).
Qed.

Print eq.
Print eq_ind.
Print Acc.

(** Exercises *)
Lemma ex_1_1: forall a b c: Prop, a /\ (b /\ c) -> (a /\ b) /\ c.
Proof.
  intros.
  elim H. intros. elim H1. intros.
  clear H H1. 
  split.
  split.
  trivial.
  trivial.
  trivial.
Qed.

Lemma ex_1_1_quick: forall a b c: Prop, a /\ (b /\ c) -> (a /\ b) /\ c.
Proof.
  intros.
  elim H. intros. elim H1. intros.
  clear H H1. 
  split; trivial.
  split; trivial.
Qed.
Lemma ex_1_3: forall a: Prop, ~~~a -> ~a.
  intros. intro. apply H. intro. apply H1. trivial.
Qed.
Print not.
(* Require Import Classical. *)
(*Lemma toto: forall a, ~~a -> a.
  tauto.*)
Print ex.
Lemma ex_1_5: forall a: Prop, ~~( a \/ ~a ).
  intros.
  intro.
  apply H.
  right.
  intro.
  apply H.
  left.
  trivial.
Qed.

(** Exercise nr. 2 *)
Fixpoint sum (n: nat): nat :=
  match n with
    | O   => O
    | S p => n + sum p
  end.
Print Init.Nat.add.
Lemma add_comm: forall n m, n + m = m + n.
  induction n. intros. simpl. induction m. simpl. trivial.
  simpl. rewrite <- IHm. trivial.
  simpl. induction m. simpl. rewrite (IHn O). simpl. trivial.
  simpl. rewrite <- IHm. rewrite (IHn (S m)). simpl. rewrite (IHn m).
  reflexivity.
Qed.
Print add_comm.
Check plus_comm.
Check plus_assoc.
Check plus_n_Sm.
Print Init.Nat.mul.

Lemma test: forall a b: nat, S a = S b -> a = b.
  intros. inversion H. trivial.
Qed.
Search S.

Lemma sum_n: forall n: nat, 2 * sum n = (1 + n) * n.
Proof.
  induction n.
  (* case O *)
  reflexivity.
  (* case S p *)
  intros.
  simpl.
  simpl in IHn.
  rewrite (plus_comm (sum n) O) in IHn.
  simpl in IHn.
  rewrite (mult_comm n (S n)). simpl.
  rewrite <- IHn.
  rewrite <- (plus_n_Sm n (n + (sum n + sum n))).
  rewrite (plus_comm (n + sum n) O). simpl.
  rewrite <- (plus_n_Sm (n + sum n) (n + sum n)).
  rewrite <- (plus_assoc n (sum n) (n + sum n)).
  rewrite (plus_comm (sum n) (n + sum n)).
  rewrite <- (plus_assoc n (sum n) (sum n)).
  reflexivity.
Qed.
Print sum_n.