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

169 commits

Author SHA1 Message Date
Leonardo de Moura
a7b895525b feat(library/tactic/simp_lemmas): simp lemmas may contain metavariables 
@dselsam `simp` now supports lemmas containing metavariables.
The metavariables are automatically converted into tmp metavars.
The new test contains a few examples.
 2017-06-28 18:17:21 -07:00
Sebastian Ullrich
08495eef27 refactor(init/meta,frontends/lean/tactic_notation): assume_tac -> «assume» etc. 
Fixes the eldoc display.

Also allow arbitrary keywords as tactics
 2017-06-28 10:43:19 -07:00
Sebastian Ullrich
9033cba7d3 feat(frontends/lean,init/meta/interactive): assume and suppose tactics 2017-06-27 18:50:10 -07:00
Leonardo de Moura
6ba425da6a feat(library/init/meta/interactive): add apply_with interactive tactic 
The new tactic allows us to set apply_cfg in interactive mode.
 2017-06-27 18:37:13 -07:00
Leonardo de Moura
cdec07fc81 feat(library/init/meta/interactive): address issue raised in comment at #1374 
The example at
https://github.com/leanprover/lean/issues/1342#issuecomment-307912291
 2017-06-27 16:45:21 -07:00
Leonardo de Moura
5a2b7348f9 feat(library/tactic/apply_tactic): make apply tactic more robust 
See issue #1342

Support for auto_param and opt_param have not been implemented yet.
 2017-06-27 10:42:26 -07:00
Mario Carneiro
b9c2659b5d fix(init/meta/interactive): generalize2 rollback if typecheck fails 2017-06-26 12:35:27 -07:00
Leonardo de Moura
ce5ca79edf feat(library/init/meta): add type_check tactic 
closes #1697
 2017-06-25 15:26:32 -07:00
Sebastian Ullrich
0a48809469 refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
Mario Carneiro
9f31096892 refactor(init/meta/interactive): rename pose -> define 2017-06-22 08:03:23 -07:00
Mario Carneiro
b775a01fba refactor(init/meta/interactive): merge assert -> note 2017-06-22 08:03:23 -07:00
Leonardo de Moura
671b6240c1 fix(library/init/meta): make sure rw still produces useful error messages 2017-06-21 20:58:59 -07:00
Leonardo de Moura
14d768ffa2 feat(library/init/meta/interactive): add simp_all tactic 
@Armael I added the simp_all tactic. See new test for an example.
 2017-06-21 20:43:56 -07:00
Leonardo de Moura
058d073cba feat(library/init/meta/interactive): allow user to write rw [f] to rewrite using the equational lemmas for f 
The tactic succeeds if the expression can be rewritten using one of the
equational lemmas associated with `f`.

See discussion at #1680
 2017-06-21 18:56:18 -07:00
Scott Morrison
629d5ebbe8 feat(init/meta/simp_tactic) tactics that revert hypotheses should allow elet expressions 
Conflicts:

	library/init/meta/simp_tactic.lean
 2017-06-21 13:58:46 -07:00
Scott Morrison
6aba80d389 feat(library/init/meta/simp_tactic,library/init/meta/interactive) interactive tactics for unfold_projection 2017-06-21 13:51:52 -07:00
Mario Carneiro
636e65a216 fix(init/meta/interactive): elab terms of change-with using same type 2017-06-20 12:34:29 -07:00
Leonardo de Moura
b8fa7f5311 fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean 
See #1664
 2017-06-18 18:33:27 -07:00
Leonardo de Moura
dc1a1c8540 refactor(library): has_to_string ==> has_repr 
See issue #1664

This is just the first step to implement proposal described at issue #1664.
 2017-06-18 18:29:19 -07:00
Armaël Guéneau
f24932748e fix(init/meta/interactive): allow dsimp to simplify several hypothesis 2017-06-12 20:37:56 -07:00
Gabriel Ebner
1a81425098 chore(library): convert comments to docstrings 2017-06-12 15:17:00 +02:00
Mario Carneiro
26a377753a fix(init/meta/interactive): let case tactic support _ names 2017-06-07 18:09:15 -07:00
Mario Carneiro
c13472a8b8 feat(init/meta/interactive): change-with tactic 
Conflicts:

	library/init/meta/interactive.lean
 2017-06-07 10:33:14 -07:00
Mario Carneiro
e8e57dcb15 feat(init/meta/interactive): change at tactic 
addresses #1641
 2017-06-07 10:17:00 -07:00
Sebastian Ullrich
79f29a693e refactor(init/meta/interactive): split file 2017-06-07 10:09:38 -07:00
Mario Carneiro
77264a6074 fix(init/meta/interactive): get rhs using relation_lhs_rhs 2017-06-07 10:03:35 -07:00
Mario Carneiro
1354514c80 feat(init/meta/interactive): specify intermediate goal in transitivity 
As suggested by @Armael on gitter
 2017-06-07 10:03:23 -07:00
Johannes Hölzl
d7fc571e36 fix(library/init/meta): show_goal also changes the goal 2017-06-05 20:07:44 -07:00
Leonardo de Moura
f5ec29ab1a feat(library/init/meta/interactive): add add_interactive command. 
@Armael: the new file `tests/lean/run/add_interactive.lean` contains a
small example. Note that we don't have auto quotation for commands yet.
So, I have to use the backtick in the example.

