wip: progress

src/Init/Data/Nat/Simproc.lean

@@ -89,6 +89,11 @@ theorem add_le_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b ≤ c + d)
 theorem add_le_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c) := by
   rw [← Nat.add_sub_assoc h, Nat.sub_le_iff_le_add]
 
+theorem add_le_eq (a b : Nat) : (a + b ≤ b) = (a = 0) := by
+  have r := add_le_add_le a 0 (Nat.le_refl b)
+  simp only [Nat.zero_add] at r
+  simp [r]
+
 theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b) := by
   have r := add_le_add_le a 0 h
   simp only [Nat.zero_add] at r
@@ -97,12 +102,34 @@ theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c
 theorem add_le_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b ≤ c) = False :=
   eq_false (Nat.not_le_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
 
+theorem add_lt_lt (a : Nat) {b c : Nat} (h : b < c) : (a + b < c) = (a < c - b) := by
+  have g := Nat.le_of_succ_le h
+  apply Eq.trans ?_ (add_le_le (a+1) g)
+  simp only [Nat.succ_add, Nat.add_assoc]
+  eq_refl
+
+theorem add_lt_ge (a : Nat) {b c : Nat} (h : b ≥ c) : (a + b < c) = False :=
+  eq_false (Nat.not_lt_of_ge (Nat.le_trans h (le_add_left b a)))
+
 theorem le_add_le (a : Nat) {b c : Nat} (h : a ≤ c) : (a ≤ b + c) = True :=
   eq_true (Nat.le_trans h (le_add_left c b))
 
-theorem le_add_ge (a : Nat) {b c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b) := by
+theorem le_add_ge {a : Nat} (b : Nat) {c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b) := by
   have r := add_le_add_ge 0 b h
   simp only [Nat.zero_add] at r
   exact r
 
+theorem lt_add_ge {a : Nat} (b : Nat) {c : Nat} (h : a ≥ c) : (a < b + c) = (a - c < b) := by
+  have r := le_add_ge b (@Nat.le.step _ _ h)
+  rw [Nat.succ_sub h] at r
+  exact r
+
+theorem add_lt_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b < c + d) = (a < c + (d - b)) := by
+  rw [← Nat.succ_le, ← Nat.succ_add, add_le_add_le _ _ h]
+  eq_refl
+
+theorem add_lt_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b < c + d) = (a + (b - d) < c) := by
+  rw [← Nat.succ_le, ← Nat.succ_add, add_le_add_ge _ _ h, Nat.succ_add]
+  eq_refl
+
 end Nat.Simproc

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -28,12 +28,6 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) :=
   let some m ← fromExpr? e.appArg! | return .continue
   return .done <| toExpr (op n m)
 
-@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
-  unless e.isAppOfArity declName arity do return .continue
-  let some n ← fromExpr? e.appFn!.appArg! | return .continue
-  let some m ← fromExpr? e.appArg! | return .continue
-  evalPropStep e (op n m)
-
 @[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
@@ -55,8 +49,6 @@ builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMo
 builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
 builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
 
-builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
-builtin_simproc [simp, seval] reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Nat) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_dsimproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``bne 4 (. != .)
 
