Error with defining function application

Stream: Formalized Formal Logic

[C7X]

I'm currently trying to define the notation f ’ x for a function f and a set x (both in a model of Z), but am running into a very specific problem with implicit arguments. Since the problem is specific to this library, I think it would be too hard to create a MWE for any other channel on this Zulip. Is this an appropriate place to send my code and ask about how to fix the problem?

[Palalansoukî]

Even if it's not wme, codes explicitly showing the imports of files in FFL would help resolve the issue.

Also, in this case, I suspect it might be conflicting with abbreviation notation for Subterm?

https://github.com/FormalizedFormalLogic/Foundation/blob/4691442cac409190af478ea0fd2cd8600047f3c7/Foundation/FirstOrder/Basic/BinderNotation.lean#L235

[C7X]

I reproduced the error with the f ’ x notation removed, and I have only one public import in my file, which is public import Foundation.FirstOrder.SetTheory.Z. It seems like the error happens because of behavior of lemma which confuses me, where terms in the type of the lemma aren't able to infer implicit parameters from the context. On the other hand, terms in #check are, which demonstrates the behavior without errors that I was expecting.

Here is a MWE, which produces the same error that I'm getting without any reliance on FFL.

import Mathlib

def test (a b : ℕ) {c : ℕ → ℕ} : Prop := b = c a

-- Implicit parameters work properly here, `test a b` can see the term of type `ℕ → ℕ` and infer it.
#check ∀ (a b : ℕ), ∀ (_ : ℕ → ℕ), test a b

-- It cannot infer here.
theorem test2 : ∀ (a b : ℕ), ∀ (_ : ℕ → ℕ), test a b := by sorry

[Palalansoukî]

This is more of a design choice than an error. If you want it to take parameter c, you'd need to write it explicitly or use a typeclass to infer c.

[C7X]

Thanks! That seems unfortunate for my application, since I want to be able to write just f ’ x, with f ∈ Y ^ X and x ∈ X in the context. Would it be much different than this if I were to use a typeclass?

[Palalansoukî]

In such cases, a common approach in lean is to return a suitable value for undefined arguments. If you want to define $f ' x$, you can define a function that returns $y$ such that $(x, y) \in f$ when $x \in \mathrm{dom} f$, and returns $\empty$ otherwise.

See also: https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

[C7X]

I guess I can try this approach. Thanks!

[C7X]

I wonder what the underlying design choice was that makes the context accessible in #check but not in theorem, even though the types are the same. Maybe I should move to #**lean4...