Default tactic script should use `plausible` instead of `sorry`

`plausible` is strictly better than `sorry` – it will only complain if it finds a concrete counter-example, and otherwise will let proofs go through. We could rename `--allow-sorry` to `--allow-plausible`.

When `--allow-plausible` is *not* given, we may still want to add `plausible` as the last tactic step if all previous steps fail. Instead of opaque errors about unsolved goals, this *may* sometimes generate a concrete counter-example, which would be more helpful to users.