Co-domain restriction for undeclared/axiom function and axioms for global lambdas

Solver/Smt/Translate/Application.lean

@@ -619,6 +619,11 @@ partial def inferUndeclFunType (t : Expr) (params : ImplicitParameters) : Expr :
      perform the following:
        - Let `∀ α₀ → ∀ α₁ ... → αₙ` := inferUndecFunType (← getFunEnvInfo f).type params
        - declare smt function `declare-fun s ((st₀) .. (stₙ₋₁)) stₙ)`
+       - assert the following proposition to constraint the codomain value:
+          - `(assert (forall ((@x₀ st₀) ... (@xₙ₋₁ stₙ₋₁))
+              (! (@isTypeₙ (s @x₁ ... @xₙ₋₁))
+                 :pattern ((s @x₁ ... @xₙ₋₁))) :qid s_cstr)`
+
      where ∀ i ∈ [0..n], αᵢ translates to Smt type stᵢ
 -/
 def generateUndeclaredFun
@@ -628,16 +633,29 @@ def generateUndeclaredFun
   -- infer fun type and removing implicit arguments (i.e., even class constraints)
   let funType := inferUndeclFunType pInfo.type params
   Optimize.forallTelescope funType fun fvars retType => do
+    let xsyms := Array.ofFn (λ f : Fin fvars.size => mkReservedSymbol s!"@x{f.val}")
     let mut pargs := (#[] : Array SortExpr)
+    let mut co_quantifiers := (#[] : SortedVars)
     for h : i in [:fvars.size] do
       let decl ← getFVarLocalDecl fvars[i]
       let st ← translateFunLambdaParamType decl.type termTranslator
       pargs := pargs.push st
+      co_quantifiers := co_quantifiers.push (xsyms[i]!, st)
     let ret ← translateFunLambdaParamType retType termTranslator
     declareFun s pargs ret
+    -- assert codomain constraint
+    if fvars.size > 0 then
+      let xIds := Array.map (λ v => smtSimpleVarId v) xsyms
+      let f_applyTerm := mkSimpleSmtAppN s xIds
+      let forallBody ← createPredQualifierAppAux f_applyTerm retType
+      let qidName := mkQid $ appendSymbol s "cstr"
+      let pattern := some #[mkPattern #[f_applyTerm], qidName]
+      assertTerm (mkForallTerm none co_quantifiers forallBody pattern)
+    else
+      assertTerm (← createPredQualifierAppAux (smtSimpleVarId s) retType)
 
 /-- Given `e := Expr.const n l`,
-     - When `n := false`
+     - When `n :1= false`
         - return `BoolTerm false`
      - When `n := False`
         - return `BoolTerm false`
@@ -962,10 +980,9 @@ def translateApp
      - let FunArrowType := ArrowTN st₁ ... stₘ rt
      - let decl ← generateFunInstDeclAux (← inferTypeEnv e) FunArrowType
      - let some @apply{k} := decl.applyInstName
+     - let sb := termTranslator b
      - When V = ∅
         - declare smt function `(declare-const @lambda{n} FunArrowType)`
-
-        - let sb := termTranslator b
         - assert the following proposition to properly constrain @lambda{n}:
           `(assert (forall ((x₁ st₁) ... (xₘ stₘ))
              (! (= (@apply{k} @lambda{n} x₁ ... xₘ) sb)
@@ -975,14 +992,17 @@ def translateApp
      - When V ≠ ∅
         - let (y₁, yt₁) ... (yₖ, ytₖ) := [(V[i], translateFunLambdaParamType V[i].type termTranslator) | i ∈ [0..V.size-1]]
         - let GlobalArrowType := ArrowTN yt₁ ... ytₖ FunArrowType
+        - let [v₁, ..., vₖ] = V
+        - let globalType ← ∀ v₁ → ... ∀ vₖ → outParam (← inferTypeEnv e)
+        - let globalDecl ← generateFunInstDeclAux globalType GlobalArrowType
+        - let some @apply{n} := globalDecl.applyInstName
         - declare smt function `(declare-const @global_lambda{n} GlobalArrowType)`
-        - declare global apply function `(declare-fun @global_apply{n} (GlobalArrowType yt₁ ... ytₖ) FunArrowType)`
-        - assert the following proposition to properly constrain @lambda{n} and @global_lambda{n}!
+        - assert the following proposition to properly constrain @global_lambda{n}!
            - `(assert (forall ((y₁, yt₁) ... (yₖ, ytₖ) (x₁, st₁) ... (xₘ, stₘ))
-               (! (= (@apply{k} (@global_apply{n} @global_lambda{n} y₁ ... yₖ) x₁ ... xₘ) sb)
-                  :pattern ((@apply{k} (@global_apply{n} @global_lambda{n} y₁ ... yₖ) x₁ ... xₘ))
+               (! (= (@apply{k} (@apply{n} @global_lambda{n} y₁ ... yₖ) x₁ ... xₘ) sb)
+                  :pattern ((@apply{k} (@apply{n} @global_lambda{n} y₁ ... yₖ) x₁ ... xₘ))
                   :qid @global_lambda{n}_def_cstr)))`
-       - return `(@global_apply{n} @global_lambda{n} y₁ ... yₖ)`
+       - return `(@apply{n} @global_lambda{n} y₁ ... yₖ)`
 -/
 def translateLambda
   (e : Expr) (termTranslator : Expr → TranslateEnvT SmtTerm) : TranslateEnvT SmtTerm := do
@@ -1005,7 +1025,8 @@ def translateLambda
    let funArrowType := paramSort arrowT ((Array.map (λ s => s.2) svars).push rt)
    -- generate apply function with corresponding congruence assertions (or retriving if already declared).
    let decl ← generateFunInstDeclAux lamType funArrowType
-   let some applyName := decl.applyInstName | throwEnvError "translateLambda: @apply instance function expected !!!"
+   let some applyName := decl.applyInstName
+       | throwEnvError "translateLambda: @apply instance function expected !!!"
    let lvars ← retrieveLocalFVars (getLambdaBody e)
    let sb ← termTranslator b
    if lvars.isEmpty then
@@ -1028,14 +1049,17 @@ def translateLambda
      gvars := gvars.push (← fvarIdToSmtSymbol fv.fvarId!, st)
     let arrowT ← declareArrowTypeSort (lvars.size + 1)
     let globalArrowType := paramSort arrowT ((Array.map (λ s => s.2) gvars).push funArrowType)
+    -- wrapping lamType within `outParam` to properly generate function instance
+    let globalType ← Optimize.mkForallFVars' lvars (mkApp (mkConst ``outParam) lamType)
+    -- generate apply function with corresponding congruence assertions for global lambda
+    let globalDecl ← generateFunInstDeclAux globalType globalArrowType
     -- declare global lambda function `(declare-const @global_lambda{n} GlobalArrowType)`
     let globalName := mkReservedSymbol s!"@global_lambda{v}"
     let globalId := smtSimpleVarId globalName
     declareConst globalName globalArrowType
-    -- declare global apply function `(declare-fun @global_apply{n} (GlobalArrowType yt₁ ... ytₖ) FunArrowType)`
-    let globalApplyName := mkReservedSymbol s!"@global_apply{v}"
-    let declArgs := Array.foldl (λ acc s => acc.push s.2) #[globalArrowType] gvars
-    declareFun globalApplyName declArgs funArrowType
+    -- asserting global lambda definition
+    let some globalApplyName := globalDecl.applyInstName
+        | throwEnvError "translateLambda: @apply instance function expected !!!"
     let gArgs := Array.foldl (λ acc s => acc.push (smtSimpleVarId s.1)) #[globalId] gvars
     let globalAppTerm  := mkSimpleSmtAppN globalApplyName gArgs
     let applyArgs := Array.foldl (λ acc s => acc.push (smtSimpleVarId s.1)) #[globalAppTerm] svars

Solver/Smt/Translate/Quantifier.lean

@@ -538,7 +538,11 @@ def generateFunInstDeclAux (t : Expr) (st : SortExpr) : TranslateEnvT IndTypeDec
        return decl
 
   where
-    generateApplyFunAndAssertions (t : Expr) (instName : SmtSymbol) (applyName : SmtSymbol): TranslateEnvT Unit := do
+    removeOutParam : Expr → Expr
+     | Expr.app (Expr.const ``outParam _) e => e
+     | e => e
+
+    generateApplyFunAndAssertions (t : Expr) (instName : SmtSymbol) (applyName : SmtSymbol) : TranslateEnvT Unit := do
      let funTypes := retrieveArrowTypes t
      let .ParamSort _ smtTypes := st | throwEnvError "defineFunAssertions: ParamSort expected but got {st}"
      let nbTypes := funTypes.size - 1
@@ -568,7 +572,8 @@ def generateFunInstDeclAux (t : Expr) (st : SortExpr) : TranslateEnvT IndTypeDec
        co_quantifiers := co_quantifiers.push (xsyms[i]!, smtTypes[i]!)
        arg_quantifiers := (arg_quantifiers.push (xsyms[i]!, smtTypes[i]!)).push (ysyms[i]!, smtTypes[i]!)
      -- isFun constraint
-     let coDomainCstr ← createPredQualifierAppAux f_applyTerm1 funTypes[nbTypes]!
+     -- Need to remove outParam on return type (if necessary) (see, translateLambda)
+     let coDomainCstr ← createPredQualifierAppAux f_applyTerm1 (removeOutParam funTypes[nbTypes]!)
      let forallCoDomain := mkForallTerm none co_quantifiers coDomainCstr none
      let f_funPredApp := mkSimpleSmtAppN instName #[fId]
      let forallFunBody := eqSmt forallCoDomain f_funPredApp

Tests/Issues.lean

@@ -26,3 +26,5 @@ import Tests.Issues.Issue25
 import Tests.Issues.Issue26
 import Tests.Issues.Issue27
 import Tests.Issues.Issue28
+import Tests.Issues.Issue29
+

Tests/Issues/Issue29.lean

@@ -0,0 +1,22 @@
+import Lean
+import Solver.Command.Tactic
+
+namespace Tests.Issue29
+
+-- Issue: Unexpected counterexample
+-- Diagnosis : We need to add codomain constraint for undeclared/axiom functions.
+
+set_option warn.sorry false
+
+class ToNat (α : Type u) where
+  toNat : α → Nat
+
+theorem toNat_cstr (α : Type) (β : Type) (_h1 : ToNat α) (_h2 : ToNat β) (x : α) (y : β) :
+  Int.ofNat (ToNat.toNat x) + Int.ofNat (ToNat.toNat y) ≥ 0 := by blaster
+
+axiom natCast : α → Nat
+
+theorem natCast_cstr (α : Type) (β : Type) (x : α) (y : β) :
+  Int.ofNat (natCast x) + Int.ofNat (natCast y) ≥ 0 := by blaster
+
+end Tests.Issue29