1.5. Coercions

norm_cast

The norm_cast family of tactics is used to normalize certain coercions (casts) in expressions.

• norm_cast normalizes casts in the target.

• norm_cast at h normalizes casts in hypothesis h.

The tactic is basically a version of simp with a specific set of lemmas to move casts upwards in the expression. Therefore even in situations where non-terminal simp calls are discouraged (because of fragility), norm_cast is considered to be safe. It also has special handling of numerals.

For instance, given an assumption

a b : ℤ
h : ↑a + ↑b < (10 : ℚ)

writing norm_cast at h will turn h into

h : a + b < 10

There are also variants of basic tactics that use norm_cast to normalize expressions during their operation, to make them more flexible about the expressions they accept (we say that it is a tactic modulo the effects of norm_cast):

• exact_mod_cast for exact and apply_mod_cast for apply. Writing exact_mod_cast h and apply_mod_cast h will normalize casts in the goal and h before using exact h or apply h.

• rw_mod_cast for rw. It applies norm_cast between rewrites.

• assumption_mod_cast for assumption. This is effectively norm_cast at *; assumption, but more efficient. It normalizes casts in the goal and, for every hypothesis h in the context, it will try to normalize casts in h and use exact h.

See also push_cast, which moves casts inwards rather than lifting them outwards.

push_cast

push_cast rewrites the goal to move certain coercions (casts) inward, toward the leaf nodes. This uses norm_cast lemmas in the forward direction. For example, ↑(a + b) will be written to ↑a + ↑b.

• push_cast moves casts inward in the goal.

• push_cast at h moves casts inward in the hypothesis h. It can be used with extra simp lemmas with, for example, push_cast [Int.add_zero].

Example:

example (a b : Nat) (h1 : ((a + b : Nat) : Int) = 10) (h2 : ((a + b + 0 : Nat) : Int) = 10) : ((a + b : Nat) : Int) = 10 := bya:ℕb:ℕh1:↑(a + b) = 10h2:↑(a + b + 0) = 10⊢ ↑(a + b) = 10 /- h1 : ↑(a + b) = 10 h2 : ↑(a + b + 0) = 10 ⊢ ↑(a + b) = 10 -/ push_casta:ℕb:ℕh1:↑(a + b) = 10h2:↑(a + b + 0) = 10⊢ ↑a + ↑b = 10 /- Now ⊢ ↑a + ↑b = 10 -/ push_cast at h1a:ℕb:ℕh2:↑(a + b + 0) = 10h1:↑a + ↑b = 10⊢ ↑a + ↑b = 10 push_cast [Int.add_zero] at h2a:ℕb:ℕh1:↑a + ↑b = 10h2:↑a + ↑b = 10⊢ ↑a + ↑b = 10 /- Now h1 h2 : ↑a + ↑b = 10 -/ exact h1All goals completed! 🐙

See also norm_cast.

assumption_mod_cast

assumption_mod_cast is a variant of assumption that solves the goal using a hypothesis. Unlike assumption, it first pre-processes the goal and each hypothesis to move casts as far outwards as possible, so it can be used in more situations.

Concretely, it runs norm_cast on the goal. For each local hypothesis h, it also normalizes h with norm_cast and tries to use that to close the goal.

exact_mod_cast

Normalize casts in the goal and the given expression, then close the goal with exact.

apply_mod_cast

Normalize casts in the goal and the given expression, then apply the expression to the goal.

rw_mod_cast

Rewrites with the given rules, normalizing casts prior to each step.

lift

Lift an expression to another type.

• Usage: 'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?.

• If n : ℤ and hn : n ≥ 0 then the tactic lift n to ℕ using hn creates a new constant of type ℕ, also named n and replaces all occurrences of the old variable (n : ℤ) with ↑n (where n in the new variable). It will remove n and hn from the context.

  • So for example the tactic lift n to ℕ using hn transforms the goal n : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3 to n : ℕ, h : P ↑n ⊢ ↑n = 3 (here P is some term of type ℤ → Prop).

• The argument using hn is optional, the tactic lift n to ℕ does the same, but also creates a new subgoal that n ≥ 0 (where n is the old variable). This subgoal will be placed at the top of the goal list.

  • So for example the tactic lift n to ℕ transforms the goal n : ℤ, h : P n ⊢ n = 3 to two goals n : ℤ, h : P n ⊢ n ≥ 0 and n : ℕ, h : P ↑n ⊢ ↑n = 3.

• You can also use lift n to ℕ using e where e is any expression of type n ≥ 0.

• Use lift n to ℕ with k to specify the name of the new variable.

• Use lift n to ℕ with k hk to also specify the name of the equality ↑k = n. In this case, n will remain in the context. You can use rfl for the name of hk to substitute n away (i.e. the default behavior).

• You can also use lift e to ℕ with k hk where e is any expression of type ℤ. In this case, the hk will always stay in the context, but it will be used to rewrite e in all hypotheses and the target.

  • So for example the tactic lift n + 3 to ℕ using hn with k hk transforms the goal n : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n to the goal n : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n.

