Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-29 23:48 ef89e9af

View on Github →

feat(data/qpf): compositional data type framework for inductive / coinductive types (#3317) First milestone of the QPF project. Includes multivariate quotients of polynomial functors and compiler for coinductive types. Not included in this PR

  • nested inductive / coinductive data types
  • universe polymorphism with more than one variable
  • inductive / coinductive families
  • equation compiler
  • efficient byte code implementation Those are coming in future PRs

Estimated changes

added theorem mvpfunctor.M.bisim'
added theorem mvpfunctor.M.bisim
added theorem mvpfunctor.M.bisim₀
added theorem mvpfunctor.M.dest_map
added theorem mvpfunctor.M.map_dest
added def mvpfunctor.M.mk
added inductive mvpfunctor.M.path
added def mvpfunctor.M
added def mvpfunctor.Mp
added def mvpfunctor.W
added theorem mvpfunctor.W_cases
added theorem mvpfunctor.W_ind
added def mvpfunctor.W_map
added theorem mvpfunctor.W_map_W_mk
added def mvpfunctor.W_mk'
added def mvpfunctor.W_mk
added theorem mvpfunctor.W_mk_eq
added inductive mvpfunctor.W_path
added def mvpfunctor.W_rec
added theorem mvpfunctor.W_rec_eq
added def mvpfunctor.Wp
added theorem mvpfunctor.Wp_ind
added def mvpfunctor.Wp_mk
added theorem mvpfunctor.Wp_rec_eq
deleted theorem pfunctor.M.coinduction'
deleted theorem pfunctor.M.coinduction
added def mvqpf.Mcongr
added def mvqpf.Mrepr
added def mvqpf.cofix.abs
added theorem mvqpf.cofix.abs_repr
added theorem mvqpf.cofix.bisim'
added theorem mvqpf.cofix.bisim
added theorem mvqpf.cofix.bisim_rel
added theorem mvqpf.cofix.bisim₂
added def mvqpf.cofix.dest
added theorem mvqpf.cofix.dest_corec
added theorem mvqpf.cofix.dest_mk
added theorem mvqpf.cofix.ext
added theorem mvqpf.cofix.ext_mk
added def mvqpf.cofix.map
added def mvqpf.cofix.mk
added theorem mvqpf.cofix.mk_dest
added def mvqpf.cofix.repr
added def mvqpf.cofix
added def mvqpf.corecF
added theorem mvqpf.corecF_eq
added theorem mvqpf.corec_roll
added theorem mvqpf.liftr_map
added theorem mvqpf.liftr_map_last'
added theorem mvqpf.liftr_map_last
added theorem mvqpf.comp.get_map
added theorem mvqpf.comp.map_mk
added def mvqpf.comp
added theorem mvqpf.const.get_map
added theorem mvqpf.const.map_mk
added def mvqpf.const
added def mvqpf.W_setoid
added theorem mvqpf.Wequiv.abs'
added theorem mvqpf.Wequiv.refl
added theorem mvqpf.Wequiv.symm
added inductive mvqpf.Wequiv
added theorem mvqpf.Wequiv_map
added def mvqpf.Wrepr
added theorem mvqpf.Wrepr_W_mk
added theorem mvqpf.Wrepr_equiv
added def mvqpf.fix.dest
added theorem mvqpf.fix.dest_mk
added def mvqpf.fix.drec
added theorem mvqpf.fix.ind
added theorem mvqpf.fix.ind_aux
added theorem mvqpf.fix.ind_rec
added def mvqpf.fix.map
added def mvqpf.fix.mk
added theorem mvqpf.fix.mk_dest
added def mvqpf.fix.rec
added theorem mvqpf.fix.rec_eq
added theorem mvqpf.fix.rec_unique
added def mvqpf.fix
added def mvqpf.fix_to_W
added def mvqpf.recF
added theorem mvqpf.recF_eq'
added theorem mvqpf.recF_eq
added def mvqpf.prj.P
added def mvqpf.prj.abs
added def mvqpf.prj.map
added def mvqpf.prj.repr
added def mvqpf.prj
added def mvqpf.quot1.map
added def mvqpf.quot1
added def mvqpf.pi
added def mvqpf.sigma
added theorem typevec.drop_fun_diag
added theorem typevec.drop_fun_id
added theorem typevec.drop_fun_prod
added theorem typevec.last_fun_prod
added theorem typevec.prod_map_id