Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Simple proof automation with reflected elaboration
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})
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment