This adds a number of lemmas for simplification of `Bool` and `Prop`
terms. It pulls lemmas from Mathlib and adds additional lemmas where
confluence or consistency suggested they are needed.
It has been tested against Mathlib using some automated test
infrastructure.
That testing module is not yet included in this PR, but will be included
as part of this.
Note. There are currently some comments saying the origin of the simp
rule. These will be removed prior to merging, but are added to clarify
where the rule came from during review.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This is still a draft PR, but includes the core exact? and apply?
tactics.
Still need to convert to builtin syntax and test on Std.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
in all uses of `CasesOnApp`, we treat `MatcherApp`s the same way,
dupliating a fair amount of relatively hairy code (and there is more to
come).
However, the `MatcherApp` abstraction is perfectly capable of
also representing `casesOn` applications, at least for the use cases
encountered so far.
So lets just (optionally) include `casesOn` applications when looking
for matchers,
and remove the `CasesOnApp` abstraction completely.
Moves the `@[coe]` attribute and associated elaborators/delaborators
from Std to Lean.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
We don't use the following hack anymore:
- /- HACK: `fvarId` is not in the scope of `mvarId`
- If this generates problems in the future, we should update the metavariable declarations. -/
- assignExprMVar mvarId (mkFVar fvarId)
This hack was corrupting the `InfoTree`.
We need `MetaM` methods such as `isProp` to improve `ppGoal`.
This commit also moves `currNamespace` and `openDecls` to
`Core.Context`. Without this change, `Meta.ppExpr` was not taking
`open` commands into account.
