Commit 2025-11-24 15:41 be57e00e

View on Github →

refactor(Nat/Log): redefine Nat.log and Nat.clog (#31990) Redefine Nat.log similarly to what Nat.logC used to use, but with fuel recursion instead of well-founded recursion. This way the definition is useful both for #eval/native_decide and for #reduce/decide. Also, refactor Nat.clog in a similar way. While the old definitions were more readable, they did not carry any nice defeq properties.

Estimated changes

added theorem Nat.clog.go_spec
modified def Nat.clog
added theorem Nat.clog_le_of_le_pow
added theorem Nat.clog_of_one_lt
modified theorem Nat.clog_pos
added theorem Nat.log.go_spec
modified def Nat.log
deleted def Nat.logC
deleted theorem Nat.log_eq_logC
modified theorem Nat.log_lt_iff_lt_pow
added theorem Nat.log_lt_of_lt_pow'
modified theorem Nat.log_of_left_le_one
modified theorem Nat.log_of_lt
added theorem Nat.pow_lt_of_lt_clog