Add rewrite rule for a pecial case of equality between if expressions

Blaster/Optimize/Hypotheses.lean

@@ -152,6 +152,63 @@ def leqZeroIntInHyps (e : Expr) : TranslateEnvT Bool := do
      let zero_lt ← mkIntLtExpr zero_int e
      return hyps.contains (mkApp (← mkPropNotOp) zero_lt)
 
+/-- Return `true` only when `e1` and `e2` are distinct Bool literals. -/
+@[always_inline, inline]
+def notEqBool? (e1 e2 : Expr) : Bool :=
+  match isBoolValue? e1, isBoolValue? e2 with
+  | .some x1, .some x2 => x1 != x2
+  | _       , _        => false
+
+/-- Return `true` only when `e1` and `e2` are distinct Nat literals. -/
+@[always_inline, inline]
+def notEqNat? (e1 e2 : Expr) : Bool :=
+  match isNatValue? e1, isNatValue? e2 with
+  | .some x1, .some x2 => x1 != x2
+  | _       , _        => false
+
+/-- Return `true` only when `e1` and `e2` are distinct Int literals. -/
+@[always_inline, inline]
+def notEqInt? (e1 e2 : Expr) : Bool :=
+  match isIntValue? e1, isIntValue? e2 with
+  | .some x1, .some x2 => x1 != x2
+  | _       , _        => false
+
+/-- Return `true` only when `e1` and `e2` are distinct UInt32 literals. -/
+@[always_inline, inline]
+def notEqUInt32? (e1 e2 : Expr) : Bool :=
+  match isUInt32Value? e1, isUInt32Value? e2 with
+  | .some x1, .some x2 => x1 != x2
+  | _       , _        => false
+
+/-- Return `true` only when `e1` and `e2` are distinct Char literals. -/
+@[always_inline, inline]
+def notEqChar? (e1 e2 : Expr) : Bool :=
+  match isCharValue? e1, isCharValue? e2 with
+  | .some x1, .some x2 => x1 != x2
+  | _       , _        => false
+
+/-- Return `true` only when `e1` and `e2` are distinct String literals. -/
+@[always_inline, inline]
+def notEqString? (e1 e2 : Expr) : Bool :=
+  match isStrValue? e1, isStrValue? e2 with
+  | .some x1, .some x2 => x1 != x2
+  | _       , _        => false
+
+/-- Return `true` only when one of the following conditions is satisfied:
+      - e1 ≠ e2 can be determined by literal comparison (Bool, Nat, Int, UInt32, Char, or String); or
+      - ¬ (e1 = e2) := _ ∈ hypothesisContext.hypothesisMap
+-/
+@[always_inline, inline]
+def notEqInHyps (sort e1 e2 : Expr) : TranslateEnvT Bool := do
+  if notEqBool?   e1 e2 then return true
+  if notEqNat?    e1 e2 then return true
+  if notEqInt?    e1 e2 then return true
+  if notEqUInt32? e1 e2 then return true
+  if notEqChar?   e1 e2 then return true
+  if notEqString? e1 e2 then return true
+  let hyps     := (← get).optEnv.hypothesisContext.hypothesisMap
+  let e1_ne_e2 := mkApp (← mkPropNotOp) (mkApp3 (← mkEqOp) sort e1 e2)
+  return hyps.contains e1_ne_e2
 
 /-- Perform the following actions:
      Let hyps := (← get).optEnv.options.hypothesisContext

Blaster/Optimize/Lemmas.lean

@@ -1,6 +1,6 @@
 
 import Blaster.Optimize.Lemmas.LemmasDecide
+import Blaster.Optimize.Lemmas.LemmasEq
 import Blaster.Optimize.Lemmas.LemmasInt
 import Blaster.Optimize.Lemmas.LemmasNat
 import Blaster.Optimize.Lemmas.LemmasProp
-

Blaster/Optimize/Lemmas/LemmasEq.lean

@@ -0,0 +1,13 @@
+import Blaster.Optimize.Env
+
+open Lean Meta Blaster.Optimize
+
+namespace Blaster
+
+/-! ## Lemmas validating the normalization and simplifications rules on `Eq` -/
+
+protected theorem Blaster.ite_equal_then_else_equal_cond {t : Type} [DecidableEq t] (c₁ c₂ : Prop) [Decidable c₁] [Decidable c₂] (t₁ e₁ t₂ e₂ : t) :
+  t₁ = t₂ → e₁ = e₂ → t₁ ≠ e₁ →
+    ((if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) ↔ c₁ = c₂) := by grind
+
+end Blaster

Blaster/Optimize/Rewriting/OptimizeEq.lean

@@ -1,5 +1,6 @@
 import Lean
 import Blaster.Optimize.Hypotheses
+import Blaster.Optimize.Rewriting.OptimizeITE
 
 open Lean Meta
 namespace Blaster.Optimize
@@ -503,6 +504,7 @@ def optimizeDecideEq (f : Expr) (args : Array Expr) : TranslateEnvT Expr := do
  if let some r ← boolEqtoEq? op1 op2 then return r
  if let some r ← decideBoolEqSimp? op1 op2 then return r
  if let some r ← decideEqDecide? op1 op2 then return r
+ if let some r ← decideEqDITE? op1 op2 then return r
  return e
 
  where
@@ -565,7 +567,7 @@ def optimizeDecideEq (f : Expr) (args : Array Expr) : TranslateEnvT Expr := do
        - return `some ¬ e` when `op1 := false ∧ op2 := decide e`
       Otherwise `none`.
    -/
