Skip to content

Commit

Permalink
Added a few theorems including some systematic gaps in integer
Browse files Browse the repository at this point in the history 
theorems where the analog was present for reals, and a few more
word theorems.

        INT_ABS_BOUNDS
        INT_EQ_LCANCEL_IMP
        INT_EQ_RCANCEL_IMP
        INT_EVENPOW_ABS
        INT_LE_LCANCEL_IMP
        INT_LE_POW_2
        INT_LE_RCANCEL_IMP
        INT_LE_RMUL_EQ
        INT_LT_LADD_IMP
        INT_LT_LCANCEL_IMP
        INT_LT_LMUL
        INT_LT_LNEG
        INT_LT_POW_2
        INT_LT_RCANCEL_IMP
        INT_LT_RMUL
        INT_LT_RNEG
        INT_LT_SQUARE
        INT_OF_NUM_SUB_CASES
        INT_POS_EQ_SQUARE
        INT_POW_EQ_1
        INT_POW_EQ_1_IMP
        INT_POW_EQ_EQ
        INT_POW_EQ_ODD
        INT_POW_EQ_ODD_EQ
        INT_POW_LBOUND
        INT_POW_LE2_ODD_EQ
        INT_POW_LT2_ODD
        INT_POW_LT2_ODD_EQ
        REAL_EVENPOW_ABS
        VAL_WORD_AND_LE
        VAL_WORD_AND_LE_MIN
        VAL_WORD_AND_WORD_LE
        VAL_WORD_OR_LE_MAX
        WORD_JOIN_NOT
        WORD_SUBWORD_NOT

Also added missing conversions WORD_JROL_CONV and WORD_JROR_CONV (for
word-word rotate operations) and included them in WORD_RED_CONV
and hence WORD_REDUCE_CONV.
  • Loading branch information
@jrh13
jrh13 committed Nov 3, 2021
1 parent 1148eeb commit 74560a4
Show file tree
Hide file tree
Showing 6 changed files with 277 additions and 12 deletions.
156 changes: 150 additions & 6 deletions CHANGES
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,151 @@
* page: https://github.com/jrh13/hol-light/commits/master *
* *****************************************************************

Wed 9th Oct 2021 int.ml
Tue 2nd Nov 2021 Library/words.ml

Added missing conversions WORD_JROL_CONV and WORD_JROR_CONV (for
word-word rotate operations) and included them in WORD_RED_CONV
and hence WORD_REDUCE_CONV.

Mon 1st Nov 2021 parser.ml

Fixed a trivial typo in the error message "closing square bracket
of list expected".

Tue 12th Oct 2021 Library/words.ml

Added a couple more word lemmas about pushing logical complements through
other constructs; the side-conditions make them a bit ugly but they can be
useful:

WORD_JOIN_NOT =
|- !v w.
dimindex(:P) <= dimindex(:M) + dimindex(:N)
==> word_join (word_not v) (word_not w) = word_not (word_join v w)

WORD_SUBWORD_NOT =
|- !x pos len.
dimindex(:N) <= len /\ pos + len <= dimindex(:M)
==> word_subword (word_not x) (pos,len) =
word_not (word_subword x (pos,len))

Sat 9th Oct 2021 Library/words.ml

Added a few more elementary word lemmas like a simple upper bound on
a concrete masking of a word:

VAL_WORD_AND_LE =
|- (!x y. val (word_and x y) <= val x) /\
(!x y. val (word_and x y) <= val y)

VAL_WORD_AND_LE_MIN =
|- !x y. val (word_and x y) <= MIN (val x) (val y)

VAL_WORD_AND_WORD_LE =
|- (!x n. val (word_and x (word n)) <= n) /\
(!x n. val (word_and (word n) x) <= n)

VAL_WORD_OR_LE_MAX =
|- !x y. MAX (val x) (val y) <= val (word_or x y)

Fri 8th Oct 2021 int.ml

Added a systematic set of missing analogs of real theorems for ints:

INT_ABS_BOUNDS : thm =
|- !x k. abs x <= k <=> --k <= x /\ x <= k

INT_EQ_LCANCEL_IMP : thm =
|- !x y z. ~(z = &0) /\ z * x = z * y ==> x = y

INT_EQ_RCANCEL_IMP : thm =
|- !x y z. ~(z = &0) /\ x * z = y * z ==> x = y

INT_LE_LCANCEL_IMP : thm =
|- !x y z. &0 < x /\ x * y <= x * z ==> y <= z

INT_LE_POW_2 : thm =
|- !x. &0 <= x pow 2

INT_LE_RCANCEL_IMP : thm =
|- !x y z. &0 < z /\ x * z <= y * z ==> x <= y

INT_LE_RMUL_EQ : thm =
|- !x y z. &0 < z ==> (x * z <= y * z <=> x <= y)

INT_LT_LADD_IMP : thm =
|- !x y z. y < z ==> x + y < x + z

INT_LT_LCANCEL_IMP : thm =
|- !x y z. &0 < x /\ x * y < x * z ==> y < z

