chore: shortcircuit eq_of_true and eq_true

leanprover · Jan 11, 2025 · 30f5362 · 30f5362
1 parent 5d7e03e
commit 30f5362
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 4 deletions.
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
@@ -569,12 +569,16 @@ def mkLetBodyCongr (a h : Expr) : MetaM Expr :=
   mkAppM ``let_body_congr #[a, h]
 
 /-- Return `of_eq_true h` -/
-def mkOfEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``of_eq_true #[h]
+def mkOfEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | eq_true _ h => return h
+  | _ => mkAppM ``of_eq_true #[h]
 
 /-- Return `eq_true h` -/
-def mkEqTrue (h : Expr) : MetaM Expr :=
-  mkAppM ``eq_true #[h]
+def mkEqTrue (h : Expr) : MetaM Expr := do
+  match_expr h with
+  | of_eq_true _ h => return h
+  | _ => return mkApp2 (mkConst ``eq_true) (← inferType h) h
 
 /--
   Return `eq_false h`

diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean
@@ -160,3 +160,10 @@ example (a1 a2 a3 : Nat) :
         a1 ≤ a2 + 5 → a2 ≤ a3 + 2 → False := by
   fail_if_success grind
   sorry
+
+
+set_option trace.grind.debug.offset.proof true in
+example (a1 a2 a3 : Nat) :
+        a1 ≤ a2 + 5 → a2 ≤ a3 + 2 → False := by
+  fail_if_success grind
+  sorry