mathlib documentation

tactic.norm_fin

norm_fin #

This file defines functions for dealing with fin n numbers as expressions.

Main definitions #

source
def tactic.norm_fin.normalize_fin (n : ℕ) (a : fin n) (b : ℕ) :
Prop

normalize_fin n a b means that a : fin n is equivalent to b : ℕ in the modular sense - that is, ↑a ≡ b (mod n). This is used for translating the algebraic operations: addition, multiplication, zero and one, which use modulo for reduction.

Equations
source
def tactic.norm_fin.normalize_fin_lt (n : ℕ) (a : fin n) (b : ℕ) :
Prop

normalize_fin_lt n a b means that a : fin n is equivalent to b : ℕ in the embedding sense - that is, ↑a = b. This is used for operations that treat fin n as the subset {0, ..., n-1} of ℕ. For example, fin.succ : fin n → fin (n+1) is thought of as the successor function, but it does not lift to a map zmod n → zmod (n+1); this addition only makes sense if the input is strictly less than n.

normalize_fin_lt n a b is equivalent to normalize_fin n a b ∧ b < n.

Equations
source
theorem tactic.norm_fin.normalize_fin_lt.coe {n : ℕ} {a : fin n} {b : ℕ} (h : tactic.norm_fin.normalize_fin_lt n a b) :
↑a = b
source
theorem tactic.norm_fin.normalize_fin_iff {n : ℕ} [fact (0 < n)] {a : fin n} {b : ℕ} :
tactic.norm_fin.normalize_fin n a b ↔ a = fin.of_nat' b
source
theorem tactic.norm_fin.normalize_fin_lt.mk {n : ℕ} {a : fin n} {b n' : ℕ} (hn : n = n') (h : tactic.norm_fin.normalize_fin n a b) (h2 : b < n') :
tactic.norm_fin.normalize_fin_lt n a b
source
theorem tactic.norm_fin.normalize_fin_lt.lt {n : ℕ} {a : fin n} {b : ℕ} (h : tactic.norm_fin.normalize_fin_lt n a b) :
b < n
source
theorem tactic.norm_fin.normalize_fin_lt.of {n : ℕ} {a : fin n} {b : ℕ} (h : tactic.norm_fin.normalize_fin_lt n a b) :
tactic.norm_fin.normalize_fin n a b
source
theorem tactic.norm_fin.normalize_fin.zero (n : ℕ) :
tactic.norm_fin.normalize_fin (n + 1) 0 0
source
theorem tactic.norm_fin.normalize_fin_lt.zero (n : ℕ) :
tactic.norm_fin.normalize_fin_lt (n + 1) 0 0
source
theorem tactic.norm_fin.normalize_fin.one (n : ℕ) :
tactic.norm_fin.normalize_fin (n + 1) 1 1
source
theorem tactic.norm_fin.normalize_fin.add {n : ℕ} {a b : fin n} {a' b' c' : ℕ} (ha : tactic.norm_fin.normalize_fin n a a') (hb : tactic.norm_fin.normalize_fin n b b') (h : a' + b' = c') :
tactic.norm_fin.normalize_fin n (a + b) c'
source
theorem tactic.norm_fin.normalize_fin.mul {n : ℕ} {a b : fin n} {a' b' c' : ℕ} (ha : tactic.norm_fin.normalize_fin n a a') (hb : tactic.norm_fin.normalize_fin n b b') (h : a' * b' = c') :
tactic.norm_fin.normalize_fin n (a * b) c'
source
theorem tactic.norm_fin.normalize_fin.bit0 {n : ℕ} {a : fin n} {a' : ℕ} (h : tactic.norm_fin.normalize_fin n a a') :
tactic.norm_fin.normalize_fin n (bit0 a) (bit0 a')
source
theorem tactic.norm_fin.normalize_fin.bit1 {n : ℕ} {a : fin (n + 1)} {a' : ℕ} (h : tactic.norm_fin.normalize_fin (n + 1) a a') :
tactic.norm_fin.normalize_fin (n + 1) (bit1 a) (bit1 a')
source
theorem tactic.norm_fin.normalize_fin_lt.succ {n : ℕ} {a : fin n} {a' b : ℕ} (h : tactic.norm_fin.normalize_fin_lt n a a') (e : a' + 1 = b) :
tactic.norm_fin.normalize_fin_lt n.succ a.succ b
source
theorem tactic.norm_fin.normalize_fin_lt.cast_lt {n m : ℕ} {a : fin m} {ha : a.val < n} {a' : ℕ} (h : tactic.norm_fin.normalize_fin_lt m a a') :
tactic.norm_fin.normalize_fin_lt n (a.cast_lt ha) a'
source
theorem tactic.norm_fin.normalize_fin_lt.cast_le {n m : ℕ} {nm : m ≤ n} {a : fin m} {a' : ℕ} (h : tactic.norm_fin.normalize_fin_lt m a a') :
tactic.norm_fin.normalize_fin_lt n (⇑(fin.cast_le nm) a) a'
source
theorem tactic.norm_fin.normalize_fin_lt.cast {n m : ℕ} {nm : m = n} {a : fin m} {a' : ℕ} (h : tactic.norm_fin.normalize_fin_lt m a a') :
tactic.norm_fin.normalize_fin_lt n (⇑(fin.cast nm) a) a'
source
theorem tactic.norm_fin.normalize_fin.cast {n m : ℕ} {nm : m = n} {a : fin m} {a' : ℕ} (h : tactic.norm_fin.normalize_fin m a a') :
tactic.norm_fin.normalize_fin n (⇑(fin.cast nm) a) a'
source
theorem tactic.norm_fin.normalize_fin_lt.cast_add {n m : ℕ} {a : fin n} {a' : ℕ} (h : tactic.norm_fin.normalize_fin_lt n a a') :
tactic.norm_fin.normalize_fin_lt (n + m) (⇑(fin.cast_add m) a) a'
source
theorem tactic.norm_fin.normalize_fin_lt.cast_succ {n : ℕ} {a : fin n} {a' : ℕ} (h : tactic.norm_fin.normalize_fin_lt n a a') :
tactic.norm_fin.normalize_fin_lt (n + 1) (⇑fin.cast_succ a) a'
source
theorem tactic.norm_fin.normalize_fin_lt.add_nat {n m m' : ℕ} (hm : m = m') {a : fin n} {a' b : ℕ} (h : tactic.norm_fin.normalize_fin_lt n a a') (e : a' + m' = b) :
tactic.norm_fin.normalize_fin_lt (n + m) (⇑(fin.add_nat m) a) b
source
theorem tactic.norm_fin.normalize_fin_lt.nat_add {n m n' : ℕ} (hn : n = n') {a : fin m} {a' b : ℕ} (h : tactic.norm_fin.normalize_fin_lt m a a') (e : n' + a' = b) :
tactic.norm_fin.normalize_fin_lt (n + m) (⇑(fin.nat_add n) a) b
source
theorem tactic.norm_fin.normalize_fin.reduce {n : ℕ} {a : fin n} {n' a' b k nk : ℕ} (hn : n = n') (h : tactic.norm_fin.normalize_fin n a a') (e1 : n' * k = nk) (e2 : nk + b = a') :
tactic.norm_fin.normalize_fin n a b
source
theorem tactic.norm_fin.normalize_fin_lt.reduce {n : ℕ} {a : fin n} {n' a' b k nk : ℕ} (hn : n = n') (h : tactic.norm_fin.normalize_fin n a a') (e1 : n' * k = nk) (e2 : nk + b = a') (hl : b < n') :
tactic.norm_fin.normalize_fin_lt n a b
source
theorem tactic.norm_fin.normalize_fin.eq {n : ℕ} {a b : fin n} {c : ℕ} (ha : tactic.norm_fin.normalize_fin n a c) (hb : tactic.norm_fin.normalize_fin n b c) :
a = b
source
theorem tactic.norm_fin.normalize_fin.lt {n : ℕ} {a b : fin n} {a' b' : ℕ} (ha : tactic.norm_fin.normalize_fin n a a') (hb : tactic.norm_fin.normalize_fin_lt n b b') (h : a' < b') :
a < b
source
theorem tactic.norm_fin.normalize_fin.le {n : ℕ} {a b : fin n} {a' b' : ℕ} (ha : tactic.norm_fin.normalize_fin n a a') (hb : tactic.norm_fin.normalize_fin_lt n b b') (h : a' ≤ b') :
a ≤ b
source
@[protected, instance]
meta def tactic.norm_fin.eval_fin_m.alternative  :
alternative tactic.norm_fin.eval_fin_m
source
@[protected, instance]
meta def tactic.norm_fin.eval_fin_m.monad  :
monad tactic.norm_fin.eval_fin_m
source
meta def tactic.norm_fin.eval_fin_m (α : Type) :
Type

The monad for the norm_fin internal tactics. The state consists of an instance cache for ℕ, and a tuple (nn, n', p) where p is a proof of n = n' and nn is n evaluated to a natural number. (n itself is implicit.) It is in an option because it is lazily initialized - for many n we will never need this information, and indeed eagerly computing it would make some reductions fail spuriously if n is not a numeral.

source
meta def tactic.norm_fin.eval_fin_m.lift {α : Type} (m : tactic α) :
tactic.norm_fin.eval_fin_m α

Lifts a tactic into the eval_fin_m monad.

source
@[protected, instance]
meta def tactic.norm_fin.eval_fin_m.has_coe {α : Type} :
has_coe (tactic α) (tactic.norm_fin.eval_fin_m α)
source
meta def tactic.norm_fin.eval_fin_m.lift_ic {α : Type} (m : tactic.instance_cache → tactic (tactic.instance_cache × α)) :
tactic.norm_fin.eval_fin_m α

Lifts an instance_cache tactic into the eval_fin_m monad.

source
meta def tactic.norm_fin.eval_fin_m.reset {α : Type} (m : tactic.norm_fin.eval_fin_m α) :
tactic.norm_fin.eval_fin_m α

Evaluates a monadic action with a fresh n cache, and restore the old cache on completion of the action. This is used when evaluating a tactic in the context of a different n than the parent context. For example if we are evaluating fin.succ a, then a : fin n and fin.succ a : fin (n+1), so the parent cache will be about n+1 and we need a separate cache for n.

source
meta def tactic.norm_fin.eval_fin_m.eval_n (n : expr) :
tactic.norm_fin.eval_fin_m (ℕ × expr × expr)

Given n, returns a tuple (nn, n', p) where p is a proof of n = n' and nn is n evaluated to a natural number. The result of the evaluation is cached for future references. Future calls to this function must use the same value of n, unless it is in a sub-context created by eval_fin_m.reset.

source
meta def tactic.norm_fin.eval_fin_m.run {α : Type} (m : tactic.norm_fin.eval_fin_m α) :
tactic α

Run an eval_fin_m action with a new cache and discard the cache after evaluation.

source
meta inductive tactic.norm_fin.match_fin_result  :
Type

The expression constructors recognized by the eval_fin evaluator. This is used instead of a direct expr pattern match because expr pattern matches generate very large terms under the hood so going via an intermediate inductive type like this is more efficient.

source
meta def tactic.norm_fin.match_fin_coe_fn (a : expr) :
expr → option tactic.norm_fin.match_fin_result

Match a fin expression of the form (coe_fn f a) where f is some fin function. Several fin functions are written this way: for example cast_le : n ≤ m → fin n ↪o fin m is not actually a function but rather an order embedding with a coercion to a function.

source
meta def tactic.norm_fin.match_fin  :
expr → option tactic.norm_fin.match_fin_result

Match a fin expression to a match_fin_result, for easier pattern matching in the evaluator.

source
meta def tactic.norm_fin.reduce_fin'  :
bool → expr → expr → expr × expr → tactic.norm_fin.eval_fin_m (expr × expr)

reduce_fin lt n a (a', pa) expects that pa : normalize_fin n a a' where a' is a natural numeral, and produces (b, pb) where pb : normalize_fin n a b if lt is false, or pb : normalize_fin_lt n a b if lt is true. In either case, b will be chosen to be less than n, but if lt is true then we also prove it. This requires that n can be evaluated to a numeral.

source
meta def tactic.norm_fin.eval_fin_lt' (eval_fin : expr → tactic.norm_fin.eval_fin_m (expr × expr)) :
expr → expr → tactic.norm_fin.eval_fin_m (expr × expr)

eval_fin_lt' eval_fin n a expects that a : fin n, and produces (b, p) where p : normalize_fin_lt n a b. (It is mutually recursive with eval_fin which is why it takes the function as an argument.)

source
meta def tactic.norm_fin.get_fin_type (a : expr) :
tactic expr

Get n such that a : fin n.

source
meta def tactic.norm_fin.eval_fin  :
expr → tactic.norm_fin.eval_fin_m (expr × expr)

Given a : fin n, eval_fin a returns (b, p) where p : normalize_fin n a b. This function does no reduction of the numeral b; for example eval_fin (5 + 5 : fin 6) returns 10. It works even if n is a variable, for example eval_fin (5 + 5 : fin (n+1)) also returns 10.

source
meta def tactic.norm_fin.eval_fin_lt  :
expr → expr → tactic.norm_fin.eval_fin_m (expr × expr)

eval_fin_lt n a expects that a : fin n, and produces (b, p) where p : normalize_fin_lt n a b.

source
meta def tactic.norm_fin.reduce_fin (lt : bool) (n a : expr) :
tactic.norm_fin.eval_fin_m (expr × expr)

Given a : fin n, eval_fin ff n a returns (b, p) where p : normalize_fin n a b, and eval_fin tt n a returns p : normalize_fin_lt n a b. Unlike eval_fin, this also does reduction of the numeral b; for example reduce_fin ff 6 (5 + 5 : fin 6) returns 4. As a result, it fails if n is a variable, for example reduce_fin ff (n+1) (5 + 5 : fin (n+1)) fails.

source
meta def tactic.norm_fin.prove_lt_fin'  :
expr → expr → expr → expr × expr → expr × expr → tactic.norm_fin.eval_fin_m expr

If a b : fin n and a' and b' are as returned by eval_fin, then prove_lt_fin' n a b a' b' proves a < b.

source
meta def tactic.norm_fin.prove_le_fin'  :
expr → expr → expr → expr × expr → expr × expr → tactic.norm_fin.eval_fin_m expr

If a b : fin n and a' and b' are as returned by eval_fin, then prove_le_fin' n a b a' b' proves a ≤ b.

source
meta def tactic.norm_fin.prove_eq_fin'  :
expr → expr → expr → expr × expr → expr × expr → tactic.norm_fin.eval_fin_m expr

If a b : fin n and a' and b' are as returned by eval_fin, then prove_eq_fin' n a b a' b' proves a = b.

source
meta def tactic.norm_fin.eval_prove_fin (f : expr → expr → expr → expr × expr → expr × expr → tactic.norm_fin.eval_fin_m expr) (a b : expr) :
tactic expr

Given a function with the type of prove_eq_fin', evaluates it with the given a and b.

source
meta def tactic.norm_fin.prove_eq_fin  :
expr → expr → tactic expr

If a b : fin n, then prove_eq_fin a b proves a = b.

source
meta def tactic.norm_fin.prove_lt_fin  :
expr → expr → tactic expr

If a b : fin n, then prove_lt_fin a b proves a < b.

source
meta def tactic.norm_fin.prove_le_fin  :
expr → expr → tactic expr

If a b : fin n, then prove_le_fin a b proves a ≤ b.

source
meta def tactic.norm_fin.mk_fin_numeral (n m : expr) :
expr → option (expr × expr)

Given expressions n and m such that n is definitionally equal to m.succ, and a natural numeral a, proves (b, ⊢ normalize_fin n b a), where n and m are both used in the construction of the numeral b : fin n.

source
meta def tactic.norm_fin.eval_rel {α : Type} (a b : expr) (f : expr → expr × expr → expr × expr → ℕ → ℕ → tactic.norm_fin.eval_fin_m α) :
tactic α

The common prep work for the cases in eval_ineq. Given inputs a b : fin n, it calls f n a' b' na nb where a' and b' are the result of eval_fin and na and nb are a' % n and b' % n as natural numbers.

source
meta def tactic.norm_fin.prove_lt_ge_fin  :
expr → expr → tactic (expr × bool × expr)

Given a b : fin n, proves either (n, tt, p) where p : a < b or (n, ff, p) where p : b ≤ a.

source
meta def tactic.norm_fin.prove_eq_ne_fin  :
expr → expr → tactic (expr × bool × expr)

Given a b : fin n, proves either (n, tt, p) where p : a = b or (n, ff, p) where p : a ≠ b.

source
meta def tactic.norm_fin.eval_ineq  :
expr → tactic (expr × expr)

A norm_num extension that evaluates equalities and inequalities on the type fin n.

example : (5 : fin 7) = fin.succ (fin.succ 3) := by norm_num
source
meta def tactic.norm_fin.as_numeral (n e : expr) :
tactic.norm_fin.eval_fin_m (option ℕ)

Evaluates e : fin n to a natural number less than n. Returns none if it is not a natural number or greater than n.

source
meta def tactic.norm_fin.eval_fin_num (a : expr) :
tactic (expr × expr)

Given a : fin n, returns (b, ⊢ a = b) where b is a normalized fin numeral. Fails if a is already normalized.

source
meta def tactic.interactive.norm_fin (hs : interactive.parse tactic.simp_arg_list) :
tactic unit

Rewrites occurrences of fin expressions to normal form anywhere in the goal. The norm_num extension will only rewrite fin expressions if they appear in equalities and inequalities. For example if the goal is P (2 + 2 : fin 3) then norm_num will not do anything but norm_fin will reduce the goal to P 1.

(The reason this is not part of norm_num is because evaluation of fin numerals uses a top down evaluation strategy while norm_num works bottom up; also determining whether a normalization will work is expensive, meaning that unrelated uses of norm_num would be slowed down with this as a plugin.)