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
- coe : β → α
- cond : α → Prop
- prf : ∀ (x : α), can_lift.cond β x → (∃ (y : β), can_lift.coe y = x)
A class specifying that you can lift elements from α
to β
assuming cond
is true.
Used by the tactic lift
.
A user attribute used internally by the lift
tactic.
This should not be applied by hand.
Equations
- nat.can_lift = {coe := coe coe_to_lift, cond := λ (n : ℤ), 0 ≤ n, prf := nat.can_lift._proof_1}
Enable automatic handling of pi types in can_lift
.
Equations
- 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 := _}
Construct the proof of cond x
in the lift tactic.
e
is the expression being lifted andh
is the specified proof ofcan_lift.cond e
.old_tp
andnew_tp
are the arguments tocan_lift
andinst
is thecan_lift
-instance.s
andto_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.)
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.
Parses an optional token "using" followed by a trailing pexpr
.
Lift an expression to another type.
- Usage:
'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?
. - If
n : ℤ
andhn : n ≥ 0
then the tacticlift n to ℕ using hn
creates a new constant of typeℕ
, also namedn
and replaces all occurrences of the old variable(n : ℤ)
with↑n
(wheren
in the new variable). It will removen
andhn
from the context.- So for example the tactic
lift n to ℕ using hn
transforms the goaln : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3
ton : ℕ, h : P ↑n ⊢ ↑n = 3
(hereP
is some term of typeℤ → Prop
).
- So for example the tactic
- The argument
using hn
is optional, the tacticlift n to ℕ
does the same, but also creates a new subgoal thatn ≥ 0
(wheren
is the old variable).- So for example the tactic
lift n to ℕ
transforms the goaln : ℤ, h : P n ⊢ n = 3
to two goalsn : ℕ, h : P ↑n ⊢ ↑n = 3
andn : ℤ, h : P n ⊢ n ≥ 0
.
- So for example the tactic
- You can also use
lift n to ℕ using e
wheree
is any expression of typen ≥ 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 userfl
for the name ofhk
to substituten
away (i.e. the default behavior). - You can also use
lift e to ℕ with k hk
wheree
is any expression of typeℤ
. In this case, thehk
will always stay in the context, but it will be used to rewritee
in all hypotheses and the target.- So for example the tactic
lift n + 3 to ℕ using hn with k hk
transforms the goaln : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n
to the goaln : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n
.
- So for example the tactic
- The tactic
lift n to ℕ using h
will removeh
from the context. If you want to keep it, specify it again as the third argument towith
, 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 ofcan_lift α β
. In this case the proof obligation is specified bycan_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 instancecan_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.