Commit graph

8744 commits

Author SHA1 Message Date
Floris van Doorn
ec38ee8df8 fix(hott/init/tactic): add replace 2016-02-07 14:06:28 -08:00
Leonardo de Moura
668758c44e fix(library/blast/blast): compilation warning on OSX 2016-02-05 13:02:02 -08:00
Leonardo de Moura
6c1c6cbbdd fix(util/lp,tests/util/lp): warning msgs on OSX 2016-02-05 11:51:20 -08:00
Leonardo de Moura
e785827688 fix(tests/util/lp/CMakeFiles): disable lp test that fails when executing ctest
This test need input parameters.
2016-02-05 10:17:48 -08:00
Leonardo de Moura
1c8d8da9cf chore(util/lp/lp_primal_core_solver): fix warning 2016-02-05 10:08:32 -08:00
Lev Nachmanson
0e4f98dc47 dev(lp): remove a warning
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:08:24 -08:00
Lev Nachmanson
a7e3befd21 dev(lp): speed up primal with sorted list
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:36 -08:00
Lev Nachmanson
ff8213a6a9 dev(lp): diminish the number of pivots of primal by sorting the columns
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
61eaef0183 dev(lp): improve the dual perormance
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
9482d508df dev(lp): fix bugs in the dual simplex high loop
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
fbe4f56aea chore(lp): remove warnings
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Leonardo de Moura
739f9e5486 fix(tests/util/lp/lp): use regular C arrays 2016-02-05 10:04:35 -08:00
Leonardo de Moura
40d4623219 fix(util/lp/lp_settings): replace fabs with std::abs 2016-02-05 10:04:35 -08:00
Leonardo de Moura
971ec72157 fix(util/lp/numeric_pair): include cmath 2016-02-05 10:04:35 -08:00
Lev Nachmanson
504c603af4 chore(lp): use std::ostream for printing routines
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
fc858d98c0 chore(lp): improve formatting
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
e9cd621855 chore(lp): improve formatting
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
28bf891b7f dev(lp): port to windows (msys2)
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
99dcad0dda dev(lp): performance tuning in find_leaving_on_harris_theta
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:35 -08:00
Lev Nachmanson
d098dfe326 dev(lp): fix infeasibility evidence check
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:34 -08:00
Leonardo de Moura
d9acf90f7b refactor(util/lp): use Lean exception 2016-02-05 10:04:34 -08:00
Leonardo de Moura
8fbf66d01a chore(util/lp): no "using", indentation 2016-02-05 10:04:34 -08:00
Leonardo de Moura
1841d17544 refactor(lp): NDEBUG ==> LEAN_DEBUG 2016-02-05 10:04:34 -08:00
Lev Nachmanson
fbb3ed8911 feat(lp): add LP solver and incremental LU factorization
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2016-02-05 10:04:34 -08:00
Leonardo de Moura
04eaf184a9 feat(frontends/lean,library/unifier): checkpoints at have-expressions
@avigad, @fpvandoorn, @rlewis1988, @dselsam

This commit modifies how have-expressions are elaborated.
Now, to process

     have H : <type>, from <proof>,
     <rest>

we first process the constraints in <type> and <proof> simultaneously.
After all these constraints are solved, the elaborator performs
a Prolog-like cut, and process the constraints in <rest>.

So, all overloads, type classes and coercions in <type> and <proof> are solved
before we start processing <rest>. Moreover, while processing <rest>, we
cannot backtrack to <type> and <proof> anymore.

I fixed all affected proofs in the standard and HoTT libraries in
previous commits pushed today and yesterday. I think most affected proofs were not using a good
style and/or were easy to fix. Here is a common pattern that does not
work anymore.

   structure has_scalar [class] (F V : Type) :=
   (smul : F → V → V)

   infixl ` • `:73 := has_scalar.smul

   proposition smul_zero (a : R) : a • (0 : M) = 0 :=
   have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
   !add.left_cancel this

The `have` doesn't work because Lean can't figure out the type of 0 before
it starts processing `!add.left_cancel this`. This is easy to fix, we just have to
annotate one of the `0`s in the `have`:

   proposition smul_zero (a : R) : a • (0 : M) = 0 :=
   have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
   !add.left_cancel this

BTW, all tactics are still being executed after all constraints are solved.
We may change that in the future. I didn't want to execute
the tactics at <proof> before <rest> because of universe
meta-variables. In Lean, unassigned universe meta-variables become
parameters. Moreover, we perform this conversion *before*
we start processing tactics. Reason: universe meta-variables
create many problems for tactics such as `rewrite`, `blast` and `simp`.

Finally, we can recover the previous behavior using the option

         set_option parser.checkpoint_have false
