From 8d438e10121784f67645ee6faa9cd314293cec01 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Mon, 12 Jun 2017 19:02:16 -0400 Subject: [PATCH] feat(library/init/meta): add coinduction method --- library/init/data/list/basic.lean | 5 + library/init/meta/coinductive_predicates.lean | 129 +++++++++++++++--- tests/lean/run/coinductive.lean | 16 +++ 3 files changed, 134 insertions(+), 16 deletions(-) diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index e34724718b..341c4a0d54 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -261,6 +261,11 @@ def ilast [inhabited α] : list α → α | [a, b] := b | (a::b::l) := ilast l +def init : list α → list α +| [] := [] +| [a] := [] +| (a::l) := a::init l + def intersperse (sep : α) : list α → list α | [] := [] | [x] := [x] diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean index f0eb3305cc..5d8c8c4098 100644 --- a/library/init/meta/coinductive_predicates.lean +++ b/library/init/meta/coinductive_predicates.lean @@ -5,7 +5,7 @@ Author: Johannes Hölzl (CMU) -/ prelude import init.meta.expr init.meta.tactic init.meta.constructor_tactic init.meta.attribute -import init.meta.interactive_base +import init.meta.interactive namespace name @@ -32,6 +32,13 @@ meta def to_implicit_binder : expr → expr | (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 @@ -67,8 +74,11 @@ meta def is_assigned (m : expr): tactic bool := meta def mk_exists_lst (args : list expr) (inner : expr) : tactic expr := args.mfoldr (λarg i:expr, do - sort l ← infer_type arg.local_type, - return $ (const `Exists [l] : expr) arg.local_type (i.lambdas [arg])) + 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 @@ -307,6 +317,20 @@ 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, @@ -368,8 +392,8 @@ meta def add_coinductive_predicate ((pd.le func_f₁ func_f₂).pis $ params ++ mono_params.join) (do ps ← intro_lst $ params.map expr.local_pp_name, - fs ← mono_params.mmap (λmp, do - [f₁, f₂, h] ← intro_lst $ mp.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) @@ -464,12 +488,22 @@ meta def add_coinductive_predicate pds.mmap' (λpd, do rules ← pds.mmap (λpd, do intros ← pd.intros.mmap (λr, do - eqs ← (list.zip pd.locals r.insts).mmap (λ⟨l, i⟩, 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), - mk_exists_lst r.loc_args $ mk_and_lst eqs), - 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), + 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) @@ -480,21 +514,22 @@ meta def add_coinductive_predicate h ← intro `h, rules ← intro_lst $ rules.map local_pp_name, apply $ pd.corec_functional.app_of_list $ ps ++ fs, - (pds.zip rules).mmap (λ⟨pd, hr⟩, solve1 $ do + (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 pd.intros.length with + match s.length with | 0 := induction h' >> skip -- h' : false | (n+1) := do hs ← elim_gen_sum n h', - (hs.zip pd.intros).mmap' (λ⟨h, r⟩, solve1 $ do - (as, h) ← elim_gen_prod (r.args.length) h [], - if pd.locals.length > 0 then do - (eqs, eq') ← elim_gen_prod (pd.locals.length - 1) 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, - apply ((const r.func_nm u_params).app_of_list $ ps ++ fs ++ as)) + apply ((const r.func_nm u_params).app_of_list $ ps ++ fs), + repeat assumption) end), exact h)), @@ -510,4 +545,66 @@ meta def add_coinductive_predicate try triv -- we setup a trivial goal for the tactic framework +/-- 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, + -- TODO: why do we need to fix the type here? + 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, all := tt }, + + -- analyse relation + g ← list.head <$> get_goals, + (list.cons _ m_is) ← return $ mvars.drop_while (λv, v ≠ 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)), + + 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, + repeat constructor), + + -- 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/tests/lean/run/coinductive.lean b/tests/lean/run/coinductive.lean index 15ce1e9a95..21722a0750 100644 --- a/tests/lean/run/coinductive.lean +++ b/tests/lean/run/coinductive.lean @@ -81,3 +81,19 @@ with walk_a : α → Prop | term : ∀a, t a → walk_a a with walk_b : β → Prop | step : ∀b, walk_a (g b) → walk_b b + + +coinductive walk_list {α : Type} (f : α → list α) (p : α → Prop) : ℕ → α → Prop +| step : ∀n a, all_list (walk_list n) (f a) → p a → walk_list (n + 1) a + +-- #check walk_a.corec_on + +example {f : ℕ → list ℕ} {a' : ℕ} {n : ℕ} {a : fin n}: + walk_list f (λ a'', a'' = a') (n + 1) a' := +begin + coinduction walk_list.corec_on generalizing a n, + show ∃ (n : ℕ), + all_list (λ (a : ℕ), ∃ {n_1 : ℕ} {a_1 : fin n_1}, n_1 + 1 = n ∧ a' = a) (f a') ∧ + a' = a' ∧ n + 1 = a_1 + 1, + admit +end