geo2a

Tactic Notation
  "`Begin " constr(lhs) := idtac.

Tactic Notation
  "≡⟨ " tactic(proof) "⟩" constr(lhs) :=
  (stepl lhs by proof).

Tactic Notation
  "≡⟨ " tactic(proof) "⟩" constr(lhs) "`End" :=
  (now stepl lhs by proof).

geo2a

This is a follow-up for Li-yao Xia's answer on my StackOverflow question

Thanks for your answer Li-yao! I have a couple of follow-up notes/questions:

A Fixpoint on terms indexed by function types A -> B is useless since
no subterms of any Select term are indexed by function types.
For the same reason, induction is useless on such terms.

geo2a

import Control.Monad.IO.Class (liftIO)

import Data.SBV

import Data.SBV.Examples.BitPrecise.Legato

prover = z3 { verbose = True
            , redirectVerbose = Just "example.smt2"
            , timing = PrintTiming
            , printBase = 10