max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/library
History
Leonardo de Moura 08169c5ac2 fix(library/unifier): fixes #809 
Daniel is correct when he says the interaction between choice
case-splits, delta case-splits, and coercions can be subtle.

I believe the following condition
https://github.com/leanprover/lean/blob/master/src/frontends/lean/elaborator.cpp#L111
reduces counter-intuitive behavior. Example, the coercion should not
influence the resulting type.
BTW, by removing this condition, many files in the library broke when I
tried to compile from scratch

      make clean-olean
      make

I used the following workaround. Given a delta-delta constraint

           f a =?= f b

If the terms are types, and no case-split will be performed, then
the delta-delta constraint is eagerly solved.
In principle, we don't need the condition that the terms are types.
However, many files break if we remove it. The problem is that many files in the standard
library are abusing the higher-order unification procedure. The
elaboration problems are quite tricky to solve.
I use the extra condition "the terms are types" because usually if they
are, "f" is morally injective, and we don't really want to unfold it.

Note that the following two cases do not work

     check '{1, 2, 3}
     check insert 1 (insert 2 (insert 3 empty))

Well, they work if we the num namespace is open, and they are
interpreted as having type (finset num)
2015-08-31 17:59:30 -10:00
..
blast feat(library/blast): add union-find datastructure 2015-05-11 16:19:51 -07:00
definitional fix(library/definitional/equations): fixes #796 2015-08-14 14:39:23 -07:00
error_handling feat(CMakeLists): add shared library 2015-08-13 11:21:05 -07:00
simplifier feat(CMakeLists): add shared library 2015-08-13 11:21:05 -07:00
tactic feat(library/tactic/apply_tactic): do not report elaboration failure in apply tactic when proof_state.report_failure() is false 2015-08-21 15:45:52 -07:00
abbreviation.cpp feat(library/abbreviation): apply eta-reduction when expanding abbreviations 2015-06-10 14:52:59 -07:00
abbreviation.h feat(library): add 'abbreviation' management module 2015-02-10 17:25:11 -08:00
aliases.cpp refactor(library/aliases): cleanup 2015-08-11 06:41:56 -07:00
aliases.h feat(frontends/lean): allow expressions to be used to define precedence, closes #335 2014-11-29 18:29:48 -08:00
annotation.cpp fix(library/annotation): add missing == and hash methods for annotation class 2015-06-01 11:27:46 -07:00
annotation.h feat(frontends/lean): treat "proof t qed" as alias for "by exact t" 2015-03-05 11:12:39 -08:00
app_builder.cpp feat(library/simplifier): simplification sets for hypothesis and conclusion 2015-07-27 14:59:21 -07:00
app_builder.h feat(library/simplifier): simplification sets for hypothesis and conclusion 2015-07-27 14:59:21 -07:00
bin_app.cpp
bin_app.h feat(library/definitional): add auxiliary functions 2014-12-03 10:28:55 -08:00
choice.cpp feat(library/tactic/rewrite_tactic): display list of overloads occurring in a failed rewrite step 2015-06-14 16:30:18 -07:00
choice.h feat(library/tactic/rewrite_tactic): display list of overloads occurring in a failed rewrite step 2015-06-14 16:30:18 -07:00
choice_iterator.cpp refactor(frontends/lean): move choice_iterator to library 2014-12-19 14:29:32 -08:00
choice_iterator.h refactor(frontends/lean): move choice_iterator to library 2014-12-19 14:29:32 -08:00
class.cpp refactor(library/tc_multigraph): improve tc_multigraph API 2015-07-01 16:01:40 -07:00
class.h feat(library/class): add is_derived_trans_instance predicate 2015-06-30 13:59:02 -07:00
class_instance_synth.cpp feat(library/class): transitive instances 2015-06-27 14:06:56 -07:00
class_instance_synth.h chore(*): fix 'breif' typos 2015-06-08 16:54:55 -07:00
CMakeLists.txt feat(CMakeLists): add shared library 2015-08-13 11:21:05 -07:00
coercion.cpp chore(library/coercion): fix style 2015-08-14 18:49:01 -07:00
coercion.h feat(library/coercion): new coercion manager 2015-07-01 16:32:34 -07:00
composition_manager.cpp fix(library/composition_manager): typo 2015-06-27 14:12:26 -07:00
composition_manager.h feat(library/composition_manager): check if existing definition is definitionally equal 2015-06-21 16:53:08 -07:00
constants.cpp fix(frontends/lean/parser): add support for decimals 2015-08-11 18:44:48 -07:00
constants.h fix(frontends/lean/parser): add support for decimals 2015-08-11 18:44:48 -07:00
constants.txt fix(frontends/lean/parser): add support for decimals 2015-08-11 18:44:48 -07:00
declaration_index.cpp feat(library/declaration_index): add 'a|abbreviation-name|declaration-name' entries in .ilean files 2014-09-04 09:30:25 -07:00
declaration_index.h feat(library/declaration_index): add 'a|abbreviation-name|declaration-name' entries in .ilean files 2014-09-04 09:30:25 -07:00
deep_copy.cpp
deep_copy.h
definition_cache.cpp feat(*): use environment fingerprint to detect when the cache cannot be used because the configuration changed, closes #75 2014-09-29 18:30:00 -07:00
definition_cache.h feat(*): use environment fingerprint to detect when the cache cannot be used because the configuration changed, closes #75 2014-09-29 18:30:00 -07:00
explicit.cpp fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241 2014-10-10 15:41:55 -07:00
explicit.h fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241 2014-10-10 15:41:55 -07:00
export.cpp fix(library/export): typos 2015-08-18 17:49:03 -07:00
export.h feat(library,shell): add --export-all command line option 2015-07-28 15:54:44 -07:00
expr_lt.cpp feat(library/expr_lt): add expression comparison operator that ignores treat level parameters as wildcards 2015-02-10 18:20:10 -08:00
expr_lt.h feat(library/expr_lt): add expression comparison operator that ignores treat level parameters as wildcards 2015-02-10 18:20:10 -08:00
expr_pair.h feat(kernel/default_converter): cache failures for (f t =?= f s) heuristic 2015-06-08 10:41:30 -07:00
expr_pair_maps.h
fingerprint.cpp feat(library): add environment fingerprint 2014-09-29 18:30:00 -07:00
fingerprint.h feat(library): add environment fingerprint 2014-09-29 18:30:00 -07:00
flycheck.cpp feat(frontends/lean): display eval/check/find_decl results using flycheck 2014-11-24 08:35:49 -08:00
flycheck.h fix(library/flycheck): crash when io_state_stream is destroyed before flycheck_scope 2014-12-02 12:11:20 -08:00
generic_exception.cpp refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception 2014-12-15 19:22:17 -08:00
generic_exception.h feat(*): distinguish between logical and runtime exceptions. 2015-01-15 16:54:55 -08:00
head_map.cpp fix(frontends/lean/pp,library/head_map): handle 'as_atomic' annotation 2015-05-29 14:51:28 -07:00
head_map.h feat(library/simplifier): add rewrite rule sets 2015-06-01 15:15:57 -07:00
hott_kernel.cpp feat(kernel/hits): add two builtin HITs: type_quotient and trunc 2015-04-23 15:32:31 -07:00
hott_kernel.h feat(*): add support for separate HoTT library 2014-12-05 14:34:02 -08:00
idx_metavar.cpp fix(library/idx_metavar): compilation problem in debug mode 2015-06-09 14:37:17 -07:00
idx_metavar.h feat(library): add idx_metavar module 2015-06-08 16:02:37 -07:00
inductive_unifier_plugin.cpp fix(library/inductive_unifier_plugin): avoid potential assertion violation 2015-06-26 17:18:29 -07:00
inductive_unifier_plugin.h
init_module.cpp feat(library): add module for tracking noncomputable definitions 2015-07-28 18:15:26 -07:00
init_module.h refactor(*): start move to explicit initialization/finalization, 2014-09-22 10:41:07 -07:00
io_state.cpp refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
io_state.h refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
io_state_stream.cpp refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception 2014-12-15 19:22:17 -08:00
io_state_stream.h refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception 2014-12-15 19:22:17 -08:00
kernel_bindings.cpp refactor(kernel/inductive): use local constants to represent introduction rules 2015-08-25 03:46:28 -07:00
kernel_bindings.h refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
kernel_serializer.cpp refactor(kernel/inductive): use local constants to represent introduction rules 2015-08-25 03:46:28 -07:00
kernel_serializer.h feat(library/module): efficient inductive_reader 2015-08-15 14:48:49 -07:00
let.cpp fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
let.h refactor(*): explicit initialization/finalization for serialization 2014-09-22 15:26:41 -07:00
level_names.cpp refactor(kernel/inductive): use local constants to represent introduction rules 2015-08-25 03:46:28 -07:00
level_names.h
local_context.cpp refactor(library/local_context): avoid hack in local_context 2015-06-18 15:41:00 -07:00
local_context.h refactor(library/local_context): avoid hack in local_context 2015-06-18 15:41:00 -07:00
locals.cpp feat(library/tactic/congruence_tactic): add congruence lemma generator 2015-06-05 22:00:10 -07:00
locals.h feat(library/tactic/congruence_tactic): add congruence lemma generator 2015-06-05 22:00:10 -07:00
match.cpp feat(library): add idx_metavar module 2015-06-08 16:02:37 -07:00
match.h feat(library): add idx_metavar module 2015-06-08 16:02:37 -07:00
max_sharing.cpp feat(library/max_sharing): maximize sharing in universe level expressions 2015-05-06 14:26:12 -07:00
max_sharing.h
metavar_closure.cpp refactor(*): start process for eliminating of opaque definitions from the kernel 2015-05-08 16:06:04 -07:00
metavar_closure.h refactor(*): start process for eliminating of opaque definitions from the kernel 2015-05-08 16:06:04 -07:00
module.cpp feat(library/module): efficient inductive_reader 2015-08-15 14:48:49 -07:00
module.h feat(kernel,library/module): only module reader can add declarations without type-checking them 2015-08-14 18:37:17 -07:00
noncomputable.cpp feat(library): add 'noncomputable' keyword for the standard library 2015-07-28 21:56:35 -07:00
noncomputable.h feat(library): add 'noncomputable' keyword for the standard library 2015-07-28 21:56:35 -07:00
normalize.cpp fix(library/normalize): fixes #801 2015-08-16 14:22:02 -07:00
normalize.h feat(library/definitional/no_confusion): add [unfold] hint to no_confusion 2015-07-07 20:07:13 -07:00
num.cpp refactor(*): add file constants.txt with all constants used by the Lean binary 2015-01-23 16:50:32 -08:00
num.h refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
occurs.cpp
occurs.h
parser_nested_exception.h feat(*): distinguish between logical and runtime exceptions. 2015-01-15 16:54:55 -08:00
placeholder.cpp refactor(*): remove dependency to thread_local C++11 keyword, the 2014-09-24 12:51:04 -07:00
placeholder.h refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
pp_options.cpp feat(library/pp_options): add 'pp.all' option 2015-06-05 08:41:46 -07:00
pp_options.h feat(library/pp_options): add 'pp.all' option 2015-06-05 08:41:46 -07:00
print.cpp fix(library/print): typo in is_used_name 2015-01-25 08:58:08 -08:00
print.h refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
private.cpp fix(library/private): use environment fingerprint to compute private decls "unique" identifier 2015-06-01 22:21:31 -07:00
private.h refactor(*): explicit initialization/finalization for environment extensions 2014-09-22 17:30:29 -07:00
projection.cpp refactor(library/projection): remove projection macro from library 2015-07-02 08:48:13 -07:00
projection.h refactor(library/projection): remove projection macro from library 2015-07-02 08:48:13 -07:00
protected.cpp fix(frontends/lean): consistent behavior for protected declarations 2015-05-18 22:35:18 -07:00
protected.h fix(frontends/lean): consistent behavior for protected declarations 2015-05-18 22:35:18 -07:00
reducible.cpp feat(frontends/lean/builtin_cmds): add 'print [reducible]', 'print [irreducible]' and 'print [quasireducible]' commands 2015-05-29 16:47:29 -07:00
reducible.h refactor(library/tactic/induction_tactic): cleanup 2015-06-22 10:23:54 -07:00
register_module.h chore(library/coercion): remove lua bindings for coercion module 2015-07-01 14:08:49 -07:00
relation_manager.cpp refactor(library/relation_manager): cleanup and add API for declaring a relation that may not be reflexive, symmetric nor transitive 2015-07-07 15:58:24 -07:00
relation_manager.h feat(library/simplifier): simplification sets for hypothesis and conclusion 2015-07-27 14:59:21 -07:00
replace_visitor.cpp refactor(kernel): replace_visitor doesn't need to be in the kernel anymore 2014-10-17 10:23:35 -07:00
replace_visitor.h refactor(kernel): replace_visitor doesn't need to be in the kernel anymore 2014-10-17 10:23:35 -07:00
resolve_macro.cpp fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
resolve_macro.h refactor(*): explicit initialization/finalization for serialization 2014-09-22 15:26:41 -07:00
scoped_ext.cpp feat(frontends/lean/decl_cmds): closes #791 2015-08-11 17:53:33 -07:00
scoped_ext.h feat(frontends/lean): add 'wait' command 2015-05-08 20:05:21 -07:00
shared_environment.cpp
shared_environment.h fix(library/shared_environment): compilation warning 2015-08-17 08:41:12 -07:00
sorry.cpp refactor(kernel): rename var_decl to constant_assumption 2014-10-02 17:55:34 -07:00
sorry.h feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message 2014-09-30 18:04:04 -07:00
standard_kernel.cpp feat(kernel): add experimental support for quotient types 2015-03-31 22:04:16 -07:00
standard_kernel.h
string.cpp fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
string.h refactor(*): explicit initialization/finalization for serialization 2014-09-22 15:26:41 -07:00
tc_multigraph.cpp feat(library/coercion): new coercion manager 2015-07-01 16:32:34 -07:00
tc_multigraph.h feat(library/coercion): new coercion manager 2015-07-01 16:32:34 -07:00
type_util.cpp
type_util.h
typed_expr.cpp fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
typed_expr.h refactor(*): explicit initialization/finalization for serialization 2014-09-22 15:26:41 -07:00
unfold_macros.cpp fix(library/unfold_macros): fixes #806 2015-08-18 17:46:47 -07:00
unfold_macros.h feat(library): export environment in textual format 2015-05-04 18:05:00 -07:00
unifier.cpp fix(library/unifier): fixes #809 2015-08-31 17:59:30 -10:00
unifier.h fix(library/unifier): fixes #705 2015-06-26 19:10:46 -07:00
unifier_plugin.cpp refactor(*): clarify name_generator ownership 2015-05-21 14:32:36 -07:00
unifier_plugin.h refactor(*): clarify name_generator ownership 2015-05-21 14:32:36 -07:00
unsolved_metavar_exception.h feat(*): distinguish between logical and runtime exceptions. 2015-01-15 16:54:55 -08:00
update_declaration.cpp refactor(kernel): rename get_weight to get_height at declaration 2015-06-30 12:59:10 -07:00
update_declaration.h
user_recursors.cpp feat(library/user_recursors): add is_user_defined_recursor predicate 2015-07-12 11:25:50 -04:00
user_recursors.h feat(library/user_recursors): add is_user_defined_recursor predicate 2015-07-12 11:25:50 -04:00
util.cpp fix(library/util): fixes #751 2015-07-28 16:30:20 -07:00
util.h feat(library/simplifier): add simplifier procedure skeleton 2015-07-21 15:08:56 -07:00