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