Leonardo de Moura
d8fa93b4a2
feat(library/init/meta/tactic): add dependent parameters for empty introv
2017-05-31 15:10:07 -07:00
Leonardo de Moura
1c6e70d170
feat(library/init/meta): introv tactic
...
@Armael: this commit implements the `introv` tactic.
The implementation uses an auxiliary `intros_dep` that introduces new
hypotheses with forward dependencies.
The `tactic.introv` tactic implemented at library/init/meta/tactic.lean
is the main implementation, but it is not nice for interactive use since
users would have to write
```
tactic.introv [`h1, `h2]
```
To make it more conveninent to use, we define another
```
meta def introv (ns : parse ident_*) : tactic unit :=
tactic.introv ns >> return ()
```
This one is in the namespace `tactic.interactive`, and
uses parser extensions. The argument `parse ident_*` instructs
the parser to parse 0 or more identifiers and create a term
of type `list name` containing these identifiers.
2017-05-31 14:09:25 -07:00
Leonardo de Moura
71ef240817
feat(library/init/meta/interactive): add nary existsi
...
@Armael, this commit implements the nary existsi.
We can now write
a) existsi t
b) existsi [t_1, t_2, t_3]
2017-05-31 13:41:25 -07:00
Jared Roesch
0a6a6d8676
chore(*): remove mini_crush
2017-05-31 10:10:47 -07:00
Jared Roesch
b33af82bc9
chore(*): remove super
2017-05-31 10:10:47 -07:00
Leonardo de Moura
d3298d518c
fix(library/equations_compiler/elim_match): whnf_pattern
2017-05-31 10:02:59 -07:00
Gabriel Ebner
b1e417805e
fix(frontends/lean/scanner): do not treat 0xFF as end-of-file
...
Fixes #1624 . We just replace 0xFF by 0x00 when reading a new input
byte. This shows up as an unexpected token error.
2017-05-31 16:54:04 +02:00
Sebastian Ullrich
834375a042
fix(library/eval_helper): evaluating tactics
2017-05-31 16:18:15 +02:00
Leonardo de Moura
00b4d4bdf6
test(tests/lean/run/psum_wf_rec): add example used on Slack to test suite
2017-05-30 16:59:35 -07:00
Leonardo de Moura
72134a7bbd
feat(library/equations_compiler/wf_rec): provide recursive equations to rel_tac
...
rel_tac is a tactic used for synthesizing a well founded relation.
The default implementation just uses type class resolution.
More sophisticated strategies may need to access the set of recursive
equations. This commit addresses this need.
2017-05-30 16:55:37 -07:00
Leonardo de Moura
d0eb7d2ed3
chore(tests/lean/run/252): fix test
2017-05-30 13:11:59 -07:00
Sebastian Ullrich
4eab11ec3d
fix(frontends/lean/structure_cmd): even less error recovery
2017-05-30 19:02:25 +02:00
Gabriel Ebner
b14a248dcd
fix(frontends/lean/structure_cmd): segfault
2017-05-29 07:37:50 +02:00
Leonardo de Moura
d10a799b79
chore(tests/lean/interactive/complete_field): fix test
2017-05-27 10:18:44 -07:00
Leonardo de Moura
1ee1e01f8c
feat(library/tactic/smt/congruence_closure): add builtin support for (@ne A a b)
...
This is needed when using cc in the standard tactic monad.
closes #1608
2017-05-26 17:06:22 -07:00
Leonardo de Moura
82e51ddad5
fix(library/constructions/injective): fixes #1609
...
@dselsam You have assumed that the left-hand-side (t) and
right-hand-side (s) of (t = s) and (t == s) are the last two arguments.
This is a reasonable assumption, and it is correct for eq, but it is
incorrect for heq.
The type of heq is
```
Π {α : Sort u_1}, α → Π {β : Sort u_1}, β → Prop
```
Do you recall other places where we may have made this assumption?
2017-05-26 16:39:38 -07:00
Leonardo de Moura
a31e3a95ae
feat(library/equations_compiler/wf_rec): improve error message for failed decreasing proofs
2017-05-26 13:55:29 -07:00
Leonardo de Moura
4bdb2da1b6
fix(library/equations_compiler): improve pull_nested_rec_fn, and make sure it communicates local propositions to the well founded recursion module
...
The bin_tree and num_consts examples can now be encoded more naturally.
2017-05-26 10:45:39 -07:00
Leonardo de Moura
62c24f9bb5
chore(*): remove pos_num and num from stdlib
2017-05-25 18:24:16 -07:00
Leonardo de Moura
7ffd7fea3d
feat(kernel): store depth of composite terms and use it in the hash code computation
...
closes #1589
2017-05-25 16:51:02 -07:00
Leonardo de Moura
438ce08748
feat(library/equations_compiler/util): cleanup equation rhs
...
The idea is to remove hints used to define a function by well founded
recursion. See new div_eqn.lean test for an example.
2017-05-25 13:09:13 -07:00
Leonardo de Moura
9b12559239
fix(library/tactic/dsimplify): fixes #1603
2017-05-25 11:21:06 -07:00
Leonardo de Moura
0bf51e63e8
fix(library/init/meta/constructor_tactic): fixes #1598
2017-05-25 09:57:15 -07:00
Leonardo de Moura
5604835672
test(tests/lean/tree_map): closes #1457
2017-05-24 17:15:12 -07:00
Leonardo de Moura
7b98484002
test(tests/lean/run/term_app2): another well founded recursion example
2017-05-24 15:58:18 -07:00
Leonardo de Moura
c396e4519a
fix(library/equations_compiler/util): missing case at prove_eq_rec_invertible
...
@dselsam You have used a function similar to prove_eq_rec_invertible in
the inductive compiler.
I'm wondering if this bug (missing case) may also occur in the inductive
compiler.
2017-05-24 14:34:54 -07:00
Leonardo de Moura
39b850fb10
fix(tests/lean/eqn_hole): test output
2017-05-24 14:34:54 -07:00
Leonardo de Moura
e3249dfdb9
test(tests/lean/run/term_app): add test for nested inductive type
2017-05-24 14:34:54 -07:00
Leonardo de Moura
9e9ebe9edd
test(tests/lean/run/even_odd): use default decreasing tactic for defining even and odd
2017-05-24 14:34:54 -07:00
Leonardo de Moura
6ad9e3ed1e
feat(library/init/meta/well_founded_tactics): add simple tactic for discharging decreasing proofs
2017-05-23 22:07:46 -07:00
Leonardo de Moura
18c7f5f1b7
refactor(library/init/data/sigma/lex): define psigma.lex
...
We actually use psigma instead of sigma in the equation compiler.
2017-05-23 20:39:09 -07:00
Leonardo de Moura
229b730c15
feat(library/equations_compiler): invoke tactics for building well founded relation, and proving recursive calls are "decreasing"
2017-05-23 16:04:55 -07:00
Leonardo de Moura
4fbb65d9f1
feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs
2017-05-23 15:00:29 -07:00
Gabriel Ebner
47629e9da3
feat(frontends/lean): make most parser_errors recoverable
2017-05-23 11:14:31 -07:00
Gabriel Ebner
95300224aa
fix(frontends/lean/builtin_cmds): suppress unhelpful #check output
2017-05-23 11:14:31 -07:00
Gabriel Ebner
183bf63e26
fix(frontends/lean/parser): pass error-recovery flag from parser to elaborator
2017-05-23 11:14:31 -07:00
Gabriel Ebner
77a2311f09
fix(frontends/lean/elaborator): segfault
2017-05-23 11:14:31 -07:00
Gabriel Ebner
166c07e1fe
fix(frontends/lean/elaborator): do not leak _elab_u names
2017-05-23 11:14:31 -07:00
Gabriel Ebner
d27a0eff15
chore(tests): fix tests
2017-05-23 11:14:31 -07:00
Gabriel Ebner
f24d790416
chore(tests/lean/fail): update to current syntax
2017-05-23 11:14:31 -07:00
Gabriel Ebner
99754188e6
feat(library/compiler/eta_expansion): also eta-expand expressions containing sorry
2017-05-23 11:14:31 -07:00
Gabriel Ebner
af63d4036b
chore(tests): update tests
2017-05-23 11:14:31 -07:00
Gabriel Ebner
8bd09fe282
chore(tests): add demo for parser error recovery
2017-05-23 11:14:30 -07:00
Gabriel Ebner
89ad117be3
chore(tests): update tests with changes to error recovery
2017-05-23 11:14:30 -07:00
Sebastian Ullrich
49e5c69447
fix(init/meta/expr): have all reflected defns accept Sort
2017-05-23 11:00:33 +02:00
Sebastian Ullrich
5a19430f60
fix(frontends/lean/scanner): wrong upos after field projection
2017-05-23 10:33:31 +02:00
Gabriel Ebner
5d6bf38b7e
chore(tests): add Leo's test case for errors in solve1-blocks
2017-05-23 07:33:12 +02:00
Gabriel Ebner
54114fd7bd
fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks
2017-05-23 07:28:34 +02:00
Gabriel Ebner
fbfec02015
fix(tests): move test away from run
2017-05-22 17:51:10 +02:00
Gabriel Ebner
cb28f382a3
fix(library/equations_compiler/elim_match): handle partially applied constructors
2017-05-22 17:17:27 +02:00
