feat(library/init/meta/transfer): add transfer and use for int
This commit introduces the transfer method. As application it is used it to prove that the integers form a commutative ring.
This commit is contained in:
Johannes Hölzl
Leonardo de Moura
parent
ca0fe37c41
commit
1f45995c16
2 changed files with 176 additions and 121 deletions
|
|
@ -6,7 +6,7 @@ Authors: Jeremy Avigad
|
|||
The integers, with addition, multiplication, and subtraction.
|
||||
-/
|
||||
prelude
|
||||
import init.data.nat.lemmas init.relator
|
||||
import init.data.nat.lemmas init.meta.transfer
|
||||
open nat
|
||||
|
||||
/- the type, coercions, and notation -/
|
||||
|
|
@ -299,132 +299,28 @@ protected lemma rel_mul : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_
|
|||
int is a ring
|
||||
-/
|
||||
|
||||
/- addition -/
|
||||
|
||||
protected lemma add_comm (a b : ℤ) : a + b = b + a :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
cases (int.left_total_rel_int_nat_nat b) with b' hb,
|
||||
apply (int.rel_eq (int.rel_add ha hb) (int.rel_add hb ha))^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma add_zero (a : ℤ) : a + 0 = a :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
apply (int.rel_eq (int.rel_add ha int.rel_zero) ha)^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma zero_add (a : ℤ) : 0 + a = a :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
apply (int.rel_eq (int.rel_add int.rel_zero ha) ha)^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma add_assoc (a b c : ℤ) : a + b + c = a + (b + c) :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
cases (int.left_total_rel_int_nat_nat b) with b' hb,
|
||||
cases (int.left_total_rel_int_nat_nat c) with c' hc,
|
||||
apply (int.rel_eq (int.rel_add (int.rel_add ha hb) hc) (int.rel_add ha (int.rel_add hb hc)))^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
/- negation -/
|
||||
|
||||
protected lemma add_left_neg (a : ℤ) : -a + a = 0 :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
apply (int.rel_eq (int.rel_add (int.rel_neg ha) ha) int.rel_zero)^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
/- multiplication -/
|
||||
|
||||
protected lemma mul_comm (a b : ℤ) : a * b = b * a :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
cases (int.left_total_rel_int_nat_nat b) with b' hb,
|
||||
apply (int.rel_eq (int.rel_mul ha hb) (int.rel_mul hb ha))^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma mul_assoc (a b c : ℤ) : a * b * c = a * (b * c) :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
cases (int.left_total_rel_int_nat_nat b) with b' hb,
|
||||
cases (int.left_total_rel_int_nat_nat c) with c' hc,
|
||||
apply (int.rel_eq (int.rel_mul (int.rel_mul ha hb) hc) (int.rel_mul ha (int.rel_mul hb hc)))^.mpr,
|
||||
simp [mul_add, add_mul]
|
||||
end
|
||||
|
||||
protected lemma mul_one (a : ℤ) : a * 1 = a :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
apply (int.rel_eq (int.rel_mul ha int.rel_one) ha)^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma one_mul (a : ℤ) : 1 * a = a :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
apply (int.rel_eq (int.rel_mul int.rel_one ha) ha)^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma mul_zero (a : ℤ) : a * 0 = 0 :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
apply (int.rel_eq (int.rel_mul ha int.rel_zero) int.rel_zero)^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma zero_mul (a : ℤ) : 0 * a = 0 :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
apply (int.rel_eq (int.rel_mul int.rel_zero ha) int.rel_zero)^.mpr,
|
||||
simp
|
||||
end
|
||||
|
||||
protected lemma distrib_left (a b c : ℤ) : a * (b + c) = a * b + a * c :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
cases (int.left_total_rel_int_nat_nat b) with b' hb,
|
||||
cases (int.left_total_rel_int_nat_nat c) with c' hc,
|
||||
apply (int.rel_eq (int.rel_mul ha (int.rel_add hb hc))
|
||||
(int.rel_add (int.rel_mul ha hb) (int.rel_mul ha hc)))^.mpr,
|
||||
simp [mul_add, add_mul]
|
||||
end
|
||||
|
||||
protected lemma distrib_right (a b c : ℤ) : (a + b) * c = a * c + b * c :=
|
||||
begin
|
||||
cases (int.left_total_rel_int_nat_nat a) with a' ha,
|
||||
cases (int.left_total_rel_int_nat_nat b) with b' hb,
|
||||
cases (int.left_total_rel_int_nat_nat c) with c' hc,
|
||||
apply (int.rel_eq (int.rel_mul (int.rel_add ha hb) hc)
|
||||
(int.rel_add (int.rel_mul ha hc) (int.rel_mul hb hc)))^.mpr,
|
||||
simp [mul_add, add_mul]
|
||||
end
|
||||
protected meta def transfer : tactic unit := do
|
||||
transfer.transfer [`relator.rel_forall_of_total, `relator.rel_not,
|
||||
`int.rel_eq, `int.rel_zero, `int.rel_one,
|
||||
`int.rel_add, `int.rel_neg, `int.rel_mul]
|
||||
|
||||
instance : comm_ring int :=
|
||||
{ add := int.add,
|
||||
add_assoc := int.add_assoc,
|
||||
add_assoc := begin int.transfer, simp, intros, trivial end,
|
||||
zero := int.zero,
|
||||
zero_add := int.zero_add,
|
||||
add_zero := int.add_zero,
|
||||
zero_add := begin int.transfer, simp, intros, trivial end,
|
||||
add_zero := begin int.transfer, simp, intros, trivial end,
|
||||
neg := int.neg,
|
||||
add_left_neg := int.add_left_neg,
|
||||
add_comm := int.add_comm,
|
||||
add_left_neg := begin int.transfer, simp, intros, trivial end,
|
||||
add_comm := begin int.transfer, simp, intros, trivial end,
|
||||
mul := int.mul,
|
||||
mul_assoc := int.mul_assoc,
|
||||
mul_assoc := begin int.transfer, simp [add_mul, mul_add], intros, trivial end,
|
||||
one := int.one,
|
||||
one_mul := int.one_mul,
|
||||
mul_one := int.mul_one,
|
||||
left_distrib := int.distrib_left,
|
||||
right_distrib := int.distrib_right,
|
||||
mul_comm := int.mul_comm }
|
||||
one_mul := begin int.transfer, simp, intros, trivial end,
|
||||
mul_one := begin int.transfer, simp, intros, trivial end,
|
||||
left_distrib := begin int.transfer, simp [add_mul, mul_add], intros, trivial end,
|
||||
right_distrib := begin int.transfer, simp [add_mul, mul_add], intros, trivial end,
|
||||
mul_comm := begin int.transfer, simp, intros, trivial end }
|
||||
|
||||
/- Extra instances to short-circuit type class resolution -/
|
||||
instance : has_sub int := by apply_instance
|
||||
|
|
@ -443,7 +339,7 @@ instance : distrib int := by apply_instance
|
|||
|
||||
protected lemma zero_ne_one : (0 : int) ≠ 1 :=
|
||||
begin
|
||||
apply (relator.rel_not (int.rel_eq int.rel_zero int.rel_one))^.mpr,
|
||||
int.transfer,
|
||||
apply nat.zero_ne_one
|
||||
end
|
||||
|
||||
|
|
|
|||
159
library/init/meta/transfer.lean
Normal file
159
library/init/meta/transfer.lean
Normal file
|
|
@ -0,0 +1,159 @@
|
|||
/-
|
||||
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Johannes Hölzl (CMU)
|
||||
-/
|
||||
prelude
|
||||
import init.meta.tactic init.meta.match_tactic init.relator init.meta.mk_dec_eq_instance
|
||||
|
||||
namespace transfer
|
||||
open tactic expr list monad
|
||||
|
||||
-- FIXME: add trace statements
|
||||
|
||||
private meta structure rel_data :=
|
||||
(in_type : expr)
|
||||
(out_type : expr)
|
||||
(relation : expr)
|
||||
|
||||
meta instance has_to_tactic_format_rel_data : has_to_tactic_format rel_data :=
|
||||
⟨λr, do
|
||||
R ← pp r^.relation,
|
||||
α ← pp r^.in_type,
|
||||
β ← pp r^.out_type,
|
||||
return $ to_fmt "(" ++ R ++ ": rel (" ++ α ++ ") (" ++ β ++ "))" ⟩
|
||||
|
||||
private meta structure rule_data :=
|
||||
(pr : expr)
|
||||
(uparams : list name) -- levels not in pat
|
||||
(params : list (expr × bool)) -- fst : local constant, snd = tt → param appears in pattern
|
||||
(uargs : list name) -- levels not in pat
|
||||
(args : list (expr × rel_data)) -- fst : local constant
|
||||
(pat : pattern) -- `R c`
|
||||
(out : expr) -- right-hand side `d` of rel equation `R c d`
|
||||
|
||||
meta instance has_to_tactic_format_rule_data : has_to_tactic_format rule_data :=
|
||||
⟨λr, do
|
||||
pr ← pp r^.pr,
|
||||
up ← pp r^.uparams,
|
||||
mp ← pp r^.params,
|
||||
ua ← pp r^.uargs,
|
||||
ma ← pp r^.args,
|
||||
pat ← pp r^.pat^.target,
|
||||
out ← pp r^.out,
|
||||
return $ to_fmt "{ ⟨" ++ pat ++ "⟩ pr: " ++ pr ++ " → " ++ out ++ ", " ++ up ++ " " ++ mp ++ " " ++ ua ++ " " ++ ma ++ " }" ⟩
|
||||
|
||||
private meta def get_lift_fun : expr → tactic (list rel_data × expr)
|
||||
| e :=
|
||||
do {
|
||||
guardb (is_constant_of (get_app_fn e) `relator.lift_fun),
|
||||
[α, β, γ, δ, R, S] ← return $ get_app_args e,
|
||||
(ps, r) ← get_lift_fun S,
|
||||
return (rel_data.mk α β R :: ps, r)} <|>
|
||||
return ([], e)
|
||||
|
||||
private meta def mark_occurences (e : expr) : list expr → list (expr × bool)
|
||||
| [] := []
|
||||
| (h :: t) := let xs := mark_occurences t in
|
||||
(h, occurs h e || any xs (λ⟨e, oc⟩, oc && occurs h e)) :: xs
|
||||
|
||||
private meta def analyse_rule (pr : expr) : tactic rule_data := do
|
||||
-- FIXME(johoelzl): take care of eta contracted terms
|
||||
t ← infer_type pr,
|
||||
(params, app (app r f) g) ← mk_local_pis t,
|
||||
(arg_rels, R) ← get_lift_fun r,
|
||||
args ← monad.for (enum arg_rels) (λ⟨n, a⟩,
|
||||
prod.mk <$> mk_local_def (mk_simple_name ("a_" ++ to_string n)) a^.in_type <*> pure a),
|
||||
a_vars ← return $ fmap prod.fst args,
|
||||
p ← head_beta (app_of_list f a_vars),
|
||||
p_data ← return $ mark_occurences (app R p) params,
|
||||
p_vars ← return $ list.map prod.fst (list.filter (λx, ↑x.2) p_data),
|
||||
u' ← return $ collect_univ_params t,
|
||||
u ← return $ collect_univ_params (app R p),
|
||||
pat ← mk_pattern (fmap level.param u) (p_vars ++ a_vars) (app R p) (fmap level.param u) (p_vars ++ a_vars),
|
||||
return $ rule_data.mk pr (list.remove_all u' u) p_data u args pat g
|
||||
|
||||
private meta def analyse_decls : list name → tactic (list rule_data) :=
|
||||
monad.mapm (λn, do
|
||||
d ← get_decl n,
|
||||
c ← return d^.univ_params^.length,
|
||||
l ← monad.for (range c) (λ_, level.param <$> mk_fresh_name),
|
||||
analyse_rule (const n l))
|
||||
|
||||
private meta def split_params_args : list (expr × bool) → list expr → list (expr × option expr) × list expr
|
||||
| ((lc, tt) :: ps) (e :: es) := let (ps', es') := split_params_args ps es in ((lc, some e) :: ps', es')
|
||||
| ((lc, ff) :: ps) es := let (ps', es') := split_params_args ps es in ((lc, none) :: ps', es')
|
||||
| _ es := ([], es)
|
||||
|
||||
private meta def param_substitutions (ctxt : list expr) :
|
||||
list (expr × option expr) → tactic (list (name × expr) × list expr)
|
||||
| (((local_const n _ bi t), s) :: ps) := do
|
||||
(e, m) ← match s with
|
||||
| (some e) := return (e, [])
|
||||
| none :=
|
||||
let ctxt' := list.filter (λv, occurs v t) ctxt in
|
||||
let ty := pis ctxt' t in
|
||||
if bi = binder_info.inst_implicit then do
|
||||
guard (bi = binder_info.inst_implicit),
|
||||
ty ← instantiate_mvars ty,
|
||||
e ← mk_instance ty,
|
||||
return (e, [])
|
||||
else do
|
||||
mv ← mk_meta_var ty,
|
||||
return (app_of_list mv ctxt', [mv])
|
||||
end,
|
||||
sb ← return $ instantiate_local n e,
|
||||
ps ← return $ fmap (prod.map sb (fmap sb)) ps,
|
||||
(ms, vs) ← param_substitutions ps,
|
||||
return ((n, e) :: ms, m ++ vs)
|
||||
| _ := return ([], [])
|
||||
|
||||
/- input expression a type `R a`, it finds a type `b`, s.t. there is a proof of the type `R a b`.
|
||||
It return (`a`, pr : `R a b`) -/
|
||||
meta def compute_transfer : list rule_data → list expr → expr → tactic (expr × expr × list expr)
|
||||
| rds ctxt e := do
|
||||
-- Select matching rule
|
||||
(i, ps, args, ms, rd) ← first (rds^.for (λrd, do
|
||||
(l, m) ← match_pattern_core semireducible rd^.pat e,
|
||||
level_map ← monad.for rd^.uparams (λl, prod.mk l <$> mk_meta_univ),
|
||||
inst_univ ← return $ (λe, instantiate_univ_params e (level_map ++ zip rd^.uargs l)),
|
||||
(ps, args) ← return $ split_params_args (list.map (prod.map inst_univ id) rd^.params) m,
|
||||
(ps, ms) ← param_substitutions ctxt ps, /- checks type class parameters -/
|
||||
return (instantiate_locals ps ∘ inst_univ, ps, args, ms, rd))),
|
||||
|
||||
(bs, hs, mss) ← monad.for (zip rd^.args args) (λ⟨⟨_, d⟩, e⟩, do
|
||||
-- Argument has function type
|
||||
(args, r) ← get_lift_fun (i d^.relation),
|
||||
((a_vars, b_vars), (R_vars, bnds)) ← monad.for (enum args) (λ⟨n, arg⟩, do
|
||||
a ← mk_local_def (("a" ++ to_string n) : string) arg^.in_type,
|
||||
b ← mk_local_def (("b" ++ to_string n) : string) arg^.out_type,
|
||||
R ← mk_local_def (("R" ++ to_string n) : string) (arg^.relation a b),
|
||||
return ((a, b), (R, [a, b, R]))) >>= (return ∘ prod.map unzip unzip ∘ unzip),
|
||||
rds' ← monad.for R_vars analyse_rule,
|
||||
|
||||
-- Transfer argument
|
||||
a ← return $ i e,
|
||||
a' ← head_beta (app_of_list a a_vars),
|
||||
(b, pr, ms) ← compute_transfer (rds ++ rds') (ctxt ++ a_vars) (app r a'),
|
||||
b' ← head_eta (lambdas b_vars b),
|
||||
return (b', [a, b', lambdas (list.join bnds) pr], ms)) >>= (return ∘ prod.map id unzip ∘ unzip),
|
||||
|
||||
-- Combine
|
||||
b ← head_beta (app_of_list (i rd^.out) bs),
|
||||
pr ← return $ app_of_list (i rd^.pr) (fmap prod.snd ps ++ list.join hs),
|
||||
return (b, pr, ms ++ list.join mss)
|
||||
|
||||
meta def transfer (ds : list name) : tactic unit := do
|
||||
rds ← analyse_decls ds,
|
||||
tgt ← target,
|
||||
|
||||
(new_tgt, pr, ms) ← compute_transfer rds [] (const `iff [] tgt),
|
||||
new_pr ← mk_meta_var new_tgt,
|
||||
|
||||
/- Setup final tactic state -/
|
||||
exact (const `iff.mpr [] tgt new_tgt pr new_pr),
|
||||
ms ← monad.for ms (λm, (get_assignment m >> return []) <|> return [m]),
|
||||
gs ← get_goals,
|
||||
set_goals (list.join ms ++ new_pr :: gs)
|
||||
|
||||
end transfer
|
||||
Loading…
Add table
Reference in a new issue