## Stream: general

### Topic: (: a ≤ b :)

#### Kevin Buzzard (Jul 04 2020 at 19:51):

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 (Jul 04 2020 at 20:15):

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 (Jul 04 2020 at 20:15):

It's used for the @[ematch] attribute

#### Mario Carneiro (Jul 04 2020 at 20:16):

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 (Jul 04 2020 at 20:16):

aka heuristic instantiation

#### Kyle Miller (Jul 04 2020 at 20:31):

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 (Jul 04 2020 at 20:31):

It is supposed to make higher order arguments explicit

#### Mario Carneiro (Jul 04 2020 at 20:32):

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

#### Mario Carneiro (Jul 04 2020 at 20:33):

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 (Jul 04 2020 at 20:36):

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?)

yes

#### Mario Carneiro (Jul 04 2020 at 20:37):

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

#### Mario Carneiro (Jul 04 2020 at 20:38):

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 (Jul 04 2020 at 20:38):

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 (Jul 04 2020 at 20:40):

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 (Jul 04 2020 at 20:41):

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

#### Mario Carneiro (Jul 04 2020 at 20:41):

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 (Jul 04 2020 at 20:42):

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

#### Eric Wieser (Apr 05 2021 at 20:57):

Is there any documentation on ematch?

Last updated: May 11 2021 at 00:31 UTC