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