@@ -107,11 +99,11 @@ private partial def NatOffset.fromExprAux (e : Expr) (inc : Nat) : Meta.SimpM (O
     return if inc != 0 then some (e, inc) else none
 
 /- Attempt to parse a `NatOffset` from an expression-/
-private def NatOffset.fromExpr? (e : Expr) (inc : Nat := 0) : Meta.SimpM (Option NatOffset) := do
+private def NatOffset.fromExpr? (e : Expr) : Meta.SimpM (Option NatOffset) := do
   match ← Nat.fromExpr? e with
-  | some n => pure (some (const (n + inc)))
+  | some n => pure (some (const n))
   | none =>
-    match ← fromExprAux e inc with
+    match ← fromExprAux e 0 with
     | none => pure none
     | some (b, o) => pure (some (offset b (toExpr o) o))
 
@@ -251,18 +243,21 @@ builtin_simproc [simp, seval] reduceBneDiff ((_ : Nat) != _) := fun e => do
     let q := mkAppN (mkConst ``Nat.Simproc.bneEqOfEqEq) #[x, y, u, v, p]
     return .visit { expr := mkBneNat u v, proof? := some q, cache := true }
 
-def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step := do
+def reduceLE (nm : Name) (arity : Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity nm arity do
     return .continue
   let x := e.appFn!.appArg!
   let y := e.appArg!
-  let some xno ← NatOffset.fromExpr? x (inc := cond isLT 1 0) | return .continue
+  let some xno ← NatOffset.fromExpr? x | return .continue
   let some yno ← NatOffset.fromExpr? y | return .continue
   match xno, yno with
   | .const xn, .const yn =>
     Meta.Simp.evalPropStep e (xn ≤ yn)
   | .offset xb xo xn, .const yn => do
-    if xn ≤ yn then
+    if xn = yn then
+      let finExpr := mkEqNat xb (toExpr 0)
+      applySimprocConst finExpr ``Nat.Simproc.add_le_eq #[xb, xo]
+    else if xn < yn then
       let finExpr := mkLENat xb (toExpr (yn - xn))
       let leProof ← mkOfDecideEqTrue (mkLENat xo y)
       applySimprocConst finExpr ``Nat.Simproc.add_le_le #[xb, xo, y, leProof]
@@ -287,7 +282,45 @@ def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step :
       let geProof ← mkOfDecideEqTrue (mkGENat xo yo)
       applySimprocConst finExpr ``Nat.Simproc.add_le_add_ge  #[xb, yb, xo, yo, geProof]
 
-builtin_simproc [simp, seval] reduceLeDiff ((_ : Nat) ≤ _) := reduceLTLE ``LE.le 4 false
+def reduceLT (nm : Name) (arity : Nat) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity nm arity do
+    return .continue
+  let x := e.appFn!.appArg!
+  let y := e.appArg!
+  let some xno ← NatOffset.fromExpr? x | return .continue
+  let some yno ← NatOffset.fromExpr? y | return .continue
+  match xno, yno with
+  | .const xn, .const yn =>
+    Meta.Simp.evalPropStep e (xn < yn)
+    -- xb < 1
+  | .offset xb xo xn, .const yn => do
+    if xn < yn then
+      let finExpr := mkLTNat xb (toExpr (yn - xn))
+      let ltProof ← mkOfDecideEqTrue (mkLTNat xo y)
+      applySimprocConst finExpr ``Nat.Simproc.add_lt_lt #[xb, xo, y, ltProof]
+    else
+      let geProof ← mkOfDecideEqTrue (mkGENat xo y)
+      applySimprocConst (mkConst ``False) ``Nat.Simproc.add_lt_ge #[xb, xo, y, geProof]
+  | .const xn, .offset yb yo yn => do
+    if xn < yn then
+      let ltProof ← mkOfDecideEqTrue (mkLTNat x yo)
+      applySimprocConst (mkConst ``True) ``Nat.Simproc.le_add_le #[x, yb, yo, ltProof]
+    else
+      let finExpr := mkLTNat (toExpr (xn - yn)) yb
+      let geProof ← mkOfDecideEqTrue (mkGENat x yo)
+      applySimprocConst finExpr ``Nat.Simproc.lt_add_ge #[x, yb, yo, geProof]
+  | .offset xb xo xn, .offset yb yo yn => do
+    if xn ≤ yn then
+      let finExpr := mkLTNat xb (if xn = yn then yb else mkAddNat yb (toExpr (yn - xn)))
+      let leProof ← mkOfDecideEqTrue (mkLENat xo yo)
+      applySimprocConst finExpr ``Nat.Simproc.add_lt_add_le  #[xb, yb, xo, yo, leProof]
+    else
+      let finExpr := mkLTNat (mkAddNat xb (toExpr (xn - yn))) yb
+      let geProof ← mkOfDecideEqTrue (mkGENat xo yo)
+      applySimprocConst finExpr ``Nat.Simproc.add_lt_add_ge  #[xb, yb, xo, yo, geProof]
+
+builtin_simproc [simp, seval] reduceLeDiff ((_ : Nat) ≤ _) := reduceLE ``LE.le 4
+builtin_simproc [simp, seval] reduceLtDiff ((_ : Nat) < _) := reduceLT ``LT.lt 4
 
 builtin_simproc [simp, seval] reduceSubDiff ((_ - _ : Nat)) := fun e => do
   unless e.isAppOfArity ``HSub.hSub 6 do

tests/lean/run/simprocNat.lean

@@ -41,7 +41,7 @@ variable (a b : Nat)
 #check_simp (1234567 : Nat) ≠ 123456 ~> True
 #check_simp (a + 400) ≠ (b + 1000) ~> a ≠ b + 600
 
-/- leq -/
+/- le -/
 
 #check_simp (1234567 : Nat) ≤ 123456 ~> False
 #check_simp (1234567 : Nat) ≤ 1234567 ~> True
@@ -68,6 +68,36 @@ variable (a b : Nat)
 #check_simp 1000 ≥ (a + 1000) ~> a = 0
 #check_simp (a + 1000) ≥ (b +  400) ~> a + 600 ≥ b
 
+/- lt -/
+
+#check_simp (1234567 : Nat) < 123456 ~> False
+#check_simp (1234567 : Nat) < 1234567 ~> False
+#check_simp (1234567 : Nat) < 1234568 ~> True
+#check_simp (123456 : Nat) < 1234567 ~> True
+
+#check_simp (a +  999) < 1000 ~> a < 1
+#check_simp (a + 1000) < 1000 ~> False
+#check_simp (a + 1000) <  400 ~> False
+#check_simp (a +  400) < 1000 ~> a < 600
+
+#check_simp 1000 < (a + 1000) ~> 0 < a
+#check_simp 400  < (a + 1000) ~> True
+#check_simp 1000 < (a +  400) ~> 600 < a
+
+#check_simp (a +  999) < (b + 1000) ~> a < b + 1
+#check_simp (a + 1000) < (b + 1000) ~> a < b
+#check_simp (a + 1000) < (b +  400) ~> a + 600 < b
+#check_simp (a +  400) < (b + 1000) ~> a < b + 600
+#check_simp (Nat.add a 400) < (Add.add b 1000) ~> a < b + 600
+#check_simp (Nat.add a 400) < b.succ.succ ~> a + 398 < b
+
+/- gt (just make sure lt rules apply) -/
+
+#check_simp (123456 : Nat) > 1234567 ~> False
+#check_simp (a +  400) > 1000 ~> a > 600
+#check_simp 1000 > (a + 1000) ~> False
+#check_simp (a + 1000) > (b +  400) ~> a + 600 > b
+
 /- beq tests -/
 
 #check_simp (1234567 : Nat) == 123456 ~> false