cases matching with

Stream: Is there code for X?

[Bolton Bailey]

Is there a tactic or arguments to combine the functionality of cases ... with ... with the functionality of cases_matching? I'd like to be able to reference by name the constructors I get from cases_matching. cases_matching ... with ... doesn't seem to work.

example (p q : Prop) (h1 : p ∨ q) : false :=
begin
  -- cases h1 with h_left h_right, -- what I want to do without referencing h1
  cases_matching (_ ∨ _) with h_left h_right, -- invalid
end

[Eric Rodriguez]

maybe you want the ‹...› syntax?

cases ‹_ ∨ _› with h_left h_right, -- valid

[Bolton Bailey]

Sweet, that works, thank you. Is there someplace I can learn more about this ‹...› syntax?

[Yaël Dillies]

Is it the same as the one you use to implicitly call assumption?

[Eric Rodriguez]

think of ‹...› as show ... by assumption

[Eric Rodriguez]

yes Yaël

[Yaël Dillies]

Ahah! Yes :wink:

[Bolton Bailey]

Cool, thanks

[Yaël Dillies]

The most useful place to use it is after a ;, because you might have want to call the exact same lemma in all of the cases but the hypotheses have to be shuffled around.

[Bolton Bailey]

I currently want to do something like the following

  cases_success <- try_core `[cases ‹_ ∨ _› with nm nm],
  match cases_success with
  | some _ := all_goals' `[rw nm at *, done <|> id { integral_domain_tactic }]
  | none := skip

But I would rather nm not just be nm every time so it doesn't overwrite itself when I call this recursively. Is there some way to get cases ‹_ ∨ _› to output the name of the value it destructs? Or to call nm <- get_unused_name and have that be inserted after with?