module Quasiquote004

import Language.Reflection

%default total

normPlus : List (TTName, Binder TT) -> TT -> Tactic
normPlus ctxt `((=) {Nat} {Nat} ~x ~y) = normPlus ctxt x `Seq` normPlus ctxt y
normPlus ctxt `(S ~n) = normPlus ctxt n
normPlus ctxt `(plus ~n (S ~m)) = Seq (Rewrite `(plusSuccRightSucc ~n ~m))
                                      (normPlus ctxt m)
normPlus _ _ = Skip


zero : List (TTName, Binder TT) -> TT -> Tactic
zero ctxt `(Nat) = Exact `(Z)
zero _ _ = Fail [TextPart "Not a Nat goal"]

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy Z
  Fizz : Fizzy n -> Fizzy (3 + n)

-- Fizzy is a correct specification of divisibility by 3 - that is, if n is
-- fizzy then there exists some k such that n = 3*k.
fizzyCorrect : (n : Nat) -> Fizzy n -> (k : Nat ** n = 3 * k)
fizzyCorrect Z ZeroFizzy = (Z ** Refl)
fizzyCorrect (S (S (S k))) (Fizz x) =
  let (k' ** ih) = fizzyCorrect k x
  in (S k' ** ?fizzyIsAOK)

someNat : Nat
someNat = ?getMeNat

notNat : String
notNat = ?getMeNat'

---------- Proofs ----------
Quasiquote004.getMeNat = proof
  applyTactic zero

Quasiquote004.fizzyIsAOK = proof
  compute
  intros
  applyTactic normPlus
  applyTactic normPlus
  rewrite ih
  trivial

Quasiquote004.getMeNat' = proof
  applyTactic zero