tactic.norm_fin

# norm_fin#

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

## Main definitions #

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
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
theorem tactic.norm_fin.normalize_fin_lt.coe {n : } {a : fin n} {b : } (h : b) :
a = b
theorem tactic.norm_fin.normalize_fin_iff {n : } [ne_zero n] {a : fin n} {b : } :
a =
theorem tactic.norm_fin.normalize_fin_lt.mk {n : } {a : fin n} {b n' : } (hn : n = n') (h : b) (h2 : b < n') :
theorem tactic.norm_fin.normalize_fin_lt.lt {n : } {a : fin n} {b : } (h : b) :
b < n
theorem tactic.norm_fin.normalize_fin_lt.of {n : } {a : fin n} {b : } (h : b) :
theorem tactic.norm_fin.normalize_fin.add {n : } {a b : fin n} {a' b' c' : } (ha : a') (hb : b') (h : a' + b' = c') :
(a + b) c'
theorem tactic.norm_fin.normalize_fin.mul {n : } {a b : fin n} {a' b' c' : } (ha : a') (hb : b') (h : a' * b' = c') :
(a * b) c'
theorem tactic.norm_fin.normalize_fin.bit0 {n : } {a : fin n} {a' : } (h : a') :
(bit0 a')
theorem tactic.norm_fin.normalize_fin.bit1 {n : } [ne_zero n] {a : fin n} {a' : } (h : a') :
(bit1 a')
theorem tactic.norm_fin.normalize_fin_lt.succ {n : } {a : fin n} {a' b : } (h : a') (e : a' + 1 = b) :
theorem tactic.norm_fin.normalize_fin_lt.cast_lt {n m : } {a : fin m} {ha : a.val < n} {a' : } (h : a') :
a'
theorem tactic.norm_fin.normalize_fin_lt.cast_le {n m : } {nm : m n} {a : fin m} {a' : } (h : a') :
((fin.cast_le nm) a) a'
theorem tactic.norm_fin.normalize_fin_lt.cast {n m : } {nm : m = n} {a : fin m} {a' : } (h : a') :
((fin.cast nm) a) a'
theorem tactic.norm_fin.normalize_fin.cast {n m : } {nm : m = n} {a : fin m} {a' : } (h : a') :
((fin.cast nm) a) a'
theorem tactic.norm_fin.normalize_fin_lt.cast_add {n m : } {a : fin n} {a' : } (h : a') :
theorem tactic.norm_fin.normalize_fin_lt.cast_succ {n : } {a : fin n} {a' : } (h : a') :
a'
theorem tactic.norm_fin.normalize_fin_lt.add_nat {n m m' : } (hm : m = m') {a : fin n} {a' b : } (h : a') (e : a' + m' = b) :
theorem tactic.norm_fin.normalize_fin_lt.nat_add {n m n' : } (hn : n = n') {a : fin m} {a' b : } (h : a') (e : n' + a' = b) :
theorem tactic.norm_fin.normalize_fin.reduce {n : } {a : fin n} {n' a' b k nk : } (hn : n = n') (h : a') (e1 : n' * k = nk) (e2 : nk + b = a') :
theorem tactic.norm_fin.normalize_fin_lt.reduce {n : } {a : fin n} {n' a' b k nk : } (hn : n = n') (h : a') (e1 : n' * k = nk) (e2 : nk + b = a') (hl : b < n') :
theorem tactic.norm_fin.normalize_fin.eq {n : } {a b : fin n} {c : } (ha : c) (hb : c) :
a = b
theorem tactic.norm_fin.normalize_fin.lt {n : } {a b : fin n} {a' b' : } (ha : a') (hb : b') (h : a' < b') :
a < b
theorem tactic.norm_fin.normalize_fin.le {n : } {a b : fin n} {a' b' : } (ha : a') (hb : b') (h : a' b') :
a b
@[protected, instance]
@[protected, instance]
meta def tactic.norm_fin.eval_fin_m (α : 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.

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

Lifts a tactic into the eval_fin_m monad.

@[protected, instance]

Lifts an instance_cache tactic into the eval_fin_m monad.

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.

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.

meta def tactic.norm_fin.eval_fin_m.run {α : Type}  :

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

• zero :
• one :
• mul :
• bit0 :
• bit1 :
• succ :
• cast_lt :
• cast_le :
• cast :
• cast_succ :

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.

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.

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

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.

meta def tactic.norm_fin.eval_fin_lt' (eval_fin : 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.)

Get n such that a : fin n.

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.

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

meta def tactic.norm_fin.reduce_fin (lt : bool) (n a : 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.

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.

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.

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.

meta def tactic.norm_fin.eval_prove_fin (f : expr ) (a b : expr) :

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

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

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

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

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.

meta def tactic.norm_fin.eval_rel {α : Type} (a b : expr) (f : expr ) :

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.

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

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

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
meta def tactic.norm_fin.as_numeral (n e : expr) :

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

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

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

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.

example : (5 : fin 7) = fin.succ (fin.succ 3) := by norm_num
example (P : fin 7  Prop) (h : P 5) : P (fin.succ (fin.succ 3)) := by norm_fin; exact h