Automating Decidable Instance Synthesis (#36)

* Add helpers to make decidability proofs a bit easier

The example usage of these tactics/macros can be seen in Sorted.lean,
SubstringSearch.lean and LinearSearch.lean. These examples make usa of a
lot of quantifers and are quite complex to be proven automatically.

* feat: a tactic for synthesizing `Decidable` instances with heuristics

* feat: allow multiple quasi-instances

This introduces some priority and might be used to avoid exceeding array
bounds.

* fix: auto-synthesis with pre-unfolding

* feat: add a score mechanism in `infer_aux_decidable_instance`

* fix one case taking too long in synthesizing `Decidable` instances

Fixed by the scoring mechanism (sounds more like a hack to work around a
bug in Lean??)

* chore: update the Velvet documentation wrt. the synthesis strategy

* chore: remove some unproven cases and move their postconditions into a new file

* fix: add `simp` into `infer_aux_decidable_instance`

* fix: also consider `>` and `≥` in scoring

* fix: an important note

---------

Co-authored-by: Dipesh Kafle <dipesh.kaphle111@gmail.com>

Author: zqy1018