2016-02-04 19:01:19 -08:00
Leonardo de Moura
30d6853ffd refactor(hott,tests): make sure HoTT library and tests still work if we introduce checkpoints in have-expressions 2016-02-04 16:58:32 -08:00
Leonardo de Moura
a08bc408c8 fix(frontends/lean/structure_cmd): fixes #967 2016-02-04 16:15:18 -08:00
Leonardo de Moura
31cc0ebb6a fix(frontends/lean/structure_cmd): fixes #968 2016-02-04 15:45:38 -08:00
Leonardo de Moura
496c84dac6 fix(frontends/lean/elaborator): fixes #982 2016-02-04 15:14:30 -08:00
Leonardo de Moura
774fa01b1a chore(library/pp_options): reduce pp default limits 2016-02-04 14:55:21 -08:00
Leonardo de Moura
f62e22b34c fix(util/sexpr/format): fixes #955
Lean was crashing because separate_tokes was traversing a DAG as a tree.
Lean was dying without memory (and getting stack overflows) because the procedure was also converting
the DAG into a tree.

This example also suggests we should reduce the limits for the pretty printer.
2016-02-04 14:55:11 -08:00
Leonardo de Moura
0268f92eb4 fix(frontends/lean/elaborator): fixes #965 2016-02-04 13:41:21 -08:00
Leonardo de Moura
42fbc63bb6 fix(library/tc_multigraph): avoid name collisions
@avigad, @fpvandoorn, @rlewis1988, @dselsam

I changed how transitive instances are named.
The motivation is to avoid a naming collision problem found by Daniel.
Before this commit, we were getting an error on the following file
tests/lean/run/collision_bug.lean.

Now, transitive instances contain the prefix "_trans_".
It makes it clear this is an internal definition and it should not be used
by users.

This change also demonstrates (again) how the `rewrite` tactic is
fragile. The problem is that the matching procedure used by it has
very little support for solving matching constraints that involving type
class instances. Eventually, we will need to reimplement `rewrite`
using the new unification procedure used in blast.

In the meantime, the workaround is to use `krewrite` (as usual).
2016-02-04 13:15:42 -08:00
Ulrik Buchholtz
dcb35008e1 feat(hott/homotopy): general connectivity elimination and the wedge connectivity lemma 2016-02-04 11:07:22 -08:00
Rob Lewis
87ec5ada07 fix(analysis/metric_space): unnecessary import, style, remove unnecessary lines 2016-02-04 11:03:28 -08:00
Rob Lewis
a675a5ede2 fix(algebra/ordered_field, analysis/real_limit): generalize theorem to ordered fields 2016-02-04 11:03:28 -08:00
Rob Lewis
f402f322aa feat(theories/analysis): add theorems about convergent sequences, functions, and continuity 2016-02-04 11:03:28 -08:00
Rob Lewis
ffed988a34 feat(data/list): add missing theorems 2016-02-04 11:03:28 -08:00
Rob Lewis
dcfc496992 feat(algebra/ordered_field): ad missing theorem 2016-02-04 11:03:28 -08:00
Rob Lewis
40a1371cd0 feat(theories/analysis): define real square roots 2016-02-04 11:03:28 -08:00
Rob Lewis
796e16bdb7 feat(library/theories/analysis): add theorems about convergent functions in metric spaces 2016-02-04 11:03:28 -08:00
Rob Lewis
cb4f71b16c feat(library/data/real): add more theorems concerning rationals embedded in reals 2016-02-04 11:03:28 -08:00
Rob Lewis
110036c4dc feat(library/algebra/ordered_field): add missing theorems 2016-02-04 11:03:28 -08:00
Leonardo de Moura
790dbc53c3 refactor(library/algebra/ring): cleanup 2016-02-03 20:07:12 -08:00
Leonardo de Moura
cb12b9b876 refactor(library): cleanup proofs
Fixed proofs that broke when we tried to implement a "checkpoint" have.
2016-02-03 19:52:23 -08:00
Leonardo de Moura
9d88db3941 perf(library/type_context): add cache for minimizing the access to is_opaque and environment::find 2016-02-02 19:47:58 -08:00
Leonardo de Moura
701d6b5016 perf(library/blast/forward/pattern): simplify is_higher_order test 2016-02-02 18:56:48 -08:00
Leonardo de Moura
a7b3dcbc09 perf(library/blast/state): do not add hypotheses that are Pi-expressions into discrimination trees 2016-02-02 18:50:23 -08:00
Leonardo de Moura
4324726a8e perf(kernel/expr_eq_fn): minimize number of calls to check_system 2016-02-02 18:16:14 -08:00
Leonardo de Moura
c55b10af1b perf(library/type_context): move check_system to strategic places 2016-02-02 16:12:53 -08:00