Fix false Valid results from empty types and type classes

Blaster/Optimize/Rewriting/Utils.lean

@@ -170,35 +170,55 @@ def isNullaryCtor (c : Name) : TranslateEnvT Bool := do
       pure (info.numFields == 0 && !info.type.isProp)
   | _ => pure false
 
-/-- Return `true` if `t` is not a Prop and corresponds to one of the following:
-    - is a sort type only when `existQuantifier` flag is not set.
-    - is prop type when `existQuantifier` flag is set.
-    - is a class constraint; or
-    - is an inductive type for which either at least one nullary constructor or an Inhabited instance exists.
- TODO: extends check to also consider parametric constructor for which each parameter type satisfy `isSortOrInhabited`.
--/
-def isSortOrInhabited (t : Expr) (existsQuantifier := false) : TranslateEnvT Bool := do
- match ← inferTypeEnv t with
- | Expr.sort u =>
-      if u.isAlwaysZero then return false
-      match t.getAppFn' with
-      | Expr.const n _ =>
-          if (← isClassConstraint n) then return true -- break if class constraint
-          else match (← getConstEnvInfo n) with
-               | ConstantInfo.inductInfo indVal =>
-                   for ctorName in indVal.ctors do
-                     -- inductive type has at least one nullary constructor
-                     if (← isNullaryCtor ctorName) then return true
-                   -- check if InHabited instance exists for t
-                   hasInhabitedInstance t
-               | _ => isSortType t
-      | _ => isSortType t
- | _ => return false
-
+/-- Construct an inhabitant using global instances and constructor fields only.
+    The optimizer retains local declarations after leaving their binders, so its
+    local instance table is not evidence that an arbitrary domain is nonempty.
+    In particular, the variable being eliminated must not witness its own domain.
+    Bounded constructor search also handles classes such as `LT α` and `BEq α`
+    without assuming that every class (e.g. `Inhabited Empty`) is inhabited. -/
+private partial def domainWitness? (t : Expr) : MetaM (Option Expr) := do
+  withLCtx (← getLCtx) #[] (go t 8)
  where
