Section PropositionalLogic.

Variables P Q R : Prop.

Theorem hilbert_axiom_S : (P -> Q -> R) -> (P -> Q) -> P -> R.
intros H1.
intros H2 H3.
apply H1.
exact H3.
exact (H2 H3).
Qed.

Theorem distr_and_or : (P /\ Q) \/ (P /\ R) -> P /\ (Q \/ R).
intros H.
destruct H as [H1 | H2].
split.
destruct H1 as [HP HQ].
exact HP.
destruct H1 as [HP HQ].
left.
exact HQ.
destruct H2 as [HP HR].
auto.
Qed.

Theorem noncontradiction : not (P /\ not P).
unfold not.
intros H.
destruct H as [H1 H2].
auto.
Qed.

End PropositionalLogic.

Section PredicateLogic.
Variable D : Set.
Variable R : D -> D -> Prop.

Theorem refl_if : (forall x y : D, R x y -> R y x) ->
                  (forall x y z : D, R x y -> R y z -> R x z) ->
                  (forall x : D, (exists y : D, R x y) -> R x x).
intros Rsym.
intros Rtrans.
intros x.
intros xR_.
destruct xR_ as [y xRy].
apply Rtrans with (y := y).
assumption.
apply Rsym.
assumption.
Qed.

Variables f g : D -> D.
Variable d : D.

Theorem example_pred_theorem : (forall x : D, exists y : D, f x = g y) ->
                               (exists c : D, forall x : D, f x = c) ->
                               (exists y : D, forall x : D, f x = g y).
intros H1 H2.
destruct H2 as [c H2'].
cut (exists y : D, c = g y).
intros H3.
destruct H3 as [yc H3'].
exists yc.
rewrite <- H3'.
assumption.
rewrite <- H2' with (x := d).
apply H1.
Qed.

End PredicateLogic.

Section GroupTheory.

Variable G : Set.
Variable operation : G -> G -> G.
Variable e : G.
Variable inv : G -> G.
Infix "*" := operation.

Hypothesis associativity : forall x y z : G, (x * y) * z = x * (y * z).
Hypothesis identity : forall x : G, x * e = e /\ e * x = x.
Hypothesis inverse  : forall x : G, x * inv x = e /\ inv x * x = e.

Theorem latin_square_property : forall a b : G, exists x : G, a * x = b.
intros a b.
exists (inv a * b).
rewrite <- associativity.
destruct inverse with (x := a) as [H _].
rewrite H.
destruct identity with (x := b) as [_ H'].
trivial.
Qed.

End GroupTheory.

Section InductiveProofs.

Theorem le_O_n : forall n : nat, O <= n.
induction n.
constructor.
constructor.
trivial.
Qed.

Theorem le_S_S : forall n m : nat, n <= m -> S n <= S m.
induction 1; constructor; trivial.
Qed.

Theorem le_plus : forall n m p, n <= m -> n <= p + m.
induction p.
simpl.
trivial.
intros H.
simpl.
constructor.
apply IHp.
trivial.
Qed.


Section GroupTheory_Declarative.

Variable G : Set.
Variable operation : G -> G -> G.
Variable e : G.
Variable inv : G -> G.
Infix "*" := operation.

Hypothesis associativity : forall x y z : G, (x * y) * z = x * (y * z).
Hypothesis identity : forall x : G, x * e = e /\ e * x = x.
Hypothesis inverse  : forall x : G, x * inv x = e /\ inv x * x = e.

Theorem latin_square_property_decl : forall a b : G, exists x : G, a * x = b.
proof.
  let a : G, b : G.
  take (inv a * b).
  have H1:(a * (inv a * b) = (a * inv a) * b) by associativity.
  have H2:(a * inv a = e) by inverse.
  have (a * (inv a * b) = e * b) by H1, H2.
                       ~= b by identity.
  hence thesis.
end proof.
Qed.

End GroupTheory_Declarative.

Theorem le_plus_decl : forall n m p : nat, n <= m -> n <= p + m.
proof.
  let n, m, p : nat be such that H:(n <= m).
  per induction on p.
  suppose it is O.
    reconsider thesis as (n <= m).
    thus thesis by H.
  suppose it is (S p') and IH:(n <= p' + m).
    reconsider thesis as (n <= S (p' + m)).
    thus thesis by IH.
  end induction.
end proof.
Qed.