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

3292 commits

Author SHA1 Message Date
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
2f2694a343 chore(tests/lean/interactive/info_tactic): fix test output 2017-07-01 13:11:07 -07:00
Sebastian Ullrich
3cdf502c58 fix(frontends/lean/pp): escape keyword-like identifiers 2017-07-01 10:38:15 -07:00
Leonardo de Moura
b05c4e09ed feat(library/init/meta): add memoize field to simp_config and dsimp_config 
We use `memoize := ff` when implementing `conv.interactive.for` and
`conv.interactive.find`.
 2017-07-01 10:37:09 -07:00
Leonardo de Moura
36cc27fa0f feat(library/init/meta/converter/interactive): add for tactic to conv mode 2017-06-30 21:27:17 -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
9504c9cabc feat(library/init/meta/converter): add support for dsimp parameters for conv mode 2017-06-30 17:37:24 -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
19f65b3b8a test(tests/lean/run/conv_tac1): another conv test 2017-06-30 12:49:41 -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
e1c76578c1 chore(tests/lean/run, doc/changes): more tests and document new feature 2017-06-29 17:12:04 -07:00
Leonardo de Moura
fe51bebab3 refactor(library/init/meta/converter): new conv monad implementation 2017-06-29 16:37:22 -07:00
Leonardo de Moura
99d55811e4 feat(library/tactic/match_tactic): automatically convert metavariables occurring in patterns into temporary metavariables (i.e., which are considered during matching) 2017-06-29 11:39:18 -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
Leonardo de Moura
6669ff2132 feat(library/init/meta): add conv interactive mode 
Remark: this is just the first step, we still need to populate the
`conv.interactive` namespace with tactics such as rewrite, simp, etc.
 2017-06-28 16:09:49 -07:00
Leonardo de Moura
adcb95626e feat(frontends/lean/tactic_notation): allow interactive tactics to take itactic arguments from a different tac_class 2017-06-28 14:51:42 -07:00
Leonardo de Moura
0b19ef82e1 feat(frontends/lean/structure_cmd): default parameter for structure/class declarations 
Remark: we support them at inductive declarations.
 2017-06-28 12:20:56 -07:00
Sebastian Ullrich
f53fa97c4a feat(frontends/lean): escape identifiers when pretty-printing 2017-06-28 10:43:19 -07:00
Mario Carneiro
bae50f8ce6 fix(tests/lean): fix tests 2017-06-27 18:55:52 -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
e971acabb0 feat(library/init/meta): handle auto_params and opt_params at apply tactic 2017-06-27 18:17:48 -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
ac19b15169 fix(library/tactic/apply_tactic): remove unnecessary code from apply_tactic, and add tests for #1342 
See issue #1342
 2017-06-27 16:07:59 -07:00
Leonardo de Moura
9b03309d83 fix(library/equations_compiler): performance problem reported by @dselsam 2017-06-27 15:24:12 -07:00
Leonardo de Moura
3300eafd39 fix(frontends/lean/parser): fixes #1705 
This is a temporary fix.
We will be able to implement a better solution after #1674.
 2017-06-27 13:20:37 -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
Leonardo de Moura
68afd4194b fix(library/tactic/simplify): fixes #1659 
@dselsam The method `try_user_congr` was leaking a temporary
meta-variable into the formula. The problem in the congruence lemma
```
dif_ctx_simp_congr :
  ∀ {α : Sort u_1} {b c : Prop} [dec_b : decidable b] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
  (h_c : b ↔ c),
    (∀ (h : c), x (h_c.mpr h) = u h) →
    (∀ (h : ¬c), y ((not_iff_not_of_iff h_c).mpr h) = v h) → dite b x y = dite c u v
```
when the hypothesis `(∀ (h : c), x (h_c.mpr h) = u h)` is processed,
`h_c` is still unassigned. `h_c` was being assigned in a second
loop (the one that I deleted). Do you see any reason for having this
second pass? I think it is an optimization, we can skip the potentially
expensive
```
   expr hyp = finalize(m_ctx, rel, r_congr_hyp).get_proof();
   expr pf = local_factory.mk_lambda(hyp);
```
if the expression has not been simplified.
Anyway, I removed this code and merged both loops.
I don't think it should impact performance since we barely use custom
congruence lemmas.
 2017-06-26 15:25:58 -07:00
Leonardo de Moura
f339f97975 fix(frontends/lean/brackets): fixes #1703 2017-06-26 12:52:52 -07:00
Daniel Selsam
d95b003c0b feat(init/meta/congr_tactic.lean): tactic to apply congruence rules 2017-06-26 09:17:53 -04:00
Leonardo de Moura
ce5ca79edf feat(library/init/meta): add type_check tactic 
closes #1697
 2017-06-25 15:26:32 -07:00
Mario Carneiro
d3d5982544 fix(init/meta/mk_dec_eq_instance): bug for dependent structures 2017-06-25 14:55:47 -07:00
Leonardo de Moura
41a1faa131 fix(frontends/lean/elaborator): check resulting type at visit_convoy 2017-06-25 10:50:40 -07:00
Gabriel Ebner
16fb5ade58 fix(library/string): correctly escape non-printable characters 
This also fixes a compiler warning on ARM, where `0 <= c` is always
true.
 2017-06-23 20:39:41 +02:00
Gabriel Ebner
30a9217a78 feat(library/type_context): unfold lemmas in major premise of acc.rec 2017-06-22 08:33:11 -07:00
Mario Carneiro
47c3c0ba84 fix(tests/*): fix tests 2017-06-22 08:24:19 -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
495093f6c0 fix(tests/run): fix tests 2017-06-22 08:03:23 -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
Leonardo de Moura
51a28828d6 chore(tests/lean/interactive/info_tactic): fix test 2017-06-21 17:03:24 -07:00
Leonardo de Moura
b9dee04fdb feat(library/tactic/simplify): add single_pass simplifier option (default is false) 2017-06-21 16:41:54 -07:00
Leonardo de Moura
9fcb3ae4b5 feat(library/tactic/simplify): store proof for refl lemmas and use them in simp 
Before this commit, simp would not silently apply refl-lemmas, and use
reflexivity. This strategy produces compact proofs but may generate
performance problems. For example, the new test timeouts without this
commit.

I believe a similar performance problem is affecting the Certigrad
project developed by @dselsam.
 2017-06-21 16:21:11 -07:00
Mario Carneiro
e6f3c5cc22 fix(tests/lean/interactive/mk_input): strip \r from input files (win) 2017-06-21 08:53:11 +02:00
Leonardo de Moura
eef4d95410 feat(frontends/lean/inductive_cmds): closes #1655 2017-06-20 16:25:18 -07:00
Leonardo de Moura
5a07b3b27c test(tests/lean/run/1688): add test for PR #1688 2017-06-20 12:36:31 -07:00
Leonardo de Moura
b25291c5c9 fix(library/tactic/simplify): fixes #1685 2017-06-20 12:27:46 -07:00
Leonardo de Moura
ce3387b246 fix(library/tactic/change_tactic): fixes #1686 2017-06-20 12:05:21 -07:00