michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
7231 commits 3 branches 0 tags 28 MiB
Commit graph

7231 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jeremy Avigad
93c2d1e9d0 refactor(library/algebra/ordered_field): rename theorems to maintain consistency with other parts of the library 2015-09-01 14:47:19 -07:00
Jeremy Avigad
92af727daf fix(library/data/real/{basic,division,order}: use notation for 0 and 1 
These changes were needed because e.g. real.add_zero was "x + zero = x", and rewrite
would not match it to a goal "t + 0".

The fix was a lot harder than I expected. At first, migrate failed with resource
errors. In the end, what worked was this: I defined the coercion from num to real
directly (rather than infer num -> nat -> int -> rat -> real).

I still don't understand what the issues are, though. There are subtle issues with
numerals and coercions and migrate.

(We are not alone. Isabelle also suffers from the fact that there are too many
"zero"s and "one"s.)
 2015-09-01 14:47:19 -07:00
Joe Hendrix
79b77b1011 fix(api): lean_ios_is_std returned incorrect result 2015-09-01 14:40:39 -07:00
Joe Hendrix
91dc9c7bd9 fix(api): fix typos in function name and comment 2015-09-01 14:40:34 -07:00
Leonardo de Moura
c84e886c7b fix(frontends/lean/notation_cmd): fixes #808 
This commit and 2b1d2c fixes #808
 2015-08-31 18:05:58 -10:00
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
Leonardo de Moura
3b19de1974 feat(library/data/num): show that num has decidable equality 2015-08-31 17:47:07 -10:00
Leonardo de Moura
63b93cf762 refactor(library/data/set/finite): make proof more robust 2015-08-31 17:26:24 -10:00
Leonardo de Moura
92716972c0 refactor(library/data/hf): add local attribute to make proofs more robust 2015-08-31 17:06:54 -10:00
Leonardo de Moura
f74d7fc266 refactor(library/data/real/basic): add extra step to help unifier 2015-08-31 16:56:05 -10:00
Leonardo de Moura
e01b155b2e refactor(library/data/int/basic): cleanup proof 
Proof was abusing the higher-order unifier
 2015-08-31 16:53:11 -10:00
Leonardo de Moura
2b1d2c21ad fix(frontends/lean/util): bug when parsing priorities and numerals are overloaded 2015-08-31 15:08:21 -10:00
Leonardo de Moura
ea05ce7fe9 fix(library/data/real/order): mark '2' as local notation 2015-08-31 15:03:18 -10:00
Leonardo de Moura
86b10ab184 feat(library/data): define perm as a special kind of equiv 
This commit also proves the basic permutation lemmas in the nominal isabelle library.
 2015-08-27 06:06:02 -10:00
Leonardo de Moura
0fb52a9a13 feat(api): add lean_get_recursor_name 2015-08-25 03:46:28 -07:00
Leonardo de Moura
1299e6ab24 test(tests/shared/env): add inductive types test 2015-08-25 03:46:28 -07:00
Leonardo de Moura
bdd8fae14d feat(api): add lean_inductive API 2015-08-25 03:46:28 -07:00
Leonardo de Moura
45163acf25 refactor(kernel/inductive): use local constants to represent introduction rules 2015-08-25 03:46:28 -07:00
Leonardo de Moura
3c4b3c1ad6 test(tests/shared/env): add total order simple tests 2015-08-23 19:55:45 -07:00
Leonardo de Moura
78e9a57e06 feat(api): add total orders for lean_name, lean_univ and lean_expr APIs 2015-08-23 19:42:22 -07:00
Leonardo de Moura
8c30067f8c fix(util/stackinfo): lazy thread initialization 
We also add a multithread example for the C API.
This example reproduces a problem reported by Joe Hendrix.
 2015-08-23 19:08:02 -07:00
Leonardo de Moura
e03c0ae93d chore(api/module): fix style 2015-08-23 09:55:25 -07:00
Leonardo de Moura
38b0a6e22c test(tests/shared/env): add type checker tests 2015-08-23 09:49:33 -07:00
Leonardo de Moura
23a490f3f1 feat(api): add lean_type_checker API 2015-08-23 09:34:31 -07:00
Leonardo de Moura
2926b41e9f fix(tests/shared/env): memory leak 2015-08-23 09:24:05 -07:00
Leonardo de Moura
b42e561bb1 feat(api): expose lean_expr pretty printing function 2015-08-23 09:09:17 -07:00
Leonardo de Moura
3798493d99 test(tests/shared/env): add import module test 2015-08-23 08:54:11 -07:00
Leonardo de Moura
6f78304f31 feat(api): APIs for importing/exporting modules 2015-08-23 08:30:55 -07:00
Leonardo de Moura
5263ef4a74 feat(api): add lean_ios API 2015-08-23 08:19:25 -07:00
Leonardo de Moura
98a27c53de refactor(api/env): use module procedures 2015-08-23 07:49:06 -07:00
Leonardo de Moura
c83b72e9b6 test(tests/shared/env): add tests for lean_env API 2015-08-22 13:35:35 -07:00
Leonardo de Moura
0aff6bd747 feat(api): add lean_env API 2015-08-22 12:37:22 -07:00
Leonardo de Moura
62e396bec6 test(tests/shared): add some tests for lean_expr C API 2015-08-22 11:08:07 -07:00
Leonardo de Moura
a7e4cd94c2 feat(api): add lean_decl API 2015-08-22 10:41:33 -07:00
Leonardo de Moura
8272ff61f6 fix(tests/shared/name): access violation 2015-08-21 18:33:06 -07:00
Leonardo de Moura
2b6033f42e feat(api): add lean_expr API 2015-08-21 17:45:13 -07:00
Leonardo de Moura
a3c404ac3b 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
Leonardo de Moura
9bae1eee29 feat(api/univ): add lean_list_univ API 2015-08-21 15:25:12 -07:00
Leonardo de Moura
35d3c6f5a5 test(tests/shared/name): add tests for lean_list_name API 2015-08-21 15:12:43 -07:00
Leonardo de Moura
adeba5c05e feat(api/name): add lean_list_name API 2015-08-21 15:04:19 -07:00
Leonardo de Moura
453bd2341d chore(README): remove coveralls "badge" 
The coveralls website is having technical problems.
We will restore the link after they fix it.
 2015-08-20 18:00:15 -07:00
Leonardo de Moura
3747ba095a fix(frontends/lean/elaborator): incorrect assertion 
It is supposed to be "!first implies is_local(from)"

fixes #807
 2015-08-20 17:56:20 -07:00
Leonardo de Moura
c32a95bb13 chore(tests/shared/options): fix compilation warning 2015-08-19 08:13:58 -07:00
Leonardo de Moura
87349dc355 feat(frontends/lean/token_table): add 'proposition' keyword 2015-08-19 08:05:31 -07:00
Leonardo de Moura
3a72cd9621 fix(frontends/lean): rename multiword keyword "suffices to show" to "suffices" 2015-08-18 17:57:53 -07:00
Daniel Selsam
0942e94321 fix(library/export): typos 2015-08-18 17:49:03 -07:00
Leonardo de Moura
2b52198702 fix(library/unfold_macros): fixes #806 2015-08-18 17:46:47 -07:00
Leonardo de Moura
3ce8c5d6f7 feat(frontends/lean): add "suffices to show A, from B, C" construct 2015-08-18 17:04:38 -07:00
Leonardo de Moura
a18983c1aa fix(api/lean_univ): typo 2015-08-18 16:01:50 -07:00
Leonardo de Moura
858971c3a5 test(tests/shared): add test for the universe C API 2015-08-18 15:32:27 -07:00