From b0e49535fa1a182cd25cf3be96e26f593ef4ef90 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Apr 2018 13:38:18 -0700 Subject: [PATCH] chore(*): remove transfer and coinductive predicates --- library/init/data/int/basic.lean | 4 +- library/init/meta/coinductive_predicates.lean | 622 ------------------ library/init/meta/default.lean | 4 +- library/init/meta/transfer.lean | 187 ------ library/init/relator.lean | 84 --- 5 files changed, 2 insertions(+), 899 deletions(-) delete mode 100644 library/init/meta/coinductive_predicates.lean delete mode 100644 library/init/meta/transfer.lean delete mode 100644 library/init/relator.lean diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index fbf58f8f8d..4720bf3d0c 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad The integers, with addition, multiplication, and subtraction. -/ prelude -import init.data.nat.gcd init.meta.transfer init.data.list +import init.data.nat.gcd init.data.list open nat /- the type, coercions, and notation -/ @@ -40,8 +40,6 @@ protected def one : int := of_nat 1 instance : has_zero int := ⟨int.zero⟩ instance : has_one int := ⟨int.one⟩ -/- definitions of basic functions -/ - def neg_of_nat : ℕ → int | 0 := 0 | (succ m) := -[1+ m] diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean deleted file mode 100644 index ac75a6beb7..0000000000 --- a/library/init/meta/coinductive_predicates.lean +++ /dev/null @@ -1,622 +0,0 @@ -/- -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.expr init.meta.tactic init.meta.constructor_tactic init.meta.attribute -import init.meta.interactive - -namespace name - -def last_string : name → string -| anonymous := "[anonymous]" -| (mk_string s _) := s -| (mk_numeral _ n) := last_string n - -end name - -namespace expr -open expr - -meta def replace_with (e : expr) (s : expr) (s' : expr) : expr := -e.replace $ λc d, if c = s then some (s'.lift_vars 0 d) else none - -meta def local_binder_info : expr → binder_info -| (local_const x n bi t) := bi -| e := binder_info.default - -meta def to_implicit_binder : expr → expr -| (local_const n₁ n₂ _ d) := local_const n₁ n₂ binder_info.implicit d -| (lam n _ d b) := lam n binder_info.implicit d b -| (pi n _ d b) := pi n binder_info.implicit d b -| e := e - -meta def get_app_fn_args_aux : list expr → expr → expr × list expr -| r (app f a) := get_app_fn_args_aux (a::r) f -| r e := (e, r) - -meta def get_app_fn_args : expr → expr × list expr := -get_app_fn_args_aux [] - -end expr - -namespace tactic -open level expr tactic - -meta def mk_local_pisn : expr → nat → tactic (list expr × expr) -| (pi n bi d b) (c + 1) := do - p ← mk_local' n bi d, - (ps, r) ← mk_local_pisn (b.instantiate_var p) c, - return ((p :: ps), r) -| e 0 := return ([], e) -| _ _ := failed - -meta def drop_pis : list expr → expr → tactic expr -| (list.cons v vs) (pi n bi d b) := do - t ← infer_type v, - guard (t =ₐ d), - drop_pis vs (b.instantiate_var v) -| [] e := return e -| _ _ := failed - -meta def mk_theorem (n : name) (ls : list name) (t : expr) (e : expr) : declaration := -declaration.thm n ls t (task.pure e) - -meta def add_theorem_by (n : name) (ls : list name) (type : expr) (tac : tactic unit) : tactic expr := do - ((), body) ← solve_aux type tac, - body ← instantiate_mvars body, - add_decl $ mk_theorem n ls type body, - return $ const n $ ls.map param - -meta def mk_exists_lst (args : list expr) (inner : expr) : tactic expr := -args.mfoldr (λarg i:expr, do - t ← infer_type arg, - sort l ← infer_type t, - return $ if arg.occurs i ∨ l ≠ level.zero - then (const `Exists [l] : expr) t (i.lambdas [arg]) - else (const `and [] : expr) t i) - inner - -meta def mk_op_lst (op : expr) (empty : expr) : list expr → expr -| [] := empty -| [e] := e -| (e :: es) := op e $ mk_op_lst es - -meta def mk_and_lst : list expr → expr := mk_op_lst `(and) `(true) - -meta def mk_or_lst : list expr → expr := mk_op_lst `(or) `(false) - -meta def elim_gen_prod : nat → expr → list expr → tactic (list expr × expr) -| 0 e hs := return (hs, e) -| (n + 1) e hs := do - [(_, [h, h'], _)] ← induction e [], - elim_gen_prod n h' (hs ++ [h]) - -private meta def elim_gen_sum_aux : nat → expr → list expr → tactic (list expr × expr) -| 0 e hs := return (hs, e) -| (n + 1) e hs := do - [(_, [h], _), (_, [h'], _)] ← induction e [], - swap, - elim_gen_sum_aux n h' (h::hs) - -meta def elim_gen_sum (n : nat) (e : expr) : tactic (list expr) := do - (hs, h') ← elim_gen_sum_aux n e [], - gs ← get_goals, - set_goals $ (gs.take (n+1)).reverse ++ gs.drop (n+1), - return $ hs.reverse ++ [h'] - -end tactic - -section -universe u - -@[user_attribute] -meta def monotonicity : user_attribute := { name := `monotonicity, descr := "Monotonicity rules for predicates" } - -lemma monotonicity.pi {α : Sort u} {p q : α → Prop} (h : ∀a, implies (p a) (q a)) : - implies (Πa, p a) (Πa, q a) := -assume h' a, h a (h' a) - -lemma monotonicity.imp {p p' q q' : Prop} (h₁ : implies p' q') (h₂ : implies q p) : - implies (p → p') (q → q') := -assume h, h₁ ∘ h ∘ h₂ - -@[monotonicity] -lemma monotonicity.const (p : Prop) : implies p p := id - -@[monotonicity] -lemma monotonicity.true (p : Prop) : implies p true := assume _, trivial - -@[monotonicity] -lemma monotonicity.false (p : Prop) : implies false p := false.elim - -@[monotonicity] -lemma monotonicity.exists {α : Sort u} {p q : α → Prop} (h : ∀a, implies (p a) (q a)) : - implies (∃a, p a) (∃a, q a) := -exists_imp_exists h - -@[monotonicity] -lemma monotonicity.and {p p' q q' : Prop} (hp : implies p p') (hq : implies q q') : - implies (p ∧ q) (p' ∧ q') := -and.imp hp hq - -@[monotonicity] -lemma monotonicity.or {p p' q q' : Prop} (hp : implies p p') (hq : implies q q') : - implies (p ∨ q) (p' ∨ q') := -or.imp hp hq - -@[monotonicity] -lemma monotonicity.not {p q : Prop} (h : implies p q) : - implies (¬ q) (¬ p) := -mt h - -end - -namespace tactic -open expr tactic - -/- TODO: use backchaining -/ -private meta def mono_aux (ns : list name) (hs : list expr) : tactic unit := do - intros, - (do - `(implies %%p %%q) ← target, - (do is_def_eq p q, eapplyc `monotone.const) <|> - (do - (expr.pi pn pbi pd pb) ← whnf p, - (expr.pi qn qbi qd qb) ← whnf q, - sort u ← infer_type pd, - (do is_def_eq pd qd, - let p' := expr.lam pn pbi pd pb, - let q' := expr.lam qn qbi qd qb, - eapply ((const `monotonicity.pi [u] : expr) pd p' q'), - skip) <|> - (do guard $ u = level.zero ∧ is_arrow p ∧ is_arrow q, - let p' := pb.lower_vars 0 1, - let q' := qb.lower_vars 0 1, - eapply ((const `monotonicity.imp []: expr) pd p' qd q'), - skip))) <|> - first (hs.map $ λh, apply_core h {md := transparency.none, new_goals := new_goals.non_dep_only} >> skip) <|> - first (ns.map $ λn, do c ← mk_const n, apply_core c {md := transparency.none, new_goals := new_goals.non_dep_only}, skip), - all_goals mono_aux - -meta def mono (e : expr) (hs : list expr) : tactic unit := do - t ← target, - t' ← infer_type e, - ns ← attribute.get_instances `monotonicity, - ((), p) ← solve_aux `(implies %%t' %%t) (mono_aux ns hs), - exact (p e) - -end tactic - -/- -The coinductive predicate `pred`: - - coinductive {u} pred (A) : a → Prop - | r : ∀A b, pred A p - -where - `u` is a list of universe parameters - `A` is a list of global parameters - `pred` is a list predicates to be defined - `a` are the indices for each `pred` - `r` is a list of introduction rules for each `pred` - `b` is a list of parameters for each rule in `r` and `pred` - `p` is are the instances of `a` using `A` and `b` - -`pred` is compiled to the following defintions: - - inductive {u} pred.functional (A) ([pred'] : a → Prop) : a → Prop - | r : ∀a [f], b[pred/pred'] → pred.functional a [f] p - - lemma {u} pred.functional.mono (A) ([pred₁] [pred₂] : a → Prop) [(h : ∀b, pred₁ b → pred₂ b)] : - ∀p, pred.functional A pred₁ p → pred.functional A pred₂ p - - def {u} pred_i (A) (a) : Prop := - ∃[pred'], (Λi, ∀a, pred_i a → pred_i.functional A [pred] a) ∧ pred'_i a - - lemma {u} pred_i.corec_functional (A) [Λi, C_i : a_i → Prop] [Λi, h : ∀a, C_i a → pred_i.functional A C_i a] : - ∀a, C_i a → pred_i A a - - lemma {u} pred_i.destruct (A) (a) : pred A a → pred.functional A [pred A] a - - lemma {u} pred_i.construct (A) : ∀a, pred_i.functional A [pred A] a → pred_i A a - - lemma {u} pred_i.cases_on (A) (C : a → Prop) {a} (h : pred_i a) [Λi, ∀a, b → C p] → C a - - lemma {u} pred_i.corec_on (A) [(C : a → Prop)] (a) (h : C_i a) - [Λi, h_i : ∀a, C_i a → [V j ∃b, a = p]] : pred_i A a - - lemma {u} pred.r (A) (b) : pred_i A p --/ - -namespace tactic -open level expr tactic - -namespace add_coinductive_predicate - -/- private -/ meta structure coind_rule : Type := -(orig_nm : name) -(func_nm : name) -(type : expr) -(loc_type : expr) -(args : list expr) -(loc_args : list expr) -(concl : expr) -(insts : list expr) - -/- private -/ meta structure coind_pred : Type := -(u_names : list name) -(params : list expr) -(pd_name : name) -(type : expr) -(intros : list coind_rule) -(locals : list expr) -(f₁ f₂ : expr) -(u_f : level) - -namespace coind_pred - -meta def u_params (pd : coind_pred) : list level := -pd.u_names.map param - -meta def f₁_l (pd : coind_pred) : expr := -pd.f₁.app_of_list pd.locals - -meta def f₂_l (pd : coind_pred) : expr := -pd.f₂.app_of_list pd.locals - -meta def pred (pd : coind_pred) : expr := -const pd.pd_name pd.u_params - -meta def func (pd : coind_pred) : expr := -const (pd.pd_name ++ "functional") pd.u_params - -meta def func_g (pd : coind_pred) : expr := -pd.func.app_of_list $ pd.params - -meta def pred_g (pd : coind_pred) : expr := -pd.pred.app_of_list $ pd.params - -meta def impl_locals (pd : coind_pred) : list expr := -pd.locals.map to_implicit_binder - -meta def impl_params (pd : coind_pred) : list expr := -pd.params.map to_implicit_binder - -meta def le (pd : coind_pred) (f₁ f₂ : expr) : expr := -(imp (f₁.app_of_list pd.locals) (f₂.app_of_list pd.locals)).pis pd.impl_locals - -meta def corec_functional (pd : coind_pred) : expr := -const (pd.pd_name ++ "corec_functional") pd.u_params - -meta def mono (pd : coind_pred) : expr := -const (pd.func.const_name ++ "mono") pd.u_params - -meta def rec' (pd : coind_pred) : tactic expr := -do let c := pd.func.const_name ++ "rec", - env ← get_env, - decl ← env.get c, - let num := decl.univ_params.length, - return (const c $ if num = pd.u_params.length then pd.u_params else level.zero :: pd.u_params) - -- ^^ `rec`'s universes are not always `u_params`, e.g. eq, wf, false - -meta def construct (pd : coind_pred) : expr := -const (pd.pd_name ++ "construct") pd.u_params - -meta def destruct (pd : coind_pred) : expr := -const (pd.pd_name ++ "destruct") pd.u_params - -meta def add_theorem (pd : coind_pred) (n : name) (type : expr) (tac : tactic unit) : tactic expr := -add_theorem_by n pd.u_names type tac - -end coind_pred - -end add_coinductive_predicate - -open add_coinductive_predicate - -/- compact_relation bs as_ps: Product a relation of the form: - R := λ as, ∃ bs, Λ_i a_i = p_i[bs] -This relation is user visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and -hence `a_i = b_j`. We need to take care when there are `p_i` and `p_j` with `p_i = p_j = b_k`. -/ -private meta def compact_relation : - list expr → list (expr × expr) → list expr × list (expr × expr) -| [] ps := ([], ps) -| (list.cons b bs) ps := - match ps.span (λap:expr × expr, ¬ ap.2 =ₐ b) with - | (_, []) := let (bs, ps) := compact_relation bs ps in (b::bs, ps) - | (ps₁, list.cons (a, _) ps₂) := let i := a.instantiate_local b.local_uniq_name in - compact_relation (bs.map i) ((ps₁ ++ ps₂).map (λ⟨a, p⟩, (a, i p))) - end - -meta def add_coinductive_predicate - (u_names : list name) (params : list expr) (preds : list $ expr × list expr) : command := do - let params_names := params.map local_pp_name, - let u_params := u_names.map param, - - pre_info ← preds.mmap (λ⟨c, is⟩, do - (ls, t) ← mk_local_pis c.local_type, - (is_def_eq t `(Prop) <|> - fail (format! "Type of {c.local_pp_name} is not Prop. Currently only " ++ - "coinductive predicates are supported.")), - let n := if preds.length = 1 then "" else "_" ++ c.local_pp_name.last_string, - f₁ ← mk_local_def (mk_simple_name $ "C" ++ n) c.local_type, - f₂ ← mk_local_def (mk_simple_name $ "C₂" ++ n) c.local_type, - return (ls, (f₁, f₂))), - - let fs := pre_info.map prod.snd, - let fs₁ := fs.map prod.fst, - let fs₂ := fs.map prod.snd, - - pds ← (preds.zip pre_info).mmap (λ⟨⟨c, is⟩, ls, f₁, f₂⟩, do - sort u_f ← infer_type f₁ >>= infer_type, - let pred_g := λc:expr, (const c.local_uniq_name u_params : expr).app_of_list params, - intros ← is.mmap (λi, do - (args, t') ← mk_local_pis i.local_type, - (name.mk_string sub p) ← return i.local_uniq_name, - let loc_args := args.map $ λe, (fs₁.zip preds).foldl (λ(e:expr) ⟨f, c, _⟩, - e.replace_with (pred_g c) f) e, - let t' := t'.replace_with (pred_g c) f₂, - return { tactic.add_coinductive_predicate.coind_rule . - orig_nm := i.local_uniq_name, - func_nm := (p ++ "functional") ++ sub, - type := i.local_type, - loc_type := t'.pis loc_args, - concl := t', - loc_args := loc_args, - args := args, - insts := t'.get_app_args }), - return { tactic.add_coinductive_predicate.coind_pred . - pd_name := c.local_uniq_name, type := c.local_type, f₁ := f₁, f₂ := f₂, u_f := u_f, - intros := intros, locals := ls, params := params, u_names := u_names }), - - /- Introduce all functionals -/ - pds.mmap' (λpd:coind_pred, do - let func_f₁ := pd.func_g.app_of_list $ fs₁, - let func_f₂ := pd.func_g.app_of_list $ fs₂, - - /- Define functional for `pd` as inductive predicate -/ - func_intros ← pd.intros.mmap (λr:coind_rule, do - let t := instantiate_local pd.f₂.local_uniq_name (pd.func_g.app_of_list fs₁) r.loc_type, - return (r.func_nm, r.orig_nm, t.pis $ params ++ fs₁)), - add_inductive pd.func.const_name u_names - (params.length + preds.length) (pd.type.pis $ params ++ fs₁) (func_intros.map $ λ⟨t, _, r⟩, (t, r)), - - /- Prove monotonicity rule -/ - mono_params ← pds.mmap (λpd, do - h ← mk_local_def `h $ pd.le pd.f₁ pd.f₂, - return [pd.f₁, pd.f₂, h]), - pd.add_theorem (pd.func.const_name ++ "mono") - ((pd.le func_f₁ func_f₂).pis $ params ++ mono_params.join) - (do - ps ← intro_lst $ params.map expr.local_pp_name, - fs ← pds.mmap (λpd, do - [f₁, f₂, h] ← intro_lst [pd.f₁.local_pp_name, pd.f₂.local_pp_name, `h], - -- the type of h' reduces to h - let h' := local_const h.local_uniq_name h.local_pp_name h.local_binder_info $ - (((const `implies [] : expr) - (f₁.app_of_list pd.locals) (f₂.app_of_list pd.locals)).pis pd.locals).instantiate_locals $ - (ps.zip params).map $ λ⟨lv, p⟩, (p.local_uniq_name, lv), - return (f₂, h')), - m ← pd.rec', - eapply $ m.app_of_list ps, -- somehow `induction` / `cases` doesn't work? - func_intros.mmap' (λ⟨n, pp_n, t⟩, solve1 $ do - bs ← intros, - ms ← apply_core ((const n u_params).app_of_list $ ps ++ fs.map prod.fst) {new_goals := new_goals.all}, - params ← (ms.zip bs).enum.mfilter (λ⟨n, m, d⟩, bnot <$> is_assigned m.2), - params.mmap' (λ⟨n, m, d⟩, mono d (fs.map prod.snd) <|> - fail format! "failed to prove montonoicity of {n+1}. parameter of intro-rule {pp_n}")))), - - pds.mmap' (λpd, do - let func_f := λpd:coind_pred, pd.func_g.app_of_list $ pds.map coind_pred.f₁, - - /- define final predicate -/ - pred_body ← mk_exists_lst (pds.map coind_pred.f₁) $ - mk_and_lst $ (pds.map $ λpd, pd.le pd.f₁ (func_f pd)) ++ [pd.f₁.app_of_list pd.locals], - add_decl $ mk_definition pd.pd_name u_names (pd.type.pis $ params) $ - pred_body.lambdas $ params ++ pd.locals, - - /- prove `corec_functional` rule -/ - hs ← pds.mmap $ λpd:coind_pred, mk_local_def `hc $ pd.le pd.f₁ (func_f pd), - pd.add_theorem (pd.pred.const_name ++ "corec_functional") - ((pd.le pd.f₁ pd.pred_g).pis $ params ++ fs₁ ++ hs) - (do - intro_lst $ params.map local_pp_name, - fs ← intro_lst $ fs₁.map local_pp_name, - hs ← intro_lst $ hs.map local_pp_name, - ls ← intro_lst $ pd.locals.map local_pp_name, - h ← intro `h, - whnf_target, - fs.mmap' existsi, - hs.mmap' (λf, econstructor >> exact f), - exact h)), - - let func_f := λpd : coind_pred, pd.func_g.app_of_list $ pds.map coind_pred.pred_g, - - /- prove `destruct` rules -/ - pds.enum.mmap' (λ⟨n, pd⟩, do - let destruct := pd.le pd.pred_g (func_f pd), - pd.add_theorem (pd.pred.const_name ++ "destruct") (destruct.pis params) (do - ps ← intro_lst $ params.map local_pp_name, - ls ← intro_lst $ pd.locals.map local_pp_name, - h ← intro `h, - (fs, h) ← elim_gen_prod pds.length h [], - (hs, h) ← elim_gen_prod pds.length h [], - eapply $ pd.mono.app_of_list ps, - pds.mmap' (λpd:coind_pred, focus1 $ do - eapply $ pd.corec_functional, - focus $ hs.map exact), - some h' ← return $ hs.nth n, - eapply h', - exact h)), - - /- prove `construct` rules -/ - pds.mmap' (λpd, - pd.add_theorem (pd.pred.const_name ++ "construct") - ((pd.le (func_f pd) pd.pred_g).pis params) (do - ps ← intro_lst $ params.map local_pp_name, - let func_pred_g := λpd:coind_pred, - pd.func.app_of_list $ ps ++ pds.map (λpd:coind_pred, pd.pred.app_of_list ps), - eapply $ pd.corec_functional.app_of_list $ ps ++ pds.map func_pred_g, - pds.mmap' (λpd:coind_pred, solve1 $ do - eapply $ pd.mono.app_of_list ps, - pds.mmap' (λpd, solve1 $ eapply (pd.destruct.app_of_list ps) >> skip)))), - - /- prove `cases_on` rules -/ - pds.mmap' (λpd, do - let C := pd.f₁.to_implicit_binder, - h ← mk_local_def `h $ pd.pred_g.app_of_list pd.locals, - rules ← pd.intros.mmap (λr:coind_rule, do - mk_local_def (mk_simple_name r.orig_nm.last_string) $ (C.app_of_list r.insts).pis r.args), - cases_on ← pd.add_theorem (pd.pred.const_name ++ "cases_on") - ((C.app_of_list pd.locals).pis $ params ++ [C] ++ pd.impl_locals ++ [h] ++ rules) - (do - ps ← intro_lst $ params.map local_pp_name, - C ← intro `C, - ls ← intro_lst $ pd.locals.map local_pp_name, - h ← intro `h, - rules ← intro_lst $ rules.map local_pp_name, - func_rec ← pd.rec', - eapply $ func_rec.app_of_list $ ps ++ pds.map (λpd, pd.pred.app_of_list ps) ++ [C] ++ rules, - eapply $ pd.destruct, - exact h), - set_basic_attribute `elab_as_eliminator cases_on.const_name), - - /- prove `corec_on` rules -/ - pds.mmap' (λpd, do - rules ← pds.mmap (λpd, do - intros ← pd.intros.mmap (λr, do - let (bs, eqs) := compact_relation r.loc_args $ pd.locals.zip r.insts, - eqs ← eqs.mmap (λ⟨l, i⟩, do - sort u ← infer_type l.local_type, - return $ (const `eq [u] : expr) l.local_type i l), - match bs, eqs with - | [], [] := return ((0, 0), mk_true) - | _, [] := prod.mk (bs.length, 0) <$> mk_exists_lst bs.init bs.ilast.local_type - | _, _ := prod.mk (bs.length, eqs.length) <$> mk_exists_lst bs (mk_and_lst eqs) - end), - let shape := intros.map prod.fst, - let intros := intros.map prod.snd, - prod.mk shape <$> - mk_local_def (mk_simple_name $ "h_" ++ pd.pd_name.last_string) - (((pd.f₁.app_of_list pd.locals).imp (mk_or_lst intros)).pis pd.locals)), - let shape := rules.map prod.fst, - let rules := rules.map prod.snd, - h ← mk_local_def `h $ pd.f₁.app_of_list pd.locals, - pd.add_theorem (pd.pred.const_name ++ "corec_on") - ((pd.pred_g.app_of_list $ pd.locals).pis $ params ++ fs₁ ++ pd.impl_locals ++ [h] ++ rules) - (do - ps ← intro_lst $ params.map local_pp_name, - fs ← intro_lst $ fs₁.map local_pp_name, - ls ← intro_lst $ pd.locals.map local_pp_name, - h ← intro `h, - rules ← intro_lst $ rules.map local_pp_name, - eapply $ pd.corec_functional.app_of_list $ ps ++ fs, - (pds.zip $ rules.zip shape).mmap (λ⟨pd, hr, s⟩, solve1 $ do - ls ← intro_lst $ pd.locals.map local_pp_name, - h' ← intro `h, - h' ← note `h' none $ hr.app_of_list ls h', - match s.length with - | 0 := induction h' >> skip -- h' : false - | (n+1) := do - hs ← elim_gen_sum n h', - (hs.zip $ pd.intros.zip s).mmap' (λ⟨h, r, n_bs, n_eqs⟩, solve1 $ do - (as, h) ← elim_gen_prod (n_bs - (if n_eqs = 0 then 1 else 0)) h [], - if n_eqs > 0 then do - (eqs, eq') ← elim_gen_prod (n_eqs - 1) h [], - (eqs ++ [eq']).mmap' subst - else skip, - eapply ((const r.func_nm u_params).app_of_list $ ps ++ fs), - iterate assumption) - end), - exact h)), - - /- prove constructors -/ - pds.mmap' (λpd, pd.intros.mmap' (λr, - pd.add_theorem r.orig_nm (r.type.pis params) $ do - ps ← intro_lst $ params.map local_pp_name, - bs ← intros, - eapply $ pd.construct, - exact $ (const r.func_nm u_params).app_of_list $ ps ++ pds.map (λpd, pd.pred.app_of_list ps) ++ bs)), - - pds.mmap' (λpd:coind_pred, set_basic_attribute `irreducible pd.pd_name), - - try triv -- we setup a trivial goal for the tactic framework - -open lean.parser -open interactive - -@[user_command] -meta def coinductive_predicate (meta_info : decl_meta_info) (_ : parse $ tk "coinductive") : lean.parser unit := do - decl ← inductive_decl.parse meta_info, - add_coinductive_predicate decl.u_names decl.params $ decl.decls.map $ λ d, (d.sig, d.intros), - decl.decls.mmap' $ λ d, do { - get_env >>= λ env, set_env $ env.add_namespace d.name, - meta_info.attrs.apply d.name, - d.attrs.apply d.name, - some doc_string ← pure meta_info.doc_string | skip, - add_doc_string d.name doc_string - } - -/-- Prepares coinduction proofs. This tactic constructs the coinduction invariant from -the quantifiers in the current goal. - -Current version: do not support mutual inductive rules (i.e. only a since C -/ -meta def coinduction (rule : expr) : tactic unit := focus1 $ -do - ctxts' ← intros, - ctxts ← ctxts'.mmap (λv, - local_const v.local_uniq_name v.local_pp_name v.local_binder_info <$> infer_type v), - mvars ← apply_core rule {approx := ff, new_goals := new_goals.all}, - -- analyse relation - g ← list.head <$> get_goals, - (list.cons _ m_is) ← return $ mvars.drop_while (λv, v.2 ≠ g), - tgt ← target, - (is, ty) ← mk_local_pis tgt, - - -- construct coinduction predicate - (bs, eqs) ← compact_relation ctxts <$> - ((is.zip m_is).mmap (λ⟨i, m⟩, prod.mk i <$> instantiate_mvars m.2)), - - solve1 (do - eqs ← mk_and_lst <$> eqs.mmap (λ⟨i, m⟩, mk_app `eq [m, i] >>= instantiate_mvars), - rel ← mk_exists_lst bs eqs, - exact (rel.lambdas is)), - - -- prove predicate - solve1 (do - target >>= instantiate_mvars >>= change, -- TODO: bug in existsi & constructor when mvars in hyptohesis - bs.mmap existsi, - iterate (econstructor >> skip)), - - -- clean up remaining coinduction steps - all_goals (do - ctxts'.reverse.mmap clear, - target >>= instantiate_mvars >>= change, -- TODO: bug in subst when mvars in hyptohesis - is ← intro_lst $ is.map expr.local_pp_name, - h ← intro1, - (_, h) ← elim_gen_prod (bs.length - (if eqs.length = 0 then 1 else 0)) h [], - (match eqs with - | [] := clear h - | (e::eqs) := do - (hs, h) ← elim_gen_prod eqs.length h [], - (h::(hs.reverse)).mmap' subst - end)) - -namespace interactive -open interactive interactive.types expr lean.parser -local postfix `?`:9001 := optional -local postfix *:9001 := many - -meta def coinduction (corec_name : parse ident) - (revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit := do - rule ← mk_const corec_name, - locals ← mmap tactic.get_local $ revert.get_or_else [], - revert_lst locals, - tactic.coinduction rule, - skip - -end interactive - -end tactic diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index 294ea75755..7800beaca1 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -8,11 +8,9 @@ import init.meta.name init.meta.options init.meta.format init.meta.rb_map import init.meta.level init.meta.expr init.meta.environment init.meta.attribute import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info -import init.meta.congr_lemma init.meta.match_tactic -import init.meta.rewrite_tactic +import init.meta.congr_lemma init.meta.match_tactic init.meta.rewrite_tactic import init.meta.derive init.meta.mk_dec_eq_instance import init.meta.simp_tactic init.meta.set_get_option_tactics import init.meta.interactive init.meta.vm import init.meta.comp_value_tactics -import init.meta.coinductive_predicates import init.meta.congr_tactic diff --git a/library/init/meta/transfer.lean b/library/init/meta/transfer.lean deleted file mode 100644 index 6fb88fe218..0000000000 --- a/library/init/meta/transfer.lean +++ /dev/null @@ -1,187 +0,0 @@ -/- -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 -import init.data.list.instances - -namespace transfer -open tactic expr list monad - -/- Transfer rules are of the shape: - - rel_t : {u} Πx, R t₁ t₂ - -where `u` is a list of universe parameters, `x` is a list of dependent variables, and `R` is a -relation. Then this rule will translate `t₁` (depending on `u` and `x`) into `t₂`. `u` and `x` -will be called parameters. When `R` is a relation on functions lifted from `S` and `R` the variables -bound by `S` are called arguments. `R` is generally constructed using `⇒` (i.e. `relator.lift_fun`). - -As example: - - rel_eq : (R ⇒ R ⇒ iff) eq t - -transfer will match this rule when it sees: - - (@eq α a b) and transfer it to (t a b) - -Here `α` is a parameter and `a` and `b` are arguments. - - -TODO: add trace statements - -TODO: currently the used relation must be fixed by the matched rule or through type class - inference. Maybe we want to replace this by type inference similar to Isabelle's transfer. - --/ - - -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 format!"({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` -(output : 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, - output ← pp r.output, - return format!"{{ ⟨{pat}⟩ pr: {pr} → {output}, {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 (u' : list name) (pr : expr) : tactic rule_data := do - t ← infer_type pr, - (params, app (app r f) g) ← mk_local_pis t, - (arg_rels, R) ← get_lift_fun r, - args ← (enum arg_rels).mmap $ λ⟨n, a⟩, - prod.mk <$> mk_local_def (mk_simple_name ("a_" ++ repr n)) a.in_type <*> pure a, - a_vars ← return $ 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 (p_data.filter (λx, ↑x.2)), - u ← return $ collect_univ_params (app R p) ∩ u', - pat ← mk_pattern (level.param <$> u) (p_vars ++ a_vars) (app R p) (level.param <$> u) (p_vars ++ a_vars), - return $ rule_data.mk pr (u'.remove_all u) p_data u args pat g - -private meta def analyse_decls : list name → tactic (list rule_data) := -mmap (λn, do - d ← get_decl n, - c ← return d.univ_params.length, - ls ← (repeat () c).mmap (λ_, mk_fresh_name), - analyse_rule ls (const n (ls.map level.param))) - -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), - e ← instantiate_mvars ty >>= mk_instance, - 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 $ prod.map sb ((<$>) 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.map (λrd, do - (l, m) ← match_pattern rd.pat e semireducible, - level_map ← rd.uparams.mmap $ λ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 (rd.params.map (prod.map inst_univ id)) m, - (ps, ms) ← param_substitutions ctxt ps, /- this checks type class parameters -/ - return (instantiate_locals ps ∘ inst_univ, ps, args, ms, rd))) <|> - (do trace e, fail "no matching rule"), - - (bs, hs, mss) ← (zip rd.args args).mmap (λ⟨⟨_, d⟩, e⟩, do - -- Argument has function type - (args, r) ← get_lift_fun (i d.relation), - ((a_vars, b_vars), (R_vars, bnds)) ← (enum args).mmap (λ⟨n, arg⟩, do - a ← mk_local_def sformat!"a{n}" arg.in_type, - b ← mk_local_def sformat!"b{n}" arg.out_type, - R ← mk_local_def sformat!"R{n}" (arg.relation a b), - return ((a, b), (R, [a, b, R]))) >>= (return ∘ prod.map unzip unzip ∘ unzip), - rds' ← R_vars.mmap (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.output) bs), - pr ← return $ app_of_list (i rd.pr) (prod.snd <$> ps ++ list.join hs), - return (b, pr, ms ++ mss.join) - -meta def transfer (ds : list name) : tactic unit := do - rds ← analyse_decls ds, - tgt ← target, - - (guard (¬ tgt.has_meta_var) <|> - fail "Target contains (universe) meta variables. This is not supported by transfer."), - - (new_tgt, pr, ms) ← compute_transfer rds [] ((const `iff [] : expr) tgt), - new_pr ← mk_meta_var new_tgt, - - /- Setup final tactic state -/ - exact ((const `iff.mpr [] : expr) tgt new_tgt pr new_pr), - ms ← ms.mmap (λm, (get_assignment m >> return []) <|> return [m]), - gs ← get_goals, - set_goals (ms.join ++ new_pr :: gs) - -end transfer diff --git a/library/init/relator.lean b/library/init/relator.lean deleted file mode 100644 index b6d67f0429..0000000000 --- a/library/init/relator.lean +++ /dev/null @@ -1,84 +0,0 @@ -/- -Copyright (c) 2017 Johannes Hölzl. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Johannes Hölzl - -Relator for functions, pairs, sums, and lists. --/ - -prelude -import init.core init.data.basic - -namespace relator -universe variables u₁ u₂ v₁ v₂ - -reserve infixr ` ⇒ `:40 - -/- TODO(johoelzl): - * should we introduce relators of datatypes as recursive function or as inductive -predicate? For now we stick to the recursor approach. - * relation lift for datatypes, Π, Σ, set, and subtype types - * proof composition and identity laws - * implement method to derive relators from datatype --/ - -section -variables {α : Type u₁} {β : Type u₂} {γ : Type v₁} {δ : Type v₂} -variables (R : α → β → Prop) (S : γ → δ → Prop) - -def lift_fun (f : α → γ) (g : β → δ) : Prop := -∀{a b}, R a b → S (f a) (g b) - -infixr ⇒ := lift_fun - -end - -section -variables {α : Type u₁} {β : out_param $ Type u₂} (R : out_param $ α → β → Prop) - -@[class] def right_total := ∀b, ∃a, R a b -@[class] def left_total := ∀a, ∃b, R a b -@[class] def bi_total := left_total R ∧ right_total R - -end - -section -variables {α : Type u₁} {β : Type u₂} (R : α → β → Prop) - -@[class] def left_unique := ∀{a b c}, R a b → R c b → a = c -@[class] def right_unique := ∀{a b c}, R a b → R a c → b = c - -lemma rel_forall_of_right_total [t : right_total R] : ((R ⇒ implies) ⇒ implies) (λp, ∀i, p i) (λq, ∀i, q i) := -assume p q Hrel H b, exists.elim (t b) (assume a Rab, Hrel Rab (H _)) - -lemma rel_exists_of_left_total [t : left_total R] : ((R ⇒ implies) ⇒ implies) (λp, ∃i, p i) (λq, ∃i, q i) := -assume p q Hrel ⟨a, pa⟩, let ⟨b, Rab⟩ := t a in ⟨b, Hrel Rab pa⟩ - -lemma rel_forall_of_total [t : bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∀i, p i) (λq, ∀i, q i) := -assume p q Hrel, - ⟨assume H b, exists.elim (t.right b) (assume a Rab, (Hrel Rab).mp (H _)), - assume H a, exists.elim (t.left a) (assume b Rab, (Hrel Rab).mpr (H _))⟩ - -lemma rel_exists_of_total [t : bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∃i, p i) (λq, ∃i, q i) := -assume p q Hrel, - ⟨assume ⟨a, pa⟩, let ⟨b, Rab⟩ := t.left a in ⟨b, (Hrel Rab).1 pa⟩, - assume ⟨b, qb⟩, let ⟨a, Rab⟩ := t.right b in ⟨a, (Hrel Rab).2 qb⟩⟩ - -lemma left_unique_of_rel_eq {eq' : β → β → Prop} (he : (R ⇒ (R ⇒ iff)) eq eq') : left_unique R -| a b c (ab : R a b) (cb : R c b) := -have eq' b b, - from iff.mp (he ab ab) rfl, -iff.mpr (he ab cb) this - -end - -lemma rel_imp : (iff ⇒ (iff ⇒ iff)) implies implies := -assume p q h r s l, imp_congr h l - -lemma rel_not : (iff ⇒ iff) not not := -assume p q h, not_congr h - -instance bi_total_eq {α : Type u₁} : relator.bi_total (@eq α) := -⟨assume a, ⟨a, rfl⟩, assume a, ⟨a, rfl⟩⟩ - -end relator