Zulip Chat Archive
Stream: new members
Topic: Problem converting between PartENat and Nat
Tony Ma (Dec 09 2024 at 04:45):
The goal I would like to prove is
import Mathlib
open multiplicity Nat
example : (multiplicity 2 (factorial 16)) % 10 = 5 := by sorry
However, it appears to "fail to synthesize HMod PartENat ℕ PartENat".
My first question is, is there a way to create impicit goal, so I could write something like (multiplicity 2 (factorial 16)).get ?_ % 10 = 5
?
And the second question is my unsuccessful conversion between PartENat and Nat. I compromised for the moment to change the goal to multiplicity 2 (factorial 16) = 15
and tried to write the proof as follows:
example : multiplicity 2 (factorial 16) = 15 := by
have h₁ : multiplicity.Finite 2 (Nat.factorial 16) := by
refine multiplicity.finite_nat_iff.mpr ⟨show 2 ≠ 1 by norm_num, Nat.factorial_pos 16⟩
have h₂ : (2 - 1) * (multiplicity 2 (factorial 16)).2 h₁ = 16 - (Nat.digits 2 16).sum := by
apply Prime.sub_one_mul_multiplicity_factorial
exact Nat.prime_two
rw [show (Nat.digits 2 16).sum = 1 by native_decide] at h₂
ring_nf at h₂
What is the way to prove multiplicity 2 16! = 15
(both sides are of type PartENat
) from (multiplicity 2 16!).get h₁ = 15
? And what is a better practice to write the proof (I found it a bit weird after writing out).
Daniel Weber (Dec 09 2024 at 08:30):
What Mathlib version are you in? docs#multiplicity was (somewhat recently) changed to be Nat-valued, so PartENat
shouldn't appear here
Daniel Weber (Dec 09 2024 at 08:35):
import Mathlib
open multiplicity Nat
example : (multiplicity 2 (factorial 16)) % 10 = 5 := by
rw [← padicValNat_def']
· rw [padicValNat_factorial (b := 5)]
· decide
· apply Nat.log_lt_of_lt_pow <;> decide
· decide
· apply factorial_pos
works on the current version
Tony Ma (Dec 09 2024 at 10:47):
I see. I think I am using a version of Nov, 2024, but I ain't quite sure how to get it. So does Lean supports something like implicit goal (as described in my previous comment)?
Matt Diamond (Dec 09 2024 at 18:21):
@Tony Ma What would an implicit goal of (multiplicity 2 (factorial 16)).get ?_ % 10 = 5
actually mean as a proposition?
Daniel Weber (Dec 09 2024 at 18:35):
I strongly recommend upgrading Mathlib, PartENat
is a pain to work with
Tony Ma (Dec 11 2024 at 06:45):
Matt Diamond 发言道:
Tony Ma What would an implicit goal of
(multiplicity 2 (factorial 16)).get ?_ % 10 = 5
actually mean as a proposition?
I am considering to do this stuff by
import Mathlib
open multiplicity Nat
lemma lm : multiplicity.Finite 2 (Nat.factorial 16) := by sorry
example : (multiplicity 2 (factorial 16)).get lm % 10 = 5 := by sorry
So I wonder if I could directly have (multiplicity 2 (factorial 16)).get ?_ % 10 = 5
and LEAN help me to figure out this implicit goal.
Tony Ma (Dec 11 2024 at 06:47):
Daniel Weber 发言道:
I strongly recommend upgrading Mathlib,
PartENat
is a pain to work with
I see. I have to use this version for this moment for some particular reason. But thanks for your comment! That's also how I think of it.
Daniel Weber (Dec 11 2024 at 07:07):
You can try using padicValNat_def
to get out of PartENat, but I don't recall its old definition
Last updated: May 02 2025 at 03:31 UTC