reduce

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.XgcdType.reduce

Lean4

/-- We can now define the full reduction function, which applies
step as long as possible, and then applies finish. Note that the
"have" statement puts a fact in the local context, and the
equation compiler uses this fact to help construct the full
definition in terms of well-founded recursion.  The same fact
needs to be introduced in all the inductive proofs of properties
given below. -/
def reduce (u : XgcdType) : XgcdType :=
  dite (u.r = 0) (fun _ => u.finish) fun _h => flip (reduce u.step)
decreasing_by apply u.step_wf _h

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru