Shorthand for decomposing a pair

Stream: general

[Andrej Bauer]

Suppose my goal is ∀ p : α × β, A. Is there a shorthand for intro xy, cases xs with x y? In Coq this is intros [x y] and in Agda it's just pattern matching against (x,y).

[Johan Commelin]

rintro \<x,y\>

[Johan Commelin]

Where \< and \> should be replaced by funny unicode brackets

[Eric Wieser]

⟨x, y⟩

[Andrej Bauer]

While I have your attention, is there a simple logic solver, along the lines of Coq tauto and firstorder?

[Johan Commelin]

tauto exists, I don't know if it does what you want

[Johan Commelin]

I think there is even tauto!!

[Johan Commelin]

For more oompf

[Mario Carneiro]

Andrej Bauer said:

Suppose my goal is ∀ p : α × β, A. Is there a shorthand for intro xy, cases xs with x y? In Coq this is intros [x y] and in Agda it's just pattern matching against (x,y).

The term mode syntax \lam \<x, y\>, also works same as in agda, and that doesn't need any mathlib tactics

[Yaël Dillies]

It's a bit fragile though. It doesnt always work in refine λ ⟨x, y⟩, _ for example.

[Mario Carneiro]

That's because it sets up a separate proof context in an auxiliary, so it can't share metavariables with the original proof. You can always do exact λ ⟨x, y⟩, begin ... end if you want to keep tacticking

[Mario Carneiro]

the same thing happens if you use match