~llee454/llee454-incident-geometry/master

  6:21 7:03 code

  7:18 7:20 review

Definition point_set_difference

  :  point_set -> point_set -> point_set

  := fun ps qs

       => list_rec

            (fun 

 

(*

  TODO Fforgot to factor in the fact that point sets are distinct.

*)

  := fun ps qs

       => let t ps rs := forall p : point, point_set_in p ps /\ ~ point_set_in p qs -> point_set_in p rs in

          let u ps := {rs | t ps rs} in

          list_rec u

            (exist

              (t nil)

              nil

              (fun p (H : In p nil /\ ~ point_set_in p qs)

                => False_ind

                     (t nil nil)

                     (and_ind

                       (fun (H0 : In p nil) _ => H0)

                       H)))

            (fun p rs (F : u rs)

              => sumbool_rec (* over in p qs *)

                   (fun _ => u (p :: rs))

                   (fun H : point_set_in p qs

                     => let (ss, H0) := F in

                        (* H0 : {ss : point_set | forall p : point, point_set_in p rs /\ ~ point_set_in p qs -> point_set_in p ss} *)

                        exist

                          (t (p :: rs))

                          ss

                          (fun q (H1 : point_set_in q (p :: rs) /\ ~ (point_set_in q qs))

                            => or_ind

                                 (fun H2 : p = q

                                   => False_ind

                                        (point_set_in q ss)

                                        (proj2 H1

                                          (H || point_set_in a qs @a by H2)))

                                 (fun H2 : In p rs

                                   => H0 (conj H2 (proj2 H1)))

                                 (proj1 H1)))

                   (fun H : ~ point_set_in p qs

                     => let (ss, H0) := F in

                        let ts := p :: ss in

                        exist

                          (t (p :: rs))

                          ts

                          (fun q (H1 : point_set_in q (p :: rs) /\ ~ (point_set_in q qs))

                            => or_ind

                                 (fun H2 : p = q

                                   => or_inrol (In q ss) H2)

                                 (fun H2 : In p rs

                                   => or_intror

                                        (p = q)

                                        (H0 (conj H2 (proj2 H1))))

                                 (proj1 H1)))

            (point_set_list ps)