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

class CanLift (α : Sort u_1) (β : Sort u_2) (coe : outParam (β → α)) (cond : outParam (α → Prop)) : Prop

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

• prf (x : α) : cond x → ∃ (y : β), coe y = x

  An element of α that satisfies cond belongs to the range of coe.

instance instCanLiftIntNatCastLeOfNat : CanLift Int Nat (fun (n : Nat) => ↑n) fun (x : Int) => 0 ≤ x

instance Pi.canLift (ι : Sort u_1) (α : ι → Sort u_2) (β : ι → Sort u_3) (coe : (i : ι) → β i → α i) (P : (i : ι) → α i → Prop) [∀ (i : ι), CanLift (α i) (β i) (coe i) (P i)] : CanLift ((i : ι) → α i) ((i : ι) → β i) (fun (f : (i : ι) → β i) (i : ι) => coe i (f i)) fun (f : (i : ι) → α i) => ∀ (i : ι), P i (f i)

Enable automatic handling of pi types in CanLift.

instance Prod.instCanLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {coeβα : β → α} {condβα : α → Prop} {coeδγ : δ → γ} {condδγ : γ → Prop} [CanLift α β coeβα condβα] [CanLift γ δ coeδγ condδγ] : CanLift (α × γ) (β × δ) (map coeβα coeδγ) fun (x : α × γ) => condβα x.fst ∧ condδγ x.snd

Enable automatic handling of product types in CanLift.

theorem Subtype.exists_pi_extension {ι : Sort u_1} {α : ι → Sort u_2} [ne : ∀ (i : ι), Nonempty (α i)] {p : ι → Prop} (f : (i : Subtype p) → α i.val) : ∃ (g : (i : ι) → α i), (fun (i : Subtype p) => g i.val) = f

instance PiSubtype.canLift (ι : Sort u_1) (α : ι → Sort u_2) [∀ (i : ι), Nonempty (α i)] (p : ι → Prop) : CanLift ((i : Subtype p) → α i.val) ((i : ι) → α i) (fun (f : (i : ι) → α i) (i : Subtype p) => f i.val) fun (x : (i : Subtype p) → α i.val) => True

instance PiSubtype.canLift' (ι : Sort u_1) (α : Sort u_2) [Nonempty α] (p : ι → Prop) : CanLift (Subtype p → α) (ι → α) (fun (f : ι → α) (i : Subtype p) => f i.val) fun (x : Subtype p → α) => True

instance Subtype.canLift {α : Sort u_1} (p : α → Prop) : CanLift α { x : α // p x } val p

def Mathlib.Tactic.lift : Lean.ParserDescr

lift e to t with x lifts the expression e to the type t by introducing a new variable x : t such that ↑x = e, and then replacing occurrences of e with ↑x. lift requires an instance of the class CanLift t' t coe cond, where t' is the type of e, and creates a side goal for the lifting condition, of the form ⊢ cond x, placing this on top of the goal stack.

Given an instance CanLift β γ, lift 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.

The norm_cast tactic can be used after lift to normalize introduced casts.

• lift e to t using h with x uses the expression h to prove the lifting condition cond e. If h is a variable, lift will try to clear it from the context. If you want to keep h in the context, write lift e to t using h with x rfl h (see below).
• If e is a variable, lift e to t is equivalent to lift e to t with e. The original variable e will be cleared from the context.
• lift e to t with x hx adds hx : ↑x = e to the context (and if e is a variable, does not clear it).
• lift e to t with x hx h adds hx : ↑x = e and h : cond e to the context (and if e is a variable, does not clear it). In particular, lift e to t using h with x hx h, where h is a variable, keeps h in the context.
• lift e to t with x rfl h adds h : cond e to the context (and if e is a variable, does not clear it). In particular, lift e to t using h with x rfl h, where h is a variable, keeps h in the context.

Examples:

def P (n : ℤ) : Prop := n = 3

example (n : ℤ) (h : P n) : n = 3 := by
  lift n to ℕ
  /-
  Two goals:
  n : ℤ, h : P n ⊢ n ≥ 0
  n : ℕ, h : P ↑n ⊢ ↑n = 3
  -/
  · unfold P at h; linarith
  · exact h

example (n : ℤ) (hn : n ≥ 0) (h : P n) : n = 3 := by
  lift n to ℕ using hn
  /-
  One goal:
  n : ℕ
  h : P ↑n
  ⊢ ↑n = 3
  -/
  exact h

example (n : ℤ) (hn : n + 3 ≥ 0) (h : P (n + 3)) :
    n + 3 = n * 2 + 3 := by
  lift n + 3 to ℕ using hn with k hk
  /-
  One goal:
  n : ℤ
  k : ℕ
  hk : ↑k = n + 3
  h : P ↑k
  ⊢ ↑k = 2 * n + 3
  -/
  unfold P at h; linarith

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Lift.getInst (old_tp new_tp : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr)

Generate instance for the lift tactic.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Lift.main (e t : Lean.TSyntax `term) (hUsing : Option (Lean.TSyntax `term)) (newVarName newEqName : Option (Lean.TSyntax `ident)) (keepUsing : Bool) : Lean.Elab.Tactic.TacticM Unit

Main function for the lift tactic.

Equations

• One or more equations did not get rendered due to their size.