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

197 commits

Author SHA1 Message Date
Sebastian Ullrich
1c389cb925 chore(init/meta/interactive): hide rw ASCII notation in syntax description 2017-07-06 14:03:08 +02:00
Leonardo de Moura
70ade81a30 feat(library/init/meta/interactive): allow user to set configuration options at unfold_projs 
See issue #1725
 2017-07-05 13:00:43 -07:00
Leonardo de Moura
bb9e3ddae2 feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 
@Armael: this change may affect your project.

The file `doc/changes.md` explains the motivation for the change.
 2017-07-05 11:42:55 -07:00
Sebastian Ullrich
c8d6b40991 refactor(frontends/lean/builtin_exprs,library): suppose ~> assume : 2017-07-05 11:20:10 -07:00
Sebastian Ullrich
2ca44459ba feat(init/meta/interactive): add from synonym for exact 2017-07-05 11:20:10 -07:00
Sebastian Ullrich
ad97607307 fix(frontends/lean/tactic_notation): always use quote_scope for parsing interactive parameters 
Replace now redundant `qexpr` parser with `parser.pexpr`
 2017-07-04 12:20:38 -07:00
Sebastian Ullrich
c3d4c468e6 fix(init/meta/interactive): whnf in assume tactic 2017-07-04 12:20:38 -07:00
Leonardo de Moura
dd3616dd16 feat(library/init/meta/interactive): simp_all ==> simp * at * 
cc @Kha
 2017-07-04 11:57:16 -07:00
Leonardo de Moura
d0ab9d0cd1 feat(library/init/meta/interactive): simp * as shorthand for simp [*] 2017-07-04 11:57:16 -07:00
Leonardo de Moura
44c901bf11 fix(library/init/meta/interactive): make sure all input hypotheses are simplified before we clear the old ones 
The new test exposes the bug.
The bug is similar to the one at `simp [h] at *` described at issue #1675
 2017-07-03 21:58:55 -07:00
Leonardo de Moura
abef98c772 refactor(library/init/meta/simp_tactic): make sure dunfold tactics use name convention used at simp, dsimp, ... 2017-07-03 21:36:17 -07:00
Leonardo de Moura
e24f3341d4 feat(library/init/meta/interactive): simp without foo ==> simp [-foo] 
This commit also adds "exception" validation.
A bad "exception" was being silently ignored.
We can also exclude hypotheses. Example: `simp [*, -h]`
 2017-07-03 17:10:46 -07:00
Leonardo de Moura
76799db032 feat(library/init/meta/interactive): simph ==> simp [*] 
This modification was suggested by @kha.

TODO:
- Use `simp [-f]` instead of `simp without f`
- Allow users to remove hypothesis from `*`. Example: `simp [*, -h]`
  for simplify using all hypotheses but `h`.
 2017-07-03 15:14:47 -07:00
Leonardo de Moura
69ed291aab refactor(library/init/meta/simp_tactic): tactic.simp_at => tactic.simp_hyp 2017-07-03 14:07:18 -07:00
Leonardo de Moura
34c212fa53 refactor(library/init/meta/simp_tactic): cleanup simp_intros mess 2017-07-03 13:46:16 -07:00
Leonardo de Moura
6b3e28d30b feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic 
This complete addresses the two pending items at 16711fcdba
 2017-07-03 13:28:46 -07:00
Leonardo de Moura
df091f5c34 feat(library/init/meta/interactive): simp and unfold can unfold projection applications 
@Armael: we finally can write `simp [proj]` to unfold the `proj`
projection application.

Remark: we still need to add similar support for `dsimp`.
 2017-07-02 16:28:04 -07:00
Leonardo de Moura
76eed7cb41 chore(library/init/meta): add to_unfold parameter to simplify, and remove redundant simp* tactics 
Remark: the `to_unfold` has not been implemented yet.
 2017-07-02 15:26:06 -07:00
Leonardo de Moura
70b27fb2d3 feat(library/init/meta/interactive): unfold is now based on the simp framework 
See issue #1694.

There is an orthogonal issue. `simp` (and consequently `unfold`) cannot be used to
reduce projections (e.g., `has_add.add`). This issue has been
previously raised by @Armael, but it was not addressed yet.
 2017-07-02 11:30:48 -07:00
Leonardo de Moura
01003b79cc fix(library/init/meta/interactive): simp [...] at * 
closes #1675

After this commit, the following example works as expected.
```
example (p : nat → Prop) (a b : nat) : a = 0 ∧ b = 0 → p (a + b) → p 0 :=
begin
  intros h₁ h₂,
  simp [h₁] at *,
  /- produces the state
     (p : nat → Prop) (a b : nat)
     h₁ : true
     h₂ : p 0
     |- p 0
  -/
  assumption
end
```
as expected.
Remark: the original issue raised by issue #1675 is actually solved by the
`simp_all` tactic.
 2017-07-01 20:50:46 -07:00
Leonardo de Moura
3422c8816e feat(library/init/meta/simp_tactic): improved simp_all tactic 
It now performs self simplification, and the performance is slightly
better. As described at issue #1675, only non dependent propositions
are considered.

@Armael: this tactic may be useful for you
 2017-07-01 20:26:29 -07:00
Leonardo de Moura
4604d7fd5a feat(library/init/meta): allow users to specify tactic for discharging subgoals in the simp tactic family 
@dselsam @Armael: this feature may be useful for you.
The doc/changes.md describes many other new features.
 2017-07-01 15:35:33 -07:00
Leonardo de Moura
7c35fae9e3 refactor(library/init/meta/simp_tactic): merge simplify_core and simplify 2017-07-01 14:13:49 -07:00
Leonardo de Moura
95c7c697a6 refactor(library/tactic/simp_lemmas): simp set generation should not be affected by transparency setting 2017-07-01 12:54:37 -07:00
Leonardo de Moura
b1bdc4690f feat(library/init/meta/simp_tactic): cleanup dunfold 
Here are modifications:
- It fails if no definition is unfolded.
  See comment https://github.com/leanprover/lean/issues/1694#issuecomment-310956315
  at issue #1694

- Users can provide configuration parameters.

- `dunfold_occs` was deleted.
 2017-06-30 20:49:20 -07:00
Leonardo de Moura
52d4189805 feat(library/tactic): add dsimp_config configuration object for the dsimp tactic family 
Now, `dsimp` fails if the goal did not change.
We can use the config object to obtain the previous behavior:
```
dsimp {fail_if_unchaged := ff}
```
See comment https://github.com/leanprover/lean/issues/1694#issuecomment-310956315
at issue #1694
 2017-06-30 17:15:10 -07:00
Leonardo de Moura
6208934134 feat(library/init/meta/converter/interactive): add support for rw at conv tactical 2017-06-30 12:41:35 -07:00
Leonardo de Moura
f7fe2a775c feat(library/init/meta/rewrite_tactic): improve rewrite tactic 
`rewrite` tactic improvements
- Add support for `auto_param` and `opt_param`
- Order new goals using the same strategies available for `apply`
- Allow user to set configuration object in interactive mode.

@Armael This commit should address the issue you raised about the order
of new goals in the `rewrite` tactic.
See new test tests/lean/run/rw1.lean for examples.
 2017-06-30 12:03:27 -07:00
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