• The tactic lift n to ℕ using h will remove h from the context. If you want to keep it, specify it again as the third argument to with, like this: lift n to ℕ using h with n rfl h.

• More generally, this can lift an expression from α to β assuming that there is an instance of CanLift α β. In this case the proof obligation is specified by CanLift.prf.

• Given an instance CanLift β γ, it can also lift α → β to α → γ; more generally, given β : Π a : α, Type*, γ : Π a : α, Type*, and [Π a : α, CanLift (β a) (γ a)], it automatically generates an instance CanLift (Π a, β a) (Π a, γ a).

lift is in some sense dual to the zify tactic. lift (z : ℤ) to ℕ will change the type of an integer z (in the supertype) to ℕ (the subtype), given a proof that z ≥ 0; propositions concerning z will still be over ℤ. zify changes propositions about ℕ (the subtype) to propositions about ℤ (the supertype), without changing the type of any variable.

zify

The zify tactic is used to shift propositions from Nat to Int. This is often useful since Int has well-behaved subtraction.

example (a b c x y z : Nat) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  zify
  zify at h
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/

zify can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.

example (a b c : Nat) (h : a - b < c) (hab : b ≤ a) : false := by
  zify [hab] at h
  /- h : ↑a - ↑b < ↑c -/

zify makes use of the @[zify_simps] attribute to move propositions, and the push_cast tactic to simplify the Int-valued expressions. zify is in some sense dual to the lift tactic. lift (z : Int) to Nat will change the type of an integer z (in the supertype) to Nat (the subtype), given a proof that z ≥ 0; propositions concerning z will still be over Int. zify changes propositions about Nat (the subtype) to propositions about Int (the supertype), without changing the type of any variable.

rify

The rify tactic is used to shift propositions from ℕ, ℤ or ℚ to ℝ. Although less useful than its cousins zify and qify, it can be useful when your goal or context already involves real numbers.

In the example below, assumption hn is about natural numbers, hk is about integers and involves casting a natural number to ℤ, and the conclusion is about real numbers. The proof uses rify to lift both assumptions to ℝ before calling linarith.

example {n : ℕ} {k : ℤ} (hn : 8 ≤ n) (hk : 2 * k ≤ n + 2) : (0 : ℝ) < n - k - 1 := byn:ℕk:ℤhn:8 ≤ nhk:2 * k ≤ ↑n + 2⊢ 0 < ↑n - ↑k - 1 rify at hn hkn:ℕk:ℤhn:8 ≤ ↑nhk:2 * ↑k ≤ ↑n + 2⊢ 0 < ↑n - ↑k - 1 /- Now have hn : 8 ≤ (n : ℝ) hk : 2 * (k : ℝ) ≤ (n : ℝ) + 2-/ linarithAll goals completed! 🐙

rify makes use of the @[zify_simps], @[qify_simps] and @[rify_simps] attributes to move propositions, and the push_cast tactic to simplify the ℝ-valued expressions.

rify can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.

example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : a < b + c := bya:ℕb:ℕc:ℕh:a - b < chab:b ≤ a⊢ a < b + c rify [hab] at h ⊢a:ℕb:ℕc:ℕhab:b ≤ ah:↑a - ↑b < ↑c⊢ ↑a < ↑b + ↑c linarithAll goals completed! 🐙

Note that zify or qify would work just as well in the above example (and zify is the natural choice since it is enough to get rid of the pathological ℕ subtraction).

qify

The qify tactic is used to shift propositions from ℕ or ℤ to ℚ. This is often useful since ℚ has well-behaved division.

declaration uses 'sorry'example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := bya:ℕb:ℕc:ℕx:ℕy:ℕz:ℕh:¬x * y * z < 0⊢ c < a + 3 * b qifya:ℕb:ℕc:ℕx:ℕy:ℕz:ℕh:¬x * y * z < 0⊢ ↑c < ↑a + 3 * ↑b qify at ha:ℕb:ℕc:ℕx:ℕy:ℕz:ℕh:¬↑x * ↑y * ↑z < 0⊢ ↑c < ↑a + 3 * ↑b /- h : ¬↑x * ↑y * ↑z < 0 ⊢ ↑c < ↑a + 3 * ↑b -/ sorryAll goals completed! 🐙

qify can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.

example (a b c : ℤ) (h : a / b = c) (hab : b ∣ a) (hb : b ≠ 0) : a = c * b := bya:ℤb:ℤc:ℤh:a / b = chab:b ∣ ahb:b ≠ 0⊢ a = c * b qify [hab] at h hb ⊢a:ℤb:ℤc:ℤhab:b ∣ ah:↑a / ↑b = ↑chb:↑b ≠ 0⊢ ↑a = ↑c * ↑b exact (div_eq_iff hb).1 hAll goals completed! 🐙

qify makes use of the @[zify_simps] and @[qify_simps] attributes to move propositions, and the push_cast tactic to simplify the ℚ-valued expressions.