max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
13268 commits 1 branch 0 tags 5.3 GiB
Commit graph

80 commits

Author SHA1 Message Date
Leonardo de Moura
aed2c442a3 chore(library/app_builder): add assertion stating that app_builder::mk_app arguments do not contain tmp metavars 2017-12-15 11:22:15 -08:00
Leonardo de Moura
47994fe14e chore(library): remove id_locked 2017-11-22 16:29:04 -08:00
Leonardo de Moura
64f575a2d5 perf(library/equations_compiler): performance problem for definitions that produce many equational lemmas 
The new test and comment at src/library/equations_compiler/util.cpp
explains the issue.
 2017-11-22 16:16:11 -08:00
Leonardo de Moura
9b03309d83 fix(library/equations_compiler): performance problem reported by @dselsam 2017-06-27 15:24:12 -07:00
Gabriel Ebner
d9f5e0bb1f fix(library/app_builder): prevent segfault 2017-05-18 09:41:31 -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
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
Daniel Selsam
538ac8d187 feat(inductive_compiler): generate injectivity lemmas 2017-03-10 22:27:18 -08:00
Leonardo de Moura
77f8479457 feat(library/type_context): allow zeta during type class resolution and app_builder 2017-03-08 23:04:56 -08:00
Leonardo de Moura
d315e424ff feat(library/congr_lemma, library/fun_info): make sure opt_param gadget do not confuse the simplifier, fun_info, congr_lemma, etc 
A definition such as

  def f (a : nat) (b : nat := a) (c : nat := a) :=
  a + b + c

should *not* be treated as a dependent function.
 2017-01-30 20:23:45 -08:00
Leonardo de Moura
e8839cbcdc feat(library/app_builder): add mk_eq_mpr that removes unnecessary propext 2017-01-20 20:27:41 -08:00
Leonardo de Moura
52c1a15313 feat(library/tactic/smt): add tactics for adding new lemmas to ematch state 2017-01-05 11:44:25 -08:00
Leonardo de Moura
ca6d3743c7 feat(library/tactic/smt): add mk_eq_true_intro mk_of_eq_true mk_eq_false_intro mk_not_of_eq_false 2017-01-02 13:39:16 -08:00
Leonardo de Moura
9065cf0350 feat(library/tactic/congruence/theory_ac): add internalization, interface with congruence closure module, and trivial/simp/orient transitions 
Still missing: superpose, collapse and compose transitions.
 2016-12-28 21:35:16 -08:00
Leonardo de Moura
a30081a715 feat(library/tactic/congruence/congruence_closure): interpreted values in the same equivalence class 2016-12-25 11:09:55 -08:00
Leonardo de Moura
b1b694a532 fix(library/tactic/congruence/congruence_closure): bugs, and add basic cc tactic 2016-12-23 19:30:45 -08:00
Leonardo de Moura
a4173467c4 feat(library/app_builder): use Semireducible if caller did not specify a transparency_mode and ctx.mode() is Reducible or None 
see discussion at #1265
 2016-12-23 14:41:22 -08:00
Leonardo de Moura
48cd421852 feat(library/tactic/congruence): add congruence closure basics 2016-12-21 20:46:25 -08:00
Leonardo de Moura
d0d75c0923 refactor(kernel): reduce number of configurations supported in the kernel 
Now, eta and impredicativity are assumed to be always true.

Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
 2016-09-27 17:07:01 -07:00
Leonardo de Moura
668be38bb2 chore(library): remove old_type_context 2016-09-19 21:34:27 -07:00
Leonardo de Moura
4875741a37 feat(library/app_builder): add mk_ite 2016-09-02 17:04:01 -07:00
Daniel Selsam
4f8db64e23 refactor(simplifier): many fixes, extensions, and tests 
fix(simplifier): missing simp rule in prop simplifier
fix(library/unfold_macros): do not look for untrusted macros when using sufficient trust level
 2016-08-19 14:57:03 -07:00
Leonardo de Moura
5ffa481634 chore(library): remove dead code 2016-08-17 10:45:54 -07:00
Leonardo de Moura
7059609f57 feat(library/equations_compiler): equations_compiler stub, add helper equations_editor, add preprocessing 
The first preprocessing step packs nary functions into unary using sigma types
 2016-08-14 17:02:36 -07:00
