notation and variables

Stream: general

[Kevin Buzzard]

It suddenly occurs to me, about 10 hours before a lecture (and I intend to spend at least 7 of those hours sleeping) that it would be cool if I could do some examples of basic arguments with equivalence relations in Lean, live in the lecture. But actually I am not sure of the best way to do this. Here's the sort of thing I want to do -- prove, for example, that if r is an equivalence relation, and r a b and r c b and r c d, then r a d. But I want to do it with notation -- I want to write a ~ b or some -- any -- random symbol, rather than the prefix notation r. However when I define r : S -> S -> Prop as a variable I find that I can't use notation, because r is a local variable, and if I define r within an example -- example (S : Type) (r : S -> S -> Prop)... then I can't figure out how to get notation working before I state the theorem. What am I missing? This is for teaching purposes, so I want it to look as slick as possible.

variables (S : Type) (r : S → S → Prop)

example (H : equivalence r) : ∀ a : S, r a a := H.1

That is not ideal either -- H.1 looks a bit weird to a mathematician :-/ But I think I'd rather have the notation, and worry about H.1 later...

[Reid Barton]

You can use local notation. For example https://gist.github.com/rwbarton/7bd5b3b19d930f577355a596a5ed8b4d#file-crec-lean-L7
I don't think the fact that I used parameter rather than variable there matters for this

[Kevin Buzzard]

import tactic.interactive

variables (S : Type) (r : S → (S → Prop))

local notation a ` ~ ` b := r a b

example (H : equivalence r) (a b c d : S)
  (Hab : a ~ b) (Hcb : c ~ b) (Hcd : c ~ d) : a ~ d :=
begin
  rcases H with ⟨Hrefl,Hsymm,Htrans⟩,
  have Hbc : b ~ c,
    exact Hsymm Hcb,
  have Hac : a ~ c,
    exact Htrans Hab Hbc,
  exact Htrans Hac Hcd,
end

Works! I am in two minds about whether to use rcases or cases twice and save myself the import.

[Kevin Buzzard]

Thanks Reid.

[Mario Carneiro]

don't save yourself the import

[Mario Carneiro]

I think it is good to show off mathlib tactics when possible

[Kevin Buzzard]

Hey! I've just noticed that the pretty printer doesn't use my nice notation for r!

[Kevin Buzzard]

aww man, that's a bit annoying. I definitely want to work with an arbitrary equivalence relation but I'd really like the notation.