From 596e65d7dfe2cf0c15522238b5a2d5734b6227cf Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Wed, 4 Jun 2025 16:10:48 +0100
Subject: [PATCH] feat: AIG.relabel(Nat)_unsat_iff  for AIGs with empty
 variable types (#8631)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR generalizes `Std.Sat.AIG. relabel(Nat)_unsat_iff` to allow the
AIG type to be empty. We generalize the proof, by showing that in the
case when `α` is empty, the environment doesn't matter, since all
environments `α → Bool` are isomorphic.

This showed up when reusing the AIG primitives for building a
k-induction based model checker to prove arbitrary width bitvector
identities.
---
 src/Std/Sat/AIG/Relabel.lean    | 26 +++++++++++++++++++++++++-
 src/Std/Sat/AIG/RelabelNat.lean | 16 +++++++++++-----
 2 files changed, 36 insertions(+), 6 deletions(-)

diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean
index f6b2665d6d..12abc2d657 100644
--- a/src/Std/Sat/AIG/Relabel.lean
+++ b/src/Std/Sat/AIG/Relabel.lean
@@ -128,7 +128,21 @@ theorem unsat_relabel {aig : AIG α} (r : α → β) {hidx} :
   specialize h (assign ∘ r)
   simp [h]
 
-theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2}
+theorem relabel_unsat_iff_of_not_Nonempty {aig : AIG α}
+    {r : α → β} {hidx1} {hidx2}
+    (hNonempty : ¬ Nonempty α) :
+    (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
+  constructor
+  · intro hα assignα
+    let assignβ : β → Bool := fun b => false
+    specialize hα assignβ
+    have hAssignα : assignα  = assignβ ∘ r := by
+      ext a
+      apply hNonempty (Nonempty.intro a) |>.elim
+    rw [hAssignα, ← denote_relabel, ← hα]
+  · apply unsat_relabel
+
+theorem relabel_unsat_iff_of_Nonempty [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2}
     (hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) :
     (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
   constructor
@@ -154,6 +168,16 @@ theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {
         contradiction
   · apply unsat_relabel
 
+/--
+`relabel` preserves unsatisfiablility.
+-/
+theorem relabel_unsat_iff {aig : AIG α} {r : α → β} {hidx1} {hidx2}
+    (hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) :
+    (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
+  by_cases hαNonempty : Nonempty α
+  · apply relabel_unsat_iff_of_Nonempty hinj
+  · apply relabel_unsat_iff_of_not_Nonempty hαNonempty
+
 namespace Entrypoint
 
 def relabel (r : α → β) (entry : Entrypoint α) : Entrypoint β :=
diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean
index 1490b9506b..5508ae9097 100644
--- a/src/Std/Sat/AIG/RelabelNat.lean
+++ b/src/Std/Sat/AIG/RelabelNat.lean
@@ -325,10 +325,7 @@ theorem relabelNat'_fst_eq_relabelNat {aig : AIG α} : aig.relabelNat'.fst = aig
 theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig.decls.size := by
   simp [relabelNat, relabelNat']
 
-/--
-`relabelNat` preserves unsatisfiablility.
--/
-theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
+theorem relabelNat_unsat_iff_of_NonEmpty [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
     (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
   dsimp only [relabelNat, relabelNat']
   rw [relabel_unsat_iff]
@@ -350,6 +347,15 @@ theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
     rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
     simp [hcase] at hn
 
+/--
+`relabelNat` preserves unsatisfiablility.
+-/
+theorem relabelNat_unsat_iff {aig : AIG α} {hidx1} {hidx2} :
+    (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
+  by_cases hNonempty : Nonempty α
+  · apply relabelNat_unsat_iff_of_NonEmpty
+  · apply relabel_unsat_iff_of_not_Nonempty hNonempty
+
 namespace Entrypoint
 
 def relabelNat' (entry : Entrypoint α) : (Entrypoint Nat × HashMap α Nat) :=
@@ -375,7 +381,7 @@ def relabelNat (entry : Entrypoint α) : Entrypoint Nat :=
 /--
 `relabelNat` preserves unsatisfiablility.
 -/
-theorem relabelNat_unsat_iff {entry : Entrypoint α} [Nonempty α] :
+theorem relabelNat_unsat_iff {entry : Entrypoint α} :
     (entry.relabelNat).Unsat ↔ entry.Unsat:= by
   simp only [Unsat, relabelNat]
   rw [AIG.relabelNat_unsat_iff]