leanprover/lean — pull request #351 by avigad (2014-11-28 15:38:03+00:00)
Title: cleaned up notation, introduced basic properties for binary operations, clean up classes for equivalence relations and congruences

I invested considerable time cleaning up the classes for equivalence relations and congruences. I have two questions.

(1) Leo, I noticed that you created another "relations" file in the logic directory. I propose merging this with algebra/relation, and moving all the classes (for equivalence and congruence) now in algebra/relation to a new file, algebra/equivalence_relation. Let me know if I should do that.

(2) Right now, to use substitution for iff and other congruence relations, we have to "open relation" to get all the instances. See, for example, logic/examples/instances_test. Should I put all the classes and instances at the top level, so we do not have to do that?

I have a new bug report: with this version of the repository, if I load data/int/basic and introduce an error anywhere in the file (by typing random characters in the middle of an existing proof), Flycheck fails and I get an error message like the one below. Let me know if I should investigate further.

Checker lean-checker returned non-zero exit code 1, but no errors from output: [93/110] generating dep... /home/avigad/projects/lean/library/data/int/flycheck_basic.d

[<__main__.FlycheckItem instance at 0xb6de1a8c>, <__main__.FlycheckItem instance at 0xb6de14ec>, <__main__.FlycheckItem instance at 0xb6de142c>, <__main__.FlycheckItem instance at 0xb6de146c>, <__main__.FlycheckItem instance at 0xb6de19ac>, <__main__.FlycheckItem instance at 0xb6de1aac>, <__main__.FlycheckItem instance at 0xb6de1aec>, <__main__.FlycheckItem instance at 0xb6de1b2c>, <__main__.FlycheckItem instance at 0xb6de1b6c>, <__main__.FlycheckItem instance at 0xb6de1bac>, <__main__.FlycheckItem instance at 0xb6de1bec>, <__main__.FlycheckItem instance at 0xb6de1c2c>, <__main__.FlycheckItem instance at 0xb6e2918c>, <__main__.FlycheckItem instance at 0xb6e2908c>, <__main__.FlycheckItem instance at 0xb6e2942c>, <__main__.FlycheckItem instance at 0xb6e2944c>, <__main__.FlycheckItem instance at 0xb6e2930c>, <__main__.FlycheckItem instance at 0xb6e22fac>, <__main__.FlycheckItem instance at 0xb6e2916c>, <__main__.FlycheckItem instance at 0xb6dd26cc>, <__main__.FlycheckItem instance at 0xb6dd260c>, <__main__.FlycheckItem instance at 0xb6dd254c>, <__main__.FlycheckItem instance at 0xb6dd248c>, <__main__.FlycheckItem instance at 0xb6dd23cc>, <__main__.FlycheckItem instance at 0xb6dd232c>, <__main__.FlycheckItem instance at 0xb6dd22ac>, <__main__.FlycheckItem instance at 0xb6dd226c>, <__main__.FlycheckItem instance at 0xb6dd228c>, <__main__.FlycheckItem instance at 0xb6dd252c>, <__main__.FlycheckItem instance at 0xb6dd25cc>, <__main__.FlycheckItem instance at 0xb6dd230c>, <__main__.FlycheckItem instance at 0xb6dd246c>, <__main__.FlycheckItem instance at 0xb6de1c8c>, <__main__.FlycheckItem instance at 0xb6dd250c>, <__main__.FlycheckItem instance at 0xb6dd274c>, <__main__.FlycheckItem instance at 0xb6dd276c>, <__main__.FlycheckItem instance at 0xb6de1cec>, <__main__.FlycheckItem instance at 0xb6de1d2c>, <__main__.FlycheckItem instance at 0xb6de1e0c>, <__main__.FlycheckItem instance at 0xb6de1e4c>, <__main__.FlycheckItem instance at 0xb6de1d6c>, <__main__.FlycheckItem instance at 0xb6de1dac>, <__main__.FlycheckItem instance at 0xb6de1dec>, <__main__.FlycheckItem instance at 0xb6de1eac>, <__main__.FlycheckItem instance at 0xb6de1eec>, <__main__.FlycheckItem instance at 0xb6de1f2c>, <__main__.FlycheckItem instance at 0xb6de1f6c>, <__main__.FlycheckItem instance at 0xb6de1fac>, <__main__.FlycheckItem instance at 0xb6de1fec>, <__main__.FlycheckItem instance at 0xb6de1c6c>, <__main__.FlycheckItem instance at 0xb6e0608c>, <__main__.FlycheckItem instance at 0xb6e060cc>, <__main__.FlycheckItem instance at 0xb6e0610c>, <__main__.FlycheckItem instance at 0xb6e0614c>, <__main__.FlycheckItem instance at 0xb6e0618c>, <__main__.FlycheckItem instance at 0xb6e061cc>, <__main__.FlycheckItem instance at 0xb6e0620c>, <__main__.FlycheckItem instance at 0xb6e0624c>, <__main__.FlycheckItem instance at 0xb6e0628c>, <__main__.FlycheckItem instance at 0xb6e062cc>, <__main__.FlycheckItem instance at 0xb6e0630c>, <__main__.FlycheckItem instance at 0xb6e0634c>, <__main__.FlycheckItem instance at 0xb6e0638c>, <__main__.FlycheckItem instance at 0xb6e063cc>, <__main__.FlycheckItem instance at 0xb6e0640c>, <__main__.FlycheckItem instance at 0xb6e0644c>, <__main__.FlycheckItem instance at 0xb6e0648c>, <__main__.FlycheckItem instance at 0xb6e064cc>, <__main__.FlycheckItem instance at 0xb6e0650c>, <__main__.FlycheckItem instance at 0xb6e0654c>, <__main__.FlycheckItem instance at 0xb6e0658c>, <__main__.FlycheckItem instance at 0xb6e065cc>, <__main__.FlycheckItem instance at 0xb6e0660c>, <__main__.FlycheckItem instance at 0xb6e0664c>, <__main__.FlycheckItem instance at 0xb6e0668c>, <__main__.FlycheckItem instance at 0xb6e066cc>, <__main__.FlycheckItem instance at 0xb6e067ac>, <__main__.FlycheckItem instance at 0xb6e067ec>, <__main__.FlycheckItem instance at 0xb6e0670c>, <__main__.FlycheckItem instance at 0xb6e0674c>, <__main__.FlycheckItem instance at 0xb6e068ec>, <__main__.FlycheckItem instance at 0xb6e0678c>, <__main__.FlycheckItem instance at 0xb6e068ac>, <__main__.FlycheckItem instance at 0xb6e0684c>, <__main__.FlycheckItem instance at 0xb6e0688c>, <__main__.FlycheckItem instance at 0xb6e0694c>, <__main__.FlycheckItem instance at 0xb6e0698c>, <__main__.FlycheckItem instance at 0xb6e069cc>, <__main__.FlycheckItem instance at 0xb6e06a0c>, <__main__.FlycheckItem instance at 0xb6e06a4c>, <__main__.FlycheckItem instance at 0xb6e06a8c>, <__main__.FlycheckItem instance at 0xb6e06b6c>, <__main__.FlycheckItem instance at 0xb6e06acc>, <__main__.FlycheckItem instance at 0xb6e06b0c>, <__main__.FlycheckItem instance at 0xb6e06b4c>, <__main__.FlycheckItem instance at 0xb6e06c6c>, <__main__.FlycheckItem instance at 0xb6e06bcc>, <__main__.FlycheckItem instance at 0xb6e06cec>, <__main__.FlycheckItem instance at 0xb6e06c0c>, <__main__.FlycheckItem instance at 0xb6e06dac>, <__main__.FlycheckItem instance at 0xb6dd2d0c>]

Checker definition probably flawed.