(: a ≤ b :)

Stream: general

[Kevin Buzzard]

Smileys in mathlib (src.order.lattice, line 19)

section
-- TODO: this seems crazy, but it also seems to work reasonably well
@[ematch] theorem le_antisymm' [partial_order α] : ∀ {a b : α}, (: a ≤ b :) → b ≤ a → a = b :=
@le_antisymm _ _
end

What's with the (: a ≤ b :)? It's not notation -- what is it?

[Kyle Miller]

According to lean/src/frontends/lean/builtin_exprs.cpp, those brackets delimit a pattern, like what comes in the left-hand-side of a let assignment. I'm not sure what that means in a type.

[Mario Carneiro]

It's used for the @[ematch] attribute

[Mario Carneiro]

I believe the meaning is that if we see a <= b in the context, then we see if we can prove b <= a and add a = b to the context

[Mario Carneiro]

aka heuristic instantiation

[Kyle Miller]

Looking through that file, there's @@foo notation for some kind of partial explicit version of foo, but I don't see the pattern for which arguments of @foo are included. It seems to include type class arguments and some quasi-random assortment of {...} arguments. Is there any documentation or explanation for partial explicit notation?

[Mario Carneiro]

It is supposed to make higher order arguments explicit

[Mario Carneiro]

the main motivation is to get to the motive in recursors like eq.rec

[Mario Carneiro]

A very short comment:

    enum class arg_mask {
        AllExplicit /* @ annotation */,
        InstHoExplicit, /* @@ annotation (i.e., instance implicit and higher-order arguments are explicit  */
        Default /* default behavior */
    };

[Kyle Miller]

I'm not too familiar with the terminology (other than the "motive is not type correct" error). So, to check, C in the following is the motive?

eq.rec : Π {α : Sort u_2} {a : α} {C : α → Sort u_1}, C a → Π {a_1 : α}, a = a_1 → C a_1

And "higher-order" refers to it being an argument of a higher sort than the rest? (Sort of like first-order vs second-order logic?)

[Mario Carneiro]

yes

[Mario Carneiro]

the higher order is because it is matched using a limited kind of higher order unification

[Mario Carneiro]

A first order match of C a_1 against a goal like a = b would set a_1 := b and C := (=) a which is not usually what we want

[Mario Carneiro]

A higher order match will find instances of a_1 in the goal, replace them with a variable x, and then set C := \lam x, ...

[Mario Carneiro]

for example if the goal is a = a then first order matching ?C a against it yields ?C := eq a, and higher order matching yields ?C := \lam x, x = x

[Kyle Miller]

Oh, I see, higher order in the sense that it's a function that's being unified (with appropriate generalization)

[Mario Carneiro]

In fact, full higher order matching yields other solutions as well, like ?C := \lam x, x = a. Lean 2 used to do backtracking on all these but it was too slow and unpredictable so higher order matching is now only used in a very limited way in recursors

[Mario Carneiro]

The @[elab_as_eliminator] attribute is a hint to lean to use higher order matching

[Eric Wieser]

Is there any documentation on ematch?