Created
July 4, 2019 12:35
-
-
Save PatrickMassot/a54fb57815ce748ebc907d66f491bb0d to your computer and use it in GitHub Desktop.
`apply_fun` tactic
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import order.basic | |
open tactic interactive (parse) interactive (loc.ns) | |
interactive.types (texpr location) lean.parser (tk) | |
local postfix `?`:9001 := optional | |
meta def apply_fun_name (e : expr) (h : name) (M : option pexpr) : tactic unit := | |
do { | |
H ← get_local h, | |
t ← infer_type H, | |
match t with | |
| `(%%l = %%r) := do | |
tactic.interactive.«have» h ``(%%e %%l = %%e %%r) ``(congr_arg %%e %%H), | |
tactic.clear H | |
| `(%%l ≤ %%r) := do | |
if M.is_some then do | |
Hmono ← M >>= tactic.i_to_expr, | |
tactic.interactive.«have» h ``(%%e %%l ≤ %%e %%r) ``(%%Hmono %%H) | |
else do { | |
n ← get_unused_name `mono, | |
tactic.interactive.«have» n ``(monotone %%e) none, | |
swap, | |
Hmono ← get_local n, | |
tactic.interactive.«have» h ``(%%e %%l ≤ %%e %%r) ``(%%Hmono %%H) }, | |
tactic.clear H | |
| _ := skip | |
end } <|> fail ("failed to apply " ++ to_string e ++ " at " ++ to_string h) | |
namespace tactic.interactive | |
/-- Apply a function to some local assumptions which are either equalities or | |
inequalities. For instance, if the context contains `h : a = b` and | |
some function `f` then `apply_fun f at h` turns `h` into `h : f a = f b`. | |
When the assumption is an inequality `h : a ≤ b`, a side goal `monotone f` | |
is created, unless this condition is provided using | |
`apply_fun f at h using P` where `P : monotone f`. -/ | |
meta def apply_fun (q : parse texpr) (locs : parse location) | |
(lem : parse (tk "using" *> texpr)?) : tactic unit := | |
do e ← tactic.i_to_expr q, | |
match locs with | |
| (loc.ns l) := do | |
l.mmap' (λ l, match l with | |
| some h := apply_fun_name e h lem | |
| none := skip | |
end) | |
| wildcard := do ctx ← local_context, | |
ctx.mmap' (λ h, apply_fun_name e h.local_pp_name lem) | |
end | |
end tactic.interactive | |
open function | |
example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : injective $ g ∘ f) : | |
injective f := | |
begin | |
intros x x' h, | |
apply_fun g at h, | |
exact H h | |
end | |
example (f : ℕ → ℕ) (a b : ℕ) (monof : monotone f) (h : a ≤ b) : f a ≤ f b := | |
begin | |
apply_fun f at h, | |
assumption, | |
assumption | |
end | |
example (f : ℕ → ℕ) (a b : ℕ) (monof : monotone f) (h : a ≤ b) : f a ≤ f b := | |
begin | |
apply_fun f at h using monof, | |
assumption | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment