@nunoplopes @aqjune
I had to add a new primitive to allow you to execute a tactic from the
`main` function. The `main` function is in the `io` monad. The new
primitive has type:
```
meta constant io.run_tactic {α : Type} (a : tactic α) : io α
```
I also added a new test that shows how to use it.
The test displays all declarations that have the `nat` prefix.
cc @kha
Reason: `rsimp` is based on the smt framework. The smt framework
has to be reimplemented. Moreover, the smt framework is currently
not using the new cache infrastructure and we pay a substantial
performance penalty.
The tactic_state object will contain a name_generator for creating fresh
names. `tactic_state.mk_empty` is bad because it does not have sufficient
information to create this name_generator.
Moreover `tactic_state.mk_empty` was only being used to convert
`tactic A` into a `parser A`.
We implement this primitive now in C++. In C++, we will be able
to use the parser name generator to initialize a fresh `tactic_state`.
The tactic `mk_fresh_name` is used to create internal unique ids.
We should not use them to create (temporary) user facing
names. Reasons:
1- They are "cryptic".
2- They are not very stable. Minor changes in Lean may change the
value returned and may break proofs that rely on these fresh names.
@aqjune @nunoplopes: See new tests at tests/lean/run/random.lean
We have two actions in `io`. By default, `io` uses the C++
random number generator, but we can force it to use a `std_gen` with
the action `set_rand_gen`.
def rand (lo : nat := std_range.1) (hi : nat := std_range.2) : io nat
def set_rand_gen : std_gen → io unit
@aqjune @nunoplopes: This commit adds basic support for random numbers.
It defines a random number generator interface, and an basic
implementation based on the Haskell one.
We can add more implementations in the future if neeeded.
The new test program has a few examples.
BTW, this is a pure Lean implementation.
If we need more performance we can provide an implementation
using C++.
The theorems themselves are unchanged, although the proofs had to be reordered and changed a bit to accomodate.
Conflicts:
library/init/algebra/ordered_field.lean
The previous `decidable_bex` was using a nasty hack.
First, it was relying on a bug in the local_context object that was
fixed at commit 6060b75e6. Note that, the type class resolution
will be even more restrictive after we implement the fix described at a75b0d8ee.
Second, it was built using tactics that are meant for constructing
proof irrelevant code (e.g., `simp`).
We also document the problem to make sure we don't spend time again
trying to understand the workaround. This is an instance of a bigger
problem that should be addressed later.
- An new simp attribute may depend on other existing attributes
- Add `[norm]` simp attribute. It is an extension of the default `[simp]` attribute.
It should be used to add extra rules for normalizing goals.
These extra rules are used to produce normal forms and/or reduce the
number of constants used in a goal. Here is an example coming from a
discussion with @kha. When working with monads, we may want to
eliminate `<$>` by using the lemma `f <$> x = x >>= pure ∘ f`.
This lemma is in the `[norm]` simp set, but it is not in `[simp]`
