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
Jared Roesch
191a3d662d
feat(leanpkg): add initial support for test command
2017-05-24 14:55:59 -07:00
Sebastian Ullrich
84997bf4de
refactor(init/meta/expr): unify expr and pexpr
2017-05-17 10:38:12 -07:00
Leonardo de Moura
cb6d5675df
chore(library/init): ^. ==> .
2017-05-16 15:00:58 -07:00
Mario Carneiro
6b28499e47
feat(init/data/list,data/list): new basic list operations from haskell
2017-05-16 14:38:43 -07:00
Leonardo de Moura
4575c9e038
feat(frontends/lean): swap (t) and ``(t) semantics
2017-05-15 09:41:31 -07:00
Mario Carneiro
7ace147f25
refactor(init/meta/tactic): replace assertv -> note, definev -> pose
2017-05-14 19:34:27 -07:00
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
