mod_cases
tactic #
The mod_cases
tactic does case disjunction on e % n
, where e : ℤ
, to yield a number of
subgoals in which e ≡ 0 [ZMOD n]≡ 0 [ZMOD n]
, ..., e ≡ n-1 [ZMOD n]≡ n-1 [ZMOD n]
are assumed.
OnModCases n a lb p
represents a partial proof by cases that
there exists 0 ≤ z < n≤ z < n
such that a ≡ z (mod n)≡ z (mod n)
.
It asserts that if ∃ z, lb ≤ z < n ∧ a ≡ z (mod n)∃ z, lb ≤ z < n ∧ a ≡ z (mod n)≤ z < n ∧ a ≡ z (mod n)∧ a ≡ z (mod n)≡ z (mod n)
holds, then p
(where p
is the current goal).
The first theorem we apply says that ∃ z, 0 ≤ z < n ∧ a ≡ z (mod n)∃ z, 0 ≤ z < n ∧ a ≡ z (mod n)≤ z < n ∧ a ≡ z (mod n)∧ a ≡ z (mod n)≡ z (mod n)
.
The actual mathematical content of the proof is here.
The end point is that once we have reduced to ∃ z, n ≤ z < n ∧ a ≡ z (mod n)∃ z, n ≤ z < n ∧ a ≡ z (mod n)≤ z < n ∧ a ≡ z (mod n)∧ a ≡ z (mod n)≡ z (mod n)
there are no more cases to consider.
Equations
- Mathlib.Tactic.ModCases.onModCases_stop p n a x h = False.elim (_ : False)
The successor case decomposes ∃ z, b ≤ z < n ∧ a ≡ z (mod n)∃ z, b ≤ z < n ∧ a ≡ z (mod n)≤ z < n ∧ a ≡ z (mod n)∧ a ≡ z (mod n)≡ z (mod n)
into
a ≡ b (mod n) ∨ ∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n)≡ b (mod n) ∨ ∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n)∨ ∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n)∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n)≤ z < n ∧ a ≡ z (mod n)∧ a ≡ z (mod n)≡ z (mod n)
,
and the a ≡ b (mod n) → p≡ b (mod n) → p→ p
case becomes a subgoal.
Equations
- One or more equations did not get rendered due to their size.
Proves an expression of the form OnModCases n a b p
where n
and b
are raw nat literals
and b ≤ n≤ n
. Returns the list of subgoals ?gi : a ≡ i [ZMOD n] → p≡ i [ZMOD n] → p→ p
.
- The tactic
mod_cases h : e % 3
will perform a case disjunction one : ℤ
and yield subgoals containing the assumptionsh : e ≡ 0 [ZMOD 3]≡ 0 [ZMOD 3]
,h : e ≡ 1 [ZMOD 3]≡ 1 [ZMOD 3]
,h : e ≡ 2 [ZMOD 3]≡ 2 [ZMOD 3]
respectively. - In general,
mod_cases h : e % n
works whenn
is a positive numeral ande
is an expression of typeℤ
. - If
h
is omitted as inmod_cases e % n
, it will be default-namedH
.
Equations
- One or more equations did not get rendered due to their size.