Lean3 and SMT Solvers for Refinement Types

f.lean

import tactic.suggest
import tactic.basic
import smt

open smt_tactic

set_option pp.all true

lemma example_of_something_for_which_smt_is_useful 
        (f : list nat → list nat) (a b c : list nat) :

        f a = [] →
        f b = [0, 1] →
        f a = f b ∨ f a = c →
        c = [] :=
begin
   using_smt intros
end


def main : {p : int // p > 0} → {r : int // r > 1}
| p := begin
        cases p with p_val p_property,
        split,
        rotate,
        {
                exact p_val+1,
        },
        {
                /- Option 1: this does not advance the goal -/
                -- using_smt intros,

                /- Option 2, simplifies a bit, but does no real work. -/
                -- smt.prove,
                
                /- Option 3: library_search looks for existing lemmas
                 and tries to use them together in a rather naïve, but 
                 useful for simple cases, way. It is the most usable,
                 and the slowest (by far!).
                -/
                library_search,


                /- Option 4: If library_search works, just replace it
                with the found expression. Fastest, but introduces a lot
                of "garbage" for those not aware of lean/mathlib lemmas.
                -/
                -- exact @int.lt_add_of_pos_left (@has_one.one.{0} int int.has_one) p_val p_property,
        }
end