We use the same approach used to define rbtree:
1- Structure with minimal number of invariants, AND
2- well_formed inductive predicate
We can use the well_formed predicate to prove auxiliary invariants later.
Example: the keys stored in every bucket have the correct hash code.
This implementation does not depend on the tactic framework,
and it is not a mess like the one in mathlib.
The problem is that `auto_param` is defined in the old `init/meta/name` module,
and we don't want to have `init/meta` dependencies in the `init/lean` modules.
The tactic mk_dec_eq_instance constructs a function using the brec_on
recursor. The compiler generates horrible code for this kind of
definition. It creates a closure for each recursive call.
Moreover, `brec_on` accumulates all intermediate results.
To generate efficient code, we need to generate a collection of
recursive equations, and then invoke the equation compiler.
cc @kha
The idea is to match the precedence used in regular programming
languages, where `x = y || x = z` is parsed as `(x = y) || (x = z)`.
This commit also adds `!x` as notation for `bnot x`
All theorems are proved without using the tactic framework.
Thus, we can define `fin/uint32/uint64` types and their operations
before we define the tactic framework.
With the current elaboration scheme, out_params and coercions do not mix well,
as evidenced by the following example by @digama:
```
variables {α : Type*} [group α]
def gpow : α → ℤ → α := sorry
instance group.has_pow : has_pow α ℤ := ⟨gpow⟩
example (a : α) : a ^ 0 = 1 := sorry -- failed to synth ⊢ has_pow α ℕ
example (a : α) : a ^ (0:ℕ) = 1 := sorry -- ok, coerces
example (a : α) : a ^ (0:ℤ) = 1 := sorry -- ok
```
The issue is that
* we first try to solve `has_pow ?α ?β`, which is postponed
* then infer `?α = nat` from `a`
* then at some point call `elaborator::synthesize()` and default `β` to `nat`
* then try to solve `has_pow nat nat`, which fails at `int =?= nat`
