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

80 commits

Author SHA1 Message Date
Leonardo de Moura
a0fb3eb2f9 feat(library/equations_compiler/equations): add helper function 2016-09-09 17:43:42 -07:00
Leonardo de Moura
15f3622cbb fix(library/equations_compiler/pack_domain): missing case 2016-09-09 13:39:51 -07:00
Leonardo de Moura
c1521b8416 feat(library/equations_compiler/elim_match): improve process_no_equation case 2016-09-09 12:40:16 -07:00
Leonardo de Moura
f64d1483e9 fix(library/equations_compiler/elim_match): avoid nontermination at process_no_equation 2016-09-09 09:00:57 -07:00
Leonardo de Moura
3857ae09f7 feat(library/equations_compiler/elim_match): add max number of steps 2016-09-09 08:48:34 -07:00
Leonardo de Moura
96fa8856bc feat(library/equations_compiler): add mk_nonrec 2016-09-08 14:09:05 -07:00
Leonardo de Moura
14d009ce92 refactor(library/equations_compiler): improve mk_equation_lemma 2016-09-08 11:50:58 -07:00
Leonardo de Moura
f4f92ed2d1 chore(library/equations_compiler/util): add comment 2016-09-08 10:28:30 -07:00
Leonardo de Moura
7d56382baa feat(library/equations_compiler/util): generate equation lemmas for equations using invertible functions 2016-09-07 17:57:10 -07:00
Leonardo de Moura
f7699d8719 fix(library/equations_compiler/elim_match): support dependent functions handling invertible functions 2016-09-07 16:04:08 -07:00
Leonardo de Moura
2f7a1a3579 feat(library/equations_compiler/elim_match): add support for invertible functions 2016-09-07 08:53:56 -07:00
Leonardo de Moura
bedb508a8f feat(library/equations_compiler): do not generate bytecode for lemmas 2016-09-06 15:14:47 -07:00
Leonardo de Moura
c9cee9a702 feat(library/equations_compiler): add flag indicating whether we are compiling a lemma or not 2016-09-06 15:09:54 -07:00
Leonardo de Moura
385a28a410 chore(library/equations_compiler/util): use nested_exception 2016-09-06 13:37:10 -07:00
Leonardo de Moura
01107f7aae feat(library/equations_compiler): generate bytecode for auxiliary definitions 2016-09-06 13:29:12 -07:00
Leonardo de Moura
ff9500d7f9 feat(library/exception): add nested_exception 2016-09-06 12:57:06 -07:00
Leonardo de Moura
d8caecff49 refactor(library/exception): avoid throw_generic_exception functions 2016-09-06 12:37:56 -07:00
Leonardo de Moura
a0b8766ffb refactor(library): merge exception modules 2016-09-06 09:12:26 -07:00
Leonardo de Moura
120bffce25 chore(library/equations_compiler/elim_match): add cases/induction tactic error message to trace 2016-09-04 17:33:26 -07:00
Leonardo de Moura
029766495b feat(library/equations_compiler/util): try to improve performance of lemma generation 
There are still performance problems. Lemma generation is fine, but the
kernel is timing out when checking the lemma. We need to provide hints
to the kernel to avoid the performance problem.
 2016-09-03 13:24:44 -07:00
Leonardo de Moura
cfbffb41ef feat(library/equations_compiler): prove equation lemmas that use if-then-else 2016-09-03 13:23:09 -07:00
Leonardo de Moura
4d7c233684 feat(library/equations_compiler/elim_match): use if-then-else when next pattern for every equation is a variable or value 2016-09-03 13:22:25 -07:00
Leonardo de Moura
6dcf0725d7 fix(library/equations_compiler): erase inaccessible annotations 2016-09-02 14:11:03 -07:00
Leonardo de Moura
13f0d4e09a refactor(library/equations_compiler): new equation lemma generation 
The idea is to generate a lemma based on the left-hand-side provided by
the user. This feature is essential for supporting the derived inductive
datatype constructors.
 2016-09-02 14:04:09 -07:00
