Library ProjectiveGeometry.Space.matroids_axioms

Require Export Omega.
Require Export sets_of_points.

Module Type Matroid (DecPoints: FSetInterface.WS).

Declare Module Export FiniteSetsDefs : BuildFSets DecPoints .

Parameter rk : set_of_points -> nat.


Axiom matroid1_a : forall X, rk X >= 0.

Axiom matroid1_b : forall X, rk X <= cardinal X.

Axiom matroid2:
forall e e':set_of_points, Subset e e' -> rk(e)<=rk(e').

Axiom matroid3:
forall e e':set_of_points,
 rk(union e e') + rk(inter e e') <= rk(e) + rk(e').

End Matroid.

Module Type Matroid' (DecPoints: FSetInterface.WS).

Declare Module Export FiniteSetsDefs : BuildFSets DecPoints.

Parameter rk : set_of_points -> nat.

Axiom rk_compat:
  forall x x', Equal x x' ->
     rk x = rk x'.


Axiom matroid1' : rk empty = 0.

Axiom matroid2':
forall X:set_of_points, forall x : Point, rk(X)<=rk (add x X) <= rk(X)+1.

Axiom matroid3': forall X y z,
   rk(add y X) = rk(add z X) ->
   rk(add z X) = rk(X) ->
   rk(X) = rk(union X (couple y z)).

End Matroid'.