Write a tactic to copy a structure while updating some fields. #1847
Labels
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
t-meta
Tactics, attributes or user commands
Currently we have various functions like
complete_lattice.copy
inorder/filter/basic
andemetric_space.replace_uniformity
intopology/metric_space/emetric_space
. I think that these functions should be generalized to a tactic (copy_struct
?) that does the following:refine_struct
).defeq
to the old one, then create a goal stating that they are actually equal. Otherwise do not treat this field as updated.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.
The text was updated successfully, but these errors were encountered: