Double-casting

Stream: mathlib4

[Sorrachai Yingchareonthawornchai]

I encounter a double-casting situation. How do I close this goal? Here, a is in Z, and ↑a⁺ is Fin n, and ↑↑a⁺ is Nat
a : ℤ
hha : a ≤ 0
⊢ ↑↑a⁺ = 0

simp [hha, posPart_eq_zero] does not work

[Julian Berman]

It's a bit easier to help if you include a #mwe.

[Sorrachai Yingchareonthawornchai]

Sure, here it is:

import Mathlib

theorem extracted_1 (n : ℕ) [inst : NeZero n] (a : ℤ) (ha : 1 ≤ ↑n + a) (hb : a ≤ ↑n - 1) (hha : a ≤ 0) :
  ↑↑a⁺ = 0 := sorry

[Yury G. Kudryashov]

This is not an #mwe that I can copy+paste, then try to prove. You need to add explicit type annotations to make sure it parses correctly.

[Yury G. Kudryashov]

Someting like (((a⁺ : Int) : Fin n) : Nat) = 0

[Yury G. Kudryashov]

You can start with

  rw [← Fin.val_zero' n, Fin.val_inj, Fin.natCast_eq_zero]

[Yury G. Kudryashov]

This way you'll no longer have Fin n.

[Yury G. Kudryashov]

Wait, you have a ≤ 0, so posPart a = 0, right?

[Sorrachai Yingchareonthawornchai]

yes

[Yury G. Kudryashov]

  simp [posPart_eq_zero.2 hha]

should work (not tested)

[Sorrachai Yingchareonthawornchai]

that works thanks. (What is posPart_eq_zero.2?)

[Yury G. Kudryashov]

It selects the right-to-left implication from posPart_eq_zero.

[Yury G. Kudryashov]

A more readable version:

  have : a⁺ = 0 := by rwa [posPart_eq_zero]
  simp [this]

[Sorrachai Yingchareonthawornchai]

Thanks a lot

[Sorrachai Yingchareonthawornchai]

x1 : ℤ
x2 : ℤ
hfxn : ↑x1 = ↑x2
⊢ x1 = x2

In hfxn, the integers are casted to Fin n (i.e., @Int.cast (Fin n) AddGroupWithOne.toIntCast x1 : Fin n)
How to remove the cast at hfxn?

[Edward van de Meent]

i don't think this is true? for example, consider what might happen when x1=0 and x2=n?

[Sorrachai Yingchareonthawornchai]

Thanks. The context is :

s : Finset ℤ := Icc (-↑n + 1) (↑n - 1)
x1 : ℤ
hx1 : x1 ∈ s
x2 : ℤ
hx2 : x2 ∈ s
x1le0 : x1 ≤ 0
x2le0 : x2 ≤ 0
hfxn : ↑x1 = ↑x2
⊢ x1 = x2

[Edward van de Meent]

rather than copy-pasting the context, please provide a #mwe

[Sorrachai Yingchareonthawornchai]

Is this one okay?

import Mathlib

example  (n : ℕ )[NeZero n] :=
  let s : Finset ℤ := Finset.Icc (-n + 1) (n - 1)
  let f :  ℤ → Fin n × Fin n  := fun (i) ↦ ( ↑(i⁺) , ↑(i⁻))
  have f_inj : Set.InjOn f ↑s := by
    simp  [Set.InjOn]
    intro x1 hx1 x2 hx2 hfx
    simp [f] at hfx
    obtain ⟨hfxp, hfxn⟩ := hfx
    obtain x1le0 | x1g0 := le_total x1 0
    obtain x2le0 | x2g0 := le_total x2 0
    have t1: x1⁺ = 0 := by rwa [posPart_eq_zero]
    have t2: x2⁺ = 0 := by rwa [posPart_eq_zero]
    have t1n: x1⁻  = -x1 := by rwa [negPart_eq_neg]
    have t2n: x2⁻  = -x2 := by rwa [negPart_eq_neg]
    rw [t1n,t2n] at hfxn
    simp at hfxn
    sorry

[Yaël Dillies]

@Sorrachai Yingchareonthawornchai, using #17061 and #17063, you can do

import Mathlib.Algebra.CharP.Defs
import Mathlib.Algebra.Order.Group.PosPart
import Mathlib.Data.ZMod.Defs

open Set

example (n : ℕ) [NeZero n] :
    InjOn (fun z : ℤ ↦ ((↑(z⁺), ↑(z⁻)) : Fin n × Fin n)) (Ioo (-n) n) :=
  ((CharP.intCast_injOn_Ico _ n).prodMap (CharP.intCast_injOn_Ico _ n)).comp
    posPart_negPart_injective.injOn fun z hz ↦
    ⟨⟨posPart_nonneg _, by simpa [NeZero.pos] using hz.2⟩,
      ⟨negPart_nonneg _, by simpa [NeZero.pos] using hz.1⟩⟩

[Sorrachai Yingchareonthawornchai]

Thanks. Should I wait for the new update from #17061 and #17063 ?

[Yaël Dillies]

Maybe someone will get them merged quickly? :wink:

[Yury G. Kudryashov]

Merged, delegated