Monomorphization of higher order function

[giuliasindoni]

I am trying to use Lean-auto in conjunction with Lean-smt.

I have this example using higher-order functions:

import Mathlib.Tactic
import Smt
import Smt.Auto

axiom world : Type

def F: Type := Nat → world

def G : Type := F → (Nat → Prop)

example (f: F) (p : G) : p f 0 ∨ ¬p f 0 := by
auto
smt

This produces this error: Auto.Monomorphization.ConstInst.ofExpr? :: G is not a `∀`

I could do monomorphization "manually":

example (f: F) (p : G) : p f 0 ∨ ¬p f 0 := by
set myprop := p f 0
smt

and this works, but I would prefer not to do this, especially as I might have many functions of like p in a single formula. Thus, I believe I should use auto.

Could you advise on this?

[giuliasindoni]

Just for more context, this is the query in smt-lib format produced by using smt_show:

query:
(set-logic ALL)
(declare-sort G 0)
(declare-const p G)
(declare-sort F 0)
(declare-const f F)
(assert (not (or (p f 0) (not (p f 0)))))
(check-sat)

[PratherConid]

You need to set_option auto.mono.mode "fol" when using Lean-auto together with lean-smt

[giuliasindoni]

Thanks a lot for the reply! Using set_option auto.mono.mode "fol" now, but the error message still appears when using auto tactic, even without using smt.

Auto.Monomorphization.ConstInst.ofExpr? :: G is not a `∀`

[PratherConid]

Ok, sorry for the confusion. Just doing set_option auto.mono.mode "fol" indeed does not solve the problem. For now to make lean-auto work on this problem you also need to unfold the types, for example (this is using lean-auto only, not lean-smt, but should also work if lean-smt is used directly)

set_option auto.mono.mode "fol"
set_option auto.smt true
example (f : Nat → world) (p : (Nat → world) → (Nat → Prop)) : p f 0 ∨ ¬p f 0 := by
  auto

Can you confirm if this works on your side?
I will think about if there's a way where lean-auto can automatically unfold some of the types. But this will be a headache because previous experiments have shown that unfolding all type definitions may cause other issues.

[giuliasindoni]

Hi, again

This does not work:


— this does not work
example (f : Nat → world) (p : (Nat → world) → (Nat → Prop)) : p f 0 ∨ ¬p f 0 := by
auto

Error message:

cannot translate 0

However using Int type instead of using Nat type seems to do the trick:

-- this works
example (f : Int → world) (p : (Int → world) → (Int → Prop)) : p f 0 ∨ ¬p f 0 := by
  auto

Both examples above fail using smt instead of auto.

Anyways, even with just auto, it seems more of a workaround at the moment than a solution, like using

example (f: F) (p : G) : p f 0 ∨ ¬p f 0 := by
set myprop := p f 0
smt

which is not really scalable.

Thanks for looking into this!

[giuliasindoni]

I was wondering, is there a reason why auto/smt can't translate when the type is Nat, but they work fine with Int? Is that something that can be easily fixed (using Nat would be more convenient in my case)?

[PratherConid]

I think the Nat/Int issue is related to lean-smt, not lean-auto. Lean-smt has problems translating Nat because Nat is not supported by smt solvers, and doing the Nat to Int conversion is nontrivial. I think there is one person on the Lean-smt side working on the Nat to Int translation right now, but please contact the author of Lean-smt. For now maybe try the zify tactic: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Zify.html, but it probably won't work for higher-order problems.