fix: Offset.Cnstr.neg

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

Hide file tree

Showing 2 changed files with 64 additions and 1 deletion.
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean
@@ -54,7 +54,10 @@ structure Offset.Cnstr (α : Type) where
   deriving Inhabited
 
 def Offset.Cnstr.neg : Cnstr α → Cnstr α
-  | { a, b, k, le } => { b, a, le, k := k + 1 }
+  | { a, b, k, le } => { a := b, b := a, le, k := -k + 1 }
+
+example (c : Offset.Cnstr α) : c.neg.neg = c := by
+  cases c; simp [Offset.Cnstr.neg]; omega
 
 def Offset.toMessageData [inst : ToMessageData α] (c : Offset.Cnstr α) : MessageData :=
   match c.k, c.le with

diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean
@@ -182,3 +182,63 @@ 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
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 + 3 ≤ #0
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 6 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1 + 2) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 ≤ #0 + 1
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 2 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 + 1 ≤ #0
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 4 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry
+
+/--
+info: [grind.offset.internalize.term] a2 ↦ #0
+[grind.offset.internalize.term] a1 ↦ #1
+[grind.offset.dist] #1 ≤ #0
+[grind.offset.internalize.term] a3 ↦ #2
+[grind.offset.dist] #0 + 3 ≤ #2
+[grind.offset.dist] #1 + 3 ≤ #2
+-/
+#guard_msgs (info) in
+set_option trace.grind.offset.internalize.term true in
+set_option trace.grind.offset.dist true in
+example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 1 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
+  fail_if_success grind
+  sorry