noob question

Stream: new members

[Wojciech Nawrocki]

Hello! Very new to Lean and logic in general; i'm interested in how i can find the function names that i might need for various deduction steps (e.g. and.intro), since the std/maths library sections of "theorem proving in lean" are empty :anguished: in particular, i want to go from ¬p → false to p

[Patrick Massot]

https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L160

[Patrick Massot]

This is in directory init of the core library, so you don't have to import anything, but it's in namespace classical so you need either open the namespace or use the full name

[Johan Commelin]

Welcome to Lean! Figuring out the names of lemmas etc is still a bit of a dark art. Most of us are learning by asking lots of questions here. So feel free to ask more :smiley:

[Patrick Massot]

Yes, welcome, and don't let constructivist Kenny scare you!

[Johan Commelin]

Also, don't mind about Kenny. He doesn't like the stuff in classical.lean. But he's a nice guy if you ignore that bit :rolling_on_the_floor_laughing:

[Bryan Gin-ge Chen]

See also this discussion in the book "Logic and Proof".

[Johan Commelin]

There's a subtle difference between constructive mathematics and constructive pedagogy.

[Rob Lewis]

But more generally, if you're looking for theorems that follow a particular pattern, you can try the #find command. e.g.

import tactic.find
#find  (¬ _ → false) → _

[Wojciech Nawrocki]

Oh, that book looks great, maybe it should also be visible in the "Documentation" section of leanprover.github.io . I'll definitely give it a go! I came across this while trying to prove de morgan both ways, and turns out classical is indeed required :) https://math.stackexchange.com/questions/120187/do-de-morgans-laws-hold-in-propositional-intuitionistic-logic

[Johan Commelin]

You can PR that book to the documentation of mathlib, if you want (-;

[Wojciech Nawrocki]

How horrible is this proof? :mischievous:

variables p q : Prop

theorem de_morgan_1_a (hnpnq: ¬p ∨ ¬q): ¬(p ∧ q) :=
  assume (hpq: p ∧ q),
  or.elim hnpnq
    (assume hnp: ¬p,
      show false, from hnp hpq.left)
    (assume hnq: ¬q,
      show false, from hnq hpq.right)

-- only provable within classical logic!
theorem de_morgan_1_b (hnpq: ¬(p ∧ q)): ¬p ∨ ¬q :=
  classical.by_contradiction
    (assume not_conclusion: ¬(¬p ∨ ¬q),
      have hpq: p ∧ q, from and.intro
        (show p, from classical.by_contradiction
          (assume hnp: ¬p,
            not_conclusion (show ¬p ∨ ¬q, from or.intro_left (¬q) hnp)))
        (show q, from classical.by_contradiction
          (assume hnq: ¬q,
            not_conclusion (show ¬p ∨ ¬q, from or.intro_right (¬p) hnq))),
      show false, from hnpq hpq)

theorem de_morgan_1: ¬(p ∧ q) ↔ ¬p ∨ ¬q :=
  -- annpoying having to specify p and q
  iff.intro (de_morgan_1_b p q) (de_morgan_1_a p q)

[Kenny Lau]

it's alright

[Bryan Gin-ge Chen]

In the last theorem, you can use underscores instead of p's and q's if you want.

[Kevin Buzzard]

It's so much easier and nicer to do it in tactic mode if you're going to spell it all out like this:

variables p q : Prop

theorem de_morgan_1_a (hnpnq: ¬p ∨ ¬q): ¬(p ∧ q) :=
begin
  intro hpq,
  cases hnpnq with hnp hnq,
  { apply hnp,
    exact hpq.left},
  { apply hnq,
    exact hpq.right}
end

[Kevin Buzzard]

You can see where you're going!

[Kevin Buzzard]

If you're going to do it in term mode you may as well just do

variables p q : Prop

theorem de_morgan_1_a (hnpnq: ¬p ∨ ¬q): ¬(p ∧ q) :=
λ hpq, or.elim hnpnq (λ hnp, hnp hpq.1) (λ hnq, hnq hpq.2)

[Kenny Lau]

yeah but you've already known Lean for a year

[Kevin Buzzard]

Kenny can you golf de_morgan_1_b?

[Kevin Buzzard]

oh it will already be in mathlib I guess

[Wojciech Nawrocki]

Thanks for the feedback! Haven't quite grasped tactics yet, so doing things explicitly for now

[Kevin Buzzard]

tactics are the bomb if you're a learner. I don't know why they leave them so late in TPIL.

[Kevin Buzzard]

theorem de_morgan_1_a (hnpnq: ¬p ∨ ¬q): ¬(p ∧ q)
| ⟨hp, hq⟩ := or.elim hnpnq (absurd hp) (absurd hq)

Mathlib's proof.

[Kevin Buzzard]

Absolutely terrifying for beginners :-)

