Change eq semantics for binders in Lambda

Strata/DL/Lambda/LExprEval.lean

@@ -84,6 +84,19 @@ def isConstrApp (F : @Factory T.base) (e : LExpr T) : Bool :=
   | some (_, _, f) => f.isConstr
   | none => false
 
+/--
+Check if `e` contains a binder (abstraction or quantifier) anywhere in its
+structure. Used to prevent reducing equality to `false` under binders, since
+syntactic inequality does not imply semantic inequality for expressions with
+binders (e.g., `λx. x+1` vs `λx. 1+x`).
+-/
+def containsBinder (e : LExpr T) : Bool :=
+  match e with
+  | .abs _ _ _ _ | .quant _ _ _ _ _ _ => true
+  | .app _ e1 e2 | .eq _ e1 e2 => containsBinder e1 || containsBinder e2
+  | .ite _ c t f => containsBinder c || containsBinder t || containsBinder f
+  | _ => false
+
 /--
 Equality of canonical values `e1` and `e2`.
 
@@ -232,7 +245,14 @@ def evalEq (n' : Nat) (σ : LState TBase) (m: TBase.Metadata) (e1 e2 : LExpr TBa
              isCanonicalValue σ.config.factory e2' then
     if eql σ.config.factory e1' e2' h.left h.right then
       LExpr.true m
-    else LExpr.false m
+    else
+      -- Do not reduce to false if either side contains a binder (abs/quant),
+      -- because syntactic inequality under binders does not imply semantic
+      -- inequality (e.g., λx. x+1 vs λx. 1+x).
+      if e1'.containsBinder || e2'.containsBinder then
+        .eq m e1' e2'
+      else
+        LExpr.false m
   else
     .eq m e1' e2'
 

Strata/DL/Lambda/Semantics.lean

@@ -110,13 +110,25 @@ inductive Step (F:@Factory Tbase) (rf:Env Tbase)
     Step F rf eelse eelse' →
     Step F rf (.ite m econd ethen eelse) (.ite m' econd ethen eelse')
 
-/-- Evaluation of equality. Reduce after both operands evaluate to values. -/
-| eq_reduce:
-  ∀ (e1 e2 eres:LExpr Tbase.mono)
+/-- Evaluation of equality to true. Always allowed. -/
+| eq_reduce_true:
+  ∀ (e1 e2:LExpr Tbase.mono)
     (H1:LExpr.isCanonicalValue F e1)
     (H2:LExpr.isCanonicalValue F e2),
-    eres = .const mc (.boolConst (LExpr.eql F e1 e2 H1 H2)) →
-    Step F rf (.eq m e1 e2) eres
+    LExpr.eql F e1 e2 H1 H2 = true →
+    Step F rf (.eq m e1 e2) (.const mc (.boolConst true))
+
+/-- Evaluation of equality to false. Only when neither side contains a binder,
+    because syntactic inequality under binders does not imply semantic inequality
+    (e.g., `λx. x+1` vs `λx. 1+x`). -/
+| eq_reduce_false:
+  ∀ (e1 e2:LExpr Tbase.mono)
+    (H1:LExpr.isCanonicalValue F e1)
+    (H2:LExpr.isCanonicalValue F e2),
+    LExpr.eql F e1 e2 H1 H2 = false →
+    e1.containsBinder = false →
+    e2.containsBinder = false →
+    Step F rf (.eq m e1 e2) (.const mc (.boolConst false))
 
 /-- Evaluation of the left-hand side of an equality. -/
 | eq_reduce_lhs:

StrataTest/DL/Lambda/LExprEvalTests.lean

@@ -109,7 +109,7 @@ example: steps_well test2 := by
   · repeat constructor
   take_step; reduce_beta
   take_step; constructor <;> try inhabited_metadata
-  · apply Step.eq_reduce <;> try discharge_isCanonicalValue
+  · apply Step.eq_reduce_false <;> try discharge_isCanonicalValue <;> try rfl
     · inhabited_metadata
   take_step; apply Step.ite_reduce_else
   apply ReflTrans.refl
@@ -144,7 +144,7 @@ example: steps_well test4 := by
   unfold steps_well Scopes.toEnv test4
   take_step; reduce_beta
   take_step; apply Step.ite_reduce_cond <;> try inhabited_metadata
-  · apply Step.eq_reduce <;> try discharge_isCanonicalValue
+  · apply Step.eq_reduce_false <;> try discharge_isCanonicalValue <;> try rfl
     · inhabited_metadata
   take_step; apply Step.ite_reduce_else
   take_step; apply Step.reduce_1; inhabited_metadata; apply Step.expand_fvar; rfl
@@ -165,7 +165,7 @@ example: steps_well test5 := by
   unfold steps_well Scopes.toEnv test5
   take_step; reduce_beta
   take_step; apply Step.ite_reduce_cond; inhabited_metadata
-  · apply Step.eq_reduce <;> try discharge_isCanonicalValue
+  · apply Step.eq_reduce_false <;> try discharge_isCanonicalValue <;> try rfl
     · inhabited_metadata
   take_step; apply Step.ite_reduce_else
   take_step; apply Step.reduce_1; inhabited_metadata; apply Step.expand_fvar; rfl