tactic.fin_cases

# Case bash #

This file provides the tactic fin_cases. fin_cases x performs case analysis on x, that is creates one goal for each possible value of x, where either:

• x : α, where [fintype α]
• x ∈ A, where A : finset α, A : multiset α or A : list α.
meta def tactic.guard_mem_fin (e : expr) :

Checks that the expression looks like x ∈ A for A : finset α, multiset α or A : list α, and returns the type α.

expr_list_to_list_expr converts an expr of type list α to a list of exprs each with type α.

TODO: this should be moved, and possibly duplicates an existing definition.

meta def tactic.fin_cases_at (nm : option name) (with_list : option pexpr) (e : expr) :

fin_cases_at with_list e performs case analysis on e : α, where α is a fintype. The optional list of expressions with_list provides descriptions for the cases of e, for example, to display nats as n.succ instead of n+1. These should be defeq to and in the same order as the terms in the enumeration of α.

fin_cases h performs case analysis on a hypothesis of the form h : A, where [fintype A] is available, or h : a ∈ A, where A : finset X, A : multiset X or A : list X.

fin_cases * performs case analysis on all suitable hypotheses.

As an example, in

example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
begin
fin_cases *; simp,
all_goals { assumption }
end


after fin_cases p; simp, there are three goals, f 0, f 1, and f 2.

fin_cases h with l takes a list of descriptions for the cases of h. These should be definitionally equal to and in the same order as the default enumeration of the cases.

For example,

example (x y : ℕ) (h : x ∈ [1, 2]) : x = y :=
begin
fin_cases h with [1, 1+1],
end


produces two cases: 1 = y and 1 + 1 = y.

When using fin_cases a on data a defined with let, the tactic will not be able to clear the variable a, and will instead produce hypotheses this : a = .... These hypotheses can be given a name using fin_cases a using ha.

For example,

example (f : ℕ → fin 3) : true :=
begin
let a := f 3,
fin_cases a using ha,
end


produces three goals with hypotheses ha : a = 0, ha : a = 1, and ha : a = 2.

fin_cases h performs case analysis on a hypothesis of the form h : A, where [fintype A] is available, or h : a ∈ A, where A : finset X, A : multiset X or A : list X.

fin_cases * performs case analysis on all suitable hypotheses.

As an example, in

example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
begin
fin_cases *; simp,
all_goals { assumption }
end


after fin_cases p; simp, there are three goals, f 0, f 1, and f 2.

fin_cases h with l takes a list of descriptions for the cases of h. These should be definitionally equal to and in the same order as the default enumeration of the cases.

For example,

example (x y : ℕ) (h : x ∈ [1, 2]) : x = y :=
begin
fin_cases h with [1, 1+1],
end


produces two cases: 1 = y and 1 + 1 = y.

When using fin_cases a on data a defined with let, the tactic will not be able to clear the variable a, and will instead produce hypotheses this : a = .... These hypotheses can be given a name using fin_cases a using ha.

For example,

example (f : ℕ → fin 3) : true :=
begin
let a := f 3,
fin_cases a using ha,
end


produces three goals with hypotheses ha : a = 0, ha : a = 1, and ha : a = 2.