[Kevin Buzzard]

The theorem is supposed to be constructing a proof of false from a proof of p and q, so the equation compiler matches the proof of p and q with a proof of p and a proof of q and then it's pretty much the same as before.

[Kevin Buzzard]

re: specifying p and q. How about this?

variables {p q : Prop} -- trick for making variables implicit

theorem de_morgan_1_a (hnpnq: ¬p ∨ ¬q): ¬(p ∧ q) :=
  assume (hpq: p ∧ q),
  or.elim hnpnq
    (assume hnp: ¬p,
      show false, from hnp hpq.left)
    (assume hnq: ¬q,
      show false, from hnq hpq.right)

-- only provable within classical logic!
theorem de_morgan_1_b (hnpq: ¬(p ∧ q)): ¬p ∨ ¬q :=
  classical.by_contradiction
    (assume not_conclusion: ¬(¬p ∨ ¬q),
      have hpq: p ∧ q, from and.intro
        (show p, from classical.by_contradiction
          (assume hnp: ¬p,
            not_conclusion (show ¬p ∨ ¬q, from or.intro_left (¬q) hnp)))
        (show q, from classical.by_contradiction
          (assume hnq: ¬q,
            not_conclusion (show ¬p ∨ ¬q, from or.intro_right (¬p) hnq))),
      show false, from hnpq hpq)

theorem de_morgan_1: ¬(p ∧ q) ↔ ¬p ∨ ¬q :=
  -- no longer annpoying
  iff.intro (de_morgan_1_b) (de_morgan_1_a)

[Wojciech Nawrocki]

Oh, that's nice! I missed that they can be made implicit globally
re: mathlib, i'll just quote TPIL: "Once again, you should exercise judgment as to whether such abbreviations enhance or diminish readability."

[Kevin Buzzard]

Instead of assuming classical logic, mathlib (in logic/basic.lean) just assumes decidability of p:

theorem de_morgan_1_b (hnpq: ¬(p ∧ q)) [decidable p] : ¬p ∨ ¬q :=
if hp : p then or.inr (λ hq, hnpq ⟨hp, hq⟩) else or.inl hp

[Kevin Buzzard]

my impression is that mathlib is not meant to be readable, they are looking for speed and breadth

[Wojciech Nawrocki]

Hm, more noob questions, what's the difference between classical logic and "decidable p"? Since LEM states that p is either true or false, isn't that effectively "p is decidable"?

[Kevin Buzzard]

Here's a classical proof.

theorem de_morgan_1_b (hnpq: ¬(p ∧ q)) : ¬p ∨ ¬q :=
or.elim (classical.em p) (λ hp, or.inr $ λ hq, hnpq ⟨hp, hq⟩) or.inl

[Chris Hughes]

Not quite, em means you know p is either true or false, decidable means you know which one.

[Kevin Buzzard]

The classical proof gives this:

#print axioms de_morgan_1_b
/-
classical.choice
quot.sound
propext
-/

The decidable proof uses no "maths axioms"

[Kevin Buzzard]

As Chris says, assuming decidability is slightly stronger. But to a mathematician like me they're all the same.

[Kevin Buzzard]

Furthermore they're all assumable without any worries :-)

[Kevin Buzzard]

Johannes Hoelzl once argued that trying to write as small proofs as possible was a good exercise.

[zaa]

Hello! Is there some way to use Lean without emacs or VisualStudio? Asking for CoqIde-like editor would be probably too much, but maybe there's some way to use Notepad or command line?

[Patrick Massot]

Sure, you can use command line, after editing your file in any editor you like

[Kenny Lau]

you can always use any editor to edit the file and then lean --make the file, although you won't be able to interact easilier

[Scott Olson]

