From 88540c590f6fdcfc3dfd59aec4f39922b7d4a967 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 18 Oct 2023 20:29:47 +0100
Subject: [PATCH] Make file compile

---
 SSA/Projects/InstCombine/AliveStatements.lean | 18 ++++++++-------
 SSA/Projects/InstCombine/ForMathlib.lean      | 16 +++++++++++--
 SSA/Projects/InstCombine/ForStd.lean          | 23 ++++++++++++++++++-
 3 files changed, 46 insertions(+), 11 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
index ff5bb11e9..29673d7bb 100644
--- a/SSA/Projects/InstCombine/AliveStatements.lean
+++ b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -8,7 +8,9 @@ open Std.BitVec
 
 def a : BitVec 2 := 0
 def c : Nat := 2
-#check a <<< c
+def b : Bool := a ≤ a
+
+#check ofBool (a ≤ a)
 #eval a <<< c
 #check a >>> c
 #eval a >>> c
@@ -129,7 +131,7 @@ theorem bitvec_AndOrXor_716 :
       try sorry
 
 theorem bitvec_AndOrXor_794 :
- ∀ (w : Nat) (a b : BitVec w), (a >ₛ b) &&& ofBool (a != b) = (a >ₛ b)
+ ∀ (w : Nat) (a b : BitVec w), ofBool (a >ₛ b) &&& ofBool (a != b) = (a >ₛ b)
 := by alive_auto
       try sorry
 
@@ -179,22 +181,22 @@ theorem bitvec_AndOrXor_1294_A__B__A__B___A__B :
       try sorry
 
 theorem bitvec_AndOrXor_1683_1 :
- ∀ (w : Nat) (a b : BitVec w), (a >ᵤ b) ||| ofBool (a == b) = (a ≥ᵤ b)
+ ∀ (w : Nat) (a b : BitVec w), ofBool (a >ᵤ b) ||| ofBool (a == b) = (a ≥ᵤ b)
 := by alive_auto
       try sorry
 
 theorem bitvec_AndOrXor_1683_2 :
- ∀ (w : Nat) (a b : BitVec w), (a ≥ᵤ b) ||| ofBool (a != b) = ofBool true
+ ∀ (w : Nat) (a b : BitVec w), ofBool (a ≥ᵤ b) ||| ofBool (a != b) = ofBool true
 := by alive_auto
       try sorry
 
 theorem bitvec_AndOrXor_1704 :
- ∀ (w : Nat) (A B : BitVec w), ofBool (B == 0) ||| (A <ᵤ B) = (B + -1 ≥ᵤ A)
+ ∀ (w : Nat) (A B : BitVec w), ofBool (B == 0) ||| ofBool (A <ᵤ B) = (B + -1 ≥ᵤ A)
 := by alive_auto
       try sorry
 
 theorem bitvec_AndOrXor_1705 :
- ∀ (w : Nat) (A B : BitVec w), ofBool (B == 0) ||| (B >ᵤ A) = (B + -1 ≥ᵤ A)
+ ∀ (w : Nat) (A B : BitVec w), ofBool (B == 0) ||| ofBool (B >ᵤ A) = (B + -1 ≥ᵤ A)
 := by alive_auto
       try sorry
 
@@ -304,7 +306,7 @@ theorem bitvec_AndOrXor_2443 :
       try sorry
 
 theorem bitvec_AndOrXor_2453 :
- ∀ (w : Nat) (y x : BitVec w), (x <ₛ y) ^^^ -1 = (x ≥ₛ y)
+ ∀ (w : Nat) (y x : BitVec w), (ofBool (x <ₛ y)) ^^^ -1 = ofBool (x ≥ₛ y)
 := by alive_auto
       try sorry
 
@@ -359,7 +361,7 @@ theorem bitvec_AndOrXor_2658 :
       try sorry
 
 theorem bitvec_AndOrXor_2663 :
- ∀ (w : Nat) (a b : BitVec w), (a ≤ᵤ b) ^^^ ofBool (a != b) = (a ≥ᵤ b)
+ ∀ (w : Nat) (a b : BitVec w), ofBool (a ≤ᵤ b) ^^^ ofBool (a != b) = (a ≥ᵤ b)
 := by alive_auto
       try sorry
 
diff --git a/SSA/Projects/InstCombine/ForMathlib.lean b/SSA/Projects/InstCombine/ForMathlib.lean
index 289ddf385..24dfc6b12 100644
--- a/SSA/Projects/InstCombine/ForMathlib.lean
+++ b/SSA/Projects/InstCombine/ForMathlib.lean
@@ -17,6 +17,20 @@ theorem getElem_eq_get {α : Type u} {n : Nat} (v : Vector α n) (i : Fin n) : v
 
 end Vector
 
+
+
+def ofBool : Bool → Bitvec 1 := fun b => b ::ᵥ Vector.nil
+
+def a : Bitvec 2 := 0
+
+def b : Prop := a ≤ a
+def bb : Bool := b
+
+#check b
+def c : Nat := 2
+#check ofBool (a ≤ a)
+
+
 namespace Bitvec
 
 def width : Bitvec n → Nat := fun _ => n
@@ -555,8 +569,6 @@ theorem one_sdiv_ref_add_cmp_select :
 
 def beq {w : Nat} (x y : Bitvec w) : Bool := x = y
 
-def ofBool : Bool → Bitvec 1 := fun b => b ::ᵥ Vector.nil
-
 def toBool : Bitvec 1 → Bool 
   | b ::ᵥ Vector.nil => b
 
diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index 2d8a70120..c46b0a43d 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -98,4 +98,25 @@ def urem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
   then none
   else some $ BitVec.ofNat w (x.toNat % y.toNat)
 
-instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
\ No newline at end of file
+instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
+
+instance decPropToBitvec1 (p : Prop) [Decidable p] : CoeDep Prop p (BitVec 1) where
+  coe := ofBool $ decide p
+
+instance {n} {x y : BitVec n} : Decidable (BitVec.ult x y) :=
+  decEq _ _
+
+instance {n} {x y : BitVec n} : Decidable (BitVec.ule x y) :=
+  decEq _ _
+
+instance {n} {x y : BitVec n} : Decidable (x < y) :=
+  sorry
+
+instance {n} {x y : BitVec n} : Decidable (x ≤ y) :=
+  sorry
+
+instance {n} {x y : BitVec n} : Decidable (x > y) :=
+  sorry
+
+instance {n} {x y : BitVec n} : Decidable (x ≥ y) :=
+  sorry
\ No newline at end of file