INT_LT_LMUL : thm =
|- !x y z. &0 < x /\ y < z ==> x * y < x * z

INT_LT_LNEG : thm =
|- !x y. --x < y <=> &0 < x + y

INT_LT_POW_2 : thm =
|- !x. &0 < x pow 2 <=> ~(x = &0)

INT_LT_RCANCEL_IMP : thm =
|- !x y z. &0 < z /\ x * z < y * z ==> x < y

INT_LT_RMUL : thm =
|- !x y z. x < y /\ &0 < z ==> x * z < y * z

INT_LT_RNEG : thm =
|- !x y. x < --y <=> x + y < &0

INT_LT_SQUARE : thm =
|- !x. &0 < x * x <=> ~(x = &0)

INT_OF_NUM_SUB_CASES : thm =
|- !m n. &m - &n = (if n <= m then &(m - n) else -- &(n - m))

INT_POS_EQ_SQUARE : thm =
|- !x. &0 <= x <=> (?y. y pow 2 = real_of_int x)

INT_POW_EQ_1 : thm =
|- !x n. x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0

INT_POW_EQ_1_IMP : thm =
|- !x n. ~(n = 0) /\ x pow n = &1 ==> abs x = &1

INT_POW_EQ_EQ : thm =
|- !n x y.
x pow n = y pow n <=>
(if EVEN n then n = 0 \/ abs x = abs y else x = y)

INT_POW_EQ_ODD : thm =
|- !n x y. ODD n /\ x pow n = y pow n ==> x = y

INT_POW_EQ_ODD_EQ : thm =
|- !n x y. ODD n ==> (x pow n = y pow n <=> x = y)

INT_POW_LBOUND : thm =
|- !x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n

INT_POW_LE2_ODD_EQ : thm =
|- !n x y. ODD n ==> (x pow n <= y pow n <=> x <= y)

INT_POW_LT2_ODD : thm =
|- !n x y. x < y /\ ODD n ==> x pow n < y pow n

INT_POW_LT2_ODD_EQ : thm =
|- !n x y. ODD n ==> (x pow n < y pow n <=> x < y)

Fri 8th Oct 2021 real.ml, int.ml

Added integer and real forms of this simple lemma:

INT_EVENPOW_ABS =
|- !x n. EVEN n ==> abs x pow n = x pow n

REAL_EVENPOW_ABS =
|- !x n. EVEN n ==> abs x pow n = x pow n

Wed 6th Oct 2021 int.ml

Added a natural integer analog of MOD_UNIQUE:

Expand All @@ -17,7 +161,7 @@ Added a natural integer analog of MOD_UNIQUE:
m rem n = p <=>
(n = &0 /\ m = p \/ &0 <= p /\ p < abs n) /\ (m == p) (mod n)

Tue 8th Oct 2021 Library/words.ml
Tue 5th Oct 2021 Library/words.ml

Added a few trivial theorems about unsigned word max/min:

Expand Down Expand Up @@ -65,11 +209,11 @@ proved automatically by WORD_ARITH_TAC.
WORD_ADC_LE_EXACT =
|- (!x y.
val(word_add (word_add x y) (word 1)) <= val x <=>
val(word_add (word_add x y) (word 1)) + 2 EXP dimindex (:N) =
val(word_add (word_add x y) (word 1)) + 2 EXP dimindex(:N) =
val x + val y + 1) /\
(!x y.
val(word_add (word_add x y) (word 1)) <= val y <=>
val(word_add (word_add x y) (word 1)) + 2 EXP dimindex (:N) =
val(word_add (word_add x y) (word 1)) + 2 EXP dimindex(:N) =
val x + val y + 1)

WORD_ADC_LE_INEXACT =
Expand All @@ -83,10 +227,10 @@ proved automatically by WORD_ARITH_TAC.
WORD_ADD_LT_EXACT =
|- (!x y.
val(word_add x y) < val x <=>
val(word_add x y) + 2 EXP dimindex (:N) = val x + val y) /\
val(word_add x y) + 2 EXP dimindex(:N) = val x + val y) /\
(!x y.
val(word_add x y) < val y <=>
val(word_add x y) + 2 EXP dimindex (:N) = val x + val y)
val(word_add x y) + 2 EXP dimindex(:N) = val x + val y)

WORD_ADD_LT_INEXACT =
|- (!x y.
Expand Down
60 changes: 60 additions & 0 deletions Library/words.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1544,6 +1544,23 @@ let VAL_WORD_AND_POW2 = prove
COND_CASES_TAC THEN REWRITE_TAC[MULT_CLAUSES; LT_EXP; EXP_LT_0] THEN
CONV_TAC NUM_REDUCE_CONV THEN ASM_MESON_TAC[BIT_TRIVIAL; NOT_LE]);;

