feat(library/init/meta): support mutual coinductive predicates
This commit is contained in:
Johannes Hölzl
Leonardo de Moura
parent
23f12a22a2
commit
4d01a6548e
2 changed files with 194 additions and 110 deletions
|
|
@ -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 ()
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue