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

205 commits

Author SHA1 Message Date
Leonardo de Moura
16e7976b1a chore(library/init/data/vector): remove [...] notation for vectors 
This is a temporary workaround. The problem is that this notation
overloads the one in list, and we currently can't handle nary
overloads in patterns.
 2017-07-26 13:45:30 +01:00
Leonardo de Moura
a258620425 feat(library/init/data/default): add vector and bitvec 2017-07-26 13:38:51 +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
fb2447468b chore(init/category/combinators): remove monad.for 
and variations, in favor of monad.map and variations
 2017-07-26 11:52:11 +01:00
Mario Carneiro
4dc261393f refactor(init/data/list): move out advanced list defs 2017-07-26 11:52:11 +01:00
Mario Carneiro
813fda9ba5 refactor(init/data/{nat,list}): rename for consistency with stdlib 2017-07-26 11:52:10 +01:00
Mario Carneiro
09f9cada65 chore(init/data/nat): rename add_one_eq_succ -> add_one 2017-07-26 11:52:10 +01:00
Mario Carneiro
cc81118892 refactor(init/data): move out some nat lemmas 2017-07-26 11:52:10 +01:00
Leonardo de Moura
4faae27069 perf(frontends/lean): add notation #[...] 
The new notation should be use to input long sequences.
Closes #1755
 2017-07-21 04:20:48 -07: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
Gabriel Ebner
ee56f71260 fix(library/init/data/nat/lemmas): make various lemmas rfl 2017-07-15 10:38:06 +01: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
Sebastian Ullrich
ac8de2472e feat(library/tactic/induction_tactic): clear hypothesis before introducing new ones 2017-07-07 10:06:30 -07:00
Gabriel Ebner
c5b6c52ad1 feat(library/init/data/nat/lemmas): decidable_linear_ordered_cancel_comm_monoid instance 2017-07-07 08:49:12 +02:00
Leonardo de Moura
9645e7588e chore(library/init/data): recent changes 2017-07-05 12:44:56 -07:00
Mario Carneiro
b557d9012d refactor(init/data/nat/gcd): swap args in gcd.induction 
to match swapped induction arg of gcd
 2017-07-05 12:37:54 -07:00
Mario Carneiro
a1cfce88d5 feat(init/data/list): filter theorems, non-meta qsort 2017-07-05 12:37:54 -07:00
Mario Carneiro
35ed9e9301 feat(init/data/ordering): ordering.or_else, string lex order 2017-07-05 12:37:54 -07:00
Mario Carneiro
387c7d46b4 refactor(init/data/fin/basic): shorten fin dec eq proof 2017-07-05 12:37:54 -07:00
Mario Carneiro
42d26a3954 feat(init/data/array): array theorems 2017-07-05 12:37:54 -07:00
Mario Carneiro
1ca6aba076 feat(data/buffer): decidable_eq instance 2017-07-05 12:37:54 -07:00
Mario Carneiro
9fc04ae812 feat(init/data/option/instances): = none of is_none 2017-07-05 12:37:54 -07:00
Mario Carneiro
0172c17447 feat(init/data/bool/lemmas): theorems about to_bool and bool coercion 2017-07-05 12:37:54 -07:00
Mario Carneiro
e2a3331c7c refactor(init/data/option/instances): option_map 2017-07-05 12:37:54 -07:00
Mario Carneiro
803af7cd63 feat(library/data/stream): more stream theorems 2017-07-05 12:37:53 -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
30f4b2f2dd refactor(library): list.taken/dropn ~> list.take/drop 2017-07-05 11:20:10 -07:00
Sebastian Ullrich
c8d6b40991 refactor(frontends/lean/builtin_exprs,library): suppose ~> assume : 2017-07-05 11:20:10 -07:00
Sebastian Ullrich
f024ccd75d refactor(frontends/lean/token_table,library): take ~> assume 2017-07-05 11:20:10 -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
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
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
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
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
Mario Carneiro
c06c62c03e refactor(init/data/nat/gcd): define gcd using eqn compiler 2017-06-27 18:55:52 -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
e705d89490 feat(init/data/int): bitwise ops for integers 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
Mario Carneiro
b775a01fba refactor(init/meta/interactive): merge assert -> note 2017-06-22 08:03:23 -07:00
Gabriel Ebner
2e142d87ae fix(library/init/data/repr): give correct implementation of nat.repr 2017-06-19 16:20:27 +02:00
Gabriel Ebner
82bb37422d fix(library/init/data/int): add to_string instance for integers 2017-06-19 14:30:58 +02:00
Leonardo de Moura
8b88f21c91 refactor(library): add has_to_string back (but it produces unquoted values) 
See issue #1664
 2017-06-18 18:30:10 -07:00