Gabriel Ebner
d5c7d078eb
fix(library/type_context): check for stack overflow
2017-05-29 14:58:34 +02:00
Gabriel Ebner
5ab28548b8
fix(library/type_context): reduce whnf stack space
2017-05-29 14:58:28 +02: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
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
5583893991
fix(library/equations_compiler/wf_rec): avoid name collision between auxiliary lemmas produced in different modules
2017-05-24 17:50:39 -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
Sebastian Ullrich
491802409a
chore(*): remove unused macro_definition_cell::pp method
2017-05-24 09:51:23 +02:00
Leonardo de Moura
a1cfe0367b
fix(library/equations_compiler/pack_domain): nested recursive calls
2017-05-23 21:50:26 -07:00
Leonardo de Moura
e163b5c884
feat(library/init/meta/expr): binder_info.other ==> binder_info.aux_decl
2017-05-23 21:42:52 -07:00
Leonardo de Moura
d8713acbdd
fix(library/tactic/eqn_lemmas): fix get_eqn_lemmas_for
2017-05-23 20:39:27 -07:00
Leonardo de Moura
290e7b9cff
feat(library/init): use Sort instead of Type for defining acc and well_founded
2017-05-23 16:40:45 -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
ca684102f6
refactor(library/tactic,frontends/lean): move tactic_evaluator to library/tactic
2017-05-23 15:30:31 -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
99754188e6
feat(library/compiler/eta_expansion): also eta-expand expressions containing sorry
2017-05-23 11:14:31 -07:00
Gabriel Ebner
5f1b5da099
feat(library/compiler/eta_expansion): eta-expand sorrys
2017-05-23 11:14:31 -07:00
Gabriel Ebner
40eb5d0556
feat(library/module_mgr): skip reverse dependency rebuild if file content is unchanged
2017-05-23 11:14:30 -07:00
Gabriel Ebner
345cd1bc2a
feat(frontends/lean/parser): error recovery in interactive tactics
2017-05-23 11:14:30 -07:00
Gabriel Ebner
00ac867ddf
feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys
2017-05-23 11:14:30 -07:00
Gabriel Ebner
1468461c47
feat(frontends/lean): recover from many parser errors
2017-05-23 11:14:30 -07:00
Gabriel Ebner
07c25338b9
feat(shell/server): add search command
2017-05-22 09:40:38 -07: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
3d088eea25
fix(library/equations_compiler): avoid name collision when pack_mutual is not used
2017-05-21 15:40:06 -07:00
Leonardo de Moura
9fb7e5c931
feat(library/equations_compiler): generate equational lemmas for auxiliary _main definitions
2017-05-21 15:21:28 -07:00
Leonardo de Moura
4e496b78d5
feat(library/equations_compiler): unpack auxiliary definition
...
We still need to unpack auxiliary lemmas, and propagate information in
the frontend.
2017-05-20 20:34:18 -07: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
Leonardo de Moura
08560acf07
fix(library/equations_compiler): bugs in wf_rec
2017-05-20 13:26:49 -07:00
Leonardo de Moura
ab03a6af16
feat(library/equations_compiler/wf_rec): avoid unnecessary revert/intro's
2017-05-20 08:58:22 -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
789d4e148f
feat(library/equations_compiler): add pack_mutual
...
This step packs a collection of mutually recursive functions into a
single one. We use `psum` to combine the different domains, and
`psum.cases_on` to combine the codomains.
2017-05-18 15:29:51 -07:00
Leonardo de Moura
22d0dc197c
fix(library/equations_compiler/pack_domain): bug in pack_domain
2017-05-18 14:24:38 -07: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
Leonardo de Moura
7d937dcfcb
fix(library/tactic/simplify): instantiate assigned metavariables in the simplifier
...
This fixes a problem similar to the one described at #1587
2017-05-18 10:52:11 -07:00
Gabriel Ebner
7353a54aac
fix(library/vm/vm): prevent segfault
2017-05-18 09:41:31 -07:00
Gabriel Ebner
d9f5e0bb1f
fix(library/app_builder): prevent segfault
2017-05-18 09:41:31 -07:00
Gabriel Ebner
4528711efb
fix(library/type_context): prevent segfault
...
Temporary metavariables appeared here when pretty-printing simp_lemmas.
2017-05-18 09:41:31 -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
4982e23dca
feat(library/equations_compiler/wf_rec): eliminate recursive calls using functional
2017-05-17 15:56:53 -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
Leonardo de Moura
1c87319b58
feat(library/equations_compiler): add wf_rec skeleton
2017-05-17 12:47:52 -07:00
Leonardo de Moura
dea8a856dc
chore(library/equations_compiler/compiler): generate error when using well founded recursion in meta definitions
2017-05-17 12:24:47 -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
