Int/Nat casting

Stream: new members

[Archibald Neil MacDonald]

Apologies for the newbie question. Any good resources on Nat/Int casting in lean4? I have:

theorem nat_is_even_or_odd (k : Nat) :  Even k ∨ Odd k

And I want to apply it to:

theorem int_is_even_or_odd (k : Int) :  Even k ∨ Odd k

But I'm not having much success in being able to write the Int definition in terms of the Nat definition.

[Yaël Dillies]

Do you know how to mathematically prove that nat_is_even_or_odd implies int_is_even_or_odd?

[Archibald Neil MacDonald]

In my head it should be trivial for the positive case, then use Odd.add_odd and Even.odd_add to massage out the additional +1's in the negative case?

[Yaël Dillies]

Okay, so you said something important here! You need to consider the positive and negative cases separately. Do you know how to do that in Lean?

[Kevin Buzzard]

In particular this is not just a question about casting, there is some mathematics which needs doing here.

[Archibald Neil MacDonald]

So far I'm trying:

theorem int_is_even_or_odd (k : Int) :  Even k ∨ Odd k := by
  match k with
  | .ofNat k => ...
  | .negSucc k => ...

And I'm not able to deal with the first arm as I'm getting stuck in trying to make ofNat behave.

[Yaël Dillies]

So now you need to prove things of the form Even n → Even (Int.ofNat n). Do you know how to do that?

[Archibald Neil MacDonald]

No that's something I'm hitting my head against the wall here!

[Kevin Buzzard]

My instinct would be not to go down this route: .negSucc is a pathological function mathematically with very little API (for example mathematicians have no name for this function, and hence have no desire to develop it). I would be more inclined to prove Even k <-> Even k.natAbs and then this would reduce you directly to the Nat case and you'll not have to deal with the +1 issues.

[Yaël Dillies]

Kevin, I agree, but I think it's instructive to keep on going here

[Yaël Dillies]

Once Archibald is done with the first arm, we can use the mathematically correct case principle for Int rather than the default one

[Kevin Buzzard]

Answering your question: I'd do it like this.

import Mathlib.Tactic

example (n : ℕ) (h : Even n) : Even (n : ℤ) := by exact?

[Kevin Buzzard]

But my point is that if the goal is to deduce int_is_even_or_odd from nat_is_even_or_odd then I think that this entire route is a red herring and the sensible route is

example (z : ℤ) : Even z ↔ Even (z.natAbs) := by exact?

i.e. "Don't split into cases at all, just take the absolute value"

[Eric Wieser]

Maybe docs#Int.induction_on ?

[Kevin Buzzard]

I don't see how this induction principle will help with reducing the int case to the nat case (but I totally agree that it's a far better induction principle than the default one!)

[Yaël Dillies]

We need docs#Int.sign_cases but it doesn't seem to exist

[Eric Wieser]

docs#Int.eq_nat_or_neg is close, but it ought to be an induction principle

[Archibald Neil MacDonald]

Sorry I had to step away. Thanks for the replies all, I was not aware of exact? so thanks for that. I'm taking a look at the source code and understand how the implementers are approaching the same proofs.

[Archibald Neil MacDonald]

Thanks for the input all.

On the same topic of int/nast casting, I have this lemma, where I'm trying to derive int_k2_mod8_eq_1 from nat_k2_mod8_eq_1. The explicit 8 cast makes me think I'm not doing this right at all, is there a better way to cast here?

lemma nat_k2_mod8_eq_1 (k : Nat) : Odd k -> (k^2) % 8 = 1 := ...

lemma int_k2_mod8_eq_1 (k : Int) : Odd k -> (k^2) % 8 = 1 := by
  intro hOdd
  rw [ ← Int.natAbs_pow_two
     , ← Int.natCast_pow
     , show (8 : Int)  = (8 : Nat) by rfl
     , Int.ofNat_mod_ofNat _ 8]
  rw [nat_k2_mod8_eq_1]; simp;
  rw [Int.natAbs_odd]; exact hOdd;

[Kevin Buzzard]

I guess one could step back and ask why you're trying to deduce a theorem about integers from a related but different theorem about naturals when you could just prove the integer case directly and perhaps with less work than deducing it from the natural case. You keep asking about casting, but casting would be deducing the natural case from the integer case.

[Archibald Neil MacDonald]

It's a fair question; as a beginner solving this for Nats is achievable for me; I don't know how to do inductive proofs on integers in lean without going into the constructors I've been told to avoid, or bounds check against the negative case in match blocks.

[Archibald Neil MacDonald]

Also I'm perhaps incorrectly thinking "this is a natural-numbers proof and the int proof should follow."

[Kevin Buzzard]

You can just prove it directly with no induction:

import Mathlib.Tactic

