Looks false to me, since `n2w a` can represent a negative number. The assumption `0 < a` doesn’t prevent this, you’d need `0w < n2w a` instead. Also, I think you’d need `a` to be strictly less than `m`. For example:
Q.prove( `0w < (n2w m : 'a word) /\ 0w < (n2w a : 'a word) /\ a < m /\ m < dimword(:'a) ==> (n2w m - n2w a :'a word) < n2w m`, rpt strip_tac \\ match_mp_tac wordsTheory.WORD_LT_SUB_UPPER \\ lfs [wordsTheory.word_lt_n2w] ) The original formulation makes more sense for unsigned less than? For example: Q.prove( `0 < a /\ a <= m /\ m < dimword(:'a) ==> (n2w m - n2w a :'a word) <+ n2w m`, rw_tac std_ss [GSYM wordsTheory.n2w_sub] \\ simp [wordsTheory.WORD_LO] ) Anthony > On 9 Feb 2016, at 00:28, Ramana Kumar <[email protected]> wrote: > > Scott informed me that it is likely false (e.g., take m = 1 and a = 2). I can > add additional assumptions that may help, though. > > Alternatively, I have a variant of the problem that looks like this: > > 0. m < dimword (:'a) > 1. a <= m > 2. 0 < m > 3. 0 < a > ---------------------------- > n2w m - n2w a < n2w m > > That one seems more likely to be true. But how to prove it? > > On 9 February 2016 at 10:02, Ramana Kumar <[email protected]> wrote: > Hi, > > Does anyone know whether the following goal is true or false? > > How would you prove it? > > If it's false, under what reasonable additional assumptions would it be true? > > 0. m < dimword (:α) > 1. m < a > 2. 0 < m > ------------------------------------ > n2w m − n2w a < n2w m > > Cheers, > Ramana > > ------------------------------------------------------------------------------ > Site24x7 APM Insight: Get Deep Visibility into Application Performance > APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month > Monitor end-to-end web transactions and take corrective actions now > Troubleshoot faster and improve end-user experience. Signup Now! > http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140_______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Site24x7 APM Insight: Get Deep Visibility into Application Performance APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month Monitor end-to-end web transactions and take corrective actions now Troubleshoot faster and improve end-user experience. Signup Now! http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
