pretty_cases tactic #

When using induction and cases, pretty_cases prints a "Try this:" advice that shows how to structure the proof with case { ... } commands. In the following example, we apply induction on a permutation assumption about lists. pretty_cases gives us a proof skeleton that explicit selects the branches and explicit names the new local constants:

example {α} (xs ys : list α) (h : xs ~ ys) : true :=
begin
  induction h,
  pretty_cases,
    -- Try this:
    --   case list.perm.nil :
    --   { admit },
    --   case list.perm.cons : h_x h_l₁ h_l₂ h_a h_ih
    --   { admit },
    --   case list.perm.swap : h_x h_y h_l
    --   { admit },
    --   case list.perm.trans : h_l₁ h_l₂ h_l₃ h_a h_a_1 h_ih_a h_ih_a_1
    --   { admit },
end

Main definitions #

• pretty_cases_advice return pretty_cases advice without printing it
• pretty_cases main tactic