Simplifying "plus" expressions with rewrite-rule combinators and quasiquotes in Idris

PlusRewrite.idr

module PlusRewrite

import Language.Reflection
import Language.Reflection.Utils

rewrite_plusSuccRightSucc : TT -> Maybe Tactic
rewrite_plusSuccRightSucc `(plus ~n (S ~m)) = Just $ Rewrite `(plusSuccRightSucc ~n ~m)
rewrite_plusSuccRightSucc `(S ~n) = rewrite_plusSuccRightSucc n
rewrite_plusSuccRightSucc `(plus ~n ~m) = rewrite_plusSuccRightSucc n <|> rewrite_plusSuccRightSucc m
rewrite_plusSuccRightSucc _ = Nothing

rewrite_plusZeroRightNeutral : TT -> Maybe Tactic
rewrite_plusZeroRightNeutral `(plus ~n Z) = Just $ Rewrite `(sym (plusZeroRightNeutral ~n))
rewrite_plusZeroRightNeutral `(S ~n) = rewrite_plusZeroRightNeutral n
rewrite_plusZeroRightNeutral `(plus ~n ~m) = rewrite_plusZeroRightNeutral n <|> rewrite_plusZeroRightNeutral m
rewrite_plusZeroRightNeutral _ = Nothing

infixr 4 <||>

(<||>) : (TT -> Maybe Tactic) -> (TT -> Maybe Tactic) -> TT -> Maybe Tactic
r1 <||> r2 = \goal => r1 goal <|> r2 goal

rewrite_eq : (TT -> Maybe Tactic) -> TT -> Maybe Tactic
rewrite_eq rew `((=) {A=~_} {B=~_} ~x ~y) = rew x <|> rew y
rewrite_eq rew tm = rew tm

simplifyPlus : Nat -> List (TTName, Binder TT) -> TT -> Tactic
simplifyPlus (S k) ctxt goal =
  case rewrite_eq (rewrite_plusSuccRightSucc <||> rewrite_plusZeroRightNeutral) goal of
    Just tac => Seq tac (ApplyTactic `(simplifyPlus ~(quote k)))
    Nothing => Skip
simplifyPlus Z _ _ = Skip


test : (n : Nat) -> plus (plus n n) 3 = (plus (S n) (S (S (plus n Z))))
test n = ?test_rhs

---------- Proofs ----------

PlusRewrite.test_rhs = proof
  intros
  applyTactic simplifyPlus 10
  trivial

PlusRewrite2.idr

module PlusRewrite

import Language.Reflection
import Language.Reflection.Utils

rewrite_app : (TT -> Maybe Tactic) -> TT -> Maybe Tactic
rewrite_app rew tm with (rew tm)
  | Just tac = Just tac
  | Nothing = case tm of
                (App x y) => rewrite_app rew x <|> rewrite_app rew y
                _ => Nothing

rewrite_nat : (TT -> Maybe Tactic) -> TT -> Maybe Tactic
rewrite_nat rew tm with (rew tm)
  | Just tac = Just tac
  | Nothing  = case tm of
                 `(S ~n) => rewrite_nat rew n
                 `(plus ~n ~m) => rewrite_nat rew n <|> rewrite_nat rew m
                 _ => Nothing


rewrite_plusSuccRightSucc : TT -> Maybe Tactic
rewrite_plusSuccRightSucc `(plus ~n (S ~m)) = Just $ Rewrite `(plusSuccRightSucc ~n ~m)
rewrite_plusSuccRightSucc _                 = Nothing

rewrite_plusZeroRightNeutral : TT -> Maybe Tactic
rewrite_plusZeroRightNeutral `(plus ~n Z)  = Just $ Rewrite `(sym (plusZeroRightNeutral ~n))
rewrite_plusZeroRightNeutral _             = Nothing

infixr 4 <||>

(<||>) : (TT -> Maybe Tactic) -> (TT -> Maybe Tactic) -> TT -> Maybe Tactic
r1 <||> r2 = \goal => r1 goal <|> r2 goal

rewrite_eq : (TT -> Maybe Tactic) -> TT -> Maybe Tactic
rewrite_eq rew `((=) {A=~_} {B=~_} ~x ~y) = rew x <|> rew y
rewrite_eq rew tm = rew tm

simplifyPlus : Nat -> List (TTName, Binder TT) -> TT -> Tactic
simplifyPlus (S k) ctxt goal =
   maybe Skip
         (flip Seq (ApplyTactic `(simplifyPlus ~(quote k))))
         (rewrite_app (rewrite_plusSuccRightSucc <||> rewrite_plusZeroRightNeutral)
                      goal)
simplifyPlus Z _ _ = Skip


test : (n : Nat) -> plus (plus n n) 3 = (plus (S n) (S (S (plus n Z))))
test n = ?test_rhs

---------- Proofs ----------

PlusRewrite.test_rhs = proof
  intros
  applyTactic simplifyPlus 10
  trivial