~llee454/llee454-incident-geometry/master

  5:58 6:12 designing

  7:50 7:55 reviewing

  7:55 8:51 coding

  5:47 6:20 designing

  6:23 6:58 coding

  := fun l => forallb (on l).

(*

*)

Definition point_set

  :  Set

  := { ps : list point | points_distinct ps }.

 

(*

*)

Definition point_set_list

  :  point_set -> list point

  := proj1_sig.

 

(*

*)

Definition point_set_distinct

  :  forall ps : point_set, points_distinct (point_set_list ps)

  := proj2_sig.

 

(*

*)

Definition point_set_in

  :  point -> point_set -> Prop

  := fun p ps

       => In p (point_set_list ps).

 

(*

*)

Definition point_set_in_dec

  :  forall (p : point) (ps : point_set), {point_set_in p ps} + {~ point_set_in p ps}

 

(*

*)

Definition point_set_subset

  :  point_set -> point_set -> Prop

  := fun ps qs

       => forall p : point, point_set_in p ps -> point_set_in p qs.

 

(*

*)

Definition point_set_disjoint

  :  point_set -> point_set -> Prop

  := fun ps qs

       => forall p : point, point_set_in p ps -> ~ point_set_in p qs.

 

(*

*)

Definition point_set_disjoint_sym

  :  forall ps qs : point_set, point_set_disjoint ps qs -> point_set_disjoint qs ps

 

(*

*)

Definition point_set_eq

  :  point_set -> point_set -> Prop

  := fun ps qs

       => point_set_subset ps qs /\ point_set_subset qs ps.

 

(*

*)

Definition point_set_nil

  :  point_set

  := exist

       (fun ps => points_distinct ps)

       nil

       points_distinct_nil.

 

(*

*)

Definition point_set_difference_strong

  :  forall ps qs : point_set, {rs : point_set | forall p : point, point_set_in p ps /\ ~ point_set_in p qs -> point_set_in p rs}

 

(*

 

(*

*)

Definition point_set_singleton

  :  forall p : point -> {ps : point_set | unique (fun q : point => point_set_is q ps) p}

 

(*

*)

Definition point_set_add

  :  forall (p : point) (ps : point_set), {qs : list point | point_set_eq (point_set_difference qs ps) (point_

  := fun p ps

       => 

 

(*

*)

Definition point_set_remove

  :  forall (p : point) (ps : point_set), point_set_in p ps -> {qs : point_set | point_set_subset qs ps /\ ~ point_set_in p qs}

 

(*

*)

Definition point_set_replace_collinear

  :  forall 

 

(*

 TODO Give me a list of the points guaranteed to exist by collinearity_axiom.

 

 TODO  A function that returns two other points when given a point that are proved to be different and distinct 

 

  : {ps : list point

      | points_distinct ps /\

        length ps = 3

 

  points_others

    : forall p : point, exists q : point, exists r : point, distinct p q r /\ noncollinear p q r

 

  my goal was to call the collinearity axiom to get three distinct noncollinear points q r s

  then form these in a list ps := q :: r :: s :: nil

  prove the elements were distinct using points_distinct_cons

  use cases over points_In_dec

    if p is in ps

      call points_distinct_remove to get qs where qs is distinct and doesnt contain

      in this case we can prove that p :: qs is noncollinear but we'd need to deepen our theory (points_collinear + thms).

    if p is not in ps

      we can take the first two points and use points_different_head and points_different_tail iterative to prove they are all different 

 

  goal

    : forall (p : point) (ps : list point) (H : points_distinct ps), points_noncollinear ps -> forall H0 : In p ps, let (qs, H1) := points_distinct_remove ps H p H0 in points_distinct (p :: qs) /\ points_noncollinear (p :: ps)

 

*)

 

(*

*)

Definition points_others_noncollinear

  : forall p : point, exists q : point, exists r : point, distinct p q r /\ noncollinear p q r

  := fun p

       => ex_ind (fun q : point =>

          ex_ind (fun r : point =>

          ex_ind

            (fun (s : point) (H : distinct q r s /\ noncollinear q r s)

              => let ps := (q :: r :: s :: nil) in

                 sumbool_ind (* over In p ps *)

                   (fun _ => exists x : point, exists y : point, distinct p x y /\ noncollinear p x y)

                   (fun H0 : In p ps

                     => let (qs, H1)

                          := points_distinct_remove ps 

                               (* TODO: points_distinct ps *)

                               p H0 in

                        let rs := p :: qs in

                        let ((x, ss), H2)

                          := points_list_destr qs

                               (lt_0_Sn 1

                                || a > 0 @a by (eq_add_S (proj1 (proj2 (proj2 H1))) : length qs = 2)) in

                        let ((y, _), H3)

                          := points_list_destr ss

                               (lt_0_Sn 0

                                || a > 0 @a by 

 

(*

Check (eq_add_S (length (1 :: 2 :: 3 :: nil)) 3 (eq_refl (length (0 :: 1 :: 2 :: 3 :: nil))) : length (1 :: 2 :: 3 :: nil) = 3).

*)

 

(*

  Proves that at least one line passes through

  each point.

*)

Definition point_line_ex

  :  forall p : point, exists l : line, on l p = true

  := fun p

       => ex_ind (fun q =>

          ex_ind (fun r =>

          ex_ind (

            fun (s : point) (H : distinct q r s /\ noncollinear q r s)

              => let qs := q :: r :: s :: nil in

                 bool_dec0

                   (fun _ => exists l : line, on l p = true)

                   (fun H : points_differentb p qs = true

                     => let H0

                          :  p <> q

                          := points_differentb_head p q (r :: s :: nil) H in

                        ex_ind

                          (fun l (H1 : unique (fun l => on l p = true /\ on l q = true) l)

                            => ex_intro

                                 (fun l => on l p = true)

                                 l

                                 (proj1 (proj1 H1)))

                          (points_line_axiom p q H0))

                   (fun H : points_differentb p qs = false

                     =>