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

ink

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

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

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

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

ink

instance instCanLiftIntNatCastInstNatCastIntLeInstLEIntOfNatInstOfNatInt : CanLift ℤ ℕ (fun n => ↑n) fun x => 0 ≤ x

Equations

• instCanLiftIntNatCastInstNatCastIntLeInstLEIntOfNatInstOfNatInt = { prf := instCanLiftIntNatCastInstNatCastIntLeInstLEIntOfNatInstOfNatInt.proof_1 }

ink

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

Enable automatic handling of pi types in can_lift.

Equations

• Pi.canLift ι α β coe P = { prf := (_ : ∀ (f : (i : ι) → α i), ((i : ι) → P i (f i)) → ∃ y, (fun i => coe i (y i)) = f) }

ink

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

ink

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

Equations

• PiSubtype.canLift ι α p = { prf := (_ : ∀ (f : (i : Subtype p) → α i.val), True → ∃ g, (fun i => g i.val) = f) }

ink

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

Equations

• PiSubtype.canLift' ι α p = PiSubtype.canLift ι (fun x => α) p

ink

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

Equations

• Subtype.canLift p = { prf := (_ : ∀ (a : α), p a → ∃ y, y.val = a) }

ink

def Mathlib.Tactic.lift : Lean.ParserDescr

Lift an expression to another type.

• Usage: 'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?.
• If n : ℤ and hn : n ≥ 0≥ 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↑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≥ 0, h : P n ⊢ n = 3⊢ n = 3 to n : ℕ, h : P ↑n ⊢ ↑n = 3↑n ⊢ ↑n = 3⊢ ↑n = 3↑n = 3 (here P is some term of type ℤ → Prop→ Prop).
• The argument using hn is optional, the tactic lift n to ℕ does the same, but also creates a new subgoal that n ≥ 0≥ 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⊢ n = 3 to two goals n : ℤ, h : P n ⊢ n ≥ 0⊢ n ≥ 0≥ 0 and n : ℕ, h : P ↑n ⊢ ↑n = 3↑n ⊢ ↑n = 3⊢ ↑n = 3↑n = 3.
• You can also use lift n to ℕ using e where e is any expression of type n ≥ 0≥ 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↑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≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n⊢ n + 3 = 2 * n to the goal n : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n↑k ⊢ ↑k = 2 * n⊢ ↑k = 2 * n↑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≥ 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.

Equations

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

ink

def Mathlib.Tactic.Lift.getInst (old_tp : Lean.Expr) (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.

ink

def Mathlib.Tactic.Lift.main (e : Lean.TSyntax `term) (t : Lean.TSyntax `term) (hUsing : Option (Lean.TSyntax `term)) (newVarName : Option (Lean.TSyntax `ident)) (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.