Section PropositionalLogic.

Variables P Q R : Prop.

Theorem hilbert_axiom_S : (P -> Q -> R) -> (P -> Q) -> P -> R.
Admitted.



Theorem distr_and_or : (P /\ Q) \/ (P /\ R) -> P /\ (Q \/ R).
Admitted.



Theorem noncontradiction : not (P /\ not P).
Admitted.


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).
Admitted.




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).
Admitted.



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.
Admitted.

End GroupTheory.



Module Redefinitions.

Inductive nat : Set :=
    O : nat
  | S : nat -> nat.

Print nat_ind.


Inductive le : nat -> nat -> Prop :=
    le_n : forall n : nat, le n n
  | le_S : forall n m : nat, le n m -> le n (S m).

Print le_ind.

Infix "<=" := le.

Inductive or (A B : Prop) : Prop :=
     or_introl : A -> or A B
   | or_intror : B -> or A B.

Print or_ind.

Theorem le_O_n : forall n : nat, O <= n.
Admitted.


Theorem le_S_S : forall n m : nat, n <= m -> S n <= S m.
Admitted.



Fixpoint plus (a b : nat) : nat :=
  match a with
     O => b
    |S a => S (plus a b)
  end.

Theorem le_plus : forall n m p, n <= m -> n <= plus p m.
Admitted.

End Redefinitions.



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.
end proof.
Admitted.

End GroupTheory_Declarative.

Theorem le_plus_decl : forall n m p : nat, n <= m -> n <= p + m.
proof.
end proof.
Admitted.