BinaryFactorial.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RationalHitting.StackLanguage.gcdBody line 8
def OAI.RationalHitting.StackLanguage.gcdLoop line 10
def OAI.RationalHitting.StackLanguage.gcdScratch line 12
lemma OAI.RationalHitting.StackLanguage.eval_gcdBody line 14
lemma OAI.RationalHitting.StackLanguage.gcd_product_halving line 55
Source documentation
Euclid's product is halved at every ordered step.
```
lemma gcd_product_halving {a b : ℕ} (ha : 0<a) (hab : a≤b) :
    2*(a*(b%a)) ≤ a*b := by
…
```
lemma OAI.RationalHitting.StackLanguage.eval_gcdLoop_ordered line 64
lemma OAI.RationalHitting.StackLanguage.eval_gcdLoop line 122
Source documentation
No value-sized fuel: the compiler executes an ordinary while loop, and Euclid's product-halving supplies a bound linear in the input bit lengths.
```
lemma eval_gcdLoop (s : Store (Fin 10)) (hs : gcdScratch s)
    (hcan0 : (wordValue (s 0)).bits=s 0) (hcan5 : (wordValue (s 5)).bits=s 5)
    (B : ℕ) (h0 : (s 0).length≤B) (h5 : (s 5).length≤B) :
    ∃ t ≤ (2*B+1)*(500*(B+1)^2+1)+1,
      Eval gcdLoop s (update (update s 0 (Nat.gcd (wordValue (s 0)) (wordValue (s 5))).bits) 5 []) t := by
…
```
Mentions: OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.gcdScratch, OAI.RationalHitting.StackLanguage.wordValue, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.gcdLoop
def OAI.RationalHitting.StackLanguage.quotient line 172
Source documentation
Destructive exact binary quotient, retaining its positive denominator.
```
def quotient : Program (Fin 10) := .seq divide (.seq (copy 7 0 9) (clear 7))
```
Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.divide, OAI.RationalHitting.StackLanguage.copy, OAI.RationalHitting.StackLanguage.clear
lemma OAI.RationalHitting.StackLanguage.eval_quotient line 174
def OAI.RationalHitting.StackLanguage.fractionArith line 207
Source documentation
Extra work registers for retaining numerator and denominator through Euclid.
```
def fractionArith : Fin 10 ↪ Fin 12 :=
…
```
lemma OAI.RationalHitting.StackLanguage.fractionArith_val line 210
def OAI.RationalHitting.StackLanguage.fractionScratch line 212
lemma OAI.RationalHitting.StackLanguage.fractionScratch_gcd line 215
lemma OAI.RationalHitting.StackLanguage.eval_fractionGcd line 223
lemma OAI.RationalHitting.StackLanguage.eval_fractionQuotient line 236
lemma OAI.RationalHitting.StackLanguage.fractionScratch_update line 248