refactor(library/init/meta/converter): new conv monad implementation
This commit is contained in:
Leonardo de Moura
parent
5dee3415a4
commit
fe51bebab3
8 changed files with 187 additions and 364 deletions
|
|
@ -6,282 +6,112 @@ Authors: Leonardo de Moura
|
|||
Converter monad for building simplifiers.
|
||||
-/
|
||||
prelude
|
||||
import init.meta.tactic init.meta.simp_tactic
|
||||
import init.meta.tactic init.meta.simp_tactic init.meta.interactive
|
||||
import init.meta.congr_lemma init.meta.match_tactic
|
||||
open tactic
|
||||
|
||||
meta structure conv_result (α : Type) :=
|
||||
(val : α) (rhs : expr) (proof : option expr)
|
||||
universe u
|
||||
|
||||
meta def conv (α : Type) : Type :=
|
||||
name → expr → tactic (conv_result α)
|
||||
|
||||
namespace conv
|
||||
|
||||
meta def lhs : conv expr :=
|
||||
λ r e, return ⟨e, e, none⟩
|
||||
|
||||
meta def change (new_p : pexpr) : conv unit :=
|
||||
λ r e, do
|
||||
e_type ← infer_type e,
|
||||
new_e ← to_expr ``(%%new_p : %%e_type),
|
||||
unify e new_e,
|
||||
return ⟨(), new_e, none⟩
|
||||
|
||||
protected meta def pure {α : Type} : α → conv α :=
|
||||
λ a r e, return ⟨a, e, none⟩
|
||||
|
||||
private meta def join_proofs (r : name) (o₁ o₂ : option expr) : tactic (option expr) :=
|
||||
match o₁, o₂ with
|
||||
| none, _ := return o₂
|
||||
| _, none := return o₁
|
||||
| some p₁, some p₂ := do
|
||||
env ← get_env,
|
||||
match env.trans_for r with
|
||||
| some trans := do pr ← mk_app trans [p₁, p₂], return $ some pr
|
||||
| none := fail format!"converter failed, relation '{r}' is not transitive"
|
||||
end
|
||||
end
|
||||
|
||||
protected meta def seq {α β : Type} (c₁ : conv (α → β)) (c₂ : conv α) : conv β :=
|
||||
λ r e, do
|
||||
⟨fn, e₁, pr₁⟩ ← c₁ r e,
|
||||
⟨a, e₂, pr₂⟩ ← c₂ r e₁,
|
||||
pr ← join_proofs r pr₁ pr₂,
|
||||
return ⟨fn a, e₂, pr⟩
|
||||
|
||||
protected meta def fail {α β : Type} [has_to_format β] (msg : β) : conv α :=
|
||||
λ r e, tactic.fail msg
|
||||
|
||||
protected meta def failed {α : Type} : conv α :=
|
||||
λ r e, tactic.failed
|
||||
|
||||
protected meta def orelse {α : Type} (c₁ : conv α) (c₂ : conv α) : conv α :=
|
||||
λ r e, c₁ r e <|> c₂ r e
|
||||
|
||||
protected meta def map {α β : Type} (f : α → β) (c : conv α) : conv β :=
|
||||
λ r e, do
|
||||
⟨a, e₁, pr⟩ ← c r e,
|
||||
return ⟨f a, e₁, pr⟩
|
||||
|
||||
protected meta def bind {α β : Type} (c₁ : conv α) (c₂ : α → conv β) : conv β :=
|
||||
λ r e, do
|
||||
⟨a, e₁, pr₁⟩ ← c₁ r e,
|
||||
⟨b, e₂, pr₂⟩ ← c₂ a r e₁,
|
||||
pr ← join_proofs r pr₁ pr₂,
|
||||
return ⟨b, e₂, pr⟩
|
||||
meta def conv (α : Type u) :=
|
||||
tactic α
|
||||
|
||||
meta instance : monad conv :=
|
||||
{ map := @conv.map,
|
||||
pure := @conv.pure,
|
||||
bind := @conv.bind,
|
||||
id_map := undefined, pure_bind := undefined, bind_assoc := undefined,
|
||||
bind_pure_comp_eq_map := undefined, bind_map_eq_seq := undefined }
|
||||
by unfold conv; apply_instance
|
||||
|
||||
meta instance : monad_fail conv :=
|
||||
by unfold conv; apply_instance
|
||||
|
||||
meta instance : alternative conv :=
|
||||
{ conv.monad with
|
||||
failure := @conv.failed,
|
||||
orelse := @conv.orelse }
|
||||
by unfold conv; apply_instance
|
||||
|
||||
meta def whnf (md : transparency := reducible) : conv unit :=
|
||||
λ r e, do n ← tactic.whnf e md, return ⟨(), n, none⟩
|
||||
namespace conv
|
||||
meta def convert (c : conv unit) (lhs : expr) (rel : name := `eq) : tactic (expr × expr) :=
|
||||
do lhs_type ← infer_type lhs,
|
||||
rhs ← mk_meta_var lhs_type,
|
||||
new_target ← mk_app rel [lhs, rhs],
|
||||
new_g ← mk_meta_var new_target,
|
||||
gs ← get_goals,
|
||||
set_goals [new_g],
|
||||
c,
|
||||
repeat reflexivity,
|
||||
n ← num_goals,
|
||||
when (n ≠ 0) (fail "convert tactic failed, there are unsolved goals"),
|
||||
set_goals gs,
|
||||
rhs ← instantiate_mvars rhs,
|
||||
new_g ← instantiate_mvars new_g,
|
||||
return (rhs, new_g)
|
||||
|
||||
meta def dsimp : conv unit :=
|
||||
λ r e, do s ← simp_lemmas.mk_default, n ← s.dsimplify e, return ⟨(), n, none⟩
|
||||
meta def lhs : conv expr :=
|
||||
do (_, lhs, rhs) ← target_lhs_rhs,
|
||||
return lhs
|
||||
|
||||
meta def try (c : conv unit) : conv unit :=
|
||||
c <|> return ()
|
||||
meta def rhs : conv expr :=
|
||||
do (_, lhs, rhs) ← target_lhs_rhs,
|
||||
return rhs
|
||||
|
||||
meta def tryb (c : conv unit) : conv bool :=
|
||||
(c >> return tt) <|> return ff
|
||||
meta def update_lhs (new_lhs : expr) (h : expr) : conv unit :=
|
||||
do transitivity,
|
||||
rhs >>= unify new_lhs,
|
||||
exact h,
|
||||
t ← target >>= instantiate_mvars,
|
||||
change t
|
||||
|
||||
meta def trace {α : Type} [has_to_tactic_format α] (a : α) : conv unit :=
|
||||
λ r e, tactic.trace a >> return ⟨(), e, none⟩
|
||||
|
||||
meta def trace_lhs : conv unit :=
|
||||
lhs >>= trace
|
||||
|
||||
meta def apply_lemmas_core (s : simp_lemmas) (prove : tactic unit) : conv unit :=
|
||||
λ r e, do
|
||||
(new_e, pr) ← s.rewrite prove r e,
|
||||
return ⟨(), new_e, some pr⟩
|
||||
|
||||
meta def apply_lemmas (s : simp_lemmas) : conv unit :=
|
||||
apply_lemmas_core s failed
|
||||
|
||||
/- adapter for using iff-lemmas as eq-lemmas -/
|
||||
meta def apply_propext_lemmas_core (s : simp_lemmas) (prove : tactic unit) : conv unit :=
|
||||
λ r e, do
|
||||
guard (r = `eq),
|
||||
(new_e, pr) ← s.rewrite prove `iff e,
|
||||
new_pr ← mk_app `propext [pr],
|
||||
return ⟨(), new_e, some new_pr⟩
|
||||
|
||||
meta def apply_propext_lemmas (s : simp_lemmas) : conv unit :=
|
||||
apply_propext_lemmas_core s failed
|
||||
|
||||
private meta def mk_refl_proof (r : name) (e : expr) : tactic expr :=
|
||||
do env ← get_env,
|
||||
match (environment.refl_for env r) with
|
||||
| (some refl) := do pr ← mk_app refl [e], return pr
|
||||
| none := fail format!"converter failed, relation '{r}' is not reflexive"
|
||||
end
|
||||
|
||||
meta def to_tactic (c : conv unit) : name → expr → tactic (expr × expr) :=
|
||||
λ r e, do
|
||||
⟨u, e₁, o⟩ ← c r e,
|
||||
match o with
|
||||
| none := do p ← mk_refl_proof r e, return (e₁, p)
|
||||
| some p := return (e₁, p)
|
||||
end
|
||||
|
||||
meta def lift_tactic {α : Type} (t : tactic α) : conv α :=
|
||||
λ r e, do a ← t, return ⟨a, e, none⟩
|
||||
|
||||
meta def apply_simp_set (attr_name : name) : conv unit :=
|
||||
lift_tactic (get_user_simp_lemmas attr_name) >>= apply_lemmas
|
||||
|
||||
meta def apply_propext_simp_set (attr_name : name) : conv unit :=
|
||||
lift_tactic (get_user_simp_lemmas attr_name) >>= apply_propext_lemmas
|
||||
meta def change (new_lhs : expr) : conv unit :=
|
||||
do (r, lhs, rhs) ← target_lhs_rhs,
|
||||
new_target ← mk_app r [new_lhs, rhs],
|
||||
tactic.change new_target
|
||||
|
||||
meta def skip : conv unit :=
|
||||
return ()
|
||||
reflexivity
|
||||
|
||||
meta def repeat : conv unit → conv unit
|
||||
| c r lhs :=
|
||||
(do
|
||||
⟨_, rhs₁, pr₁⟩ ← c r lhs,
|
||||
guard (¬ lhs =ₐ rhs₁),
|
||||
⟨_, rhs₂, pr₂⟩ ← repeat c r rhs₁,
|
||||
pr ← join_proofs r pr₁ pr₂,
|
||||
return ⟨(), rhs₂, pr⟩)
|
||||
<|> return ⟨(), lhs, none⟩
|
||||
meta def whnf : conv unit :=
|
||||
lhs >>= tactic.whnf >>= change
|
||||
|
||||
meta def first {α : Type} : list (conv α) → conv α
|
||||
| [] := conv.failed
|
||||
| (c::cs) := c <|> first cs
|
||||
meta def dsimp (s : option simp_lemmas := none) : conv unit :=
|
||||
do s ← match s with
|
||||
| some s := return s
|
||||
| none := simp_lemmas.mk_default
|
||||
end,
|
||||
lhs >>= s.dsimplify >>= change
|
||||
|
||||
meta def match_pattern (p : pattern) : conv unit :=
|
||||
λ r e, tactic.match_pattern p e >> return ⟨(), e, none⟩
|
||||
|
||||
meta def mk_match_expr (p : pexpr) : tactic (conv unit) :=
|
||||
do new_p ← pexpr_to_pattern p,
|
||||
return (λ r e, tactic.match_pattern new_p e >> return ⟨(), e, none⟩)
|
||||
|
||||
meta def match_expr (p : pexpr) : conv unit :=
|
||||
λ r e, do
|
||||
new_p ← pexpr_to_pattern p,
|
||||
tactic.match_pattern new_p e >> return ⟨(), e, none⟩
|
||||
|
||||
meta def funext (c : conv unit) : conv unit :=
|
||||
λ r lhs, do
|
||||
guard (r = `eq),
|
||||
(expr.lam n bi d b) ← return lhs,
|
||||
let aux_type := expr.pi n bi d (expr.const `true []),
|
||||
(result, _) ← solve_aux aux_type $ do {
|
||||
x ← intro1,
|
||||
c_result ← c r (b.instantiate_var x),
|
||||
let rhs := expr.lam n bi d (c_result.rhs.abstract x),
|
||||
match c_result.proof : _ → tactic (conv_result unit) with
|
||||
| some pr := do
|
||||
let aux_pr := expr.lam n bi d (pr.abstract x),
|
||||
new_pr ← mk_app `funext [lhs, rhs, aux_pr],
|
||||
return ⟨(), rhs, some new_pr⟩
|
||||
| none := return ⟨(), rhs, none⟩
|
||||
end },
|
||||
return result
|
||||
|
||||
meta def congr_core (c_f c_a : conv unit) : conv unit :=
|
||||
λ r lhs, do
|
||||
guard (r = `eq),
|
||||
(expr.app f a) ← return lhs,
|
||||
f_type ← infer_type f >>= tactic.whnf,
|
||||
guard (f_type.is_arrow),
|
||||
⟨(), new_f, of⟩ ← try c_f r f,
|
||||
⟨(), new_a, oa⟩ ← try c_a r a,
|
||||
rhs ← return $ new_f new_a,
|
||||
match of, oa with
|
||||
| none, none :=
|
||||
return ⟨(), rhs, none⟩
|
||||
| none, some pr_a := do
|
||||
pr ← mk_app `congr_arg [a, new_a, f, pr_a],
|
||||
return ⟨(), new_f new_a, some pr⟩
|
||||
| some pr_f, none := do
|
||||
pr ← mk_app `congr_fun [f, new_f, pr_f, a],
|
||||
return ⟨(), rhs, some pr⟩
|
||||
| some pr_f, some pr_a := do
|
||||
pr ← mk_app `congr [f, new_f, a, new_a, pr_f, pr_a],
|
||||
return ⟨(), rhs, some pr⟩
|
||||
private meta def congr_aux : list congr_arg_kind → list expr → tactic (list expr × list expr)
|
||||
| [] [] := return ([], [])
|
||||
| (k::ks) (a::as) := do
|
||||
(gs, largs) ← congr_aux ks as,
|
||||
match k with
|
||||
| congr_arg_kind.fixed := return $ (gs, a::largs)
|
||||
| congr_arg_kind.fixed_no_param := return $ (gs, largs)
|
||||
| congr_arg_kind.eq := do
|
||||
a_type ← infer_type a,
|
||||
rhs ← mk_meta_var a_type,
|
||||
g_type ← mk_app `eq [a, rhs],
|
||||
g ← mk_meta_var g_type,
|
||||
return (g::gs, a::rhs::g::largs)
|
||||
| congr_arg_kind.cast := return $ (gs, a::largs)
|
||||
| _ := fail "congr tactic failed, unsupported congruence lemma"
|
||||
end
|
||||
| ks as := fail "congr tactic failed, unsupported congruence lemma"
|
||||
|
||||
meta def congr (c : conv unit) : conv unit :=
|
||||
congr_core c c
|
||||
meta def congr : conv unit :=
|
||||
do (r, lhs, rhs) ← target_lhs_rhs,
|
||||
guard (r = `eq),
|
||||
let fn := lhs.get_app_fn,
|
||||
let args := lhs.get_app_args,
|
||||
cgr_lemma ← mk_congr_lemma_simp fn (some args.length),
|
||||
g::gs ← get_goals,
|
||||
(new_gs, lemma_args) ← congr_aux cgr_lemma.arg_kinds args,
|
||||
let g_val := cgr_lemma.proof.mk_app lemma_args,
|
||||
unify g g_val,
|
||||
set_goals $ new_gs ++ gs,
|
||||
return ()
|
||||
|
||||
meta def bottom_up (c : conv unit) : conv unit :=
|
||||
λ r e, do
|
||||
s ← simp_lemmas.mk_default,
|
||||
(a, new_e, pr) ←
|
||||
ext_simplify_core () {} s
|
||||
(λ u, return u)
|
||||
(λ a s r p e, failed)
|
||||
(λ a s r p e, do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, tt))
|
||||
r e,
|
||||
return ⟨(), new_e, some pr⟩
|
||||
|
||||
meta def top_down (c : conv unit) : conv unit :=
|
||||
λ r e, do
|
||||
s ← simp_lemmas.mk_default,
|
||||
(a, new_e, pr) ←
|
||||
ext_simplify_core () {} s
|
||||
(λ u, return u)
|
||||
(λ a s r p e, do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, tt))
|
||||
(λ a s r p e, failed)
|
||||
r e,
|
||||
return ⟨(), new_e, some pr⟩
|
||||
|
||||
meta def find (c : conv unit) : conv unit :=
|
||||
λ r e, do
|
||||
s ← simp_lemmas.mk_default,
|
||||
(a, new_e, pr) ←
|
||||
ext_simplify_core () {} s
|
||||
(λ u, return u)
|
||||
(λ a s r p e,
|
||||
(do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, ff))
|
||||
<|>
|
||||
return ((), e, none, tt))
|
||||
(λ a s r p e, failed)
|
||||
r e,
|
||||
return ⟨(), new_e, some pr⟩
|
||||
|
||||
meta def find_pattern (pat : pattern) (c : conv unit) : conv unit :=
|
||||
λ r e, do
|
||||
s ← simp_lemmas.mk_default,
|
||||
(a, new_e, pr) ←
|
||||
ext_simplify_core () {} s
|
||||
(λ u, return u)
|
||||
(λ a s r p e, do
|
||||
matched ← (tactic.match_pattern pat e >> return tt) <|> return ff,
|
||||
if matched
|
||||
then do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, ff)
|
||||
else return ((), e, none, tt))
|
||||
(λ a s r p e, failed)
|
||||
r e,
|
||||
return ⟨(), new_e, some pr⟩
|
||||
|
||||
meta def findp : pexpr → conv unit → conv unit :=
|
||||
λ p c r e, do
|
||||
pat ← pexpr_to_pattern p,
|
||||
find_pattern pat c r e
|
||||
|
||||
meta def conversion (c : conv unit) : tactic unit :=
|
||||
do (r, lhs, rhs) ← (target_lhs_rhs <|> fail "conversion failed, target is not of the form 'lhs R rhs'"),
|
||||
(new_lhs, pr) ← to_tactic c r lhs,
|
||||
(unify new_lhs rhs <|>
|
||||
do new_lhs_fmt ← pp new_lhs,
|
||||
rhs_fmt ← pp rhs,
|
||||
fail (to_fmt "conversion failed, expected" ++
|
||||
rhs_fmt.indent 4 ++ format.line ++ "provided" ++
|
||||
new_lhs_fmt.indent 4)),
|
||||
exact pr
|
||||
meta def funext : conv unit :=
|
||||
repeat $ do
|
||||
(r, lhs, rhs) ← target_lhs_rhs,
|
||||
guard (r = `eq),
|
||||
(expr.lam n _ _ _) ← return lhs,
|
||||
tactic.applyc `funext,
|
||||
intro n,
|
||||
return ()
|
||||
|
||||
end conv
|
||||
|
|
|
|||
|
|
@ -10,20 +10,17 @@ import init.meta.interactive init.meta.converter.conv
|
|||
|
||||
namespace conv
|
||||
meta def save_info (p : pos) : conv unit :=
|
||||
λ r lhs, do
|
||||
ts ← tactic.read,
|
||||
-- TODO(Leo): include context
|
||||
tactic.save_info_thunk p (λ _, ts.format_expr lhs) >>
|
||||
return ⟨(), lhs, none⟩
|
||||
do s ← tactic.read,
|
||||
tactic.save_info_thunk p (λ _, s.to_format tt)
|
||||
|
||||
meta def step {α : Type} (c : conv α) : conv unit :=
|
||||
c >> return ()
|
||||
|
||||
meta def istep {α : Type} (line0 col0 line col : nat) (c : conv α) : conv unit :=
|
||||
λ r lhs ts, (@scope_trace _ line col (λ _, (c >> return ()) r lhs ts)).clamp_pos line0 line col
|
||||
tactic.istep line0 col0 line col c
|
||||
|
||||
meta def execute (c : conv unit) : tactic unit :=
|
||||
conversion c
|
||||
c
|
||||
|
||||
namespace interactive
|
||||
open lean.parser
|
||||
|
|
@ -33,52 +30,104 @@ open interactive.types
|
|||
meta def itactic : Type :=
|
||||
conv unit
|
||||
|
||||
meta def skip : conv unit :=
|
||||
conv.skip
|
||||
|
||||
meta def whnf : conv unit :=
|
||||
conv.whnf
|
||||
|
||||
meta def dsimp : conv unit :=
|
||||
conv.dsimp
|
||||
|
||||
meta def trace_state : conv unit :=
|
||||
conv.trace_lhs
|
||||
meta def trace_lhs : conv unit :=
|
||||
lhs >>= tactic.trace
|
||||
|
||||
meta def change (p : parse texpr) : conv unit :=
|
||||
conv.change p
|
||||
tactic.i_to_expr p >>= conv.change
|
||||
|
||||
meta def congr : conv unit :=
|
||||
conv.congr
|
||||
|
||||
meta def funext : conv unit :=
|
||||
conv.funext
|
||||
|
||||
private meta def is_relation : conv unit :=
|
||||
(lhs >>= tactic.relation_lhs_rhs >> return ())
|
||||
<|>
|
||||
tactic.fail "current expression is not a relation"
|
||||
|
||||
meta def to_lhs : conv unit :=
|
||||
is_relation >> congr >> tactic.swap >> skip
|
||||
|
||||
meta def to_rhs : conv unit :=
|
||||
is_relation >> congr >> skip
|
||||
|
||||
meta def done : conv unit :=
|
||||
tactic.done
|
||||
|
||||
meta def find (p : parse qexpr) (c : itactic) : conv unit :=
|
||||
λ r lhs, do
|
||||
pat ← tactic.pexpr_to_pattern p,
|
||||
s ← simp_lemmas.mk_default, -- to be able to use congruence lemmas @[congr]
|
||||
(found, new_lhs, pr) ←
|
||||
tactic.ext_simplify_core ff {zeta := ff, beta := ff, single_pass := tt, eta := ff, proj := ff} s
|
||||
do (r, lhs, _) ← tactic.target_lhs_rhs,
|
||||
pat ← tactic.pexpr_to_pattern p,
|
||||
s ← simp_lemmas.mk_default, -- to be able to use congruence lemmas @[congr]
|
||||
(found, new_lhs, pr) ←
|
||||
tactic.ext_simplify_core ff {zeta := ff, beta := ff, single_pass := tt, eta := ff,
|
||||
proj := ff, fail_if_unchaged := ff} s
|
||||
(λ u, return u)
|
||||
(λ found s r p e, do
|
||||
guard (not found),
|
||||
matched ← (tactic.match_pattern_core reducible pat e >> return tt) <|> return ff,
|
||||
guard matched,
|
||||
⟨u, new_e, pr⟩ ← c r e,
|
||||
⟨new_e, pr⟩ ← c.convert e r,
|
||||
return (tt, new_e, pr, ff))
|
||||
(λ a s r p e, tactic.failed)
|
||||
r lhs,
|
||||
if not found then tactic.fail "find converter failed, pattern was not found"
|
||||
else return ⟨(), new_lhs, some pr⟩
|
||||
when (not found) $ tactic.fail "find converter failed, pattern was not found",
|
||||
update_lhs new_lhs pr
|
||||
|
||||
meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
|
||||
(ids : parse without_ident_list) (cfg : tactic.simp_config := {}) : conv unit :=
|
||||
do s ← tactic.mk_simp_set no_dflt attr_names hs ids,
|
||||
(r, lhs, rhs) ← tactic.target_lhs_rhs,
|
||||
(new_lhs, pr) ← tactic.simplify_core cfg s r lhs,
|
||||
update_lhs new_lhs pr,
|
||||
return ()
|
||||
|
||||
end interactive
|
||||
end conv
|
||||
|
||||
namespace tactic
|
||||
namespace interactive
|
||||
open lean
|
||||
open lean.parser
|
||||
open interactive
|
||||
open interactive.types
|
||||
open tactic
|
||||
local postfix `?`:9001 := optional
|
||||
|
||||
meta def conv (c : conv.interactive.itactic) : tactic unit :=
|
||||
private meta def conv_at (h_name : name) (c : conv unit) : tactic unit :=
|
||||
do h ← get_local h_name,
|
||||
h_type ← infer_type h,
|
||||
(new_h_type, pr) ← c.convert h_type,
|
||||
replace_hyp h new_h_type pr,
|
||||
return ()
|
||||
|
||||
private meta def conv_target (c : conv unit) : tactic unit :=
|
||||
do t ← target,
|
||||
(new_t, pr) ← c.to_tactic `eq t,
|
||||
(new_t, pr) ← c.convert t,
|
||||
replace_target new_t pr
|
||||
|
||||
meta def find (p : parse qexpr) (c : conv.interactive.itactic) : tactic unit :=
|
||||
conv $ conv.interactive.find p c
|
||||
meta def conv (loc : parse (tk "at" *> ident)?)
|
||||
(p : parse (tk "in" *> qexpr)?)
|
||||
(c : conv.interactive.itactic) : tactic unit :=
|
||||
do let c :=
|
||||
match p with
|
||||
| some p := _root_.conv.interactive.find p c
|
||||
| none := c
|
||||
end,
|
||||
match loc with
|
||||
| some h := conv_at h c
|
||||
| none := conv_target c
|
||||
end
|
||||
|
||||
end interactive
|
||||
end tactic
|
||||
|
|
|
|||
|
|
@ -17,7 +17,13 @@ namespace tactic_state
|
|||
/-- Create a tactic state with an empty local context and a dummy goal. -/
|
||||
meta constant mk_empty : environment → options → tactic_state
|
||||
meta constant env : tactic_state → environment
|
||||
meta constant to_format : tactic_state → format
|
||||
/-- Format the given tactic state. If `target_lhs_only` is true and the target
|
||||
is of the form `lhs ~ rhs`, where `~` is a simplification relation,
|
||||
then only the `lhs` is displayed.
|
||||
|
||||
Remark: the parameter `target_lhs_only` is a temporary hack used to implement
|
||||
the `conv` monad. It will be removed in the future. -/
|
||||
meta constant to_format (s : tactic_state) (target_lhs_only : bool := ff) : format
|
||||
/-- Format expression with respect to the main goal in the tactic state.
|
||||
If the tactic state does not contain any goals, then format expression
|
||||
using an empty local context. -/
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ Author: Leonardo de Moura
|
|||
#include "library/vm/interaction_state_imp.h"
|
||||
#include "library/compiler/vm_compiler.h"
|
||||
#include "library/tactic/tactic_state.h"
|
||||
#include "library/tactic/simp_lemmas.h"
|
||||
|
||||
namespace lean {
|
||||
/* is_ts_safe is required by the interaction_state implementation. */
|
||||
|
|
@ -161,7 +162,7 @@ format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) con
|
|||
return fmt(e);
|
||||
}
|
||||
|
||||
format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g) const {
|
||||
format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g, bool target_lhs_only) const {
|
||||
options opts = get_options().update_if_undef(get_pp_purify_locals_name(), false);
|
||||
bool inst_mvars = get_pp_instantiate_mvars(opts);
|
||||
metavar_decl decl = mctx().get_metavar_decl(g);
|
||||
|
|
@ -176,30 +177,35 @@ format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g) con
|
|||
bool unicode = get_pp_unicode(get_options());
|
||||
if (!lctx.empty())
|
||||
r += line();
|
||||
format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
|
||||
expr type = decl.get_type();
|
||||
if (inst_mvars)
|
||||
type = mctx_tmp.instantiate_mvars(type);
|
||||
r += turnstile + space() + nest(indent, fmt(type));
|
||||
expr rel, lhs, rhs;
|
||||
if (target_lhs_only && is_simp_relation(env(), type, rel, lhs, rhs)) {
|
||||
r += format("|") + space() + nest(indent, fmt(lhs));
|
||||
} else {
|
||||
format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
|
||||
r += turnstile + space() + nest(indent, fmt(type));
|
||||
}
|
||||
if (get_pp_goal_compact(get_options()))
|
||||
r = group(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
format tactic_state::pp_core(formatter_factory const & fmtf) const {
|
||||
format tactic_state::pp_core(formatter_factory const & fmtf, bool target_lhs_only) const {
|
||||
format r;
|
||||
bool first = true;
|
||||
for (auto const & g : goals()) {
|
||||
if (first) first = false; else r += line() + line();
|
||||
r += pp_goal(fmtf, g);
|
||||
r += pp_goal(fmtf, g, target_lhs_only);
|
||||
}
|
||||
if (first) r = format("no goals");
|
||||
return r;
|
||||
}
|
||||
|
||||
format tactic_state::pp_core() const {
|
||||
format tactic_state::pp_core(bool target_lhs_only) const {
|
||||
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
|
||||
return pp_core(fmtf);
|
||||
return pp_core(fmtf, target_lhs_only);
|
||||
}
|
||||
|
||||
format tactic_state::pp_expr(expr const & e) const {
|
||||
|
|
@ -235,8 +241,8 @@ vm_obj tactic_state_env(vm_obj const & s) {
|
|||
return to_obj(tactic::to_state(s).env());
|
||||
}
|
||||
|
||||
vm_obj tactic_state_to_format(vm_obj const & s) {
|
||||
return to_obj(tactic::to_state(s).pp_core());
|
||||
vm_obj tactic_state_to_format(vm_obj const & s, vm_obj const & target_lhs_only) {
|
||||
return to_obj(tactic::to_state(s).pp_core(to_bool(target_lhs_only)));
|
||||
}
|
||||
|
||||
format pp_expr(tactic_state const & s, expr const & e) {
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ private:
|
|||
friend class optional<tactic_state>;
|
||||
tactic_state():m_ptr(nullptr) {}
|
||||
explicit tactic_state(tactic_state_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
format pp_goal(formatter_factory const & fmtf, expr const & g) const;
|
||||
format pp_goal(formatter_factory const & fmtf, expr const & g, bool target_lhs_only = false) const;
|
||||
public:
|
||||
tactic_state(environment const & env, options const & o, name const & decl_name,
|
||||
metavar_context const & ctx, list<expr> const & gs,
|
||||
|
|
@ -85,9 +85,9 @@ public:
|
|||
friend void swap(tactic_state & a, tactic_state & b) { std::swap(a.m_ptr, b.m_ptr); }
|
||||
friend bool is_eqp(tactic_state const & a, tactic_state const & b) { return a.m_ptr == b.m_ptr; }
|
||||
|
||||
format pp_core(formatter_factory const & fmtf) const;
|
||||
format pp_core(formatter_factory const & fmtf, bool target_lhs_only = false) const;
|
||||
format pp_expr(formatter_factory const & fmtf, expr const & e) const;
|
||||
format pp_core() const;
|
||||
format pp_core(bool target_lhs_only = false) const;
|
||||
format pp() const;
|
||||
format pp_expr(expr const & e) const;
|
||||
format pp_goal(expr const & g) const;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":5,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"}
|
||||
{"message":"file invalidated","response":"ok","seq_num":0}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff} → tactic unit"},"response":"ok","seq_num":6}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff} → tactic unit"},"response":"ok","seq_num":8}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff} → tactic unit"},"response":"ok","seq_num":10}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff} → tactic unit"},"response":"ok","seq_num":12}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"state":"⊢ false","tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchaged := tt} → tactic unit"},"response":"ok","seq_num":6}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":0,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchaged := tt} → tactic unit"},"response":"ok","seq_num":8}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":1,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchaged := tt} → tactic unit"},"response":"ok","seq_num":10}
|
||||
{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.\n\n- `simp at *` simplifies all the hypotheses and the goal.\n\n- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.","source":,"tactic_param_idx":2,"tactic_params":["only?","[expr, ...]?","(with id*)?","(without id*)?","(at (* | id*))?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.only_flag → interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, single_pass := ff, fail_if_unchaged := tt} → tactic unit"},"response":"ok","seq_num":12}
|
||||
{"record":{"full-id":"tactic.get_env","source":,"tactic_params":[],"type":"tactic environment"},"response":"ok","seq_num":14}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
example (a b : nat) : (λ x, a + x) 0 = b + 1 + a :=
|
||||
begin
|
||||
find (_ + 1) { change nat.succ b },
|
||||
conv in (_ + 1) { change nat.succ b },
|
||||
guard_target (λ x, a + x) 0 = nat.succ b + a,
|
||||
admit
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,68 +0,0 @@
|
|||
open tactic conv
|
||||
open tactic
|
||||
|
||||
run_cmd mk_simp_attr `foo
|
||||
run_cmd mk_simp_attr `bla
|
||||
|
||||
constant f : nat → nat → nat
|
||||
@[foo] lemma f_lemma : ∀ x, f x x = 0 :=
|
||||
sorry
|
||||
|
||||
constant g : nat → nat
|
||||
@[bla] lemma g_lemma : ∀ x, g x = x :=
|
||||
sorry
|
||||
|
||||
example (a b c : nat) : (λ x, g (f (a + 0) (sizeof x))) a = 0 :=
|
||||
by conversion $
|
||||
whnf >>
|
||||
trace_lhs >>
|
||||
apply_simp_set `bla >>
|
||||
dsimp >>
|
||||
trace "after defeq simplifier" >>
|
||||
trace_lhs >>
|
||||
change ```(f a a) >>
|
||||
trace_lhs >>
|
||||
apply_simp_set `foo >>
|
||||
trace_lhs
|
||||
|
||||
set_option trace.app_builder true
|
||||
|
||||
@[simp] lemma sizeof_nat_eq (n : ℕ) : sizeof n = n := rfl
|
||||
|
||||
example (a b c : nat) : (λ x, g (f x (sizeof x))) = (λ x, 0) :=
|
||||
by conversion $
|
||||
funext $ do
|
||||
trace_lhs,
|
||||
apply_simp_set `bla,
|
||||
dsimp,
|
||||
apply_simp_set `foo
|
||||
|
||||
constant h : nat → nat → nat
|
||||
|
||||
lemma ex (a : nat) : (λ a, h (f a (sizeof a)) (g a)) = (λ a, h 0 a) :=
|
||||
by conversion $
|
||||
bottom_up $
|
||||
(apply_simp_set `foo <|> apply_simp_set `bla <|> dsimp)
|
||||
|
||||
lemma ex2 {A : Type} [comm_group A] (a b : A) : b * 1 * a = a * b :=
|
||||
by conversion $
|
||||
bottom_up (apply_simp_set `default)
|
||||
|
||||
lemma ex3 (p q r : Prop) : (p ∧ true ∧ p) = p :=
|
||||
by conversion $
|
||||
bottom_up (apply_propext_simp_set `default)
|
||||
|
||||
#print "---------"
|
||||
|
||||
lemma ex4 (a b c : nat) : g (g (g (f (f (g (g a)) (g (g a))) a))) = g (g (g (f (f a a) a))) :=
|
||||
by conversion $
|
||||
findp ```(λ x, f (g x) (g x)) $
|
||||
trace "found pattern" >> trace_lhs >>
|
||||
bottom_up (apply_simp_set `bla)
|
||||
|
||||
lemma ex5 (a b c : nat) : g (g (g (f (f (g (g a)) (g (g a))) a))) = g (g (g (f (f a a) a))) :=
|
||||
by conversion $
|
||||
find $
|
||||
match_expr ```(λ x, f (g x) (g x)) >>
|
||||
trace "found pattern" >> trace_lhs >>
|
||||
bottom_up (apply_simp_set `bla)
|
||||
Loading…
Add table
Reference in a new issue