by exactI

Stream: general

[Johan Commelin]

I have a question for Lean hackers (@Gabriel Ebner @Mario Carneiro @Simon Hudon etc).
Here is the main statement from LTE:

theorem main [BD.suitable c']
  (r r' : ℝ≥0) [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r' ≤ 1)] :
  ∀ m : ℕ,
  ∃ (k : ℝ≥0) [fact (1 ≤ k)],
  ∃ c₀ : ℝ≥0,
  ∀ (S : Type) [fintype S],
  ∀ (V : NormedGroup) [normed_with_aut r V],
  by exactI (Mbar_system V S r r' BD c').is_bdd_exact_for_bdd_degree_above_idx k m c₀ :=
sorry

All of this looks pretty reasonable, but the by exactI is of course a bit annoying.

Do you think we can change Lean so that it will trigger a cache reset when it parses [normed_with_aut r V] (or any other [foobar]) after :?

I realise that this would lead to 3 extra cache resets in the current statement... is that expensive?

[Gabriel Ebner]

It's not impossible. The real question is: how important is this to you given that it will be fixed in :four_leaf_clover: and that we have a workaround in :three:?

[Gabriel Ebner]

You can also make notation if you find the current workaround to be too ugly.

[Johan Commelin]

How would that work?

[Johan Commelin]

You mean some notation for the by exactI?

[Gabriel Ebner]

I think you can do this using user notation.

[Johan Commelin]

I don't know what you have in mind, sorry

[Gabriel Ebner]

This seems to work, you just need to adapt it to exactI:

open tactic expr
open lean
open lean.parser
open interactive
open tactic

reserve prefix `♯ᵢ `:100

@[user_notation]
meta def exact_notation (_ : parse $ tk "♯ᵢ") (e : parse lean.parser.pexpr) : parser pexpr := do
expr.macro d [_] ← pure ``(by skip),
pure $ expr.macro d [const ``tactic.interactive.exact [] (cast undefined e.reflect)]

#check ♯ᵢ 1

[Johan Commelin]

Ooh wow! I would have never been able to write that myself

[Johan Commelin]

I'll try it out

[Gabriel Ebner]

Yes, I would have liked to write ``(by exact %%e) , but lean doesn't let me do that.

[Johan Commelin]

@Gabriel Ebner if I replace by exactI with ♯ᵢ then I get unexpected token

[Johan Commelin]

sorry, that was a copy-paste error... let me try better

[Johan Commelin]

With

@[user_notation]
meta def exact_notation (_ : parse $ tk "♯ᵢ") (e : parse lean.parser.pexpr) : parser pexpr := do
expr.macro d [_] ← pure ``(by skip),
pure $ expr.macro d [const `tactic.interactive.exactI [] (cast undefined e.reflect)]

it works! @Gabriel Ebner thanks a lot, this is very nice indeed!

[Gabriel Ebner]

You should also change lean.parser.pexpr to (lean.parser.pexpr 0) (then it parses more like $ or by exactI)

[Johan Commelin]

aah, cool, let me try that

[Johan Commelin]

theorem main [BD.suitable c']
  (r r' : ℝ≥0) [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r' ≤ 1)] :
  ∀ m : ℕ,
  ∃ (k : ℝ≥0) [fact (1 ≤ k)],
  ∃ c₀ : ℝ≥0,
  ∀ (S : Type) [fintype S],
  ∀ (V : NormedGroup) [normed_with_aut r V],​
    (Mbar_system V S r r' BD c').is_bdd_exact_for_bdd_degree_above_idx k m c₀ :=
sorry

@Gabriel Ebner this is awesome!

[Johan Commelin]

1. yes, that is totally a zero-width space after that final ,
2. this statement looks a lot better
3. this also solves another annoying bug: with by exactI if you Ctrl-clicked on is_bdd_exact_for_bdd_degree_above_idx it would go to the definition of exactI instead of the definition that you actually want. Now "Go to definition" works as expected

[Sebastien Gouezel]

Of course, a better solution would be to have explicit k and c₀ in terms of m, and put everything left of the colon :-)

[Johan Commelin]

I do not yet have enough understanding of the proof to know whether that is an option

[Adam Topaz]

Maybe explicit can even mean classical.some?

[Adam Topaz]

But I guess we still need to understand what properties of k are needed :)

[Sebastien Gouezel]

I'm pretty sure the proof has to give an explicit k, because you couldn't do a proof by contradiction by quantifying over every type and every normed group like that (no way to take a limit and argue that the limit has a nice behavior, as one often does in proofs that give something non-explicit). Although this "explicit" might be completely untractable :-)