From 4d01a6548e5ca75015a60b4cd61e25edd3a2f4d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Sat, 3 Jun 2017 16:07:49 -0400 Subject: [PATCH] feat(library/init/meta): support mutual coinductive predicates --- library/init/meta/coinductive_predicates.lean | 281 ++++++++++++------ tests/lean/run/coinduction.lean | 23 +- 2 files changed, 194 insertions(+), 110 deletions(-) diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean index 4696faf71b..9ff3a9fdb0 100644 --- a/library/init/meta/coinductive_predicates.lean +++ b/library/init/meta/coinductive_predicates.lean @@ -4,14 +4,11 @@ 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 +import init.meta.expr init.meta.tactic init.meta.constructor_tactic 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' else none - meta def local_binder_info : expr → binder_info | (local_const x n bi t) := bi | e := binder_info.default @@ -58,135 +55,223 @@ The coinductive predicate `pred`: where `u` is a list of universe parameters `A` is a list of global parameters - `a` are the indices - `r` is a list of introduction rules - `b` is a list of parameters for each rule in `r` + `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) (f : a → Prop) : a → Prop - | r : ∀a f, b[pred/f] → pred.functional a f p + 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) (f f' : a → Prop) (h : ∀b, f b → f' b) : - ∀p, pred.functional A f p → 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 := pred.functional.rec A f (pred.functional A f') (take p, pred.functional.r A f' p[mono with h]) - def {u} pred (A) (a) : Prop := - ∃f, (∀a, f a → pred.functional A f a) ∧ f a + 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.corec_functional (A) (C : a → Prop) (h : ∀a, C a → pred.functional A C a) : - ∀a, C a → pred A a := - take a ha, ⟨C, h, ha⟩ + lemma {u} pred_i.corec_functional (A) [(C : a → Prop)] (h : ∀[a], [C a] → pred.functional A [C] a) : + ∀a, C_i a → pred_i A a := + take a ha, ⟨[C], [h], ha⟩ - lemma {u} pred.destruct (A) (a) : pred A a → pred.functional A (pred A) a := + lemma {u} pred_i.destruct (A) (a) : pred A a → pred.functional A [pred A] a := Exists.rec (a → Prop) (λf, (∀a, f a → pred.functional A f a) ∧ f a) (pred.functional A (pred A a) a) h $ take f, and.rec.{0} (∀a, f a → pred.functional A f a) (f a) $ assume h₁ : ∀a, f a → pred.functional A f a, assume h₂ : f a, pred.functional.mono A f (pred A) (pred.corec_functional A f h₁) a (h₁ a h₂)) - lemma {u} pred.construct (A) : ∀a, pred.functional A (pred A) a → pred A a := + lemma {u} pred_i.construct (A) : ∀a, pred_i.functional A [pred A] a → pred_i A a := pred.corec_functional A (pred.functional A (pred A)) (pred.functional.mono A (pred A) (pred.functional A (pred A)) (pred.destruct A)) - lemma {u} pred.r (A) (b) : pred A p := - pred.construct A p $ pred.functional.r A (pred A) b - + lemma {u} pred.r (A) (b) : pred_i A p := + pred_i.construct A p $ pred_i.functional.r A [pred A] b -/ +open level expr tactic + +namespace add_coinductive_predicate + +/- private -/ meta structure pred_predata : Type := +(u_params : list level) +(params : list expr) +(pd_name : name) +(pred : expr) +(type : expr) +(intros : list (name × expr)) +(locals : list expr) +(f₁ f₂ : expr) +(u_f : level) +(func : expr) + +namespace pred_predata + +meta def f₁_l (pd : pred_predata) : expr := +pd.f₁.app_of_list pd.locals + +meta def f₂_l (pd : pred_predata) : expr := +pd.f₂.app_of_list pd.locals + +meta def func_g (pd : pred_predata) : expr := +pd.func.app_of_list $ pd.params + +meta def pred_g (pd : pred_predata) : expr := +pd.pred.app_of_list $ pd.params + +meta def le (pd : pred_predata) (f₁ f₂ : expr) : expr := +(imp (f₁.app_of_list pd.locals) (f₂.app_of_list pd.locals)).pis pd.locals + +meta def corec (pd : pred_predata) : expr := +const (pd.pd_name ++ "corec_functional") pd.u_params + +meta def mono (pd : pred_predata) : expr := +const (pd.func.const_name ++ "mono") pd.u_params + +meta def construct (pd : pred_predata) : expr := +const (pd.pd_name ++ "construct") pd.u_params + +meta def destruct (pd : pred_predata) : expr := +const (pd.pd_name ++ "destruct") pd.u_params + +end pred_predata + +end add_coinductive_predicate + +open add_coinductive_predicate + meta def add_coinductive_predicate - (n : name) (us : list name) (p : nat) (type : expr) (irules : list (name × expr)) : command := do - let us' := us.map param, + (u_params : list name) (params : list expr) (preds : list $ expr × list expr) : command := do + let params_names := params.map local_pp_name, + let u_params' := u_params.map param, - /- introduce locals to represent global parameters -/ - (gs, type') ← mk_local_pisn type p, - (ls, `(Prop)) ← mk_local_pis type', - let gs_names := gs.map local_pp_name, - let ls_names := ls.map local_pp_name, + pds ← preds.mmap (λ⟨c, is⟩, do + (ls, `(Prop)) ← mk_local_pis c.local_type, + f₁ ← mk_local_def `f₁ c.local_type, + f₂ ← mk_local_def `f₂ c.local_type, + sort u_f ← infer_type f₁ >>= infer_type, + let func : expr := const (c.local_pp_name ++ "functional") u_params', + return {tactic.add_coinductive_predicate.pred_predata . + pd_name := c.local_pp_name, + pred := const c.local_pp_name u_params', type := c.local_type, + intros := is.map (λi, (i.local_pp_name, i.local_type)), + locals := ls, params := params, u_params := u_params', + f₁ := f₁, f₂ := f₂, u_f := u_f, func := func}), - -- vv this will be two lists of functions to support mutual induction - f ← mk_local_def `f type', - f₂ ← mk_local_def `f' type', - sort u_f ← infer_type f >>= infer_type, + let f₁ := pds.map pred_predata.f₁, + let f₂ := pds.map pred_predata.f₂, - /- define often occuring subterms -/ - let pred : expr := const n us', - let pred_g := pred.app_of_list gs, - let pred_gl := pred_g.app_of_list ls, + /- Introduce all functionals -/ + pds.mmap (λpd:pred_predata, do + let func_f₁ := pd.func_g.app_of_list $ f₁, + let func_f₂ := pd.func_g.app_of_list $ f₂, - let func_type := type'.pis $ gs ++ [f], - let func_name := n ++ "functional", - let func : expr := const func_name us', - let func_g := func.app_of_list gs, - let func_f := func_g f, - let func_f₂ := func_g f₂, - let func_pred_l := func.app_of_list $ gs ++ [pred_g] ++ ls, + /- Define functional for `pd` as inductive predicate -/ + func_intros ← pd.intros.mmap (λ⟨nr, t⟩, do + (bs, t') ← mk_local_pis t, + (name.mk_string sub p) ← return $ nr, + let bs := bs.map $ expr.instantiate_locals $ pds.map (λpd:pred_predata, (pd.pd_name, pd.f₁)), + let t' := expr.instantiate_local pd.pd_name (pd.func.app_of_list $ params ++ f₁) t', + return ((p ++ "functional") ++ sub, t'.pis $ params ++ f₁ ++ bs)), + let func_type := pd.type.pis $ params ++ f₁, + add_inductive pd.func.const_name u_params (params.length + preds.length) func_type func_intros, - let f_l := f.app_of_list ls, - let f₂_l := f₂.app_of_list ls, - let f_le_func := (f_l.imp $ func_f.app_of_list ls).pis ls, - - /- define `functional` as inductive predicate -/ - func_intros ← irules.mmap (λ⟨nr, t⟩, do - (ls, t') ← drop_pis gs t >>= mk_local_pis, - let ls' := ls.map $ λe, e.replace_with pred_g f, - let t' := t'.replace_with pred_g func_f, - (name.mk_string sub p) ← return $ nr, - return ((p ++ "functional") ++ sub, t'.pis $ gs ++ [f] ++ ls')), - add_inductive func_name us (p + 1) func_type func_intros, - - /- prove monotonicity of `functional` -/ - let mono_func : expr := (imp (func_f.app_of_list ls) (func_f₂.app_of_list ls)).pis ls, - mono ← add_theorem_by (func_name ++ "mono") us - ((imp ((imp f_l f₂_l).pis ls) mono_func).pis $ gs ++ [f, f₂]) (do - gs ← intro_lst gs_names, - [f₁, f₂, hf] ← intro_lst [`f₁, `f₂, `hf], - m ← mk_const (func_name ++ "rec"), -- `rec`'s universes are not always `us`, e.g. eq, wf, false - apply $ m.app_of_list gs, -- somhow `induction` / `cases` doesn't work? + /- Prove monotonicity rule -/ + let mono_type := + pds.foldl (λc (pd:pred_predata), ((pd.le pd.f₁ pd.f₂).imp c).pis [pd.f₁, pd.f₂]) $ + pd.le func_f₁ func_f₂, + add_theorem_by (pd.func.const_name ++ "mono") u_params (mono_type.pis $ params) (do + params ← intro_lst params_names, + hf ← pds.mmap (λpd, do + [f₁, f₂, hf] ← intro_lst [`f₁, `f₂, `hf], + return (f₂, hf)), + let fs₂ := hf.map prod.fst, + let hfs := hf.map prod.snd, + m ← mk_const (pd.func.const_name ++ "rec"), + -- ^^ `rec`'s universes are not always `u_params`, e.g. eq, wf, false + apply $ m.app_of_list params, -- somhow `induction` / `cases` doesn't work? focus $ func_intros.map (λ⟨n, t⟩, do bs ← intros, - ms ← apply_core ((const n us').app_of_list $ gs ++ [f₂]) { all := tt }, - gs ← (ms.zip bs).mfilter (λ⟨m, d⟩, is_assigned m), - focus $ gs.map (λ⟨m, d⟩, apply d <|> (apply hf >> apply d)))), + ms ← apply_core ((const n u_params').app_of_list $ params ++ fs₂) { all := tt }, + params ← (ms.zip bs).mfilter (λ⟨m, d⟩, is_assigned m), + focus $ params.map (λ⟨m, d⟩, apply d <|> first (hfs.map $ λ hf, apply hf >> apply d))))), - /- define `pred` as fixed point of `functional` -/ - add_decl $ mk_definition n us type $ - (((const `Exists [u_f] : expr) type' ((`(and) f_le_func f_l).lambdas [f])).lambdas $ gs ++ ls), + pds.mmap (λpd:pred_predata, do + let func_f := pd.func_g.app_of_list $ pds.map pred_predata.f₁, - /- prove `corec_functional` rule -/ - corec ← add_theorem_by (n ++ "corec_functional") us - ((f_le_func.imp ((imp f_l pred_gl).pis ls)).pis $ gs ++ [f]) (do - intro_lst gs_names, [C, hC] ← intro_lst [`C, `hC], intro_lst ls_names, hls ← intro `hls, - refine ``(exists.intro %%C (and.intro %%hC %%hls))), + /- define final predicate -/ + pred_body ← (do + corec ← pds.mfoldl + (λcont pd, to_expr ``(%%(pd.le pd.f₁ func_f) ∧ %%cont)) + (pd.f₁.app_of_list pd.locals), + pds.mfoldl (λcont pd, to_expr ``(@Exists %%pd.type %%(cont.lambdas [pd.f₁]))) corec), + add_decl $ mk_definition pd.pred.const_name u_params (pd.type.pis $ params) $ + pred_body.lambdas $ params ++ pd.locals, - /- prove `destruct` rule -/ - destruct ← add_theorem_by (n ++ "destruct") us ((imp pred_gl func_pred_l).pis $ gs ++ ls) (do - gs ← intro_lst gs_names, ls ← intro_lst ls_names, h ← intro `h, - [([f, hf], [])] ← induction h [`f, `hf], - [([h₁, h₂], [])] ← induction hf [`h₁, `h₂], - apply $ mono.app_of_list $ gs ++ [f], - exact $ corec.app_of_list $ gs ++ [f, h₁], - exact $ h₁.app_of_list $ ls ++ [h₂]), + /- prove `corec_functional` rule -/ + let corec_type := pds.foldl (λc pd, (pd.le pd.f₁ func_f).imp c) (pd.le pd.f₁ pd.pred_g), + add_theorem_by (pd.pred.const_name ++ "corec_functional") u_params (corec_type.pis $ params ++ f₁) (do + params ← intro_lst params_names, + fs ← intro_lst $ f₁.map local_pp_name, + hs ← intro_lst $ f₁.map (λf, mk_simple_name "hc"), + ls ← intro_lst $ pd.locals.map local_pp_name, + h ← intro `h, + whnf_target, + fs.mmap existsi, + hs.mmap (λf, constructor >> exact f), + exact h)), + + let func_f := λpd : pred_predata, pd.func_g.app_of_list $ pds.map pred_predata.pred_g, - /- prove `construct` rule -/ - let construct_type := (imp func_pred_l pred_gl).pis $ gs ++ ls, - construct ← add_theorem_by (n ++ "construct") us construct_type (do - gs ← intro_lst gs_names, - let pred := pred.app_of_list gs, - let func_pred := func.app_of_list $ gs ++ [pred], - apply $ corec.app_of_list $ gs ++ [func_pred], - apply $ mono.app_of_list $ gs ++ [pred, func_pred], - exact $ destruct.app_of_list gs), + /- prove `destruct` rules -/ + pds.enum.mmap (λd:ℕ × pred_predata, do + let n := d.1, + let pd := d.2, + let destruct := (pd.le pd.pred_g (func_f pd)).pis $ params, + add_theorem_by (pd.pred.const_name ++ "destruct") u_params destruct (do + params ← intro_lst params_names, + ls ← intro_lst $ pd.locals.map local_pp_name, + h ← intro `h, + (fs, h) ← pds.mfoldl (λ(c:list expr × expr) (pd:pred_predata), do + [([f, hf], [])] ← induction c.2 [`f, `hf], + return (c.1 ++ [f], hf)) + ([], h), + (hs, h) ← pds.mfoldl (λ(c:list expr × expr) (pd:pred_predata), do + [([h, h'], [])] ← induction c.2 [`h, `h'], + return (c.1 ++ [h], h')) + ([], h), + apply $ pd.mono.app_of_list $ params, + pds.mmap (λpd:pred_predata, focus1 $ do + apply $ pd.corec.app_of_list $ params, + focus $ hs.map exact), + some h' ← return $ hs.nth n, + apply h', + exact h)), + + /- prove `construct` rules -/ + pds.mmap (λpd:pred_predata, + add_theorem_by (pd.pred.const_name ++ "construct") u_params + ((pd.le (func_f pd) pd.pred_g).pis $ params) (do + params ← intro_lst params_names, + apply $ pd.corec.app_of_list $ params, + apply $ pd.mono.app_of_list $ params, + focus $ pds.map (λpd, apply pd.destruct))), /- prove constructors -/ - irules.mmap (λ⟨nr, t⟩, add_theorem_by nr us t $ do - (name.mk_string sub p) ← return nr, - let func_rule : expr := (const ((p ++ "functional") ++ sub) us'), - gs ← intro_lst gs_names, bs ← intros, - apply $ construct.app_of_list $ gs, - exact $ func_rule.app_of_list $ gs ++ [pred.app_of_list gs] ++ bs), + pds.mmap (λpd:pred_predata, do + pd.intros.mmap (λ⟨nr, t⟩, do + let t : expr := expr.instantiate_locals (pds.map (λpd:pred_predata, + (pd.pd_name, (const pd.pd_name u_params').app_of_list params))) t, + add_theorem_by nr u_params (t.pis params) $ do + (name.mk_string sub p) ← return nr, + let func_rule : expr := (const ((p ++ "functional") ++ sub) u_params'), + params ← intro_lst params_names, bs ← intros, + apply $ pd.construct.app_of_list $ params, + exact $ func_rule.app_of_list $ params ++ [pd.pred.app_of_list params] ++ bs)), return () diff --git a/tests/lean/run/coinduction.lean b/tests/lean/run/coinduction.lean index dcd9cee812..65d3c879b4 100644 --- a/tests/lean/run/coinduction.lean +++ b/tests/lean/run/coinduction.lean @@ -1,28 +1,27 @@ /- test cases for coinduction -/ import data.stream -open expr tactic - -/- +open level expr tactic coinductive {u} all_stream {α : Type u} (s : set α) : stream α → Prop | step {} : ∀{a : α} {ω : stream α}, a ∈ s → all_stream ω → all_stream (a :: ω) --/ - +/- run_cmd do let n := `all_stream, let p := 2, let u := `u, let us : list name := [u], - let Ty : expr := sort $ level.succ $ level.param u, - type ← to_expr ``(Π{α : %%Ty} (s : set α), stream α → Prop), - let l' : expr := local_const n n binder_info.default type, - intro₁ ← to_expr ``(∀{α : %%Ty} {s : set α} {a : α} {ω : stream α}, a ∈ s → %%l' s ω → %%l' s (a :: ω)), - let intro₁ := instantiate_local n (const n [level.param u]) intro₁, - let intros := [(`all_stream.step, intro₁)], - add_coinductive_predicate n us p type intros + let Ty : expr := sort $ succ $ param u, + let α := local_const `α `α binder_info.implicit Ty, + let s := local_const `s `s binder_info.default ((const `set [param u] : expr) $ α), + type ← to_expr ``(stream %%α → Prop), + let l : expr := local_const n n binder_info.default type, + intro₁ ← to_expr ``(∀{a : %%α} {ω : stream %%α}, a ∈ %%s → %%l ω → %%l (a :: ω)), + let intros := [local_const `all_stream.step `all_stream.step binder_info.default intro₁], + add_coinductive_predicate us [α, s] [(l, intros)] +-/ #print prefix all_stream