Golfing a sequence of applies

Stream: general

[Chris Birkbeck]

I'm trying to get better at golfing proofs and I was wondering if there is some nice golfing one can do with things of the form:

lemma My_lem : foo  :=
begin
  apply A,
  apply B,
  apply C,
  apply C,
 end

I've got quite a few of these (specially when proving some function is continuous, like in #13500) and it feels like there is just something basic I'm missing (or perhaps I shouldn't be proving things this way!).

[Johan Commelin]

apply_rules maybe?

[Yaël Dillies]

refine A (B $ C $ C _) with maybe some more underscores in between?

[Chris Birkbeck]

Johan Commelin said:

apply_rules maybe?

Oh I didn't know about this, it seems to help sometimes, thanks!

[Chris Birkbeck]

Yaël Dillies said:

refine A (B $ C $ C _) with maybe some more underscores in between?

Ah thanks, I'd not thought of trying to use a refine here, it also works for some of them!

[Floris van Doorn]

Yael's tip, together with the use of projection notation (continuous_on_const.smul hf instead of continuous_on.smul continuous_on_const hf) can greatly shrink the size of some of your continuity proofs.

[Damiano Testa]

Also lumping them together in a show_term { tactics } will give you a single expression. Whether it is reasonable or not, depends on what you feed it!

In the case you give, it should return an output similar to what Yaël describes. I'm not sure if it will use dot-notation aggressively, though. It wi also fill in all the underscores, some of which you can replace again with underscores.

[Patrick Johnson]

Maybe it would be useful if we had a tactic like this:

import tactic
section
setup_tactic_parser
meta def tactic.interactive.apply_list : parse pexpr_list → tactic unit :=
monad.mapm' tactic.interactive.apply
end

The proof would simply be apply_list [A, B, C, C] and we don't need to worry about underscores.

[Kevin Buzzard]

If I have a proof which is only apply and use and refine and exact I usually change all the applys and uses to refines and then start doing the jigsaw puzzle to make it all into one line.

  apply A,
  apply B,
  apply C,
  apply C,

->

  refine A _,
  refine B _ _,
    refine C _,
  refine C _,

->

exact A (B (C _) (C _)

[Jireh Loreaux]

Isn't this exactly what show_term is useful for though? (Admittedly, I always forget about show_term myself)

[Mario Carneiro]

show_term won't tell you which underscores are allowed, although you can always just try replacing things with _