lemma int_k2_mod8_eq_1 (k : ℤ) : Odd k → (k^2) % 8 = 1 := by
  rintro ⟨w, rfl⟩ -- k=2w+1
  rcases Int.even_or_odd w with ⟨x, rfl⟩ | ⟨x, rfl⟩ -- w=2x or 2x+1
  · have : (1 + 8 * (x + 2 * x^2)) % 8 = 1 := by simp
    convert this; ring
  · have : (1 + 8 * (1 + 3 * x + 2 * x^2)) % 8 = 1 := by simp
    convert this; ring

For me that's the easiest proof because it just writes itself; every odd k is either 4x+1 or 4x+3 and in both cases it's just a direct calculation to show that the square is 1 mod 8.

[Archibald Neil MacDonald]

Cheers Kevin, seems a lot more elegant than my own attempts. There's some keywords I'm not too familiar with, so that's a big help in pointing out the gaps in my knowledge.

[Kevin Buzzard]

Here's a proof using your idea of going through Nat. We're fortunate that Odd k iff Odd k.natAbs and k^2 = (k.natAbs)^2 are both in the library. The norm_cast tactic is something you could be interested in.

import Mathlib.Tactic

lemma nat_k2_mod8_eq_1 (k : Nat) : Odd k -> (k^2) % 8 = 1 := sorry

lemma int_k2_mod8_eq_1 (k : Int) : Odd k -> (k^2) % 8 = 1 := by
  intro hOdd
  rw [ ← Int.natAbs_pow_two]
  have foo : Odd (k.natAbs) := by exact Odd.natAbs hOdd
  have bar := nat_k2_mod8_eq_1 _ foo
  norm_cast -- goal is bar modulo casts

[Kevin Buzzard]

golfing:

import Mathlib.Tactic

lemma nat_k2_mod8_eq_1 (k : Nat) : Odd k -> (k^2) % 8 = 1 := sorry

lemma int_k2_mod8_eq_1 (k : Int) : Odd k -> (k^2) % 8 = 1 := by
  intro hOdd
  rw [ ← Int.natAbs_pow_two]
  exact_mod_cast nat_k2_mod8_eq_1 _ <| Odd.natAbs hOdd

[Kevin Buzzard]

more golfing:

import Mathlib.Tactic

lemma nat_k2_mod8_eq_1 {k : Nat} : Odd k -> (k^2) % 8 = 1 := sorry

lemma int_k2_mod8_eq_1 {k : Int} (hOdd : Odd k) : (k^2) % 8 = 1 := by
  rw [ ← Int.natAbs_pow_two]
  exact_mod_cast nat_k2_mod8_eq_1 <| Odd.natAbs hOdd

[Michael Stoll]

Here is a variant using ZMod 8:

import Mathlib

lemma aux : ∀ a : ZMod 8, (2 * a + 1) ^ 2 = 1 := by decide

example (x : ℤ) : Odd x → (x ^ 2) % 8 = 1 := by
  rintro ⟨y, rfl⟩
  have := aux y
  norm_cast at this
  nth_rw 2 [show (1 : ℤ) = 1 % 8 from rfl]
  refine Int.ModEq.eq ?_
  rwa [show (8 : ℤ) = (8 : ℕ) from rfl, ← ZMod.int_cast_eq_int_cast_iff]

(It would be nice to be able to go more directly between a % 8 = 1 and an equality in ZMod 8 ...)

[Kevin Buzzard]

The price we pay of having three ways % and _ ≡ _ [ZMOD n] and ZMod n to say basically the same thing is that we need good API to move between all three of these things. I agree that it's frustrating that half your proof is moving from (z : ZMod 8) = 1 to z % 8 = 1.

[Michael Stoll]

Yeah, I would argue that stating these in terms of equalities in ZMod n is actually the best way, and so it should be easy to convert to and from this...

[Michael Stoll]

Slightly golfed:

import Mathlib

lemma aux : ∀ a : ZMod 8, (2 * a + 1) ^ 2 = 1 := by decide

example (x : ℤ) : Odd x → (x ^ 2) % 8 = 1 := by
  rintro ⟨y, rfl⟩
  have := aux y
  norm_cast at this
  nth_rw 2 [show (1 : ℤ) = 1 % 8 from rfl]
  exact Int.ModEq.eq <| (ZMod.int_cast_eq_int_cast_iff _ 1 8).mp this

[Michael Stoll]

A bit more principled, but still somewhat painful:

import Mathlib

lemma aux : ∀ a : ZMod 8, (2 * a + 1) ^ 2 = 1 := by decide

example (x : ℤ) : Odd x → (x ^ 2) % 8 = 1 := by
  rintro ⟨y, rfl⟩
  have := aux y
  norm_cast at this
  apply_fun ZMod.val at this
  apply_fun ((↑) : ℕ → ℤ) at this
  have inst : Fact (1 < 8) := ⟨by norm_num⟩ -- needed for `ZMod.val_one`
  rwa [ZMod.val_int_cast, ZMod.val_one, Int.Nat.cast_ofNat_Int] at this