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
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
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
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
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
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
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
Sebastian Ullrich
49e5c69447
fix(init/meta/expr): have all reflected defns accept Sort
2017-05-23 11:00:33 +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
Leonardo de Moura
f742d9c9d8
feat(library/equations_compiler/pack_domain): use psigma instead of sigma
2017-05-20 19:14:10 -07:00
Leonardo de Moura
fa863496da
feat(library/equations_compiler): prove equational lemmas for auxiliary definition
2017-05-20 16:38:32 -07:00
Daniel Selsam
0bc855149a
feat(inductive_compiler): generate sizeof_spec for nested constructors
2017-05-20 08:30:57 -07:00
Sebastian Ullrich
9507297687
fix(init/meta/expr,library): reflect should accept Props
...
Fixes #1590
2017-05-19 14:17:06 +02:00
Leonardo de Moura
b69cf7ef43
fix(library/tactic/rewrite_tactic): instantiate assign metavars before rewriting
...
fixes #1587
2017-05-18 10:57:03 -07:00
Sebastian Ullrich
9b86808345
fix(frontends/lean/structure_cmd): parent structures may use different universe params
...
Fixes #1585
2017-05-18 09:35:14 -07:00
Leonardo de Moura
737136e8fd
feat(library/equations_compiler/wf_rec): apply well_founded.fix
2017-05-17 16:44:53 -07:00
Leonardo de Moura
7cf848cbb2
chore(tests/lean/run/wfrec1): cleanup example
2017-05-17 16:06:45 -07:00
Leonardo de Moura
56823a22b7
feat(library/equations_compiler/wf_rec): use has_well_founded type class to generate default well founded relation when one is not provided
2017-05-17 14:37:21 -07:00
Sebastian Ullrich
84997bf4de
refactor(init/meta/expr): unify expr and pexpr
2017-05-17 10:38:12 -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
Leonardo de Moura
76ff23c154
chore(tests/lean): fix tests
2017-05-14 19:40:36 -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
14425bd2d3
fix(frontends/lean/decl_util): double-elaboration of include params
2017-05-14 19:19:22 -07:00
Gabriel Ebner
85673cdd8d
fix(frontends/lean/definition_cmds): examples in noncomputable theories
2017-05-13 09:04:07 +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
Sebastian Ullrich
aa601d3e51
chore(tests): move tests to correct dir
2017-05-09 16:02:41 -07:00
Gabriel Ebner
b536df3596
feat(library/type_context): add option to unfold lemmas
2017-05-08 10:14:47 -07:00
Gabriel Ebner
40bf75cbff
fix(library/equations_compiler/structural_rec): fix indices
2017-05-07 15:52:39 +02:00
Gabriel Ebner
4b22e2309c
refactor(system/io): use spawn_args structure in all process functions
2017-05-04 16:41:11 -07:00
Gabriel Ebner
f0d22ed3e5
feat(library/process,system/io): set environment variables for spawned processes
2017-05-04 16:41:11 -07:00
Daniel Selsam
b7d20a333f
chore(src/library/constants): rm unused constants
2017-05-04 16:34:32 -07:00