In case you're not familiar, the Lean reference manual recommends use with Visual Studio Code, which is actually a completely separate IDE from Visual Studio, which is cross platform, simpler, etc. I personally find the experience using Lean in VSCode similar to using CoqIde

[Kenny Lau]

(why isn't easilier a word?)

[zaa]

Ok, then I will both try Visual Studio Code and get used to lean --make.
Thank you!

[Kevin Buzzard]

I'm not sure lean --make will be much fun, but I could imagine it would work. Two other possibilities are the Lean Web Editor, and CoCalc; these are both web-based ways to run Lean. I use unix and am quite anti-MS software in general (and they typically don't target my platform anyway) but actually I've had a very positive experience using VS code in linux. Emacs runs in a terminal window.

[zaa]

Lean: Error: Command failed: lean --version 'lean' is not recognized as an internal or external command, operable program or batch file.

Trying to run Lean extension in VSCode. I have added both necessary paths to PATH, but, it seems, i'm missing something else.

[Kenny Lau]

maybe you have a space in your path

[zaa]

It's working now, yay. I just closed and reopened VSCode.

[Chris Hughes]

(why isn't easilier a word?)

I think it's because it's an adverb not an adjective. Off the top of my head, I can't think of any English adverbs that can be suffixed with -er.

[zaa]

Does Lean have a tactic similar to Omega in coq?

[Kevin Buzzard]

I believe the answer is "not yet". I know nothing about Coq but I've heard people talk about Omega. Can you briefly describe what it does? Another noob question :-)

[Kevin Buzzard]

We have linarith and cc.

[Mario Carneiro]

I think omega is cooper

[zaa]

It solves goals in Presburger arithmetic. Equalities containing only addition and substraction (and multiplication by constant, ofc).

For example: 8n = 4m+3 -> False

[Mario Carneiro]

what do you use it for? is it just divisibility goals like that one?

[zaa]

Oh, it seems to work with inequalities too. Will test on Coq a bit, as I have already forgotten things.

[Mario Carneiro]

no, my question is when do you think "I should use omega"

[Mario Carneiro]

I know about presburger arithmetic but I think it's probably a bit too wide a target - I doubt people really need the crazy quantifier complexity part

[zaa]

https://coq.inria.fr/refman/addendum/omega.html - found the documentation.
There's an example:
z > 0 -> 2 * z + 1 > z

As far as i can remember, I mostly used it for goals like
[inequality/equality] -> [another one] -> x = something
or A <= x <= B
or maybe False

[Mario Carneiro]

cooper is a tactic for presburger arithmetic written in lean by Seul Baek, but I don't think it is ready for production

[Kevin Buzzard]

https://coq.inria.fr/refman/addendum/omega.html - found the documentation.

Oh thank you! I know nothing about Coq or where to look for this stuff.

[zaa]

Yes, that's the website where it lives. I had fun with Coq for some time but paused it some year ago (will return to it soon, probably simultaneously to more serious lean learning).

[zaa]

Next noob question:
Is there some simple example/tutorial of quotient types - how to define and use them?

[Reid Barton]

There is a section in TPIL: https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients

[Reid Barton]

For a real-world example you can take a look at linear_algebra.quotient_module

[zaa]

Thank you!

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/teaching.20use.20of.20quotients.20in.20Lean

[Kevin Buzzard]

I wrote https://github.com/kbuzzard/xena/blob/master/xenalib/m1f/zmod37.lean specifically to help some of my students to learn about using quotients in Lean.

[Wojciech Nawrocki]

Using my old thread for more noob questions:
Can I use something like cases but without stating the hypothesis name? Namely, I'd like a tactic that splits conjunctions into two hypotheses and disjunctions into two goals. More generally, how does one go about searching for tactics that do something?

[Johan Commelin]

split will split goals.

[Wojciech Nawrocki]

Yep, sorry I should've specified - I want to split hypotheses.

[Johan Commelin]

Like have h1 := h.left, have h2 := h.right?

[Johan Commelin]

And now you want to do that automatically for all hypotheses, recursively?

[Reid Barton]

cases does both of those things already, so I guess you mean something that applies cases automatically?

[Wojciech Nawrocki]

Yep, that would be for ANDs, but without stating what the name is, and also do it for ORs (in which case two or more goals would appear). Yep, automatically and recursively.

[Reid Barton]

I think the answer to the more general question is "read through https://github.com/leanprover/mathlib/blob/master/docs/tactics.md, and then look through tactic.interactive in mathlib and more generally the rest of tactic.* to find more things"

[Reid Barton]

tidy does things like this; it tries a bunch of different tactics in a loop, one of which is auto_cases

[Wojciech Nawrocki]

That looks about right, thanks!

[Rob Lewis]

safe will do this, and a bit more. I think it should be less aggressive than tidy.

[Wojciech Nawrocki]

Oh damn, it just solves everything by itself O.o

[Keeley Hoek]

c.f. auto_cases

[Wojciech Nawrocki]

More questions!
What's the syntax for matching on inductive constructors by name? E.g. for list, something like Nil => 0, Cons(hd, tl) => 1 + (len tl) would be a Rust way to define len recursively

[Bryan Gin-ge Chen]

Do you mean something like this?

def len : list α → ℕ
| list.nil := 0
| (list.cons a b) := 1 + len b

[Wojciech Nawrocki]

Yep that's it - thanks!

[Wojciech Nawrocki]

Ignore me, mixed up my languages.

[Wojciech Nawrocki]

Is there any reason why fin and multiset don't support the {1, 2, 3} notation that set does? What's the best way to construct concrete finsets?

[Johan Commelin]

Do you want a type or a set?

[Chris Hughes]

You need decidable_eq α to use that notation for finset α.

[Chris Hughes]

For multisets this works for me without any decidability assumptions

example {α : Type*} (a b c : α) : multiset α := {a,b,c}

[Wojciech Nawrocki]

@Johan Commelin a concrete set, say {v} for some given v: \a
@Chris Hughes ah indeed, why does set not require it then?

[Chris Hughes]

They notation is for has_insert.insert
For sets insert a s := {b : α | b = a ∨ b ∈ s}, and there's no decidable equality required.

For finsets, there has to be an underlying list with no duplicates, so it has to check whether a is already in the set, which requires decidable_eq

[Wojciech Nawrocki]

Then given a singleton set, how can I extract the element? I tried folding it into a list to grab the first element, but fold requires commutativity and list.append is not commutative.

[Chris Hughes]

Do you have a proof that it's a singleton? I think there's a PR about finite unique computable choice.

[Wojciech Nawrocki]

Yeah, i'm grabbing it under the assumption that card vals = 1.

[Chris Hughes]

do you need it to be computable? You can use finset.exists_mem_of_ne_empty if you don't. Do you need the fact that everything in the singleton is equal?

[Wojciech Nawrocki]

I think exists_mem_of_ne_empty will work. thx!

[Wojciech Nawrocki]

So now i'm seeing a really strange error when trying to decompose the Exists:

constant α: Type
constant a: α
constant as: finset α
#check a ∈ as -- Prop
constant ex : ∃ (a : α), a ∈ as
def test := match ex with ⟨a, b⟩ := -- induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
  0
end

[Kevin Buzzard]

The recursor only eliminates into prop and your goal is a type

[Kevin Buzzard]

so the recursor cannot be applied

[Wojciech Nawrocki]

Yep, I just realised this. Basically, i'm trying to extract a concrete value of the type \a from a proof of existence. But I guess this could only work in purely constructionist logic?

[Kevin Buzzard]

There are tools in the classical namespace which should let you do this

[Kevin Buzzard]

You shouldn't use constants by the way, you should use variables -- they work a bit better and there's less risk

[Wojciech Nawrocki]

Oh yeah, that was just to make the example code short

[Chris Hughes]

It should be possible to define the function you want constructively, but it hasn't been done yet.

[Kevin Buzzard]

import data.finset
variable {α: Type}
variable {a: α}
variable {as: finset α}
#check a ∈ as -- Prop
variable ex : ∃ (a : α), a ∈ as
noncomputable def test : α := classical.some ex

[Kevin Buzzard]

Right -- this noncomputable approach works for any existence statement. But I now understand that in the specific case of finsets you might be able to do better.

[Bryan Gin-ge Chen]

This is the relevant PR, right?

[Kevin Buzzard]

import data.finset

variables {α : Type} {a : α} {as : finset α} (ex : ∃ (a : α), a ∈ as)

noncomputable def test : α := classical.some ex

Shorter and no constants ;-)

