4.6. Proofs about particular values🔗

Lean's kernel can evaluate Hex.Modular.symMod and Hex.Modular.Crt.push. In compiled code push uses GMP's extended Euclidean algorithm, and in the kernel it uses a version written in Lean that is proved equal to it. So decide +kernel proves statements about particular Chinese remainder computations:

example : sunzi.map (·.value) = some 23 := by⊢ Option.map (fun x => x.value) sunzi = some 23
  decide +kernelAll goals completed! 🐙

The definition of ratRecon? is deliberately not exposed to the kernel, which would otherwise have to run the Euclidean algorithm. Its check Hex.Modular.ratReconCheck is exposed, and together with ratRecon?_complete it proves what ratRecon? returns without running the Euclidean algorithm in the kernel:

example : ratRecon? 68 101 7 7 = some (2 / 3) :=
  ratRecon?_complete (by⊢ 2 * 7 * 7 < ↑101 decideAll goals completed! 🐙)
    (by⊢ (Int.ofNat (2 / 3).den * 68 - (2 / 3).num) % ↑101 = 0 decide +kernelAll goals completed! 🐙) (by⊢ ↑(2 / 3).num.natAbs ≤ 7 ∧ ↑(2 / 3).den ≤ 7 decide +kernelAll goals completed! 🐙)