Lean4 tutorials : understanding the ▸

Stream: new members

[Shubham Kumar]

So there is a statement in the tutorial

The macro h ▸ e uses more effective heuristics for computing this implicit parameter, and often succeeds in situations where applying Eq.subst fails.

I don't understand what is the underlying mechanism or semantics of ▸ that is different from Eq.subst

[Mario Carneiro]

The function is just Eq.subst (or Eq.substr, but that's not super important). The difference is in the elaborator, the thing that decides how to fill in the higher order argument motive to the Eq.subst application. The generic elaborator for applying functions uses a different heuristic which is based on matching the goal against an application, while the \t elaborator uses a heuristic more similar to rw, where it takes the entire goal and replaces all occurrences of the LHS of the provided equality with the variable

[Shubham Kumar]

so the ▸ acts as a tactic, is that what you are trying to say because it does some magic underneath by replacing all occurrences of the LHS

[Kevin Buzzard]

(deleted)

[Jason Rute]

I think it is more accurate to say that it acts as semantic sugar where the de-sugaring depends on context a bit. I think it uses a macro, and I don’t think it technically goes through the tactic framework, but I could be mistaken on the difference. In particular, tactics are not saved, in Lean, but notation, and some other forms of semantic sugar are. In this case at least some of the information about ▸ is saved while other parts seem to be rewritten before saving the proof.

For a really straight forward proof, it saves it internally as I type it:

def abEq (A B : Type) (a : A) (ab : A = B): B :=
  ab ▸ a

#print abEq
-- def abEq : (A B : Type) → A → A = B → B :=
-- fun A B a ab => ab ▸ a

However, if I use the equality in the opposition order, then Lean swaps the order of the equalities as it saves the proof.

def baEq (A B : Type) (a : A) (ba : B = A): B :=
  ba ▸ a

#print baEq
-- def baEq : (A B : Type) → A → B = A → B :=
-- fun A B a ba => (_ : A = B) ▸ a

The _ is just pretty printing which hides certain proofs when pretty printing. To see the proof, we can change the pretty printer settings:

set_option pp.proofs true     -- to see proofs of Eq.symm
#print baEq
-- def baEq : (A B : Type) → A → B = A → B :=
-- fun A B a ba => Eq.symm ba ▸ a

The remaining ▸ are notation for Eq.rec:

set_option pp.notation false  -- to remove ▸
#print baEq
-- def baEq : (A B : Type) → A → Eq B A → B :=
-- fun A B a ba => Eq.rec a (Eq.symm ba)

Eq.rec (the built in recursor for equality) has a lot of implicit parameters which are filled in automatically:

set_option pp.explicit true   -- to see implicit params
#print baEq
-- def baEq : (A B : Type) → A → @Eq Type B A → B :=
--fun A B a ba => @Eq.rec Type A (fun x h => x) a B (@Eq.symm Type B A ba)

This feature is discussed a bit more in docs4#Eq and in Equality section of the manual.

[Shubham Kumar 🦀 (he/him)]

Thanks @Jason Rute that makes it a little bit clearer