[Wojciech Nawrocki]

Also works with constants, but fair enough :)
Anyhow, I need it to be computable because I want to extract concrete elements from concrete sets and do things with them

[Kenny Lau]

something that almost works:

[Kenny Lau]

import data.finset

lemma list.perm_singleton {α : Type*} {L : list α} {x : α} (H : L ~ [x]) : L = [x] :=
begin
  generalize_hyp hs : [x] = S at H ⊢,
  induction H,
  case list.perm.nil { refl },
  case list.perm.skip : y L₁ L₂ H ih {
    cases hs, cases list.perm_nil.1 H, refl
  },
  case list.perm.swap { injections },
  case list.perm.trans : L₁ L₂ L₃ H12 H23 ih1 ih2 {
    cases hs, cases ih2 rfl, cases ih1 rfl, refl
  }
end

def extract {α : Type*} (s : finset α) (hs : s.card = 1) : α :=
finset.rec_on s
  (λ m, quotient.hrec_on m
    (λ L _, list.cases_on L
      (assume hcard : 0 = 1, absurd hcard dec_trivial)
      (λ hd tl hcard, hd))
    (λ L₁ L₂ HL, function.hfunext (congr_arg _ $ quotient.sound HL) $
    λ hnd1 hnd2 hheq, begin
  cases L₂,
  case list.nil { cases list.perm_nil.1 HL, refl },
  case list.cons : hd₂ tl₂ {
    cases L₁,
    case list.nil { cases list.perm_nil.1 (list.perm.symm HL) },
    case list.cons : hd₁ tl₁ {
      apply function.hfunext,
      { simp only [finset.card_def, multiset.card],
        rw quotient.sound HL },
      intros hcard₁ hcard₂ hheq,
      cases multiset.card_eq_one.1 hcard₁ with x₁ hx₁,
      cases multiset.card_eq_one.1 hcard₂ with x₂ hx₂,
      cases list.perm_singleton (quotient.exact hx₁),
      cases list.perm_singleton (quotient.exact hx₂),
      cases list.perm_singleton HL,
      refl
    }
  }
end)) hs

