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

6955 commits

Author SHA1 Message Date
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
3bc5cf8d0e feat(frontends/lean/elaborator): improve error message 2016-09-03 13:21:54 -07:00
Leonardo de Moura
a60f4e2699 fix(library/type_context): index out of bounds 2016-09-03 13:21:54 -07:00
Leonardo de Moura
4875741a37 feat(library/app_builder): add mk_ite 2016-09-02 17:04:01 -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
0afef31be6 feat(library/tactic/defeq_simplifier): reimplement defeq simp lemma cache 2016-09-02 09:10:09 -07:00
Leonardo de Moura
02316c39b8 feat(frontends/lean/elaborator): throw an error if a local instance is declared in the middle of a declaration 2016-09-01 18:06:38 -07:00
Leonardo de Moura
0ec22bb2cf refactor(library/type_context): new type class instance cache 2016-09-01 17:37:30 -07:00
Leonardo de Moura
ef9f9f1de0 fix(library/type_context): make sure local instances are not reset at set_env 2016-09-01 15:12:32 -07:00
Leonardo de Moura
a38264439f fix(library/attribute_manager): get_instances returns deleted instances 2016-09-01 14:48:03 -07:00
Leonardo de Moura
39dc336310 feat(library/tactic/user_attribute): add set_basic_attribute and unset_attribute tactics 2016-09-01 14:17:05 -07:00
Leonardo de Moura
ff05f16caa fix(library/type_context): store instance fingerprint 2016-09-01 09:01:43 -07:00
Leonardo de Moura
e061e9acab refactor(frontends/lean/elaborator): remove elaborator::ctx() 
The plan is to make `type_context` a transient object in the elaborator.
 2016-09-01 08:28:30 -07:00
Leonardo de Moura
381f2dc434 chore(frontends/lean/elaborator): simplify mk_pp_ctx 2016-09-01 08:15:36 -07:00
Leonardo de Moura
cc6d764c6c refactor(library/tactic/defeq_simplifier): use new type_context 2016-08-31 17:52:47 -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
4e33ca472d feat(library/tactic/defeq_simplifier): add helper function 2016-08-31 15:12:19 -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
3cc8b58433 feat(library/util): add get_constructor_rec_args 2016-08-30 20:09:41 -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
a8690205c9 feat(library/type_context): improve on_is_def_eq_failure for stuck terms 2016-08-30 10:51:40 -07:00
Leonardo de Moura
08f4d87806 fix(library/type_context): complete_instance 
The previous version was using typeclass inference to instantiate
arbitrary metavars in occurring in the input expression `e`.
This is incorrect. We should only use typeclass inference if the
metavariable is the argument of a function application (f ... ?m ...)
and the argument is marked and instance-implicit.
 2016-08-30 10:50:40 -07:00
Leonardo de Moura
240a77c692 chore(library/type_context): replace auto with actual type 2016-08-30 08:31:35 -07:00
Leonardo de Moura
a1e8610e64 fix(library/type_context): take annotations into account at is_stuck 2016-08-30 08:29:15 -07:00
Leonardo de Moura
85cf20a5b4 fix(library/type_context): missing case: stuck projections 
type_context only unfolds projections when they reduce.
 2016-08-30 08:13:58 -07:00
Leonardo de Moura
bd99de9bf8 fix(frontends/lean/pp): remove unnecessary parenthesis when pretty printing (A -> (Pi (b : B), C b)) 2016-08-29 16:36:04 -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
78f81034c6 feat(library): add helper methods 2016-08-29 08:31:33 -07:00
Leonardo de Moura
b317d4bc58 refactor(library/tactic): add hsubstitution module 2016-08-29 08:19:05 -07:00
Leonardo de Moura
cb7c82fdd5 feat(library/type_context): make sure annotations are ignored at is_def_eq 2016-08-28 14:42:50 -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
206bf613d5 feat(library/tactic/subst_tactic): use substitutions instead of name_map<name> in the subst_tactic (low level) API 2016-08-28 13:29:44 -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
16a99436b4 fix(frontends/lean/elaborator): make sure all inductive datatype parameters in constructor applications are marked as inaccessible 2016-08-28 07:58:18 -07:00
Leonardo de Moura
b37b4f3dc8 fix(frontends/lean/elaborator): implicit terms are marked as inaccessible in patterns 2016-08-28 07:58:06 -07:00
Leonardo de Moura
ae63821cdb fix(frontends/lean/elaborator): reject inaccessible annotation inside inaccessible annotation 2016-08-28 07:57:44 -07:00
Leonardo de Moura
7b37762231 fix(frontends/lean/elaborator): make sure elaborated term is based on what the user wrote 2016-08-28 07:57:34 -07:00