mathlib documentation

tactic.lift

lift tactic #

This file defines the lift tactic, allowing the user to lift elements from one type to another under a specified condition.

Tags #

lift, tactic

source
@[class]
structure can_lift (α : Sort u_1) (β : Sort u_2) :
Sort (max 1 (imax u_2 u_1) u_1)

A class specifying that you can lift elements from α to β assuming cond is true. Used by the tactic lift.

Instances
source
meta def can_lift_attr  :
(user_attribute (list name))

A user attribute used internally by the lift tactic. This should not be applied by hand.

source
@[protected, instance]
def nat.can_lift  :
can_lift ℤ ℕ
Equations
source
@[protected, instance]
def pi.can_lift (ι : Type u_1) (α : ι → Type u_2) (β : ι → Type u_3) [Π (i : ι), can_lift (α i) (β i)] :
can_lift (Π (i : ι), α i) (Π (i : ι), β i)

Enable automatic handling of pi types in can_lift.

Equations
source
@[protected, instance]
def pi_subtype.can_lift (ι : Type u_1) (α : ι → Type u_2) [ne : ∀ (i : ι), nonempty (α i)] (p : ι → Prop) :
can_lift (Π (i : subtype p), α ↑i) (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi_subtype.can_lift' (ι : Type u_1) (α : Type u_2) [ne : nonempty α] (p : ι → Prop) :
can_lift (subtype p → α) (ι → α)
Equations
source
meta def tactic.get_lift_prf (h : option pexpr) (old_tp new_tp inst e : expr) (s : simp_lemmas) (to_unfold : list name) :
tactic expr

Construct the proof of cond x in the lift tactic.

  • e is the expression being lifted and h is the specified proof of can_lift.cond e.
  • old_tp and new_tp are the arguments to can_lift and inst is the can_lift-instance.
  • s and to_unfold contain the information of the simp set used to simplify.

If the proof was specified, we check whether it has the correct type. If it doesn't have the correct type, we display an error message (but first call dsimp on the expression in the message).

If the proof was not specified, we create assert it as a local constant. (The name of this local constant doesn't matter, since lift will remove it from the context.)

source
meta def tactic.lift (p t : pexpr) (h : option pexpr) (n : list name) :
tactic unit

Lift the expression p to the type t, with proof obligation given by h. The list n is used for the two newly generated names, and to specify whether h should remain in the local context. See the doc string of tactic.interactive.lift for more information.

source
meta def tactic.using_texpr  :
lean.parser (option pexpr)

Parses an optional token "using" followed by a trailing pexpr.

source
meta def tactic.to_texpr  :
lean.parser pexpr

Parses a token "to" followed by a trailing pexpr.

source
meta def tactic.interactive.lift (p : interactive.parse interactive.types.texpr) (t : interactive.parse tactic.to_texpr) (h : interactive.parse tactic.using_texpr) (n : interactive.parse interactive.types.with_ident_list) :
tactic unit

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).
    • 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 = 3 and n : ℤ, h : P n ⊢ n ≥ 0.
  • 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 can_lift α β. In this case the proof obligation is specified by can_lift.cond.
  • Given an instance can_lift β γ, it can also lift α → β to α → γ; more generally, given β : Π a : α, Type*, γ : Π a : α, Type*, and [Π a : α, can_lift (β a) (γ a)], it automatically generates an instance can_lift (Π 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.