text_formalization/leg/affprops.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: affprops                                                       *)
   5 (* Chapter: LEG                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-07                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 module type Affprops_def_type = sig
  12   val affprops_goal : term
  13   val affprops : thm
  14 end;;
  15
  16 (*
  17  simp_def2 was assumed as an axiom in collect_geom.ml.
  18  Here is a proof.
  19  The first and last clauses were corrected  by inserting DISJOINT.
  20 *)
  21
  22 flyspeck_needs "leg/AFF_SGN_TAC.hl";;
  23
  24
  25 module Affprops : Affprops_def_type = struct
  26
  27
  28   let AFF_SGN_TAC = Aff_sgn_tac.AFF_SGN_TAC;;
  29
  30   let affprops_goal = `(!a b v0.
  31           DISJOINT {a,b} {v0} ==> aff_gt {a, b} {v0} =
  32           {x | ?ta tb t.
  33                    ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
  34           aff_ge {a, b} {v0} =
  35           {x | ?ta tb t.
  36                    ta + tb + t = &1 /\
  37                    &0 <= t /\
  38                    x = ta % a + tb % b + t % v0}) /\
  39      (!x y z.
  40           conv0 {x, y, z} =
  41           {t | ?a b c.
  42                    a + b + c = &1 /\
  43                    &0 < a /\
  44                    &0 < b /\
  45                    &0 < c /\
  46                    t = a % x + b % y + c % z}) /\
  47      (!x y z.
  48           affine hull {x, y, z} =
  49           {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z})/\
  50  (!v1 v2 v3.
  51           DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
  52           {x | ?t2 t3 t1.
  53                    t2 + t3 + t1 = &1 /\
  54                    t1 < &0 /\
  55                    x = t2 % v2 + t3 % v3 + t1 % v1}) `;;
  56
  57 let affprops_2_1_goal = `!a b v0.
  58           DISJOINT {a,b} {v0} ==>  aff_gt {a, b} {v0} =
  59           {x | ?ta tb t.
  60                    ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} `;;
  61
  62  let affprops_2_1 = prove(affprops_2_1_goal,AFF_SGN_TAC);;
  63
  64
  65 let affprops_ge_2_1_goal = `(!a b v0.
  66           DISJOINT {a,b} {v0} ==>
  67           aff_ge {a, b} {v0} =
  68           {x | ?ta tb t.
  69                    ta + tb + t = &1 /\
  70                    &0 <= t /\
  71                    x = ta % a + tb % b + t % v0})`;;
  72
  73 let affprops_ge_2_1 = prove(affprops_ge_2_1_goal,AFF_SGN_TAC);;
  74
  75   let affprops_0_3_goal = `     (!x y z.
  76           conv0 {x, y, z} =
  77           {t | ?a b c.
  78                    a + b + c = &1 /\
  79                    &0 < a /\
  80                    &0 < b /\
  81                    &0 < c /\
  82                    t = a % x + b % y + c % z})`;;
  83
  84 let affprops_0_3 = prove(affprops_0_3_goal,REWRITE_TAC[conv0] THEN AFF_SGN_TAC);;
  85
  86   let affprops_3_0_goal = `     (!x y z.
  87           affine hull {x, y, z} =
  88           {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z}) `;;
  89
  90 let affprops_3_0 = prove(affprops_3_0_goal,
  91     REWRITE_TAC[AFFINE_HULL_3] THEN SET_TAC[]);;
  92
  93   let affprops_lt_2_1_goal = ` (!v1 v2 v3.
  94           DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
  95           {x | ?t2 t3 t1.
  96                    t2 + t3 + t1 = &1 /\
  97                    t1 < &0 /\
  98                    x = t2 % v2 + t3 % v3 + t1 % v1}) `;;
  99
 100 let affpropos_lt_2_1 = prove(affprops_lt_2_1_goal,AFF_SGN_TAC);;
 101
 102
 103  let affprops_goal = `(!a b v0.
 104           DISJOINT {a,b} {v0} ==> aff_gt {a, b} {v0} =
 105           {x | ?ta tb t.
 106                    ta + tb + t = &1 /\ &0 < t /\ x = ta % a + tb % b + t % v0} /\
 107           aff_ge {a, b} {v0} =
 108           {x | ?ta tb t.
 109                    ta + tb + t = &1 /\
 110                    &0 <= t /\
 111                    x = ta % a + tb % b + t % v0}) /\
 112      (!x y z.
 113           conv0 {x, y, z} =
 114           {t | ?a b c.
 115                    a + b + c = &1 /\
 116                    &0 < a /\
 117                    &0 < b /\
 118                    &0 < c /\
 119                    t = a % x + b % y + c % z}) /\
 120      (!x y z.
 121           affine hull {x, y, z} =
 122           {t | ?a b c. a + b + c = &1 /\ t = a % x + b % y + c % z})/\
 123  (!v1 v2 v3.
 124           DISJOINT {v2,v3} {v1} ==> aff_lt {v2, v3} {v1} =
 125           {x | ?t2 t3 t1.
 126                    t2 + t3 + t1 = &1 /\
 127                    t1 < &0 /\
 128                    x = t2 % v2 + t3 % v3 + t1 % v1}) `;;
 129
 130 let affprops  = prove(affprops_goal,
 131   REWRITE_TAC[affprops_0_3;affprops_3_0 ;affpropos_lt_2_1] THEN
 132   REPEAT STRIP_TAC THEN
 133   ASM_SIMP_TAC[affprops_2_1;affprops_ge_2_1]);;
 134
 135
 136 end;;