Beginner question: proofs involving Nat->Int conversions

Stream: new members

[Zack Weinberg]

Consider this pair of theorems:

theorem A (a b : Int)
  : a - b < 0 ↔ a < b
  := by
  apply Iff.intro
  . intro hl
    apply Int.lt_of_sub_neg
    exact hl
  . intro hr
    apply Int.sub_neg_of_lt
    exact hr

theorem B (a b: Nat)
  : (Int.ofNat a) - (Int.ofNat b) < 0 ↔ a < b
  := by
  apply Iff.intro
  . intro hl
    apply Int.lt_of_sub_neg
    exact hl
  . intro hr
    apply Int.sub_neg_of_lt
    exact hr

I doubt that's the most elegant way to prove A but that's not the key issue (although I'd happily take advice re cleaner ways to prove it, and yes, I know it's probably a lemma somewhere). The key issue is that it seems to me the exact same proof should apply to B, because (Int.ofNat α) is an Int. But the first case fails at apply Int.lt_of_sub_neg with

tactic 'apply' failed, failed to unify
  ?a < ?b
with
  a < b
case mp
a b : Nat
hl : ofNat a - ofNat b < 0
⊢ a < b

and I don't understand why.

The second case fails in a more explicable way: hr: a < b is not an exact match for ⊢ ofNat a < ofNat b. I can rescue this by inserting a simp before exact hr, but I don't know how simp manages to rewrite ofNat a < ofNat b into a < b and therefore I am uncomfortable leaving it so. Relatedly, inserting a simp at the beginning of the process

theorem C (a b: Nat)
  : (Int.ofNat a) - (Int.ofNat b) < 0 ↔ a < b
  := by
  simp
  apply Iff.intro
  -- etc

does something else I don't understand: it turns ⊢ ofNat a - ofNat b < 0 ↔ a < b into ⊢ ↑a - ↑b < 0 ↔ a < b. I have no idea what the up-arrows mean and cannot even figure out how to search for an explanation in the manual.

Any/all advice would be appreciated, except please don't tell me I should use mathlib, because I can't use mathlib, because of <https://github.com/leanprover-community/ProofWidgets4/issues/115>. Thanks in advance.

[Bolton Bailey]

apply Int.lt_of_sub_neg fails here because the conclusion of that theorem is a statement about integers and your goal is a statement about naturals. You will probably need Int.ofNat_lt

[Bolton Bailey]

Here is one way to prove B, for example:

theorem A (a b : Int)
  : a - b < 0 ↔ a < b
  := by
  apply Iff.intro
  . intro hl
    apply Int.lt_of_sub_neg
    exact hl
  . intro hr
    apply Int.sub_neg_of_lt
    exact hr

theorem B (a b: Nat)
  : (Int.ofNat a) - (Int.ofNat b) < 0 ↔ a < b
  := by
  rw [A]
  apply Iff.intro
  · intro h
    exact Int.ofNat_lt.mp h
  · intro h
    exact Int.lt_of_toNat_lt h

[Notification Bot]

12 messages were moved from this topic to #new members > Installing lean from a linux distro by Eric Wieser.