fix: mTrans at grind offset

leanprover · Jan 12, 2025 · 222cb56 · 222cb56
1 parent 912327c
commit 222cb56
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean b/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
@@ -61,9 +61,9 @@ def mkTrans (nodes : PArray Expr) (pi₁ : ProofInfo) (pi₂ : ProofInfo) (v : N
     else if k₂ > 0 then
       let ke₂ := toExpr k₂.toNat
        if k₂ > k₁ then
-         mkApp7 (mkConst ``Nat.ro_lo_1) u w v ke₁ ke₂ p₁ p₂
-       else
          mkApp8 (mkConst ``Nat.ro_lo_2) u w v ke₁ ke₂ rfl_true p₁ p₂
+       else
+         mkApp7 (mkConst ``Nat.ro_lo_1) u w v ke₁ ke₂ p₁ p₂
     else
       let ke₂ := toExpr (-k₂).toNat
       mkApp7 (mkConst ``Nat.ro_ro) u w v ke₁ ke₂ p₁ p₂

diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean
@@ -167,3 +167,18 @@ example (a1 a2 a3 : Nat) :
         a1 ≤ a2 + 5 → a2 ≤ a3 + 2 → False := by
   fail_if_success grind
   sorry
+
+/--
+info: [grind.offset.internalize.term] a1 ↦ #0
+[grind.offset.internalize.term] a2 ↦ #1
+[grind.offset.dist] #0 ≤ #1 + 2
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #1 + 3 ≤ #2
+[grind.offset.dist] #0 + 1 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (a1 a2 a3 : Nat) : a1 ≤ a2 + 2 → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry