is there a tactic?

Stream: general

[Sean Leather]

Is there a tactic for (part of) this?

by cases l; apply exists.intro; assumption; assumption

[Johan Commelin]

Will tidy do this? Or can it not yet do exists.intro?

[Sean Leather]

I've never used tidy.

[Johan Commelin]

It is really cool. You'll need import tactic.tidy.

[Kenny Lau]

I'd just write the whole thing in term mode

[Sean Leather]

Kenny: I had that, but the tactic is more robust to changes in l, which are happening.

[Sean Leather]

Also, l has a lot of fields, so either using pattern matching or cases l with ... is annoyingly long.

[Johan Commelin]

Does tidy work?

[Sean Leather]

by cases l; tidy works

[Sean Leather]

by cases l; tidy {trace_result:=tt} doesn't print anything. :concerned:

[Johan Commelin]

Huh, so tidy won't do the cases for you? I expected that it would try that, as some last resort...

[Johan Commelin]

@Sean Leather You can use hole commands to let VScode replace tidy with the proof it generated.

[Sean Leather]

I suppose that would be listed here if it did:

meta def default_tactics : list (tactic string) :=
[ reflexivity                                 >> pure "refl",
  `[exact dec_trivial]                        >> pure "exact dec_trivial",
  propositional_goal >> assumption            >> pure "assumption",
  `[ext1]                                     >> pure "ext1",
  intros1                                     >>= λ ns, pure ("intros " ++ (" ".intercalate (ns.map (λ e, e.to_string)))),
  auto_cases,
  `[apply_auto_param]                         >> pure "apply_auto_param",
  `[dsimp at *]                               >> pure "dsimp at *",
  `[simp at *]                                >> pure "simp at *",
  fsplit                                      >> pure "fsplit",
  injections_and_clear                        >> pure "injections_and_clear",
  propositional_goal >> (`[solve_by_elim])    >> pure "solve_by_elim",
  `[unfold_aux]                               >> pure "unfold_aux",
  tidy.run_tactics ]

[Johan Commelin]

what does auto_cases do?

[Sean Leather]

No idea. :slight_smile:

[Sean Leather]

  t' ← whnf t',
  let use_cases := match t' with
  | `(empty)     := tt
  | `(pempty)    := tt
  | `(unit)      := tt
  | `(punit)     := tt
  | `(ulift _)   := tt
  | `(plift _)   := tt
  | `(prod _ _)  := tt
  | `(and _ _)   := tt
  | `(sigma _)   := tt
  | `(subtype _) := tt
  | `(Exists _)  := tt
  | `(fin 0)     := tt
  | `(sum _ _)   := tt -- This is perhaps dangerous!
  | `(or _ _)    := tt -- This is perhaps dangerous!
  | _            := ff

[Sean Leather]

Looks like it's restricted to certain patterns.

[Johan Commelin]

Right... I guess that makes sense.

[Johan Commelin]

Anyway, we still golfed your proof (-;

[Johan Commelin]

It makes sense that cases l remains in the proof. It is probably an "idea". After that it is "follow your nose"

[Sean Leather]

Yep, thanks! I learned something new.

[Sean Leather]

It would be nice to see what tidy is doing, though.

[Keeley Hoek]

Sean, are you using a version of mathlib which incorporates this commit?
https://github.com/leanprover/mathlib/commit/e95111d38c0b2d666f70624ce25a5d728e0db376

[Sean Leather]

@Keeley Hoek No, certainly not. Thanks!