let VAL_WORD_AND_LE = prove
(`(!x y:N word. val(word_and x y) <= val x) /\
(!x y:N word. val(word_and x y) <= val y)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[val_def] THEN MATCH_MP_TAC NSUM_LE THEN
REWRITE_TAC[FINITE_NUMSEG_LT] THEN X_GEN_TAC `i:num` THEN
SIMP_TAC[IN_ELIM_THM; BIT_WORD_AND; LE_MULT_LCANCEL; LE_BITVAL]);;

let VAL_WORD_AND_LE_MIN = prove
(`!x y:N word. val(word_and x y) <= MIN (val x) (val y)`,
REWRITE_TAC[ARITH_RULE `x <= MIN y z <=> x <= y /\ x <= z`] THEN
REWRITE_TAC[VAL_WORD_AND_LE]);;

let VAL_WORD_AND_WORD_LE = prove
(`(!(x:N word) n. val(word_and x (word n)) <= n) /\
(!(x:N word) n. val(word_and (word n) x) <= n)`,
MESON_TAC[VAL_WORD_AND_LE; LE_TRANS; LE_REFL; VAL_WORD_LE]);;

let word_or = new_definition
`word_or = bitwise2 (\/)`;;

Expand Down Expand Up @@ -1576,6 +1593,11 @@ let VAL_WORD_OR_LE = prove
REPEAT STRIP_TAC THEN MATCH_MP_TAC VAL_LE_BITS THEN
SIMP_TAC[BIT_WORD_OR]);;

let VAL_WORD_OR_LE_MAX = prove
(`(!x y:N word. MAX (val x) (val y) <= val(word_or x y))`,
REWRITE_TAC[ARITH_RULE `MAX y z <= x <=> y <= x /\ z <= x`] THEN
REWRITE_TAC[VAL_WORD_OR_LE]);;

let word_xor = new_definition
`word_xor = bitwise2 (\x y. ~(x <=> y))`;;

Expand Down Expand Up @@ -2957,6 +2979,16 @@ let VAL_WORD_JOIN_SIMPLE = prove
REWRITE_TAC[LE_MULT_LCANCEL; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
REWRITE_TAC[EXP_EQ_0; ARITH_EQ]]);;

let WORD_JOIN_NOT = prove
(`!v w. dimindex(:P) <= dimindex(:M) + dimindex(:N)
==> (word_join:(M)word->(N)word->(P)word) (word_not v) (word_not w) =
word_not(word_join v w)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[WORD_EQ_BITS_ALT] THEN
SIMP_TAC[BIT_WORD_JOIN; BIT_WORD_NOT; COND_SWAP] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[BIT_GUARD] THEN EQ_TAC THEN SIMP_TAC[] THEN
ASM_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Subwords, where the (pos,len) argument is (lsb_position,length) *)
(* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -3149,6 +3181,16 @@ let WORD_SUBWORD_XOR = prove
REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_XOR] THEN
ONCE_REWRITE_TAC[BIT_GUARD] THEN CONV_TAC TAUT);;

let WORD_SUBWORD_NOT = prove
(`!(x:M word) pos len.
dimindex(:N) <= len /\ pos + len <= dimindex(:M)
==> word_subword (word_not x) (pos,len):N word =
word_not (word_subword x (pos,len))`,
REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_NOT] THEN
SIMP_TAC[ARITH_RULE `i < MIN m n <=> i < m /\ i < n`] THEN
REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[DE_MORGAN_THM] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Bit recursion equations for "linear" operations. *)
(* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -5901,6 +5943,22 @@ let WORD_JUSHR_CONV =
NUM_MOD_CONV) THENC
WORD_USHR_CONV;;

let WORD_JROL_CONV =
let pth = prove
(`word_jrol (word(NUMERAL m):N word) (word(NUMERAL n):N word) =
word_rol (word(NUMERAL m):N word) (val(word(NUMERAL n):N word))`,
REWRITE_TAC[word_jrol]) in
GEN_REWRITE_CONV I [pth] THENC RAND_CONV WORD_VAL_CONV THENC
WORD_ROL_CONV;;

let WORD_JROR_CONV =
let pth = prove
(`word_jror (word(NUMERAL m):N word) (word(NUMERAL n):N word) =
word_ror (word(NUMERAL m):N word) (val(word(NUMERAL n):N word))`,
REWRITE_TAC[word_jror]) in
GEN_REWRITE_CONV I [pth] THENC RAND_CONV WORD_VAL_CONV THENC
WORD_ROR_CONV;;

let WORD_JDIV_CONV =
let pth = prove
(`word_jdiv (word(NUMERAL m):N word) (word(NUMERAL n)) =
Expand Down Expand Up @@ -5979,6 +6037,8 @@ let WORD_RED_CONV =
`word_jshl (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHL_CONV;
`word_jshr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHR_CONV;
`word_jushr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JUSHR_CONV;
`word_jrol (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROL_CONV;
`word_jror (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROR_CONV;
`word_jdiv (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JDIV_CONV;
`word_jrem (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JREM_CONV]
(basic_net()) in
Expand Down
Loading

0 comments on commit 74560a4

Please sign in to comment.