-   decideBoolEqSimp? (op1: Expr) (op2 : Expr) : TranslateEnvT (Option Expr) := do
+   decideBoolEqSimp? (op1 : Expr) (op2 : Expr) : TranslateEnvT (Option Expr) := do
     match op1, decide'? op2 with
     | Expr.const ``true _, some e => return some e -- no need to restart
     | Expr.const ``false _, some e =>
@@ -579,7 +581,7 @@ def optimizeDecideEq (f : Expr) (args : Array Expr) : TranslateEnvT Expr := do
        - return `some e1 = (true = e2)` when `op1 := e2 ∧ op2 := decide e1`
       Otherwise `none`.
    -/
-   decideEqDecide? (op1: Expr) (op2 : Expr) : TranslateEnvT (Option Expr) := do
+   decideEqDecide? (op1 : Expr) (op2 : Expr) : TranslateEnvT (Option Expr) := do
      match decide'? op1, decide'? op2 with
      | some e1, some e2 =>
           setRestart
@@ -592,6 +594,23 @@ def optimizeDecideEq (f : Expr) (args : Array Expr) : TranslateEnvT Expr := do
           return mkApp3 f (← mkPropType) e1 (mkApp3 f (← mkBoolType) (← mkBoolTrue) op1)
      | _, _ => return none
 
+   /- Given `op1` and `op2` corresponding to the operands for `Eq`,
+       - return `some c = b` when `op1 := (if c then e1 else e2) ∧ op2 := (if b then e1 else e2) ∧ e1 ≠ e2`
+      Otherwise `none`.
+   -/
+   decideEqDITE? (op1 op2 : Expr) : TranslateEnvT (Option Expr) := do
+     match dite'? op1, dite'? op2 with
+     | some (sort, c, e1, e2), some (_, b, e3, e4) =>
+         let e1' ← extractDependentITEExpr e1
+         let e2' ← extractDependentITEExpr e2
+         let e3' ← extractDependentITEExpr e3
+         let e4' ← extractDependentITEExpr e4
+         if exprEq e1' e3' && exprEq e2' e4' && (← notEqInHyps sort e1' e2') then
+           setRestart
+           return mkApp3 (← mkEqOp) (← mkPropType) c b
+         return none
+     | _, _ => return none
+
 
 /-- Apply simplification and normalization rules on `Eq` and `BEq.beq` :
 -/

Tests/Smt.lean

@@ -6,4 +6,3 @@ import Tests.Smt.SmtMatch
 import Tests.Smt.SmtNat
 import Tests.Smt.SmtPredQualifier
 import Tests.Smt.SmtRecFun
-

Tests/Smt/SmtEqArith.lean

@@ -324,4 +324,45 @@ namespace Test.SmtEqArith
 #blaster (gen-cex: 0) (solve-result: 1) [∀ (x y z : Int), x > 0 → z > 0 → 0 < x + y]
 #blaster (only-optimize: 1) [∀ (x y z : Int), x > 0 → z ≥ 0 → 0 < x + z]
 
+#blaster [∀ (c b : Prop) [Decidable b] [Decidable c] (e1 e2 : Nat), c = b → (if c then e1 else e2) = (if b then e1 else e2)]
+
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable b] [Decidable c], (if c then 1 else 0) = (if b then 1 else 0) → c = b]
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable b] [Decidable c], (if c then "a" else "b") = (if b then "a" else "b") → c = b]
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable b] [Decidable c], (if c then true else false) = (if b then true else false) → c = b]
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable b] [Decidable c], c = b → (if c then 1 else 0) = (if b then 1 else 0)]
+
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable b] [Decidable c] (e1 e2 : Nat), e1 ≠ e2 →
+  (if c then e1 else e2) = (if b then e1 else e2) → c = b]
+
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable b] [Decidable c] (e1 e2 : Nat), e2 ≠ e1 →
+  (if c then e1 else e2) = (if b then e1 else e2) → c = b]
+
+#blaster (only-optimize: 1) [∀ (c : Prop) [Decidable c] (e1 e2: Nat),
+  (if c then e1 else e2) = (if c then e1 else e2)]
+
+#blaster (only-optimize: 1) [∀ (c : Prop) [Decidable c] (e1 : Nat),
+  (if c then e1 else e1) = e1]
+
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable b] [Decidable c] (e1 e2 e3 : Nat), e1 ≠ e2 →
+  (if c then (if b then e1 else e1) else e2) = (if b then (if b then e1 else e1) else e2) → c = b]
+
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable c] [Decidable b] (e1 e2 : Int),
+  if e1 ≠ e2 then
+    (if c then e1 else e2) = (if b then e1 else e2) → c = b
+  else
+    true
+]
+
+#blaster (only-optimize: 1) [∀ (c b : Prop) [Decidable c] [Decidable b] (e1 e2 e3 e4 : Int),
+  if e1 ≠ e2 then
+    (if c then e1 else e2) = (if b then e1 else e2) → c = b
+  else
+    (if c then e1 else e1) = e1
+]
+
+#blaster (only-optimize: 1) [∀ (c : Prop) [Decidable c] (e1 e2 : Int), e1 ≠ e2 → (if c then e1 else e2) = (if c then e1 else e2)]
+#blaster (only-optimize: 1) [∀ (c : Prop) [Decidable c] (e1 e2 : Int), (if c then e1 else e2) = (if c then e1 else e2)]
+
+#blaster (gen-cex: 0) (solve-result: 1) [∀ (c b : Prop) [Decidable b] [Decidable c] (e1 e2 : Nat), (if c then e1 else e2) = (if b then e1 else e2) → c = b]
+
 end Test.SmtEqArith