Documentation

Mathlib.Tactic.ModCases

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.

def Mathlib.Tactic.ModCases.OnModCases (n : ) (a : ) (lb : ) (p : Sort u_1) :
Sort (imax1u_1)

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).

Equations
@[inline]

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.

Equations
@[inline]

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
@[inline]

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.
partial def Mathlib.Tactic.ModCases.proveOnModCases {u : Lean.Level} (n : Q()) (a : Q()) (b : Q()) (p : Qq.QQ (Lean.Expr.sort u)) :
Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Tactic.ModCases.OnModCases [u]) n) a) b) p) × List Lean.MVarId)

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 on e : ℤ and yield subgoals containing the assumptions h : 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 when n is a positive numeral and e is an expression of type .
  • If h is omitted as in mod_cases e % n, it will be default-named H.
Equations
  • One or more equations did not get rendered due to their size.