@Kha: this is a good candidate for the future command parser extensions.
 2017-06-05 16:43:15 -07:00
Leonardo de Moura
3140243bad chore(library/init/meta/interactive): reduce code duplication 2017-06-05 15:36:44 -07:00
Leonardo de Moura
ea8ecfd390 fix(library/init/meta/interactive): use replace_target at simp_goal 
replace_target uses id_locked.
The id_locked solution is more robust because simp may build a proof
using refl lemmas, but type_context may not be able to establish that
the previous and new target are definitionally equal.

@Armael This commit fixes the issue in the KreMLin proof you showed me.
Now, the following tactic succeeds (as expected)
```
        simp [lowstar_semantics.apply_ectx],
```
and the resulting goal is
```
...
|- exp.subbuf (exp.loc (b, n, list.nil field)) a_1 = exp.subbuf ↑?m_1 ?m_2
```
 2017-06-05 15:21:20 -07:00
Jeremy Avigad
c68326ac14 feat(library/init/meta/interactive): update simp docstring 2017-06-04 13:23:26 -07:00
Jeremy Avigad
d045042ae7 refactor(library/init/meta/interactive): remove special printing of loc, style fixes 2017-06-04 13:23:26 -07:00
Jeremy Avigad
c09aa24977 refactor(library/init/meta/interactive): make mk_simp_set public 2017-06-04 13:23:26 -07:00
Jeremy Avigad
c2df664c39 feat(library/init/meta/tactic): make tactics that introduce a local constant return the expr 2017-06-04 13:23:26 -07:00
Jeremy Avigad
7fe0fff91d feat(library/init/meta/interactive): add 'only' option for simp, dimph, dimp_intros, and dsimp 2017-06-04 13:23:26 -07:00
Jeremy Avigad
862d23f6b6 fix(library/init/meta/interactive): disallow wildcard in rewrite 2017-06-04 13:23:26 -07:00
Jeremy Avigad
4160f23847 fix(library/init/meta/interactive): fix printing of description string for locations 2017-06-04 13:23:26 -07:00
Jeremy Avigad
649118c99a fix(library/init/meta/interactive): remove sorry in dunfold_occs 2017-06-04 13:23:26 -07:00
Jared Roesch
998f90b849 feat(library/init/meta/interactive): add support for location wildcards 
This allows users to now use  to apply a tactic in all hypotheses as well as the goal, we add support for all
interactive tactics using location: rewrite, simp, dsimp, unfold, and delta including each tactics many variants.
 2017-06-04 13:23:26 -07:00
Leonardo de Moura
81e97de463 feat(library/init/meta/interactive): allow metavars in the show_goal tactic 2017-06-01 19:46:38 -07:00
Leonardo de Moura
18467bd302 feat(library/init/meta/interactive): add show_goal tactic for structuring proofs in interactive tactic mode 2017-06-01 18:36:50 -07:00
Leonardo de Moura
5446df1609 feat(library/init/meta/interactive): add interactive done tactic 2017-06-01 17:28:52 -07:00
Leonardo de Moura
1c6e70d170 feat(library/init/meta): introv tactic 
@Armael: this commit implements the `introv` tactic.
The implementation uses an auxiliary `intros_dep` that introduces new
hypotheses with forward dependencies.

The `tactic.introv` tactic implemented at library/init/meta/tactic.lean
is the main implementation, but it is not nice for interactive use since
users would have to write
```
tactic.introv [`h1, `h2]
```
To make it more conveninent to use, we define another
```
meta def introv (ns : parse ident_*) : tactic unit :=
tactic.introv ns >> return ()
```
This one is in the namespace `tactic.interactive`, and
uses parser extensions. The argument `parse ident_*` instructs
the parser to parse 0 or more identifiers and create a term
of type `list name` containing these identifiers.
 2017-05-31 14:09:25 -07:00
Leonardo de Moura
71ef240817 feat(library/init/meta/interactive): add nary existsi 
@Armael, this commit implements the nary existsi.
We can now write
a) existsi t
b) existsi [t_1, t_2, t_3]
 2017-05-31 13:41:25 -07:00
Sebastian Ullrich
9fa31b2858 fix(init/meta/interactive): handle pure in parser signature descs 2017-05-31 16:05:02 +02:00
Mario Carneiro
9c29206386 feat(init/meta/injection_tactic): injections tactic 
Runs injection repeatedly on the LC and subgoals
 2017-05-27 06:15:47 -04:00
Mario Carneiro
6e88119f55 feat(init/meta/injection_tactic): better injection tactic 
(1) The lhs and rhs will be reduced to whnf before getting the constructor apps
(2) If the lhs and rhs are distinct constructors, it discharges the goal by contradiction
(3) The interactive injection tactic will try to close the goal by assumption if successful
 2017-05-27 04:59:40 -04:00
Mario Carneiro
57837c2b3e fix(init/meta/tactic): let by_cases handle elimination to Type 2017-05-27 04:14:06 -04:00
Mario Carneiro
1d3887dd3f fix(init/meta/interactive): bug in generalize2 2017-05-27 04:13:57 -04:00