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

34 commits

Author SHA1 Message Date
Leonardo de Moura
ab487ea4ac feat(frontends/lean): allow ; instead of in in let-decls 2019-06-27 17:12:03 -07:00
Leonardo de Moura
d2d2c32c81 feat(library/init/data/nat/bitwise): use lean::nat_land and lean::nat_lor 2019-05-31 21:55:57 -07:00
Leonardo de Moura
b66f5dcf5c chore(library/init): avoid wf_term_hack 2019-03-27 12:12:21 -07:00
Leonardo de Moura
3fe5cf1528 chore(library/init/core): remove another weirdness: the bs at bnot, band and bor 2019-03-22 12:57:31 -07:00
Leonardo de Moura
2be87ecd92 chore(library/init): Bool.tt => Bool.true and Bool.ff => Bool.false 2019-03-21 15:06:44 -07:00
Leonardo de Moura
2ea0baeb99 chore(library): use lowercase in imports 2019-03-21 15:06:44 -07:00
Sebastian Ullrich
beda5f5f43 chore(library): capitalize types and namespaces 2019-03-21 15:06:43 -07:00
Leonardo de Moura
2032b10482 feat(library/init/data): bitwise operations 2019-03-09 10:19:35 -08:00
Leonardo de Moura
a023128738 chore(*): reduce corelib 2018-04-10 13:11:40 -07:00
Leonardo de Moura
746134d11c feat(library/init/meta/interactive): add goal tagging support for by_cases 
This commit also incorporates changes suggested at commit 84a1911949dec94.
 2017-12-13 15:17:13 -08:00
Leonardo de Moura
49e7a642c3 feat(library/init/meta/interactive): merge ginduction and induction 
This commit is based on 638b34b16de6443.
The changes were applied manually to make sure all changes are
compatible with our plans to `induction`.
 2017-12-07 19:10:10 -08:00
Leonardo de Moura
6d96741010 feat(library): provide names for constructor arguments 
Motivation: `cases` and `induction` tactics use these names when the
user does not provide them.
 2017-12-04 16:25:16 -08:00
Leonardo de Moura
c943576e5a feat(library/init): add funext tactic 2017-12-04 14:54:39 -08:00
Leonardo de Moura
b7322e28c1 feat(library): do not using simp lemmas for sorting arguments of AC operators by default 2017-12-03 15:03:58 -08:00
Mario Carneiro
bd19736b21 feat(init/data/nat/bitwise): definitional lemmas for nat.shiftl 2017-07-28 16:47:53 +01:00
Leonardo de Moura
1ec65bed44 refactor(library/init): move bitvector to main repo 
@digama0 I moved bitvec back to the main repo, and many nat lemmas.
I want these lemmas here for now. I will need some of them for future
decision procedures.
 2017-07-26 13:35:38 +01:00
Mario Carneiro
cc81118892 refactor(init/data): move out some nat lemmas 2017-07-26 11:52:10 +01:00
Sebastian Ullrich
7d39b3e948 refactor(init/meta/interactive): merge generalize and generalize2 and introduce nicer syntax 2017-07-20 01:51:00 -07:00
Mario Carneiro
4ae2f87bc8 refactor(init/meta/tactic): use dite instead of cases in by_cases 
This fixes the issue in PR #1752 by using `dite`, which is essentially nondependent cases, so that the decidable instances are not substituted.
 2017-07-20 01:28:21 -07:00
Leonardo de Moura
b7b331957a chore(library/init/data/nat/bitwise): we now support rw [f] for applying f-eqn_lemmas 2017-07-07 12:03:47 -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
Leonardo de Moura
9a41f0f899 fix(library/init/meta/tactic): by_cases tactic 
Before this commit, the `by_cases p` tactic would synthesize
`inst : decidable p` type class resolution, and then use the
`cases` tactic (dependent elimination). This would create
problems since occurrences of `inst` would be replaced with
`decidable.is_true h` in one branch, and `decidable.is_false h` in the
other. Where `h`s (we have two of them, one for each branch) are
fresh hypotheses introduced by the `cases` tactic.
For example, assume we have the term in our goal.

        `@ite p inst A a b`

This term would become

        `@ite p (decidable.is_true h) A a b` (in the first branch where `h : p`)

and
        `@ite p (decidable.is_false h) A a b` (in the second where `h : not p`)

Now, suppose we try to executed the following tactic in the first branch

        `rw [if_pos h]`

it will fail since `if_pos h` is actually `@if_pos p inst h`, and
we will not be able to unify

        `@ite p (decidable.is_true h) A a b =?= @ite p inst ?A ?a ?b`

This commit workarounds this problem by applying cases on
`@decidable.em p inst : p or not p` instead of `inst : decidable p`.
Thus, the term `inst` is not replaced with `decidable.is_true h` and
`decidable.is_false h`.

The new test `tests/lean/run/simp_dif.lean` demonstrates the problem above.
 2017-07-02 21:34:10 -07:00
Leonardo de Moura
16711fcdba feat(library/tactic/dsimplify): new configuration options for dsimp 
TODO for `dsimp`:
- Add an option for reducing [reducible] definitions
- Add (to_unfold : list name) similar to the one in the `simp` tactic
 2017-07-02 18:26:03 -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
Mario Carneiro
9f2980a524 feat(init/data/int): int lemmas, more bitwise theorems 2017-06-27 18:55:52 -07:00
Mario Carneiro
9f4f93e931 feat(init/data/int): prove int bitwise ops 2017-06-27 18:55:52 -07:00
Mario Carneiro
a63bafcc5c refactor(init/data/nat/bitwise): change definitions to avoid WF 
The type-correctness of binary_rec_eq (the statement, not the proof) depends on unfolding the embedded well-founded definition of mod. This definition avoids it by using two simpler functions bodd and div2 that reduce well in the kernel.
 2017-06-27 18:55:52 -07:00
Gabriel Ebner
30a9217a78 feat(library/type_context): unfold lemmas in major premise of acc.rec 2017-06-22 08:33:11 -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
Leonardo de Moura
293ab6a032 fix(library/init/data/nat/bitwise): broken lemma 2017-05-31 15:08:03 -07:00
Mario Carneiro
41b928a546 feat(init/data/nat/bitwise): properties of bitwise ops 2017-05-31 14:18:44 -07:00
Mario Carneiro
18b622d709 chore(init/data/nat): modify bitwise defs 2017-05-31 14:18:44 -07:00
Leonardo de Moura
cbca84a8ea chore(library/init/data/nat/bitwise): fix copyright date 2017-05-30 13:05:37 -07:00
Mario Carneiro
860e2d904d feat(init/data/nat): bitwise operations 2017-05-30 12:47:44 -07:00