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

113 commits

Author SHA1 Message Date
Sebastian Ullrich
27c1d2f4fb fix(init/meta/interactive): simp: accept local refs as simp names 2017-05-14 19:19:22 -07:00
Sebastian Ullrich
eb60df4409 fix(init/meta/interactive): case didn't find some cases 2017-05-14 19:19:22 -07:00
Sebastian Ullrich
808ab73d93 refactor(init): use list for expr.macro args 2017-05-14 19:17:28 -07:00
Sebastian Ullrich
171a96a8de refactor(library): remove all instances of `(...) 2017-05-12 19:13:48 +02:00
Sebastian Ullrich
4b21b13649 refactor(init): replace has_quote class with reflected 2017-05-09 16:02:42 -07:00
Sebastian Ullrich
d0c2c73b35 refactor(init/meta,tools): rename now tactic to done 
It was pointed out that Coq already uses `now` for a different kind of tactic.
And `done` is more descriptive anyway.
 2017-05-03 11:18:31 +02:00
Leonardo de Moura
08e094139d feat(library/init/meta): add by_contradiction and by_cases to tactic.interactive 2017-04-26 12:54:52 -07:00
Mario Carneiro
7ef4428124 add new interactive tactics skip, ginduction, exacts 2017-04-23 11:48:33 -07:00
Sebastian Ullrich
b3884d5f42 refactor(init/meta/interactive,frontends/lean/token_table): introduce generalizing keyword in Lean 2017-04-16 15:11:49 -07:00
Sebastian Ullrich
8ea2bc08cb feat(init/meta/interactive): add generalizing parameter to induction 2017-04-11 17:07:28 -07:00
Sebastian Ullrich
70a2c402ac feat(init/meta/interactive): Isabelle-like case tactic 2017-04-11 17:07:28 -07:00
Leonardo de Moura
71685e4dd6 feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 
Replace `^.` with `.` in the stdlib
 2017-03-28 17:47:49 -07:00
Leonardo de Moura
6183c7676e feat(frontends/lean): use . for field access 2017-03-28 15:29:54 -07:00
Leonardo de Moura
161879b1bf feat(library/init/meta): add helper tactic guard_target for generating tests 2017-03-27 17:38:40 -07:00
Leonardo de Moura
b09968a37b feat(library/tactic/simplify): add beta := tt to simp 2017-03-27 17:38:31 -07:00
Leonardo de Moura
494e5b65c5 feat(library/init/meta/tactic): add apply_auto_param and apply_opt_param tactics 
see #1485
 2017-03-27 13:42:08 -07:00
Sebastian Ullrich
b3a0eb9bfc fix(init/meta/interactive): mk_simp_set: also remove equational lemmas 2017-03-27 13:42:08 -07:00
Sebastian Ullrich
dfd84666e2 feat(library): add functor, applicative, and monad laws, and prove them correct for non-meta instances 2017-03-27 13:42:08 -07:00
Gabriel Ebner
a8ba78e20a refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic 2017-03-23 09:07:08 +01:00
Gabriel Ebner
098d6f8f2a refactor(init/meta/tactic): remove report_errors argument from to_expr 2017-03-23 09:03:42 +01:00
Sebastian Ullrich
a5db5ae4de refactor(init/meta/interactive): rw: parse - separately to remove hack 2017-03-22 07:54:12 -07:00
Sebastian Ullrich
9cf80a6c94 feat(init/meta/interactive): rw goal info on ] 2017-03-22 07:54:12 -07:00
Sebastian Ullrich
da7e21696e feat(init/meta/interactive): rw goal info on , 2017-03-22 07:54:12 -07:00
Leonardo de Moura
fdadada3a9 fix(frontends/lean): fixes #1468 
@kha I had to add yet another hack to fix this issue.

In notation declarations, names are resolved at notation declaration time.
So, users do not expect them to be resolved again at tactic execution time.

I addressed this problem by wrapping constants occurring in notation
declarations with a "frozen_name" annotation. This transformation is
only performed if m_in_quote is true.
Then resolve_names_fn at elaborator.cpp will not try to resolve the
names again.

This change broke two other modules. `-` notation for inverting
equations at `rw`, and `calc` expressions inside quotes.
The broke for the same reason. They were not expecting the constants
to be wrapped with an annotation.
 2017-03-18 13:48:21 -07:00
Sebastian Ullrich
7c31e62b16 feat(init/meta/interactive): improve pretty-printing of list_of and itactic 2017-03-17 18:20:44 -07:00
Sebastian Ullrich
421a6d6f01 feat(frontends/lean/interactive,emacs): highlight current tactic parameter 2017-03-17 18:20:44 -07:00
Sebastian Ullrich
c46936d180 fix(frontends/lean/interactive): hard-code tactic pretty printing 2017-03-17 18:20:44 -07:00
Sebastian Ullrich
803d3073ae feat(frontends/lean): add interactive.type_formatter attribute and use it to pretty print interactive tactics 2017-03-17 18:20:44 -07:00
Sebastian Ullrich
0792bc13db feat(frontends/lean/elaborator,init/meta/interactive): relax expr pattern elaboration and use it to implement a tactic signature pretty printer 2017-03-17 18:20:44 -07:00
Leonardo de Moura
3e757d890a feat(library/tactic/intro_tactic): allow '_' in interactive mode as the anonymous name for intros, cases, induction 2017-03-09 15:42:36 -08:00
Leonardo de Moura
51958df84b chore(frontends/lean/token_table): remove dead keywords 2017-03-07 14:00:49 -08:00
Sebastian Ullrich
a053175714 refactor(init/meta,library/vm): use structure for position information 2017-02-21 11:06:39 -08:00
Leonardo de Moura
296d4b0f09 refactor(library/tactic, library/init/meta): simplify_config => simp_config 2017-02-19 13:10:36 -08:00
Leonardo de Moura
b52e8d67be feat(library/init/meta): simp&intro tactics 2017-02-19 13:02:27 -08:00
Leonardo de Moura
0d22410e2e feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode 2017-02-19 12:11:22 -08:00
Sebastian Ullrich
b9424975b3 refactor(init/meta): replace dynamically-checked quotes where possible 2017-02-17 19:59:57 -08:00
Leonardo de Moura
c51d9ad4f4 feat(library/init/meta): add simph: a shorter simp_using_hs 2017-02-17 13:45:03 -08:00
Leonardo de Moura
d3c340a30c feat(library/init/meta): improve induction tactic interface 
It uses .rec recursor when it is not specified
 2017-02-17 10:58:51 -08:00
Sebastian Ullrich
84f3e2a492 refacotr(init/meta/interactive): clean up parameter gadgets 2017-02-17 15:41:58 +01:00
Sebastian Ullrich
69ed7b940f refactor(init/meta/interactive): query position information dynamically 2017-02-17 15:41:58 +01:00
Sebastian Ullrich
d15591a2d8 feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters 2017-02-17 13:45:56 +01:00
Leonardo de Moura
1ab2bb7714 feat(frontends/lean/elaborator): eta-expand function applications until we consume all optional and auto parameters 2017-02-14 17:38:08 -08:00
Leonardo de Moura
1b412b6cc0 feat(library/init/meta): new cases that reverts also composite terms 
The previous `cases` tactic would only use the revert/intro idiom
for `cases h` when `h` is a hypothesis
 2017-02-14 13:30:36 -08:00
Leonardo de Moura
f650a1b873 refactor(library/init/meta): avoid '_core' idiom using default parameters 
I kept a few core methods (e.g., exact_core and apply_core). Reason:
if we use default parameters

    meta constant exact (e : expr) (md := semireducible) : tactic unit

then, we will not be able to write

    to_expr p >>= exact

The workaround is

    do t <- to_expr p, exact t

or
    to_expr p >>= (fun x, exact x)

One alternative is to change how we handle default parameters, and
eta-expand applications that involve default parameters.
We may also have an attribute [eta_expand]. Then

    attribute [eta_expand] foo

instructs the elaborator to automatically eta-expand foo-applications.
The attribute would give users more control, and avoid potential
performance problems. Without the attribute, then for every function
application the elaborator has to check the type and decide whether it
must be eta-expanded or not.

@gebner @kha What do you think?
 2017-02-14 09:46:55 -08:00
Johannes Hölzl
bb136d63ab feat(src/library/tactic): tactic.cases_core returns for each new goal the used constructor, a list of introduced hypotheses, and substitutions for dependent hypotheses 2017-02-10 16:07:33 -08:00
Johannes Hölzl
d7af5515d2 feat(src/library/tactic): tactic.induction_core returns for each new goal the list of introduced hypotheses and substitutions for dependent hypotheses 
Also add to_obj(buffer<vm_obj>) to construct a vm-list of vm objects.
 2017-02-10 16:07:33 -08:00
Leonardo de Moura
c0e6314f14 fix(library/init/meta,library/tactic/elaborate): bad error position when to_expr is used outside of interactive mode 2017-02-09 18:44:50 -08:00
Leonardo de Moura
5e397795cf fix(library/init/meta): focus tactic 
This commit also add the interactive tactic 'focus'
 2017-02-09 10:02:19 -08:00
Leonardo de Moura
a28d6a94fd feat(library/init/meta): add any_goals tactic 2017-02-06 16:23:29 -08:00
Leonardo de Moura
ae06844f57 chore(library/init/meta): remove unnecessarily '| failed' annotations 
tactic and smt_tactic are instaces of monad_fail
 2017-02-05 20:12:42 -08:00