tactic.lift - mathlib docs

pi.can_lift ι α β = {coe := λ (f : Π (i : ι), β i) (i : ι), can_lift.coe (f i), cond := λ (f : Π (i : ι), α i), ∀ (i : ι), can_lift.cond (β i) (f i), prf := _}

source

theorem subtype.exists_pi_extension {ι : Sort u_1} {α : ι → Sort u_2} [ne : ∀ (i : ι), nonempty (α i)] {p : ι → Prop} (f : Π (i : subtype p), α ↑i) :

∃ (g : Π (i : ι), α i), (λ (i : subtype p), g ↑i) = f

source

@[protected, instance]

def pi_subtype.can_lift (ι : Sort u_1) (α : ι → Sort u_2) [ne : ∀ (i : ι), nonempty (α i)] (p : ι → Prop) :

can_lift (Π (i : subtype p), α ↑i) (Π (i : ι), α i)

Equations

pi_subtype.can_lift ι α p = {coe := λ (f : Π (i : ι), α i) (i : subtype p), f ↑i, cond := λ (_x : Π (i : subtype p), α ↑i), true, prf := _}

source

@[protected, instance]

def pi_subtype.can_lift' (ι : Sort u_1) (α : Sort u_2) [ne : nonempty α] (p : ι → Prop) :

can_lift (subtype p → α) (ι → α)

Equations

pi_subtype.can_lift' ι α p = pi_subtype.can_lift ι (λ (_x : ι), α) p

source

@[protected, instance]

def subtype.can_lift {α : Sort u_1} (p : α → Prop) :

can_lift α {x // p x}

Equations

subtype.can_lift p = {coe := coe coe_to_lift, cond := p, prf := _}

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

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.

source

def tactic_doc.tactic.lift :

tactic_doc_entry

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.

mathlib documentation

lift tactic #

Tags #