-- Tactics

open import Nat
open import Logic
open import Bool
import Equality

data Even : ℕ → Set where
  even-base : Even zero
  even-step : ∀ {n : ℕ} → Even n → Even (succ (succ n))

lemma-4-is-even : Even 4
lemma-4-is-even = even-step (even-step even-base)

lemma-6-is-even : Even 6
lemma-6-is-even = even-step (even-step (even-step even-base))

lemma-5-is-not-even : ¬ (Even 5)
lemma-5-is-not-even (even-step (even-step ()))

module Attempt1 where

  open Equality

  -- A function to compute whether some number is even.
  is-even : ℕ -> Bool
  is-even zero = true
  is-even (succ zero) = false
  is-even (succ (succ n)) = is-even n
  
  -- This theorem states that the is-even function is "one-sided correct".
  -- Namely, when is-even n == true, then n is even.
  -- (The theorem does not say that when is-even n == false, then n is not even).
  theorem-is-even : ∀ (n : ℕ) -> is-even n == true -> Even n
  theorem-is-even zero hyp = even-base
  theorem-is-even (succ zero) ()
  theorem-is-even (succ (succ n)) hyp = even-step (theorem-is-even n hyp)
  
  tactic-is-even : ∀ {n : ℕ} -> is-even n == true -> Even n
  tactic-is-even {n} hyp = theorem-is-even n hyp
  
  -- We now have a simple tactic to prove that specific even numbers are
  -- even.
  lemma-1002-is-even : Even 1002
  lemma-1002-is-even = tactic-is-even auto
  
module Attempt2 where

  -- Let's try to do the same thing, but without using equality.

  -- If A is a set, then Maybe A is a set with one additional element,
  -- i.e., Maybe A ≅ A + 1. Note that a function A -> Maybe B
  -- is essentially the same thing as a partial function.
  -- We have Maybe A := {Nothing} ∪ {Just x | x ∈ A}
  data Maybe (A : Set) : Set where
    Nothing : Maybe A
    Just : A -> Maybe A

  -- A semi-decision procedure for evenness.
  is-even? : (n : ℕ) -> Maybe (Even n)
  is-even? zero = Just even-base
  is-even? (succ zero) = Nothing
  is-even? (succ (succ n)) with is-even? n
  is-even? (succ (succ n)) | Nothing = Nothing
  is-even? (succ (succ n)) | Just x = Just (even-step x)

  -- The following function uses a type-level computation.
  -- This means that what it computes is a type!
  isJust : ∀ {A} -> Maybe A -> Set
  isJust Nothing = False
  isJust (Just x) = True

  fromJust : ∀ {A} -> (z : Maybe A) -> isJust z -> A
  fromJust Nothing ()
  fromJust (Just x) hyp = x

  tactic-even : {n : ℕ} -> isJust (is-even? n) -> Even n
  tactic-even {n} x = fromJust (is-even? n) x

  lemma-1002-is-even : Even 1002
  lemma-1002-is-even = tactic-even <>

  lemma-1000-is-even : Even 1000
  lemma-1000-is-even = tactic-even <>

  -- This kind of tactic only works for "ground" terms, i.e., terms
  -- that don't contain any variables.
  lemma-square-even : ∀ n -> Even n -> Even (n * n)
  lemma-square-even n hyp = tactic-even {!!}