Leonardo de Moura
a50cbf07ab fix(library/app_builder): do not try to instantiate type class instances that have been explicitly provided 2016-07-20 19:42:21 -04:00
Leonardo de Moura
e4b028c596 feat(library/app_builder): add efficient mk_congr_arg 
mk_congr_arg was a bottleneck at perm_ac tactic.
New tests are 10x faster after this commit.
 2016-07-04 16:16:58 -07:00
Leonardo de Moura
6526a48c50 feat(library/tactic/ac_tactics): add 'perm_ac' tactic 
TODO: add macro to postpone proof generation
 2016-07-03 23:09:25 +01:00
Leonardo de Moura
59f2b9e8c2 refactor(library/type_context): "metavar_context & m_mctx" ==> "metavar_context m_mctx" 2016-06-25 13:08:03 -07:00
Daniel Selsam
e1bc0a68e6 refactor(simplifier): port skeleton to new tactic framework 
Conflicts:
	library/init/meta/tactic.lean
	src/library/tactic/tactic_state.cpp
 2016-06-24 15:20:40 -07:00
Leonardo de Moura
6063d2fc80 feat(library): add cache_helper 2016-06-22 17:10:03 -07:00
Leonardo de Moura
7390e8afda refactor(library/app_builder): simplify app_builder API 2016-06-22 16:57:49 -07:00
Leonardo de Moura
6e007cd12f fix(library/app_builder): use current context when tracing 2016-06-20 10:29:43 -07:00
Leonardo de Moura
73b21b9e48 fix(library): assertion violations 2016-06-17 13:16:17 -07:00
Leonardo de Moura
bceb9aa4f7 refactor(library/app_builder): port app_builder to new type_context 2016-06-14 16:16:07 -07:00
Leonardo de Moura
8dde1489f9 refactor(library/util): isolate util procedures that depend on old_type_checker 2016-03-21 13:36:08 -07:00
Leonardo de Moura
f67181baf3 chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
Leonardo de Moura
32268b71d2 feat(library/app_builder): avoid redundant heq_of_eq(eq_of_heq(H)) proofs 2016-01-10 19:29:34 -08:00
Leonardo de Moura
2b38d0fe9b chore(library/app_builder): improve trace message 2016-01-10 18:31:54 -08:00
Leonardo de Moura
cf8307ee20 feat(library/app_builder): use types in app_builder trace messages 2016-01-10 17:29:11 -08:00
Leonardo de Moura
934f3b67ff feat(library/blast/congruence_closure): basic support for heterogeneous equality 
We still have to process the general congruence lemmas.
 2016-01-10 12:53:05 -08:00
Leonardo de Moura
42cdda227a feat(library/congr_lemma_manager): add heterogeneous equality congruence lemmas 2016-01-09 15:41:08 -08:00
Leonardo de Moura
403966792d feat(library/app_builder): add helper heq methods 2016-01-09 12:46:14 -08:00
Leonardo de Moura
fcf532ea67 chore(library/app_builder): fix typo in trace message 2016-01-03 15:16:50 -08:00
Leonardo de Moura
7da64a768f refactor(library/type_context): with the new tracing infrastructure, type_context doesn't need an io_state 2015-12-08 14:58:08 -08:00
Leonardo de Moura
9b69ccd2f8 feat(library/app_builder): add trace messages to app_builder 2015-12-08 13:43:15 -08:00
Leonardo de Moura
9df10a4048 feat(library): add tracing messages to app_builder and congr_lemma_manager 2015-12-08 13:36:11 -08:00
Leonardo de Moura
80725cc416 fix(library): references to algebra in the source code 2015-12-05 23:50:26 -08:00
Leonardo de Moura
00e34683f2 feat(library/app_builder): (try to) address not-issue and other reducibility annotation related issues in the app_builder 2015-12-04 16:03:06 -08:00
Leonardo de Moura
a8b6a286dd fix(library/app_builder): make sure app_builder works even if iff is marked as reducible 2015-12-04 13:51:56 -08:00
Leonardo de Moura
fc461ce832 feat(library/app_builder): avoid redundant proof terms at mk_of_iff_true and mk_not_of_iff_false 2015-11-22 15:49:17 -08:00