Commit 2023-01-09 15:05 a445a5e1

feat: refactor of solve_by_elim (#856) This is a thorough refactor of solve_by_elim.

• Bug fixes and additional tests.
• Support for removing local hypotheses using solve_by_elim [-h].
• Use symm on hypotheses and exfalso on the goal, as needed.
• To support that, MetaM level tooling for the symm tactic. (rfl and trans deserve the same treatment at some point.)
• Additional hooks for flow control in solve_by_elim (suspending goals to return to the user, rejecting branches, running arbitrary procedures on the goals).
• Using those hooks, reimplement apply_assumption and apply_rules as thin wrappers around solve_by_elim, allowing access to new features (removing hypotheses, symm and exfalso) for free.
• Using those hooks, fix library_search using so example (P Q : List ℕ) (h : ℕ) : List ℕ := by library_search using P, Q -- exact P ∩ Q