From 8719c17f1a363c0463d74b90e558b2aaa24645d6 Mon Sep 17 00:00:00 2001
From: Son HO
Date: Sat, 22 Jun 2024 15:07:14 +0200
Subject: Do some cleanup in the Lean backend (#257)

---
 backends/lean/Base/Core.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 backends/lean/Base/Core.lean

(limited to 'backends/lean/Base/Core.lean')

diff --git a/backends/lean/Base/Core.lean b/backends/lean/Base/Core.lean
new file mode 100644
index 00000000..89dd199b
--- /dev/null
+++ b/backends/lean/Base/Core.lean
@@ -0,0 +1,17 @@
+
+import Lean
+
+/- This lemma is generally useful. It often happens that (because we
+   make a split on a condition for instance) we have `x ≠ y` in the context
+   and need to simplify `y ≠ x` somewhere. -/
+@[simp]
+theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+
+/- This is generally useful, and doing without is actually quite cumbersome.
+
+   Note that the following theorem does not seem to be necessary (we invert `x`
+   and `y` in the conclusion), probably because of `neq_imp`:
+   `¬ x = y → ¬ y == x`
+ -/
+@[simp]
+theorem neq_imp_nbeq [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ x == y := by simp [*]
-- 
cgit v1.2.3