Proving sizeOf lt for Int is the same as Int lt

Stream: lean4

[Anders Christiansen Sørby]

How can I prove this to create this range

theorem Int.sizeOf_lt: ∀ a b : Int, a < b → sizeOf a < sizeOf b := by eq_refl

def Int.range (start stop : Int) : List Int :=
  if h : start < stop then
    have : sizeOf (stop - (start + 1)) < sizeOf (stop - start) := by {
      apply Int.sizeOf_lt
      rw [
        Int.sub_eq_add_neg, Int.neg_add, ←Int.add_assoc,
        Int.sub_eq_add_neg, ←Int.sub_eq_add_neg, ←Int.sub_eq_add_neg
      ]
      apply Int.sub_lt_self (stop-start)
      apply Int.zero_lt_one
    }
    start :: range (start + 1) stop
  else
    []
termination_by range start stop => stop - start

[Anders Christiansen Sørby]

Isn't Int.sizeOf_lt pretty obvious?

[James Gallicchio]

unfortunately it is untrue:

theorem Int.sizeOf_lt: ∀ a b : Int, a < b → sizeOf a < sizeOf b := sorry
example : False := by
  have := Int.sizeOf_lt (-2) 1 (by decide)
  revert this; rw [imp_false, Nat.not_lt]
  decide

[James Gallicchio]

Maybe try Int.natAbs (stop - start) as the measure? There should be lemmas for then manipulating such terms correctly. The Int sizeOf instance seems to not be intended for general use.

[James Gallicchio]

(This seems like an easy footgun for beginners... @Mario Carneiro would it be reasonable to add a WF instance to Std with invImage Int.natAbs as the measure? I think that is what most people would expect the behavior to be here)

[Mario Carneiro]

I think those are the same?

[James Gallicchio]

I believe the sizeOf instance adds 1 for negations.

[Mario Carneiro]

it might add 1 in both cases but otherwise it should be the same

[James Gallicchio]

example : sizeOf (1 : Int) = 2 := by decide
example : sizeOf (-1 : Int) = 1 := by decide

[James Gallicchio]

:face_with_raised_eyebrow: which is NOT what I was expecting

[James Gallicchio]

(also the Int sizeOf has ~no lemmas in mathlib or std, whereas natAbs has many)

[Mario Carneiro]

oh right of course, -1 is negSucc 0 so it has size 0 + 1

[James Gallicchio]

I keep forgetting we don't use one of the fancy Z encodings from HoTT >_>

[Mario Carneiro]

I think it would be best not to try to guess a measure here

[Mario Carneiro]

The example above actually wants toNat (stop - start) not natAbs (stop - start) as the measure

[Mario Carneiro]

which is the same as subNatNat stop start

[Henrik Böving]

James Gallicchio said:

unfortunately it is untrue:

theorem Int.sizeOf_lt: ∀ a b : Int, a < b → sizeOf a < sizeOf b := sorry
example : False := by
  have := Int.sizeOf_lt (-2) 1 (by decide)
  revert this; rw [imp_false, Nat.not_lt]
  decide

could slimcheck have falsified this?

[Mario Carneiro]

sizeOf is not computable so maybe not

[James Gallicchio]

My gut says either toNat or natAbs would be better than the status quo with it defaulting to sizeOf. Either toNat or natAbs work in Anders' case since we have start < stop, and most use cases are going to be in the same boat.

[Mario Carneiro]

import Mathlib.Util.CompileInductive
import Mathlib.Tactic.SlimCheck

compile_inductive% Int

theorem Int.sizeOf_lt: ∀ a b : Int, a < b → sizeOf a < sizeOf b := by slim_check
-- ===================
-- Found problems!
-- a := -1
-- b := 0
-- guard: -1 < 0
-- issue: 1 < 1 does not hold
-- (0 shrinks)
-- -------------------

[Henrik Böving]

huzzah

[Mario Carneiro]

James Gallicchio said:

My gut says either toNat or natAbs would be better than the status quo with it defaulting to sizeOf. Either toNat or natAbs work in Anders' case since we have start < stop, and most use cases are going to be in the same boat.

No defaulted sizeOf would help here, because the definition is not decreasing on start or stop or (start, stop)

[Mario Carneiro]

so you need to give a termination_by anyway, and in that case you can choose to use a useful measure

[Mario Carneiro]

The builtin decreasing tactics are structured to work well on the compiler-generated sizeOf. If that doesn't work, then just specify your own termination measure and ignore sizeOf entirely

[James Gallicchio]

I guess my discomfort is because anders' code has a termination_by measure, but the sizeOf was still inserted into that measure because of the default WellFoundedRelation:

instance (priority := low) [SizeOf α] : WellFoundedRelation α :=
  sizeOfWFRel

which seems like an easy footgun to overlook here.

[Mario Carneiro]

I think anders' code should be treated as incorrect, the integers are not well founded

[Mario Carneiro]

it's just unfortunate that because termination checking in lean is a ball of heuristics we can't just come out and say that, and instead we give some misleading hints relating to the compiler-internal sizeOf function

[James Gallicchio]

Is that default WFR instance used extensively?

[James Gallicchio]

I'm wondering if maybe it leads to more confusion than it is worth..??

[Mario Carneiro]

well of course, it is used by termination proofs when you don't use termination_by at all

[James Gallicchio]

hm. unfortunate.

[Mario Carneiro]

removing that instance (and the default SizeOf instance that sets everything to 1) would mean that not finding an instance is a new failure mode of definitions, which is something we would have to explain and I'm not sure that's better than the status quo

[Anders Christiansen Sørby]

How do I show 0 < stop -start when I already have start < stop? And why is showing something so trivial so complex? Shouldn't there be tactics and lemmas that solve these pretty easily?

open Int in
def Int.range (start stop : Int) : Array Int :=
  if h : start < stop then
    have : natAbs (stop - (start + 1)) < natAbs (stop - start) := by {
      rw [
        Int.sub_eq_add_neg, Int.neg_add, ←Int.add_assoc,
        Int.sub_eq_add_neg, ←Int.sub_eq_add_neg, ←Int.sub_eq_add_neg
      ]
      have h3 : 0 < stop - start := by apply ←Int.lt_of_sub_pos stop start;apply h
      generalize stop - start = a
      apply ←h -- here I want to be able to replace 0 <= a -> natAbs a = a
      apply Int.natAbs_lt_natAbs_of_nonneg_of_lt
      apply Int.sub_lt_self a
      apply Int.zero_lt_one
    }
    #[start] ++ (range (start + 1) stop)
  else
    #[]
termination_by range start stop => natAbs (stop - start)

[Mario Carneiro]

docs#Int.sub_pos_of_lt

[Mario Carneiro]

if you are using mathlib, then yes there are things like linarith that will take care of problems like this

[Anders Christiansen Sørby]

I'm not using mathlib currently. Just Std. I'm trying to make a game.

[Mario Carneiro]

Here's a simpler (and faster) implementation which avoids the need for a messy termination proof:

def Int.range (start stop : Int) : Array Int :=
  let rec go
    | 0, _, arr => arr
    | n+1, start, arr => go n (start + 1) (arr.push start)
  let n := (stop - start).toNat
  go n start (Array.mkEmpty n)

[Anders Christiansen Sørby]

Thanks

[Kim Morrison]

@Anders Christiansen Sørby these sorts of things work out of the box via omega:

import Std.Tactic.Omega.Frontend

example (x y : Int) (h : x < y) : 0 < y - x := by omega
example (x y : Int) (h : x < y) : Int.natAbs (y - (x + 1)) < Int.natAbs (y - x) := by omega