[Kenny Lau]

@Chris Hughes can you fix this?

[Chris Hughes]

example {α : Type*} (s : finset α) : s.card = 1 → {a : α // s = finset.singleton a} :=
finset.rec_on s (λ s, @quotient.rec_on_subsingleton _ _
  (λ t : multiset α, Π (nodup : multiset.nodup t),
    finset.card {val := t, nodup := nodup} = 1 → {a // finset.mk t nodup = finset.singleton a})
      (λ l, ⟨λ a b, funext (λ x, funext (λ y, subtype.eq $ finset.singleton_inj.1 $
        by rw [← (a x y).2, ← (b x y).2]))⟩) s
  (λ l, list.rec_on l (λ _ h, nat.no_confusion h)
    (λ a l _ _ h, have l.length = 0, from nat.succ_inj h,
      ⟨a, finset.eq_of_veq $ by dsimp; rw [list.length_eq_zero.1 this]; refl⟩)) )

[Chris Hughes]

Not very pretty

[Kenny Lau]

import data.finset

lemma list.perm_singleton {α : Type*} {L : list α} {x : α} (H : L ~ [x]) : L = [x] :=
begin
  generalize_hyp hs : [x] = S at H ⊢,
  induction H,
  case list.perm.nil { refl },
  case list.perm.skip : y L₁ L₂ H ih {
    cases hs, cases list.perm_nil.1 H, refl
  },
  case list.perm.swap { injections },
  case list.perm.trans : L₁ L₂ L₃ H12 H23 ih1 ih2 {
    cases hs, cases ih2 rfl, cases ih1 rfl, refl
  }
end

def extract {α : Type*} (s : finset α) (hs : s.card = 1) : α :=
finset.rec_on s
  (λ m, quotient.rec_on m
    (λ L _, show L.length = 1 → α, from list.cases_on L
      (λ H, absurd H dec_trivial)
      (λ hd tl H, hd))
    (λ L₁ L₂ HL, begin
  ext H1 H2, rcases list.length_eq_one.1 H2 with ⟨x₂, rfl⟩,
  cases list.perm_singleton HL, refl
end)) hs

my version

[Kenny Lau]

well yours is much shorter

[Kenny Lau]

clever use of subsingleton...

[Kenny Lau]

theorem extract_mem {α : Type*} (s : finset α) (hs : s.card = 1) :
  extract s hs ∈ s :=
begin
  induction s with m _,
  rcases m with L,
  cases L with hd tl, { cases hs },
  left, refl
end

[Kenny Lau]

@Wojciech Nawrocki so we have 2 solutions now

[Kenny Lau]

(i.e. mine and Chris's solution)

[Wojciech Nawrocki]

Oh wow, these are quite complex! I wonder if i should have just used lists instead :P but thanks a lot

[Kenny Lau]

related: https://github.com/leanprover/mathlib/pull/421

[Wojciech Nawrocki]

When a goal contains a reducible definition, how can i expand it to work with the internals? Namely, in here:

  @[reducible]
  def compose_partial (f₁: α → option β) (f₂: β → option γ)
    : α → option γ :=
  (λ a: α, option.cases_on (f₁ a) none (λ x, f₂ x))

  notation [parsing_only] a `⬝ₚ` b := compose_partial b a

  theorem compose_none (f₁: α → option β) (f₂: β → option γ) (x: α) (h: f₁ x = none)
    : (f₂ ⬝ₚ f₁) x = none :=
  begin
    sorry
  end

I would like to expand compose_partial to carry through the none and get back a none.

[Rob Lewis]

You can use unfold compose_partial. simp [compose_partial] or dsimp [compose_partial] can also be useful.

[Wojciech Nawrocki]

Ah, unfold. Thanks!

[Kenny Lau]

@[reducible] means that the typeclass system will automatically unfold it

[Kenny Lau]

but only the typeclass system

[Wojciech Nawrocki]

How can I make an instance of a dependent product (x, p x) where p is some proposition depending on x? Lean complains about impredicativity:

type mismatch at application
  (n, h)
term
  h
has type
  n = 4 : Prop
but is expected to have type
  ?m_1 : Type ?

[Chris Hughes]

use subtype

[Chris Hughes]

If you're using prod, it won't work because it's non dependent and it doesn't accept Propositions.

[Reid Barton]

Parentheses are only for prod, yeah

[Wojciech Nawrocki]

Oh I see, thanks!

[Kenny Lau]

prod is non-dependent sigma

[Kenny Lau]

but if it's proposition then you're better off using subtype which is a sort of specialize sigma

[Wojciech Nawrocki]

Given an inductive type with some variants that take arguments, e.g.

inductive Foo: Type
| A : nat -> Foo
| B: Foo

Is there a better way of saying that a particular x: Foo was constructed by A regardless of what the argument was than \ex n: nat, x = A n?

[Kevin Buzzard]

I don't think so. "x was constructed by A and I don't know what the argument was" is exactly \ex n: nat, x = A n, right? What's wrong with this way of saying it?

[Chris Hughes]

Other approaches

def p : foo → Prop
| (A n) := true
| B     := false

inductive p : foo → Prop
| bar : p (A n)

[Kevin Buzzard]

That first one is a much better way :-) I don't understand the second one!

[Wojciech Nawrocki]

Hm, I guess it might just be nice to have a shorthand like p in Chris's example for when the constructor is unwieldy, e.g. has lots of arguments. p would sound better as e.g. is_A

[Rob Lewis]

The second one is an inductive proposition. I think you need inductive instead of def. This seems like the "canonical" way to me, and you can easily prove it equivalent to one using exists.

[Chris Hughes]

The inductive one gives you a nice recursor.

[Bryan Gin-ge Chen]

Is there another typo in the second one? I'm trying to figure out how to use it and I'm getting unknown identifier 'n'

[Rob Lewis]

It should look like

inductive Foo : Type
| A : nat -> Foo
| B: Foo

inductive Foo.is_A : Foo → Prop
| of_A (n) : Foo.is_A (Foo.A n)

[Rob Lewis]

The idea being, Foo.is_A is a family of propositions. For any n : nat, Foo.is_A.of_A n is a proof of Foo.is_A (Foo.A n).

[Bryan Gin-ge Chen]

Thanks! I'd tried adding n after bar and I forgot that the parentheses were necessary.