(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definition: affprops                                                       *)
(* Chapter: LEG                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-07                                                           *)
(* ========================================================================== *)


module type Affprops_def_type = sig
  val affprops_goal : term
  val affprops : thm
end;;

(*
 simp_def2 was assumed as an axiom in collect_geom.ml.
 Here is a proof.
 The first and last clauses were corrected  by inserting DISJOINT.
*)

flyspeck_needs "leg/AFF_SGN_TAC.hl";;


module Affprops : Affprops_def_type = struct


  let AFF_SGN_TAC = Aff_sgn_tac.AFF_SGN_TAC;;

  let affprops_goal = `(!a b v0.
          DISJOINT {a,b} {v0} ==> aff_gt {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
          aff_ge {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\
                   &0 <= t /\
                   x = ta % a + tb % b + t % v0}) /\
     (!x y z.
          conv0 {x, y, z} =
          {t | ?a b c.
                   a + b + c = &1 /\
                   &0 < a /\
                   &0 < b /\
                   &0 < c /\
                   t = a % x + b % y + c % z}) /\
     (!x y z.
          affine hull {x, y, z} =
          {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z})/\
 (!v1 v2 v3.
          DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
          {x | ?t2 t3 t1.
                   t2 + t3 + t1 = &1 /\
                   t1 < &0 /\
                   x = t2 % v2 + t3 % v3 + t1 % v1}) `;;

let affprops_2_1_goal = `!a b v0.
          DISJOINT {a,b} {v0} ==>  aff_gt {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} `;;

 
let affprops_2_1 = prove(affprops_2_1_goal,AFF_SGN_TAC);;

let affprops_ge_2_1_goal = `(!a b v0.
          DISJOINT {a,b} {v0} ==>  
          aff_ge {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\
                   &0 <= t /\
                   x = ta % a + tb % b + t % v0})`;;

let affprops_ge_2_1 = prove(affprops_ge_2_1_goal,AFF_SGN_TAC);;
  let affprops_0_3_goal = `     (!x y z.
          conv0 {x, y, z} =
          {t | ?a b c.
                   a + b + c = &1 /\
                   &0 < a /\
                   &0 < b /\
                   &0 < c /\
                   t = a % x + b % y + c % z})`;;

let affprops_0_3 = prove(affprops_0_3_goal,REWRITE_TAC[conv0] THEN AFF_SGN_TAC);;
  let affprops_3_0_goal = `     (!x y z.
          affine hull {x, y, z} =
          {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z}) `;;

let affprops_3_0 = prove(affprops_3_0_goal,
    REWRITE_TAC[AFFINE_HULL_3] THEN SET_TAC[]);;
  let affprops_lt_2_1_goal = ` (!v1 v2 v3.
          DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
          {x | ?t2 t3 t1.
                   t2 + t3 + t1 = &1 /\
                   t1 < &0 /\
                   x = t2 % v2 + t3 % v3 + t1 % v1}) `;;

let affpropos_lt_2_1 = prove(affprops_lt_2_1_goal,AFF_SGN_TAC);;

 let affprops_goal = `(!a b v0.
          DISJOINT {a,b} {v0} ==> aff_gt {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
          aff_ge {a, b} {v0} =
          {x | ?ta tb t.
                   ta + tb + t = &1 /\
                   &0 <= t /\
                   x = ta % a + tb % b + t % v0}) /\
     (!x y z.
          conv0 {x, y, z} =
          {t | ?a b c.
                   a + b + c = &1 /\
                   &0 < a /\
                   &0 < b /\
                   &0 < c /\
                   t = a % x + b % y + c % z}) /\
     (!x y z.
          affine hull {x, y, z} =
          {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z})/\
 (!v1 v2 v3.
          DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
          {x | ?t2 t3 t1.
                   t2 + t3 + t1 = &1 /\
                   t1 < &0 /\
                   x = t2 % v2 + t3 % v3 + t1 % v1}) `;;

let affprops  = prove(affprops_goal,
  REWRITE_TAC[affprops_0_3;affprops_3_0 ;affpropos_lt_2_1] THEN
  REPEAT STRIP_TAC THEN
  ASM_SIMP_TAC[affprops_2_1;affprops_ge_2_1]);;

end;;