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

4193 commits

Author SHA1 Message Date
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
b59e1b0a2e fix(library/eval_helper): evaluating under-applied functions 2017-05-31 16:18:17 +02:00
Sebastian Ullrich
834375a042 fix(library/eval_helper): evaluating tactics 2017-05-31 16:18:15 +02: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
d489955600 fix(library/vm/vm_nat): bitwise operators 2017-05-30 13:09:17 -07:00
Mario Carneiro
9d676776b5 feat(library/vm/vm_nat): implementations of bitwise ops 2017-05-30 12:47:44 -07:00
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