Add formalization of affine arithmetic done by Magnus

Affine_Magnus/affine.ml

+
+#use "hol.ml";;
+
+prioritize_real();;
+
+let affine_INDUCT,affine_RECURSION = define_type
+  "affine = Central real | Eps real num affine";;
+
+let aff_CASES = prove(
+  `!a. (?c. a = Central c) \/ (?k r ax. a = Eps k r ax)`,
+  MATCH_MP_TAC affine_INDUCT THEN
+  SIMP_TAC [injectivity "affine"] THEN
+  MESON_TAC []);;
+
+let restrict_def = define `
+  restrict (r:real) = if r < & (0-1) then & (0-1) else
+                      if & 1 < r then & 1 else r
+`;;
+
+let alookup_def = define `
+  (alookup [] n = NONE) /\
+  (alookup (CONS (x,y) xs) n = if x = n then SOME y else alookup xs n)
+`;;
+
+let get_eps_def = define `
+  get_eps index env =
+    match alookup env index with
+      SOME r -> restrict r
+    | NONE -> & 0
+`;;
+
+let aff_def = define `
+  (aff env (Central r) = r) /\
+  (aff env (Eps c k a) = c * get_eps k env + aff env a)
+`;;
+
+let neg_def = define `
+  (neg (Central r) = Central (&0 - r)) /\
+  (neg (Eps c k a) = Eps (&0 - c) k (neg a))
+`;;
+
+let aff_neg = prove(
+  `!env a1. aff env (neg a1) = &0 - aff env a1`,
+  STRIP_TAC THEN
+  MATCH_MP_TAC affine_INDUCT THEN
+  SIMP_TAC [aff_def;neg_def] THEN
+  REPEAT STRIP_TAC THEN
+  SIMP_TAC [REAL_SUB_RDISTRIB;REAL_POLY_CLAUSES;
+    REAL_SUB_LZERO;REAL_NEG_ADD]);;
+let aff_neg = REWRITE_RULE [REAL_SUB_LZERO] aff_neg;;
+
+let add_def = define `
+  (add (Central r1) (Central r2) = Central (r1+r2)) /\
+  (add (Central r1) (Eps c k a) = Eps c k (add (Central r1) a)) /\
+  (add (Eps c k a) (Central r2) = Eps c k (add a (Central r2))) /\
+  (add (Eps c1 k1 a1) (Eps c2 k2 a2) =
+     if k1 < k2 then Eps c1 k1 (add a1 (Eps c2 k2 a2)) else
+     if k2 < k1 then Eps c2 k2 (add (Eps c1 k1 a1) a2) else
+       Eps (c1+c2) k1 (add a1 a2))
+`;;
+
+let sub_def = define `
+  sub a1 a2 = add a1 (neg a2)
+`;;
+
+let size_def = define `
+  (size (Central r) = 0) /\
+  (size (Eps c k a) = 1 + size a)
+`;;
+
+let rec PAT_ASSUM pat t =
+  FIRST_X_ASSUM (fun th ->
+    if can (MATCH_MP (DISCH_ALL (ASSUME pat))) th then t th else NO_TAC);;
+
+g `!n a1 a2 env.
+     size a1 + size a2 <= n ==>
+     aff env (add a1 a2) = aff env a1 + aff env a2`;;
+e (MATCH_MP_TAC num_WF);;
+e (REPEAT STRIP_TAC);;
+e (STRIP_ASSUME_TAC (SPEC `a1:affine` aff_CASES));;
+e (STRIP_ASSUME_TAC (SPEC `a2:affine` aff_CASES));;
+
+  e (ASM_SIMP_TAC [add_def;aff_def]);;
+
+e (ASM_SIMP_TAC [add_def;aff_def]);;
+e (FIRST_X_ASSUM (MP_TAC o SPEC `size ax`));;
+e (MATCH_MP_TAC (MESON [] `b /\ (b1 ==> b2) ==> (b ==> b1) ==> b2`));;
+e CONJ_TAC;;
+
+  e (PAT_ASSUM `n <= m:num` MP_TAC);;
+  e (ASM_SIMP_TAC [size_def] THEN ARITH_TAC);;
+
+(* not complete, so let's cheat it with new_axiom below *)
+
+let aff_add_lemma = new_axiom
+  `!n a1 a2 env.
+     size a1 + size a2 <= n ==>
+     aff env (add a1 a2) = aff env a1 + aff env a2`;;
+
+let aff_add =
+  (REWRITE_RULE [LE_REFL] o
+   SPECL [`size a1 + size a2`;`a1:affine`;`a2:affine`])
+     aff_add_lemma;;
+
+let aff_sub = prove(
+  `!env a1. aff env (sub a1 a2) = aff env a1 - aff env a2`,
+  SIMP_TAC [sub_def;aff_add;aff_neg;real_sub]);;

Affine_Magnus/affineScript.sml

+open HolKernel Parse boolLib bossLib lcsymtacs;
+open ratTheory rat_extraTheory arithmeticTheory
+     listTheory rich_listTheory alistTheory;
+
+val _ = new_theory "affine";
+
+(* Type for affine expression *)
+
+val _ = Datatype `
+  affine = Central rat | Eps rat num affine
+`
+
+(* The aff function returns the rat value of an affine expression *)
+
+val restrict_def = Define `
+  restrict (r:rat) = if r < -1 then -1 else
+                     if 1 < r then 1 else r
+`
+
+val get_eps_def = Define `
+  get_eps index env =
+    case ALOOKUP env (index:num) of
+    | SOME r => restrict r
+    | NONE => 0
+`
+
+val aff_def = Define `
+  (aff env (Central r) = r) /\
+  (aff env (Eps c k a) = c * get_eps k env + aff env a)
+`
+
+(* Negation *)
+
+val neg_def = Define `
+  (neg (Central r) = Central (-r)) /\
+  (neg (Eps c k a) = Eps (-c) k (neg a))
+`
+
+val aff_neg = store_thm("aff_neg",
+  ``∀env a1. aff env (neg a1) = - aff env a1``,
+  Induct_on `a1`
+  \\ fs [aff_def,neg_def,RAT_AINV_LMUL,RAT_AINV_ADD]);
+
+(* Addition *)
+
+val add_def = Define `
+  (add (Central r1) (Central r2) = Central (r1+r2)) /\
+  (add (Central r1) (Eps c k a) = Eps c k (add (Central r1) a)) /\
+  (add (Eps c k a) (Central r2) = Eps c k (add a (Central r2))) /\
+  (add (Eps c1 k1 a1) (Eps c2 k2 a2) =
+     if k1 < k2 then Eps c1 k1 (add a1 (Eps c2 k2 a2)) else
+     if k2 < k1 then Eps c2 k2 (add (Eps c1 k1 a1) a2) else
+       Eps (c1+c2) k1 (add a1 a2))
+`
+
+val aff_add = store_thm("aff_add",
+  ``∀a1 a2 env. aff env (add a1 a2) = aff env a1 + aff env a2``,
+  recInduct (theorem "add_ind") \\ rw [aff_def,add_def]
+  \\ fs [RAT_RDISTRIB,AC RAT_ADD_ASSOC RAT_ADD_COMM]
+  \\ `k1 = k2` by decide_tac \\ fs []);
+
+(* Subtraction *)
+
+val sub_def = Define `
+  sub a1 a2 = add a1 (neg a2)
+`
+
+val aff_sub = store_thm("aff_sub",
+  ``∀env a1 a2. aff env (sub a1 a2) = aff env a1 - aff env a2``,
+  fs [sub_def, aff_add, aff_neg, RAT_SUB_ADDAINV, RAT_ADD_LID]);
+
+(* Max and min *)
+
+val central_def = Define `
+  (central (Central r) = r) /\
+  (central (Eps c k a) = central a)
+`
+
+val max_eps_def = Define `
+  (max_eps (Central r) = 0) /\
+  (max_eps (Eps c k a) = (if c < 0 then -c else c) + max_eps a)
+`
+
+val max_def = Define `
+  max a = central a + max_eps a
+`
+
+val min_def = Define `
+  min a = central a - max_eps a
+`
+
+val get_eps_le = prove(
+  ``r * get_eps n env <= if r < 0 then -r else r``,
+  fs [get_eps_def] \\ every_case_tac
+  \\ fs [RAT_MUL_RZERO,GSYM RAT_LEQ_LES]
+  \\ once_rewrite_tac [GSYM RAT_AINV_0]
+  \\ fs [RAT_LES_AINV]
+  \\ TRY (imp_res_tac RAT_LES_ANTISYM \\ NO_TAC)
+  \\ fs [restrict_def] \\ rw []
+  \\ fs [rat_mul_minus_1,RAT_MUL_RID,RAT_LES_REF]
+  \\ fs [RAT_LEQ_LES]
+  \\ TRY (match_mp_tac RAT_LEQ_TRANS
+          \\ qexists_tac `0` \\ fs [RAT_LES_IMP_LEQ,rat_le_0] \\ NO_TAC)
+  THEN1 (match_mp_tac RAT_LEQ_TRANS
+    \\ qexists_tac `r * -1`
+    \\ rpt strip_tac \\ TRY (fs [rat_mul_minus_1,RAT_LEQ_REF] \\ NO_TAC)
+    \\ fs [RAT_LE_MULT_LCANCEL]
+    \\ imp_res_tac RAT_LES_ANTISYM \\ fs [])
+  THEN1
+   (match_mp_tac RAT_LEQ_TRANS
+    \\ qexists_tac `r * 1`
+    \\ rpt strip_tac \\ TRY (fs [RAT_MUL_RID,RAT_LEQ_REF] \\ NO_TAC)
+    \\ Cases_on `r = 0` \\ fs [RAT_MUL_LZERO,RAT_LEQ_REF]
+    \\ `0 < r` by fs [rat_leq_def]
+    \\ fs [RAT_LE_MULT_LCANCEL]));
+
+val max_thm = store_thm("max_thm",
+  ``∀env a. aff env a <= max a``,
+  Induct_on `a`
+  \\ fs [max_def,aff_def,max_eps_def,central_def,
+         RAT_SUB_RID,RAT_LEQ_REF,RAT_ADD_RID]
+  \\ rpt strip_tac \\ assume_tac get_eps_le \\ rw [] \\ fs []
+  \\ rpt (first_x_assum (mp_tac o SPEC_ALL)) \\ rw[]
+  \\ imp_res_tac RAT_ADD_MONO
+  \\ fs [AC RAT_ADD_COMM RAT_ADD_ASSOC]);
+
+val le_get_eps = prove(
+  ``-(if r < 0 then -r else r) <= r * get_eps n env``,
+  fs [get_eps_def] \\ every_case_tac
+  \\ fs [RAT_MUL_RZERO,GSYM RAT_LEQ_LES,RAT_AINV_AINV]
+  \\ TRY (imp_res_tac RAT_LES_ANTISYM \\ NO_TAC)
+  \\ once_rewrite_tac [GSYM RAT_AINV_0]
+  \\ fs [RAT_LES_AINV]
+  \\ fs [restrict_def] \\ rw []
+  \\ fs [rat_mul_minus_1,RAT_MUL_RID,RAT_LES_REF]
+  \\ fs [RAT_LEQ_LES]
+  \\ TRY (match_mp_tac RAT_LEQ_TRANS
+          \\ qexists_tac `0` \\ fs [RAT_LES_IMP_LEQ,rat_le_0] \\ NO_TAC)
+  THEN1 (match_mp_tac RAT_LEQ_TRANS
+    \\ qexists_tac `r * 1`
+    \\ rpt strip_tac \\ TRY (fs [RAT_MUL_RID,RAT_LEQ_REF] \\ NO_TAC)
+    \\ fs [RAT_LE_MULT_LCANCEL]
+    \\ imp_res_tac RAT_LES_ANTISYM \\ fs [])
+  THEN1
+   (match_mp_tac RAT_LEQ_TRANS
+    \\ qexists_tac `r * -1`
+    \\ rpt strip_tac \\ TRY (fs [rat_mul_minus_1,RAT_LEQ_REF] \\ NO_TAC)
+    \\ Cases_on `r = 0` \\ fs [RAT_MUL_LZERO,RAT_LEQ_REF]
+    \\ `0 < r` by fs [rat_leq_def]
+    \\ fs [RAT_LE_MULT_LCANCEL]));
+
+val min_thm = store_thm("min_thm",
+  ``∀env a. min a <= aff env a``,
+  Induct_on `a`
+  \\ fs [min_def,aff_def,max_eps_def,central_def,
+         RAT_SUB_RID,RAT_LEQ_REF,RAT_ADD_RID]
+  \\ fs [RAT_AINV_ADD,RAT_SUB_ADDAINV]
+  \\ rpt strip_tac \\ assume_tac le_get_eps \\ rw [] \\ fs []
+  \\ rpt (first_x_assum (mp_tac o SPEC_ALL)) \\ rw[]
+  \\ imp_res_tac RAT_ADD_MONO
+  \\ fs [AC RAT_ADD_COMM RAT_ADD_ASSOC]);
+
+(* Multiplication *)
+
+(* Division *)
+
+val _ = export_theory();

Affine_Magnus/rat_extraScript.sml

+open HolKernel Parse boolLib bossLib;
+open ratTheory arithmeticTheory listTheory rich_listTheory alistTheory;
+
+val _ = new_theory "rat_extra";
+
+val rat_mul_minus_1 = store_thm("rat_mul_minus_1",
+  ``(r * -1 = -r) /\ (-1 * r = -r)``,
+  fs [GSYM RAT_AINV_RMUL,RAT_MUL_RID,GSYM RAT_AINV_LMUL,RAT_MUL_LID]);
+
+val rat_le_0 = store_thm("rat_le_0",
+  ``(0 <= -r <=> r <= 0) /\
+    (-r <= 0 <=> 0 <= r)``,
+  fs [GSYM RAT_LEQ_LES]
+  \\ once_rewrite_tac [GSYM RAT_AINV_0]
+  \\ fs [RAT_LES_AINV]
+  \\ rewrite_tac [RAT_AINV_0]);
+
+val RAT_LE_MULT_LCANCEL = store_thm("RAT_LE_MULT_LCANCEL",
+  ``(r * x <= r * y <=> (r = 0) \/ if 0 < r then x <= y else y <= x)``,
+  Cases_on `r = 0` \\ fs [RAT_MUL_LZERO,RAT_LEQ_REF]
+  \\ fs [GSYM RAT_LEQ_LES] \\ rw []
+  \\ fs [RAT_LES_LMUL_POS]
+  \\ `r < 0` by metis_tac [RAT_LES_TOTAL]
+  \\ fs [RAT_LES_LMUL_NEG]);
+
+val _ = export_theory();