Documentation

Mathlib.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

class CanLift (α : Sort u_1) (β : Sort u_2) (coe : outParam (βα)) (cond : outParam (αProp)) :
  • prf : ∀ (x : α), cond xy, coe y = x

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

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

Instances
    instance Pi.canLift (ι : Sort u_1) (α : ιSort u_2) (β : ιSort u_3) (coe : (i : ι) → β iα i) (P : (i : ι) → α iProp) [∀ (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 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, (fun i => 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 => f i.val) fun x => True
    instance PiSubtype.canLift' (ι : Sort u_1) (α : Sort u_2) [Nonempty α] (p : ιProp) :
    CanLift (Subtype pα) (ια) (fun f i => f i.val) fun x => True
    instance Subtype.canLift {α : Sort u_1} (p : αProp) :
    CanLift α { x // p x } Subtype.val p

    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.

    Instances For

      Generate instance for the lift tactic.

      Instances For
        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) :

        Main function for the lift tactic.

        Instances For