Simple proof automation with reflected elaboration

NatInd.idr

module NatInd

import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

trivial : Elab ()
trivial = do compute
             g <- snd <$> getGoal
             case !(forgetTypes g) of
               `((=) {A=~A} {B=~_} ~x ~_) =>
                  apply [| (Var (UN "Refl")) A x |]
               `(():Type) =>
                 apply `(():())
               _ => fail [TermPart g, TextPart "is not trivial"]

test1 : 2 + 4 = 6
test1 = %runElab (trivial *> solve)

test2 : if True then () else Nat
test2  = %runElab (trivial *> solve)


natInd : (P : Nat -> Type) -> P Z -> ((n : Nat) -> P n -> P (S n)) -> (n : Nat) -> P n
natInd P z s Z     = z
natInd P z s (S k) = s k (natInd P z s k)

||| Perform induction over the natural numbers.  Returns a pair
||| consisting of the names of the holes left for the base and step
||| cases.
induction : TTName -> Elab (TTName, TTName)
induction n =
  do g <- snd <$> getGoal
     motive <- RBind n (Lam `(Nat)) <$> forgetTypes g
     baseH <- gensym "base"
     claim baseH [| motive `(Z) |]
     unfocus baseH
     stepH <- gensym "step"
     claim stepH `((k : Nat) ->
                   ~(RApp motive (Var (UN "k"))) ->
                   ~(RApp motive (RApp `(S) (Var (UN "k")))))
     unfocus stepH
     apply `(natInd ~motive ~(Var baseH) ~(Var stepH) ~(Var n))
     solve
     return (baseH, stepH)

total
theorem : (n : Nat) -> plus n 1 = S n
theorem n =
  %runElab (do names <- induction `{n}
               focus (fst names);
                 do trivial ; solve
               focus (snd names);
                 do compute
                    attack
                    intro (Just (UN "x"))
                    intro (Just (UN "ih"))
                    rewriteWith (Var (UN "ih"))
                    trivial
                    solve
               solve)

||| Do Nat induction in the easy way - by encapsulating the common
||| pattern of a trivial base case and an induction step that just
||| rewrites with the hypothesis.
easyInduction : TTName -> Elab ()
easyInduction n = (do names <- induction n
                      focus (fst names);
                        do trivial ; solve
                      focus (snd names);
                        do compute
                           attack
                           m <- gensym "m"
                           ih <- gensym "ih"
                           intro (Just m)
                           intro (Just ih)
                           rewriteWith (Var ih)
                           trivial
                           solve
                      solve)
                  <|> (do g <- snd <$> getGoal
                          fail [ TextPart "Can't solve goal "
                               , TermPart g
                               , TextPart "with easy induction."])




theorem' : (n : Nat) -> n + 1 = S n
theorem' n = %runElab (easyInduction `{n})


plusSuccR : (n, m : Nat) -> n + (S m) = S (n + m)
plusSuccR n m = %runElab (easyInduction `{n})

plusZeroRightId : (n : Nat) -> n + 0 = n
plusZeroRightId n = %runElab (easyInduction `{n})

assoc : (n,m,o : Nat) -> n + (m + o) = (n + m) + o
assoc n m o = %runElab (easyInduction `{n})