The Coq mailing list

[Julien Narboux <Julien.Narboux AT inria.fr>]

Hi Jean,

I am perhaps a bit far away from your original idea/question.
But if you have somehow a definition a predicate expressing that three 
points are collinear then you may want to use something like that for 
is_a_line :

Parameter Point : Set.
Parameter Col : Point -> Point -> Point -> Prop.

Definition is_a_line : (Point -> Prop) -> Prop :=
  fun S : Point -> Prop => exists A, exists B, A<>B /\ forall x, S x 
<-> Col x A B.

This is more or less what is done by Tarski, Szmielew and Schwabhäuser 
in the book Metamathematische Methoden in der Geometrie.

I have started to formalize this book.

But it seems that this formalization will not suit your needs because 
first it is classical and second I have chosen to keep the concept of 
line implicit.
It is less intuitive than an approach using a definition of a line, but 
it saves some lemmas/unfolds.

This is also what is usually done in the automated theorem proving 
community : for example lines are implicit in the Wu, area and Gröbner 
basis methods.

On the other side, of course there is the Hilbert's axiomatic which is 
based on both points and lines.

Parameter Point : Set.
Parameter Line : Set.

From my personal experience, from the formalization point of view, the
Hilbert axiomatic has the following advantages :
- it is easier to convince someone that the axioms are "true".
- lines and points are treated the same way
- intuitive properties appear early in the formalization (in Tarski's 
axiomatic, he needs 60 pages to prove the existence of the midpoint.)

Tarski axiomatic has the following advantages :
- it contains fewer axioms
- it is easy to generalize to any dimension
- the axioms "includes" degenerated cases, this leads to more "generic" 
proof than using Hilbert's.

Hope it helps.

Julien









Yves Bertot a écrit :
> It seems odd that any property would be understood as a line.  More
> over, what would be the meaning of your axiom when instantiated for
> the predicate (fun x => True).  Even if you manage to pass through
> the problem of having your sigma-types being accepted, this would
> tantamount (after decomposition of the axiom) to working in the
> following context.
>
> Parameter Point :Set.
> Definition Line := Point ->Prop.
> Parameter A:Point.
> Parameter B:Point.
> Parameter C:Point.
> Parameter I4: forall D:Line, {~(D A)}+{~(D B)}+{~(D C)}.
>
> But this context implies False: just take the following
> proof:
>
> Theorem the_contradiction : False.
> Proof.
> destruct (my_algo (fun x => True)) as [[H | H]| H]; apply H;exact I.
> Qed. 
>
> I would rather believe you need to have a predicate on predicates
> that distinguishes the lines from other propositions 
> and you should work in a context of this form:
>
> Parameter Point : Set.
> Parameter is_a_line : (Point -> Prop) -> Prop.
>
> Now, to pass through the problem of having your sigma-types accepted,
> replace any instance of { x : A & B} with sigT(fun x : A => B).
>
> Here is an example which is accepted in my version of Coq
>
> Axiom I4 :
>   sigT (fun A:Point =>
>          sigT (fun B:Point => 
>                 sigT (fun C:Point =>
>                        forall D:Point->Prop, is_a_line D ->
>                          {~(D A)}+{~(D B)}+{~(D B)}))).
>
> I guess you have a clearer idea than me about what should be in the
> definition of "is_a_line", to make sure you capture the geometrical
> intuition you have in mind.
>
> Yves
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club