-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refactor: bundle wn
and wr
into DivModState
#21
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@bollu I also made some naming changes as I went along, I'm marking them with comments so you know to make those changes to the main PR even if we decide against merging this one
src/Init/Data/BitVec/Bitblast.lean
Outdated
rw [Nat.shiftRight_eq_div_pow] | ||
apply Nat.div_eq_of_lt n.isLt | ||
} | ||
def DivModState.Lawful.init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
def DivModState.Lawful.init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) : | |
def DivModState.lawful_init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) : |
divRec m args (divSubtractShift args qr) := rfl | ||
|
||
/-- The output of `divRec` is a lawful state -/ | ||
theorem lawful_divRec {args : DivModArgs w} {qr : DivModState w} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I decided to rename this from the somewhat ambiguous "correct" to "lawful"
src/Init/Data/BitVec/Bitblast.lean
Outdated
@@ -671,13 +690,14 @@ private theorem two_mul_add_sub_lt_of_lt_of_lt_two (h : a < x) (hy : y < 2) : | |||
|
|||
/-- We show that the output of `divSubtractShift` is lawful, which tells us that it | |||
obeys the division equation. -/ | |||
def divSubtractShiftProof (qr : DivModState w) (h : qr.Poised wr wn n d) : | |||
DivModState.Lawful w (wr + 1) (wn - 1) n d (divSubtractShift n d wn qr) := by | |||
def lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not a fan of divSubtractShiftProof
as a name, so I renamed it to lawful_...
@bollu: I didn't really like how
Lawful
had so many parameters flying about, and in particular, how it's basically impossible to tell what, say,Lawful w w 0 n d qr
means.So, I made a refactor to bundle
wn
andwr
as fields of theDivModState
(I'm a huge fan of this, it makes stuff much easier to read!), and while I was at it, also bundledn
andd
into aDivModArgs
struct (this one I think is an improvement overall, but a much less clearcut one: it does make some call sites look a bit awkward).Anyway, It's a pretty big refactor, hence the PR to your PR (the base branch of this one is the upstream PR).