-   isSortType (t : Expr) : TranslateEnvT Bool :=
-     if existsQuantifier then return t.isProp
-     else return true
+  go (t : Expr) (fuel : Nat) : MetaM (Option Expr) := do
+    if fuel == 0 then return none
+    let u ← getLevel t
+    let constraint := mkApp (mkConst ``Nonempty [u]) t
+    if let .some proof ← trySynthInstance constraint then
+      return mkApp2 (mkConst ``Classical.choice [u]) t proof
+    let t ← whnf t
+    if let .forallE name domain body bi := t then
+      return ← Lean.Meta.withLocalDecl name bi domain fun x => do
+        let some value ← go (body.instantiate1 x) (fuel - 1) | return none
+        return some (← Lean.Meta.mkLambdaFVars #[x] value)
+    let .const name levels := t.getAppFn | return none
+    let .inductInfo info ← getConstInfo name | return none
+    if info.numIndices != 0 then return none
+    for ctor in info.ctors do
+      let mut value := mkAppN (mkConst ctor levels) (t.getAppArgs.extract 0 info.numParams)
+      let mut type ← inferType value
+      let mut complete := true
+      while type.isForall do
+        let some field ← go type.bindingDomain! (fuel - 1)
+          | complete := false; break
+        value := mkApp value field
+        type := type.bindingBody!.instantiate1 field
+      if complete then return some value
+    return none
+
+/-- An unused quantifier may be removed only over a known nonempty domain.
+    Being a type, a function type, or a type class is not sufficient: Lean
+    permits empty instances of all three. Proposition binders are handled by
+    the implication rules instead. -/
+def isSortOrInhabited (t : Expr) (existsQuantifier := false) : TranslateEnvT Bool := do
+  let .sort u ← inferTypeEnv t | return false
+  if u.isAlwaysZero then return false
+  if t.isSort then return !existsQuantifier || t.isProp
+  withLocalContext do
+    try
+      return (← domainWitness? t).isSome
+    catch _ =>
+      -- Failure to find evidence means that the quantifier must be retained.
+      return false
 
 /-- Return `! e` when `b = false`. Otherwise return `e`. -/
 def toBoolNotExpr (b : Bool) (e : Expr) : TranslateEnvT Expr := do

Blaster/Smt/Translate/Quantifier.lean

@@ -1368,8 +1368,10 @@ def translateForAll
      let decl ← v.fvarId!.getEnvDecl
      if (← isPropEnv decl.type) then
        updatePremises (← termTranslator decl.type)
-     -- need to filter out class constraints
-     else if !(← isClassConstraintExpr decl.type) then
+     -- Erasing a class binder is valid only if its domain is nonempty.
+     -- `Inhabited α`, for example, must retain its membership qualifier:
+     -- otherwise an empty α spuriously satisfies `¬ (∀ _ : Inhabited α, False)`.
+     else if !(← isClassConstraintExpr decl.type) || !(← isSortOrInhabited decl.type) then
        translateQuantifier v decl.type termTranslator
    let fbody ← termTranslator b
    genForAllTerm fbody

Tests/FixedIssues.lean

@@ -34,3 +34,4 @@ import Tests.FixedIssues.Issue34
 import Tests.FixedIssues.Issue35
 import Tests.FixedIssues.Issue36
 import Tests.FixedIssues.Issue225
+import Tests.FixedIssues.Issue226

Tests/FixedIssues/Issue226.lean

@@ -0,0 +1,63 @@
+import Blaster
+import Tests.Utils
+
+namespace Tests.Issue226
+
+-- Kernel-checked counterexamples. None uses Blaster or sorry.
+theorem empty_type_counterexample : ¬ (∀ α : Type, (∀ _ : α, False) → False) := by
+  intro h
+  exact h Empty Empty.elim
+
+theorem empty_arrow_counterexample : ¬ (∀ α β : Type, (∀ _ : α → β, False) → False) := by
+  intro h
+  exact h Unit Empty (fun f => Empty.elim (f ()))
+
+theorem empty_class_counterexample : ¬ (∀ α : Type, ∃ _ : Inhabited α, True) := by
+  intro h
+  obtain ⟨inst, _⟩ := h Empty
+  exact Empty.elim inst.default
+
+theorem erased_class_counterexample : ¬ (∀ α : Type, (∀ _ : Inhabited α, False) → False) := by
+  intro h
+  exact h Empty (fun inst => Empty.elim inst.default)
+
+-- Preserve vacuous quantifiers both during optimization and SMT translation.
+#testOptimize ["KeepEmptyTypeDomain"]
+  (∀ α : Type, (∀ _ : α, False) → False) ===>
+  (∀ α : Type, ¬ ∀ _ : α, False)
+#testOptimize ["KeepEmptyClassDomain"]
+  (∀ α : Type, ∃ _ : Inhabited α, True) ===>
+  (∀ α : Type, ∃ _ : Inhabited α, True)
+
+#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
+  [∀ α : Type, (∀ _ : α, False) → False]
+#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
+  [∀ α β : Type, (∀ _ : α → β, False) → False]
+#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
+  [∀ α : Type, ∃ _ : Inhabited α, True]
+#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
+  [∀ α : Type, (∀ _ : Inhabited α, False) → False]
+
+-- An instance encountered in an earlier, now closed binder must not provide
+-- an inhabitant for a later binder over the same type.
+#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
+  [∀ α : Type, (∀ _ : Inhabited α, True) → (∀ _ : α, False) → False]
+
+-- Positive coverage: construct inhabitants of ordinary classes and functions
+-- from their fields, rather than assuming that every class has an instance.
+#testOptimize ["InhabitedRelationClass"]
+  (∀ α : Type, ∃ _ : LT α, True) ===> True
+#testOptimize ["InhabitedEqualityClass"]
+  (∀ α : Type, ∃ _ : BEq α, True) ===> True
+
+inductive Color where
+  | red
+inductive Box (α : Type) where
+  | wrap : Color → Box α
+
+#testOptimize ["InhabitedConstructorFields"]
+  (∀ α : Type, ∃ _ : Box α, True) ===> True
+#testOptimize ["InhabitedFunctionCodomain"]
+  (∀ α : Type, ∃ _ : α → Color, True) ===> True
+
+end Tests.Issue226

Tests/Optimize/OptimizeBEq/BEqList.lean

@@ -4,6 +4,9 @@ import Tests.Utils
 open Lean Elab Command Term
 
 namespace Test.BEqList
+
+-- Quantifiers over arbitrary α must remain even when the body becomes False:
+-- α may be empty, so replacing the whole quantified formula by False is unsound.
 /-! ## Test objectives to validate normalization and simplification rules on ``BEq.beq instance on generic `List -/
 
 /-! Test cases for `reduceApp` rule on ``BEq.beq. -/
@@ -12,11 +15,13 @@ namespace Test.BEqList
 #testOptimize [ "BEqListCst_1" ] ∀ (α : Type), [BEq α] → (List.nil : List α) == List.nil ===> True
 
 -- List.nil == [x, y, z] ===> False (with Type(x) = α)
-#testOptimize [ "BEqListCst_2" ] ∀ (α : Type) (x y z : α), [BEq α] → List.nil == [x, y, z] ===> False
+#testOptimize [ "BEqListCst_2" ] ∀ (α : Type) (x y z : α), [BEq α] → List.nil == [x, y, z] ===>
+  ∀ (α : Type) (x y z : α), False
 
 -- [x, y] == [x, y, z] ===> False
 -- NOTE: Reduce to False via `reduceApp` rule, which is also applicable on recursive functions
-#testOptimize [ "BEqListCst_3" ] ∀ (α : Type) (x y z : α), [BEq α] → [x, y] == [x, y, z] ===> False
+#testOptimize [ "BEqListCst_3" ] ∀ (α : Type) (x y z : α), [BEq α] → [x, y] == [x, y, z] ===>
+  ∀ (α : Type) (x y z : α), False
 
 
 /-! Test cases to ensure that the following simplification rules must not be applied on

Tests/Optimize/OptimizeEq/OptimizeEq.lean

@@ -5,6 +5,9 @@ open Lean Elab Command Term
 
 namespace Test.OptimizeEq
 
+-- Quantifiers over arbitrary α must remain even when the body becomes False:
+-- α may be empty, so replacing the whole quantified formula by False is unsound.
+
 /-! ## Test objectives to validate normalization and simplification rules on ``Eq -/
 
 -- False = True ===> False
@@ -135,13 +138,16 @@ inductive Color where
 #testOptimize [ "EqConstructor_13" ] ∀ (α : Type), (List.nil : List α) = (List.nil : List α) ===> True
 
 -- List.nil = [x, y, z] ===> False
-#testOptimize [ "EqConstructor_14" ] ∀ (α : Type) (x y z : α), List.nil = [x, y, z] ===> False
+#testOptimize [ "EqConstructor_14" ] ∀ (α : Type) (x y z : α), List.nil = [x, y, z] ===>
+  ∀ (α : Type) (x y z : α), False
 
 -- [x, y] = [x, y, z] ===> False
-#testOptimize [ "EqConstructor_15" ] ∀ (α : Type) (x y z : α), [x, y] = [x, y, z] ===> False
+#testOptimize [ "EqConstructor_15" ] ∀ (α : Type) (x y z : α), [x, y] = [x, y, z] ===>
+  ∀ (α : Type) (x y z : α), False
 
 -- [z, y] = [x, y, z] ===> False
-#testOptimize [ "EqConstructor_15" ] ∀ (α : Type) (x y z : α), [z, y] = [x, y, z] ===> False
+#testOptimize [ "EqConstructor_15" ] ∀ (α : Type) (x y z : α), [z, y] = [x, y, z] ===>
+  ∀ (α : Type) (x y z : α), False
 
 -- [a + b, c] = [a + b, c, b] ===> False
 #testOptimize [ "EqConstructor_16" ] [a + b, c] = [a + b, c, b] ===> False
@@ -153,7 +159,8 @@ inductive Color where
 #testOptimize [ "EqConstructor_17" ] [b + a, c] = [a + c, c] ===> [Nat.add a b, c] = [Nat.add a c, c]
 
 -- [f x, y] = [f x, y, z] ==> False
-#testOptimize [ "EqConstructor_18" ] ∀ (α : Type) (f : α -> α) (x y z : α), [f x, y] = [f x, y, z] ===> False
+#testOptimize [ "EqConstructor_18" ] ∀ (α : Type) (f : α -> α) (x y z : α), [f x, y] = [f x, y, z] ===>
+  ∀ (α : Type) (f : α → α) (x y z : α), False
 
 -- [f x, z] = [f y, z] ==> [f x, z] = [f y, z]
 -- Must remain unchanged

Tests/Optimize/OptimizeExists/COIExists.lean

@@ -4,6 +4,9 @@ import Tests.Utils
 open Lean Elab Command Term
 
 namespace Test.COIExists
+
+-- Unused variables over arbitrary types/function spaces retain vacuity.
+-- Inhabited constructor fields now also justify eliminating a domain.
 /-! ## Test objectives to validate COI reduction on `∃`. -/
 
 /-! Test cases for COI reduction rule:
@@ -145,7 +148,7 @@ inductive Color where
 #testOptimize [ "ExistsCOI_17" ] ∀ (α : Type) (β : Type) (x : α) (y z : β), ∃ (f : α → β), ∃ (a b c : Bool),
                                    let cond := !((!a || ((b || c) && !(c || b))) || a);
                                    (if cond then f x else y) = z ===>
-                                 ∀ (α : Type) (β : Type) (y z : β), ∃ (_f : α → β), y = z
+  ∀ (α β : Type) (_x : α) (y z : β), ∃ (_f : α → β), y = z
 
 -- ∀ (α : Type) (β : Type), ∃ (f : α → β), ∃ (a b c : Bool), ∀ (x : α) (y z : β),
 --  let cond := !((!a || ((b || c) && !(c || b))) || a);
@@ -155,7 +158,7 @@ inductive Color where
 #testOptimize [ "ExistsCOI_18" ] ∀ (α : Type) (β : Type), ∃ (f : α → β), ∃ (a b c : Bool), ∀ (x : α) (y z : β),
                                    let cond := !((!a || ((b || c) && !(c || b))) || a);
                                    (if cond then f x else y) = z ===>
-                                 ∀ (α : Type) (β : Type), ∃ (_f : α → β), ∀ (y z : β), y = z
+  ∀ (α β : Type), ∃ (_f : α → β), ∀ (_x : α) (y z : β), y = z
 
 -- ∀ (α : Type), ∃ (x y : α), ∃ (ys : List α), ∀ (a b c : Bool) (xs : List α), [LT α] → [Decidable (x < y)] →
 --  let cond := ((!a || ((b || c) && !(c || b))) || a);
@@ -235,21 +238,21 @@ inductive ColorDegree (α : Type u) where
 --  let cond := ((!a || ((b || c) && !(c || b))) || a) && (!(b && a) || (a && b));
 --  (if cond then x else y) = z ===>
 --  ∀ (α : Type) (x z : ColorDegree α), ∃ (y : ColorDegree α), x = z
--- Test case: COI reduction rules not applicable when inductive type does not have at least one nullary constructor.
+-- Constructor-field search can witness ColorDegree α via ColorDegree.red Color.transparent.
 #testOptimize [ "ExistsCOIUnchanged_10" ] ∀ (α : Type) (a b c : Bool) (x z : ColorDegree α), ∃ (y : ColorDegree α),
                                             let cond := ((!a || ((b || c) && !(c || b))) || a) && (!(b && a) || (a && b));
                                             (if cond then x else y) = z ===>
-                                          ∀ (α : Type) (x z : ColorDegree α), ∃ (_y : ColorDegree α), x = z
+  ∀ (α : Type) (x z : ColorDegree α), x = z
 
 -- ∀ (α : Type) ∃ (y : ColorDegree α), ∀ (a b c : Bool) (x z : ColorDegree α),
 --  let cond := ((!a || ((b || c) && !(c || b))) || a) && (!(b && a) || (a && b));
 --  (if cond then x else y) = z ===>
 --  ∀ (α : Type) ∃ (y : ColorDegree α), ∀ (x z : ColorDegree α), x = z
--- Test case: COI reduction rules not applicable when inductive type does not have at least one nullary constructor.
+-- Constructor-field search can witness ColorDegree α via ColorDegree.red Color.transparent.
 #testOptimize [ "ExistsCOIUnchanged_11" ] ∀ (α : Type), ∃ (y : ColorDegree α), ∀ (a b c : Bool) (x z : ColorDegree α),
                                             let cond := ((!a || ((b || c) && !(c || b))) || a) && (!(b && a) || (a && b));
                                             (if cond then x else y) = z ===>
-                                          ∀ (α : Type), ∃ (_y : ColorDegree α), ∀ (x z : ColorDegree α), x = z
+  ∀ (α : Type) (x z : ColorDegree α), x = z
 
 inductive NoInstance where
  | first (n : Nat) (h : n < 0) : NoInstance
@@ -291,6 +294,6 @@ inductive NoInstance where
 #testOptimize [ "ExistsCOIUnchanged_15" ] ∀ (α : Type) (β : Type), ∃ (f : α → β), ∃ (a b c : Bool), ∀ (x : α) (y z : β),
                                              let cond := ((!a || ((b || c) && !(c || b))) || a);
                                              (if cond then f x else y) = z ===>
-                                          ∀ (α : Type) (β : Type), ∃ (f : α → β), ∀ (x : α) (z : β), z = f x
+  ∀ (α β : Type), ∃ (f : α → β), ∀ (x : α) (_y z : β), z = f x
 
 end Test.COIExists

Tests/Optimize/OptimizeForAll/COIForAll.lean

@@ -4,6 +4,9 @@ import Tests.Utils
 open Lean Elab Command Term
 
 namespace Test.COIForAll
+
+-- Unused variables over arbitrary types/function spaces retain vacuity.
+-- Inhabited constructor fields now also justify eliminating a domain.
 /-! ## Test objectives to validate COI reduction on `∀` and `→`. -/
 
 /-! Test cases for COI reduction rule:
@@ -81,7 +84,7 @@ inductive Color where
   ∀ (α : Type) (a b c : Bool) (x y : α) (xs ys : List α), [LT α] → [Decidable (x < y)] →
       let cond := !((!a || ((b || c) && !(c || b))) || a);
       (if cond then if x < y then [x, y] else [y, x] else ys) = xs ===>
-  ∀ (α : Type) (xs ys : List α), xs = ys
+  ∀ (α : Type) (x y : α) (xs ys : List α), xs = ys
 
 -- ∀ (α : Type) (β : Type) (f : α → β) (x : α) (y z : β) (a b c : Bool),
 --  let cond := !((!a || ((b || c) && !(c || b))) || a);
@@ -91,7 +94,7 @@ inductive Color where
 #testOptimize [ "ForallCOI_10" ]
   ∀ (α : Type) (β : Type) (f : α → β) (x : α) (y z : β) (a b c : Bool),
     let cond := !((!a || ((b || c) && !(c || b))) || a); (if cond then f x else y) = z ===>
-  ∀ (β : Type) (y z : β), y = z
+  ∀ (α β : Type) (f : α → β) (x : α) (y z : β), y = z
 
 
 -- ∀ (α : Type) (a b c : Bool) (x y : α) (xs ys : List α), [LT α] → [Decidable (x < y)] →
@@ -160,12 +163,12 @@ inductive ColorDegree (α : Type u) where
 --  let cond := ((!a || ((b || c) && !(c || b))) || a) && (!(b && a) || (a && b));
 --  (if cond then x else y) = z ===>
 -- ∀ (α : Type) (x y z : ColorDegree α), x = z
--- Test case: COI reduction rules not applicable when inductive type does not have at least one nullary constructor.
+-- Constructor-field search can witness ColorDegree α via ColorDegree.red Color.transparent.
 #testOptimize [ "ForallCOIUnchanged_7" ]
   ∀ (α : Type) (a b c : Bool) (x y z : ColorDegree α),
     let cond := ((!a || ((b || c) && !(c || b))) || a) && (!(b && a) || (a && b));
     (if cond then x else y) = z ===>
-  ∀ (α : Type) (x _y z : ColorDegree α), x = z
+  ∀ (α : Type) (x z : ColorDegree α), x = z
 
 inductive NoInstance where
  | first (n : Nat) (h : n < 0) : NoInstance
@@ -198,6 +201,6 @@ inductive NoInstance where
 #testOptimize [ "ForallCOIUnchanged_10" ]
   ∀ (α : Type) (β : Type) (f : α → β) (x : α) (y z : β) (a b c : Bool),
     let cond := ((!a || ((b || c) && !(c || b))) || a); (if cond then f x else y) = z ===>
-  ∀ (α : Type) (β : Type) (f : α → β) (x : α) (z : β), z = f x
+  ∀ (α β : Type) (f : α → β) (x : α) (y z : β), z = f x
 
 end Test.COIForAll

Tests/Optimize/OptimizeUnfold/UnfoldBEq.lean

@@ -5,6 +5,9 @@ open Lean Elab Command Term
 
 namespace Tests.UnfoldBEq
 
+-- Quantifiers over arbitrary α must remain even when the body becomes False:
+-- α may be empty, so replacing the whole quantified formula by False is unsound.
+
 /-! ## Test objectives to validate `BEq.beq unfolding -/
 
 /-! Test cases to validate unfolding of `BEq.beq only when reduced to a constant value or via rewriting. -/
@@ -92,7 +95,8 @@ variable (c : Nat)
 #testOptimize [ "UnfoldBEq_26" ] ∀ (α : Type), [BEq α] → (List.nil : List α) != List.nil ===> False
 
 -- ∀ (α : Type) (x y z : α), [BEq α] → List.nil == [x, y, z] ===> False
-#testOptimize [ "UnfoldBEq_27" ] ∀ (α : Type) (x y z : α), [BEq α] → List.nil == [x, y, z] ===> False
+#testOptimize [ "UnfoldBEq_27" ] ∀ (α : Type) (x y z : α), [BEq α] → List.nil == [x, y, z] ===>
+  ∀ (α : Type) (x y z : α), False
 
 -- ∀ (α : Type) (x y z : α), [BEq α] → List.nil != [x, y, z] ===> True
 #testOptimize [ "UnfoldBEq_28" ] ∀ (α : Type) (x y z : α), [BEq α] → List.nil != [x, y, z] ===> True

Tests/Optimize/OptimizeUnfold/UnfoldEq.lean

@@ -5,6 +5,9 @@ open Lean Elab Command Term
 
 namespace Tests.UnfoldEq
 
+-- Quantifiers over arbitrary α must remain even when the body becomes False:
+-- α may be empty, so replacing the whole quantified formula by False is unsound.
+
 /-! ## Test objectives to validate `Eq unfolding -/
 
 
@@ -106,7 +109,8 @@ variable (c : Nat)
 #testOptimize [ "UnfoldEq_30" ] ∀ (α : Type), (List.nil : List α) ≠ List.nil ===> False
 
 -- ∀ (α : Type) (x y z : α), List.nil = [x, y, z] ===> False
-#testOptimize [ "UnfoldEq_31" ] ∀ (α : Type) (x y z : α), List.nil = [x, y, z] ===> False
+#testOptimize [ "UnfoldEq_31" ] ∀ (α : Type) (x y z : α), List.nil = [x, y, z] ===>
+  ∀ (α : Type) (x y z : α), False
 
 -- ∀ (α : Type) (x y z : α), List.nil ≠ [x, y, z] ===> True
 #testOptimize [ "UnfoldEq_32" ] ∀ (α : Type) (x y z : α), List.nil ≠ [x, y, z] ===> True