Porting Nat.mod_def

Stream: mathlib4

[Eric Wieser]

Well I can't get the · to work in lean/Init/Data/Nat/Div.lean

[Notification Bot]

20 messages were moved here from #mathlib4 > Data.Fin.Basic (mathlib4#1084) by Eric Wieser.

[Eric Wieser]

I'm still confused by why the · syntax isn't working for me; is there a non-unicode alternative I can use to focus goals?

[Reid Barton]

.

[Eric Wieser]

I still get expected command

[Eric Wieser]

For code like

        cases x
        . sorry
        . sorry

[Eric Wieser]

It works fine without the .s and the space after them

[Reid Barton]

cases'? this isn't really how Lean 4 cases is meant to be used I think

[Eric Wieser]

Not available in the file I'm in

[Mario Carneiro]

it might be that . isn't available in that file? I forget if it is defined in stage 0 or stage 1

[Eric Wieser]

I just reproved it from scratch, it was easier:

private theorem mod_core_congr {x y f1 f2} (h1 : x ≤ f1) (h2 : x ≤ f2) :
    Nat.modCore y f1 x = Nat.modCore y f2 x :=
  by
    induction f1 generalizing x f2 with
    | zero =>
      cases h1
      clear h2
      induction f2 with
      | zero => rfl
      | succ f2 ih =>
        rw [Nat.modCore, Nat.modCore, Nat.zero_sub, ←ih, Nat.modCore, ite_self]
    | succ f1 ih =>
      rw [Nat.modCore]
      induction f2 generalizing f1 with
      | zero =>
        cases h2
        rw [Nat.modCore, Nat.zero_sub, ih (Nat.zero_le _) (Nat.zero_le _), Nat.modCore,
          ite_self]
      | succ f2 ih2 =>
        rw [Nat.modCore]
        refine' ite_congr rfl (fun h => _) (fun _ => rfl)
        cases x with
        | zero => cases Nat.lt_of_lt_of_le h.1 h.2
        | succ x => cases y with
          | zero => cases h.1
          | succ y =>
            simp only [succ_sub_succ]
            exact ih
              (Nat.le_trans (Nat.sub_le _ _) (le_of_succ_le_succ h1))
              (Nat.le_trans (Nat.sub_le _ _) (le_of_succ_le_succ h2))

theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
  show Nat.modCore y x x = if 0 < y ∧ y ≤ x then Nat.modCore y (x - y) (x - y) else x
  cases x with
  | zero =>
    cases y with
    | zero => rfl
    | succ y =>
      rw [Nat.zero_sub, Nat.modCore, ite_self]
  | succ x =>
    cases y with
    | zero => rfl
    | succ y =>
      refine' ite_congr rfl (fun _ => mod_core_congr _ (Nat.le_refl _)) (fun _ => rfl)
      rw [Nat.succ_sub_succ]
      exact Nat.sub_le _ _