Zulip Chat Archive
Stream: general
Topic: How to check whether a term is (0: Nat)?
Dexin Zhang (Mar 08 2025 at 16:07):
t.isConstOf ``Nat.zero doesn't work...
import Lean
open Lean Meta Elab Tactic
elab "test" t:term : tactic => do
let t ← whnf (← elabTerm t none)
logInfo m!"{t.isConstOf ``Nat.zero}"
example : False := by
test 0 -- false
Markus Himmel (Mar 08 2025 at 16:10):
How about this:
import Lean
open Lean Meta Elab Tactic
elab "test" t:term : tactic => do
let o ← getOfNatValue? (← elabTerm t none) `Nat
let isZero := o.any (·.1 = 0)
logInfo m!"{isZero}"
example : False := by
test 0 -- true
test 1 -- false
test (0 : Int) -- false
Markus Himmel (Mar 08 2025 at 16:12):
Though I'm not sure if it's exactly what exactly you want. The code I posted returns false for test Nat.zero.
Dexin Zhang (Mar 08 2025 at 16:14):
Thanks! I think getNatValue? is enough for me
Dexin Zhang (Mar 08 2025 at 16:14):
Or there might be a nicer way?
Markus Himmel (Mar 08 2025 at 16:15):
This could also work for you:
import Lean
open Lean Meta Elab Tactic
elab "test" t:term : tactic => do
let t ← elabTerm t none
let b ← isDefEq t (.const `Nat.zero [])
logInfo m!"{b}"
example : False := by
test 0 -- true
test 1 -- false
test (0 : Int) -- false
test Nat.zero -- true
Aaron Liu (Mar 08 2025 at 16:15):
Why do you need this?
Dexin Zhang (Mar 08 2025 at 16:19):
Aaron Liu said:
Why do you need this?
I'm writing a tactic that process terms of xxx n (xxx : Nat → Type), but if it's xxx 0 I can do some special stuffs
Dexin Zhang (Mar 08 2025 at 16:20):
I find getRawNatValue? exactly what I want
elab "test" t:term : tactic => do
let t ← whnf (← elabTerm t none)
logInfo m!"{getRawNatValue? t == some 0}"
example : False := by
test 0 -- true
Aaron Liu (Mar 08 2025 at 16:52):
I would suggest something like this
import Lean
open Lean Meta Elab Term
def test (stx : Syntax) : TermElabM Bool := do
let t ← elabTerm stx (some Nat.mkType)
withNewMCtxDepth (isDefEq t (mkNatLit 0))
Kyle Miller (Mar 08 2025 at 18:02):
The issue here is that elabTerm is only initializing term elaboration. There are still pending elaboration problems (the fact that it is a Nat will only be resolved later, once default instances are considered).
Kyle Miller (Mar 08 2025 at 18:03):
@Aaron Liu's isDefEq solution appears to work because it's assigning metavariables (the instances are assignable)
Kyle Miller (Mar 08 2025 at 18:04):
Edit: actually, it looks like you were using the Tactic version of elabTerm in your initial post, which does have a step to complete all elaboration problems. I have to check what's going on.
Kyle Miller (Mar 08 2025 at 18:08):
Ok, it looks like you are already working with getRawNatValue? and figured out the solution (I should read the whole thread before commenting). There's also Expr.rawNatLit? that would work here, which does basically the same thing. I changed elabTerm to Tactic.elabTerm to reduce risk of confusion about which one you're using:
import Lean
open Lean Meta Elab Tactic
elab "test" t:term : tactic => do
let t ← whnf (← Tactic.elabTerm t none)
let isZero := t.rawNatLit? == some 0
logInfo m!"{isZero}"
example : False := by
test 0 -- true
Kyle Miller (Mar 08 2025 at 18:14):
If you're looking for a natural number literal, I believe the correct answer is docs#Lean.Meta.getNatValue?
elab "test" t:term : tactic => do
let t ← Tactic.elabTerm t none
let isZero := (← getNatValue? t) == some 0
logInfo m!"{isZero}"
I would strongly suggest not using whnf or isDefEq unless you do indeed want to reduce an expression to a literal, potentially performing an expensive calculation.
Eric Wieser (Mar 09 2025 at 23:41):
(deleted)
loogle (Mar 09 2025 at 23:41):
:exclamation: unknown identifier 'Expr'
Did you mean Nat.Linear.Expr -> Option Nat, Nat.SOM.Expr -> Option Nat, or something else?
Eric Wieser (Mar 09 2025 at 23:41):
@loogle Lean.Expr -> Option Nat
loogle (Mar 09 2025 at 23:41):
:search: Lean.Expr.nat?, Lean.Expr.rawNatLit?, and 8 more
Eric Wieser (Mar 09 2025 at 23:42):
Is there a description anywhere of how all these differ?
Eric Wieser (Mar 09 2025 at 23:42):
@loogle Lean.Expr -> Lean.MetaM Nat
loogle (Mar 09 2025 at 23:43):
:search: Lean.Meta.getExpectedNumArgs, Lean.Meta.NormCast.countCoes, and 4 more
Aaron Liu (Mar 09 2025 at 23:44):
Why would you need MetaM?
Eric Wieser (Mar 09 2025 at 23:48):
That was a bad loogle query guess, but I think docs#getNatValue? is in metam
Aaron Liu (Mar 09 2025 at 23:48):
Eric Wieser said:
Is there a description anywhere of how all these differ?
I'll type something up
Aaron Liu (Mar 10 2025 at 00:24):
Here
Last updated: May 02 2025 at 03:31 UTC