Commit 2024-02-21 19:28 ffbaf173

View on Github →

fix: refactor of fun_prop and several bug fixes (#10724) fix: refactor of fun_prop and several bug fixes

  1. support for proving recursive functions fun_prop correctly uses local hypothesis coming from induction step
  2. unfolds let variables when necessary
  3. unfolds id, Function.comp, Function.uncurry, HasUncurry.uncurry Many theorems in mathlib are stated using id, Function.comp etc. to prevent restating all these theorems fun_prop just unfolds these common functions.
  4. does not get blocked by autoParam or outParam
  5. support for custom bundled morphism coercions. DFunLike.coe is not hardcoded anymore and any morphism coercion can be registered with @[fun_prop_coe] attribute
  6. internal counter to prevent infinite loops

Estimated changes

deleted inductive StateList
deleted def StateListM
deleted def StateListT.run'
deleted def StateListT.run
deleted def StateListT
modified theorem Con_id
added theorem Con_let
added def LinHom.mk'
modified theorem Lin_comp
modified theorem add_Con
added theorem add_Lin'
added theorem add_Lin
added def bar
added theorem bar_lin
added theorem conHom_lin_in_fn'
added def diag
added theorem diag_Con
added theorem foo1_lin
added theorem foo2_lin
added def foo3
added def foo
added theorem foo_lin
added def iterate
added theorem iterate_con
added theorem kaboom
added theorem linHom_lin_in_fn'
added theorem linHom_mk'
added def myUncurry