mathlib

mathlib copied to clipboard

Currently we have various functions like complete_lattice.copy in order/filter/basic and emetric_space.replace_uniformity in topology/metric_space/emetric_space. I think that these functions should be generalized to a tactic (copy_struct?) that does the following:

1. Takes a structure and a partially filled structure (like in refine_struct).
2. Add all explicitly specified fields to the resulting structure.
3. For each updated field test if the new value is not defeq to the old one, then create a goal stating that they are actually equal. Otherwise do not treat this field as updated.
4. For other fields: a) if its type does not depend on updated fields, then copy it from the old structure; b) otherwise if its type is a Type*, fail; the user should explicitly specify the desired value in this case; c) otherwise prove this proposition using some rewrites on equalities from step 2.