Proving cong_arg for function of arity 2

Stream: general

[Ben]

I have the following function (that sort of represents natural number subtraction/difference)

def reduce : Nat → Nat → Nat × Nat
  | .succ n1, .succ n2 => reduce n1 n2
  | 0, .succ n2 => (0, n2.succ)
  | .succ n1, 0 => (n1.succ, 0)
  | 0, 0 => (0, 0)

#eval reduce 5 2 -- (3, 0)
#eval reduce 10 8 -- (2, 0)
#eval reduce 10 6 -- (4, 0)
#eval reduce 16 12 -- (4, 0)
#eval reduce 8 10 -- (0, 2)

For a larger theorem I need to show that the fixing the left results in a function that does represent congruent argument. But am having a little problem with it. Any help appreciated

theorem reduce.of_zero (n m: Nat) (h1: n = 0 ∨ m = 0) : (reduce n m) = (n, m) := by
  cases h1 with
  | inl h2 => rw [h2]; induction m; rfl; rfl;
  | inr h2 => rw [h2]; induction n; rfl; rfl;

theorem reduce.left_zero (n: Nat) : reduce 0 n = (0, n) := reduce.of_zero _ n (Or.inl rfl)
theorem reduce.left_cong (a b c: Nat) : reduce a b = reduce a c → b = c := by
  intro h1
  -- want to do something like
  -- rw [congrArg] at h1
  induction a generalizing b with
  | zero => rw [reduce.left_zero, reduce.left_zero] at h1; exact (Prod.ext_iff.mp h1).right;
  | succ a ih => {
    sorry
  }

[Eric Wieser]

What you're describing is not "congruent argument", but injectivity

[Eric Wieser]

And unfortunately, the rewrite you want to do amounts to the statement you were trying to prove in the first place; so I think you need to rethink your proof strategy here!

[Eric Wieser]

I would guess you need to induct on b and c as well

[Kyle Miller]

Yeah, this is an injectivity theorem — the relationship is that injectivity theorems are converses of congruence theorems. Here's an approach:

def reduce : Nat → Nat → Nat × Nat
  | .succ n1, .succ n2 => reduce n1 n2
  | 0, .succ n2 => (0, n2.succ)
  | .succ n1, 0 => (n1.succ, 0)
  | 0, 0 => (0, 0)

theorem reduce_zero_left (a : Nat) : reduce a 0 = (a, 0) := by cases a <;> rfl
theorem reduce_zero_right (a : Nat) : reduce 0 a = (0, a) := by cases a <;> rfl

theorem swap_reduce (a b : Nat) : Prod.swap (reduce a b) = reduce b a := by
  induction a generalizing b with
  | zero => cases b <;> rfl
  | succ _ ih =>
    cases b
    · rfl
    · unfold reduce
      rw [ih]

theorem reduce_add_add (a b k : Nat) : reduce (a + k) (b + k) = reduce a b := by
  induction k with
  | zero => rfl
  | succ _ ih => exact ih

theorem reduce_of_le (a b : Nat) (h : a ≤ b) : reduce a b = (0, b - a) := by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  have := reduce_add_add 0 k a
  rw [Nat.zero_add, Nat.add_comm k] at this
  rw [this, reduce_zero_right, Nat.add_sub_cancel_left]

theorem reduce_of_ge (a b : Nat) (h : b ≤ a) : reduce a b = (a - b, 0) := by
  rw [← swap_reduce, reduce_of_le _ _ h]
  rfl

theorem reduce.left_inj (a b c : Nat) (h : reduce a b = reduce a c) : b = c := by
  obtain hb | hb := Nat.le_or_ge a b
    <;> obtain hc | hc := Nat.le_or_ge a c
    <;> simp [reduce_of_le, reduce_of_ge, hb, hc] at h
    <;> omega

[Kyle Miller]

These theorems let you prove the stronger property of reduce:

theorem reduce_eq_iff (a b a' b' : Nat) : reduce a b = reduce a' b' ↔ a + b' = b + a' := by
  obtain h1 | h1 := Nat.le_or_ge a b
    <;> obtain h2 | h2 := Nat.le_or_ge a' b'
    <;> simp [reduce_of_le, reduce_of_ge, h1, h2]
    <;> omega