Sebastian Ullrich
84997bf4de
refactor(init/meta/expr): unify expr and pexpr
2017-05-17 10:38:12 -07:00
Leonardo de Moura
cb6d5675df
chore(library/init): ^. ==> .
2017-05-16 15:00:58 -07:00
Mario Carneiro
6b28499e47
feat(init/data/list,data/list): new basic list operations from haskell
2017-05-16 14:38:43 -07:00
Leonardo de Moura
0091cef9f2
feat(library/tactic): start algebraic normalizer
2017-05-15 21:46:19 -07:00
Leonardo de Moura
4575c9e038
feat(frontends/lean): swap (t) and ``(t) semantics
2017-05-15 09:41:31 -07:00
Mario Carneiro
7ace147f25
refactor(init/meta/tactic): replace assertv -> note, definev -> pose
2017-05-14 19:34:27 -07:00
Sebastian Ullrich
27c1d2f4fb
fix(init/meta/interactive): simp: accept local refs as simp names
2017-05-14 19:19:22 -07:00
Sebastian Ullrich
eb60df4409
fix(init/meta/interactive): case didn't find some cases
2017-05-14 19:19:22 -07:00
Sebastian Ullrich
808ab73d93
refactor(init): use list for expr.macro args
2017-05-14 19:17:28 -07:00
Sebastian Ullrich
42eb0c680e
feat(kernel/inductive,library/inductive_compiler): do not enforce positivity rule on meta inductives
2017-05-14 19:17:28 -07:00
Sebastian Ullrich
171a96a8de
refactor(library): remove all instances of `(...)
2017-05-12 19:13:48 +02:00
Sebastian Ullrich
4b21b13649
refactor(init): replace has_quote class with reflected
2017-05-09 16:02:42 -07:00
Sebastian Ullrich
ead6318ee0
feat(frontends/lean/elaborator): substitute reflected locals into expr quotes
2017-05-09 16:02:41 -07:00
Sebastian Ullrich
2825c5fbcc
feat(frontends/lean/elaborator): elaborate ``(e) to type reflected e` if possible and add coercion reflected -> expr
2017-05-09 16:02:41 -07:00
Daniel Selsam
d727abeefc
chore(library/inductive_compiler/nested.cpp): prove all theorems in C++
2017-05-04 16:34:32 -07:00
Sebastian Ullrich
d0c2c73b35
refactor(init/meta,tools): rename now tactic to done
...
It was pointed out that Coq already uses `now` for a different kind of tactic.
And `done` is more descriptive anyway.
2017-05-03 11:18:31 +02:00
Leonardo de Moura
55fee26b36
feat(library/class): add attribute for tracking symbols occurring in instances of type classes
...
For more information see:
https://github.com/leanprover/lean/wiki/Refactoring-structures
The new attribute [algebra] implements the [algebraic_class] described
in the page above.
2017-05-01 18:02:30 -07:00
Leonardo de Moura
f6b47ea5c7
feat(library/init/category): add has_map type class, delete fmap
2017-05-01 10:13:02 -07:00
Leonardo de Moura
5cef84709f
refactor(library): avoid auxiliary definitions such as add/mul/le/etc
...
See Section "Other goodies" at
https://github.com/leanprover/lean/wiki/Refactoring-structures
This commit also improves the support for projections in the
unifier/matcher.
Now, we consider the extra case-split for projections.
Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce.
This is needed in the standard library because we now have constraints such as:
```
@has_le.le ?A ?s ?a ?b =?= @has_le.le nat nat.has_add x y
```
If we reduce the right hand side, we get the unsolvable constraint
```
@has_le.le ?A ?s ?a ?b =?= nat.le x y
```
Before this change, the constraint was `@le ?A ?s ?a ?b =?= @le nat nat.has_add x y`, and we already perform a case-split in this case.
Moreover, projections were eagerly reduced whenever possible.
The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out.
I worked around this issue by performing the case-split only when the constraint contains meta-variables.
There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`.
2017-05-01 08:52:19 -07:00
Leonardo de Moura
fc9a8ed3be
fix(library/init/meta/smt): fail tactic result type
2017-04-30 14:39:51 -07:00
Sebastian Ullrich
0ca6e2c96f
refactor(library/{type_context,compiler/preprocess},frontends/lean/elaborator): use opaque, general type class instead of special app elaboration for eval_expr
2017-04-27 16:04:59 -07:00
Sebastian Ullrich
4479eebaf0
feat(init/meta/{environment,pexpr}): expose some structure APIs
2017-04-27 16:04:41 -07:00
Leonardo de Moura
cabb4350d9
feat(library): instances are not reducible by default anymore
...
Motivation: see "Other goodies" section at
https://github.com/leanprover/lean/wiki/Refactoring-structures
We had to add a new transparency mode: Instances at type_context.
In this mode, instances and reducible definitions are considered
transparent.
The new mode is used in the defeq_canonizer, code generator,
and sizeof lemma generation at inductive_compiler.
We also use the new mode in the unfold tactics.
2017-04-26 14:10:11 -07:00
Leonardo de Moura
08e094139d
feat(library/init/meta): add by_contradiction and by_cases to tactic.interactive
2017-04-26 12:54:52 -07:00
Johannes Hölzl
b27100ec5a
fix(library/init/meta/transfer): add check if target contains (universe) meta variables (see #1535 )
2017-04-25 17:46:48 -07:00
Mario Carneiro
7ef4428124
add new interactive tactics skip, ginduction, exacts
2017-04-23 11:48:33 -07:00
Sebastian Ullrich
b3884d5f42
refactor(init/meta/interactive,frontends/lean/token_table): introduce generalizing keyword in Lean
2017-04-16 15:11:49 -07:00
Leonardo de Moura
210b7c8fb7
fix(library/tactic): fixes #1513
...
Implement rename tactic in Lean using revert/intro
2017-04-15 11:34:24 -07:00
Sebastian Ullrich
8ea2bc08cb
feat(init/meta/interactive): add generalizing parameter to induction
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
70a2c402ac
feat(init/meta/interactive): Isabelle-like case tactic
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
c8c8c27654
feat(init/meta): add has_to_format instances and prefer direct has_to_tactic_format implementations
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
026c5ee509
fix(library/init/meta/expr,library/vm/vm_expr): fix macro args
2017-04-11 17:07:28 -07:00
Leonardo de Moura
ad859817b1
feat(frontends/lean): allow local decls to shadow namespaces
2017-03-29 16:09:45 -07:00
Leonardo de Moura
71685e4dd6
feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term
...
Replace `^.` with `.` in the stdlib
2017-03-28 17:47:49 -07:00
Leonardo de Moura
87932f1c56
feat(frontends/lean): change notation for inaccessible patterns
...
The following are accepted
.(t)
._
We don't accept .t anymore because it will conflict with the field
access notation.
2017-03-28 16:09:15 -07:00
Leonardo de Moura
6183c7676e
feat(frontends/lean): use . for field access
2017-03-28 15:29:54 -07:00
Leonardo de Moura
8e2dcb8ad8
chore(frontends/lean): remove ^. variants (~> and ↣)
...
This modification was motivated by a discussion at slack.
2017-03-28 12:23:33 -07:00
Leonardo de Moura
1cef8af1be
feat(library/tactic/simplify): add eta := tt to simp
2017-03-27 17:38:40 -07:00
Leonardo de Moura
eea46610ea
fix(library/tactic/simplify): missing projection reduction, add proj := tt to simp
2017-03-27 17:38:40 -07:00
Leonardo de Moura
161879b1bf
feat(library/init/meta): add helper tactic guard_target for generating tests
2017-03-27 17:38:40 -07:00
Leonardo de Moura
b09968a37b
feat(library/tactic/simplify): add beta := tt to simp
2017-03-27 17:38:31 -07:00
Leonardo de Moura
494e5b65c5
feat(library/init/meta/tactic): add apply_auto_param and apply_opt_param tactics
...
see #1485
2017-03-27 13:42:08 -07:00
Sebastian Ullrich
b3a0eb9bfc
fix(init/meta/interactive): mk_simp_set: also remove equational lemmas
2017-03-27 13:42:08 -07:00
Sebastian Ullrich
c7b47c7b7f
fix(system/io): try to fix io monad
2017-03-27 13:42:08 -07:00
Sebastian Ullrich
dfd84666e2
feat(library): add functor, applicative, and monad laws, and prove them correct for non-meta instances
2017-03-27 13:42:08 -07:00
Sebastian Ullrich
3ead6be9ca
feat(init): add default value proofs to the monadic hierarchy
2017-03-27 13:42:08 -07:00
Gabriel Ebner
a8ba78e20a
refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic
2017-03-23 09:07:08 +01:00
Gabriel Ebner
098d6f8f2a
refactor(init/meta/tactic): remove report_errors argument from to_expr
2017-03-23 09:03:42 +01:00
Gabriel Ebner
c8fff9f4ff
refactor(init/meta/interaction_monad): replace rstep by istep
2017-03-23 09:03:41 +01:00
Sebastian Ullrich
a5db5ae4de
refactor(init/meta/interactive): rw: parse - separately to remove hack
2017-03-22 07:54:12 -07:00
