Library ProjectiveGeometry.Plane.projective_plane_inst

Require Export decidability.

Module AbstractProjectivePlane : ProjectivePlane.

Parameter Point :Set.
Parameter Line:Set.
Parameter Incid : Point -> Line -> Prop.

Axiom incid_dec : forall (A:Point)(l:Line), {Incid A l} + {~Incid A l}.

Axiom a1_exist : forall ( A B :Point) ,{l:Line | Incid A l /\ Incid B l}.

Axiom a2_exist : forall (l1 l2:Line), {A:Point | Incid A l1 /\ Incid A l2}.

Axiom uniqueness : forall (A B :Point)(l1 l2:Line),
   Incid A l1 -> Incid B l1 -> Incid A l2 -> Incid B l2 -> A=B\/l1=l2.

Axiom a3: {A:Point & {B :Point & {C:Point & {D :Point |
  (forall l :Line, dist4 A B C D/\
    (Incid A l /\ Incid B l -> ~Incid C l /\ ~Incid D l)
    /\ (Incid A l /\ Incid C l -> ~Incid B l /\ ~Incid D l)
    /\ (Incid A l /\ Incid D l -> ~Incid C l /\ ~Incid B l)
    /\ (Incid C l /\ Incid B l -> ~Incid A l /\ ~Incid D l)
    /\ (Incid D l /\ Incid B l -> ~Incid C l /\ ~Incid A l)
    /\ (Incid C l /\ Incid D l -> ~Incid B l /\ ~Incid A l))}}}}.

End AbstractProjectivePlane.

Require Export forth.

Module AbstractProjectivePlane' := forth.forth AbstractProjectivePlane.

Export AbstractProjectivePlane.
Export AbstractProjectivePlane'.