Leonardo de Moura
7724fbed93 fix(library/equations_compiler/elim_match): do not use constructor transition for below arguments 2016-09-02 12:51:39 -07:00
Leonardo de Moura
b3d78208be fix(library/equations_compiler/elim_match): typo 2016-09-02 12:39:21 -07:00
Leonardo de Moura
3e4d8d0f75 fix(library/equations_compiler/elim_match): dead variable 2016-09-02 12:39:05 -07:00
Leonardo de Moura
bf096eb292 chore(library/equations_compiler/structural_rec): "lemmas" ==> "equations" 2016-09-02 11:17:38 -07:00
Leonardo de Moura
691b200244 feat(library/equations_compiler/util): add [eqn_sanitizer] attribute for defeq lemmas that should be automatically applied 2016-09-02 11:06:31 -07:00
Leonardo de Moura
3384139d38 chore(library/tactic/defeq_simplifier): improve error messages 2016-08-31 17:52:36 -07:00
Leonardo de Moura
54fd9adb47 feat(library/equations_compiler): use defeq simplifier to cleanup types of automatically synthesized lemmas 2016-08-31 15:54:03 -07:00
Leonardo de Moura
51a338d9a1 fix(library/equations_compiler/structural_rec): support for reflexive inductive datatypes 2016-08-31 10:46:32 -07:00
Leonardo de Moura
924c98832b feat(library/equations_compiler/structural_rec): generate eqn lemmas at structural_rec 2016-08-31 09:07:17 -07:00
Leonardo de Moura
33514dd6ea feat(library/equations_compiler/structural_rec): process aux lemmas 2016-08-30 20:09:57 -07:00
Leonardo de Moura
2fc0e5fa05 feat(library/equations_compiler/structural_rec): add aux definition 2016-08-30 18:33:24 -07:00
Leonardo de Moura
253fcdcc51 fix(library/equations_compiler/elim_match): equation lemma generation 2016-08-30 15:00:43 -07:00
Leonardo de Moura
001991dbeb feat(frontends/lean): use equations_header 2016-08-30 13:45:59 -07:00
Leonardo de Moura
230db1bc92 feat(library/equations_compiler/structural_rec): generate brec_on-based function 
We still need to generate lemmas and induction principle.
 2016-08-29 15:58:13 -07:00
Leonardo de Moura
f1f45cc2b7 feat(library/equations_compiler/structural_rec): better support for structural recursion (based on brec_on) 
For example, before this commit, structural_rec would not support the
function to_nat defined below.

```
set_option new_elaborator true

inductive foo : bool → Type
| Z  : foo ff
| O  : foo ff → foo tt
| E  : foo tt → foo ff

definition to_nat : ∀ {b}, foo b → nat
| .ff Z     := 0
| .tt (O n) := to_nat n + 1
| .ff (E n) := to_nat n + 1
```
 2016-08-29 10:51:09 -07:00
Leonardo de Moura
b08af16d5f refactor(library/equations_compiler): remove unnecessary abstraction 
We changed how we are going to process derived inductive datatypes.
 2016-08-29 09:25:01 -07:00
Leonardo de Moura
b317d4bc58 refactor(library/tactic): add hsubstitution module 2016-08-29 08:19:05 -07:00
Leonardo de Moura
1a675d69fc refactor(library/tactic/induction_tactic,library/tactic/cases_tactic): replace name_map<name> with substitutions at induction_tactic 
This commit also removes dead code from cases_tactic
 2016-08-28 14:09:22 -07:00
Leonardo de Moura
f0f9880ece refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic): 
new design for elim_match

I still need to fix lemma generation, and refactor induction/subst tactics
 2016-08-28 13:15:10 -07:00
Leonardo de Moura
95e8228e8a refactor(library/tactic/cases_tactic): improve low-level API 2016-08-25 16:34:40 -07:00
Leonardo de Moura
cf15218eea chore(library/equations_compiler/compiler): add new trace option 2016-08-25 10:45:08 -07:00
Leonardo de Moura
41b6358de6 chore(library/equations_compiler/elim_match): add helper methods 2016-08-25 10:44:50 -07:00
Leonardo de Moura
7851b9c097 fix(frontends/lean/definition_cmds): parameter handling 2016-08-23 21:13:54 -07:00
Leonardo de Moura
a93eada058 feat(library/type_context): improved (and simplified) cache management for type_context 2016-08-23 17:56:58 -07:00
Leonardo de Moura
27e06c80ba feat(library/equations_compiler/elim_match): generate auxiliary definition and lemmas for match 2016-08-22 17:59:54 -07:00
Leonardo de Moura
d8447b4c53 feat(library/equations_compiler/elim_match): add noequation transition 2016-08-22 13:53:35 -07:00