mod_cases tactic #
mod_cases tactic does case disjunction on
e % n, where
e : ℤ, to yield a number of
subgoals in which
e ≡ 0 [ZMOD n], ...,
e ≡ n-1 [ZMOD n] are assumed.
OnModCases n a lb p represents a partial proof by cases that
0 ≤ z < n such that
a ≡ z (mod n).
It asserts that if
∃ z, lb ≤ z < n ∧ a ≡ z (mod n) holds, then
p is the current goal).
The successor case decomposes
∃ z, b ≤ z < n ∧ a ≡ z (mod n) into
a ≡ b (mod n) ∨ ∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n),
a ≡ b (mod n) → p case becomes a subgoal.
- The tactic
mod_cases h : e % 3will perform a case disjunction on
e : ℤand yield subgoals containing the assumptions
h : e ≡ 0 [ZMOD 3],
h : e ≡ 1 [ZMOD 3],
h : e ≡ 2 [ZMOD 3]respectively.
- In general,
mod_cases h : e % nworks when
nis a positive numeral and
eis an expression of type
his omitted as in
mod_cases e % n, it will be default-named