[Agda] Small-scale reflection in Agda

[Jean-Philippe Bernardy]

-- In this file I show on examples how to implement Coq-style
-- small-scale reflection in Agda.

-- The Coq implementation of theses examples was explained to me by
-- Anders Mörtberg, and the suggestion to work with the Dec type is
-- due to Stevan Andjelkovic.


-- Case study. I prove two simple theorems using three different
-- methods:

--  1. "Direct" encoding of propositions in Set.

--  2. An encoding of small-scale reflection closely related to the
--  one in Coq.

--  3. Small-scale reflection using the 'Dec' type, as suggested by
--  Stevan.

-- The two theorems that we prove are:

-- 1. ∀ a b -> (a ≤ b) -> suc a ≤ suc b.
-- This problem shows the power of reflection: using it, the
-- conclusion of the theorem computes to ⊤ and it therefore trivial to
-- prove.

-- 2. (a b c : ℕ) ->  dividesP a b -> dividesP a c -> dividesP a (b + c)
-- In the proof of the above, reflection is an hindrance. The problem
-- is used to measure the overhead of reflection.



-- Conclusions:

-- 1. The benefits of small-scale reflection can be reaped in Agda as
-- well, but the syntactic overhead might be justified only for
-- specific problems.

-- 2. As Stevan suspected, it seems nicer to depart slightly
-- from the Coq implementation and use the notion of decidable
-- predicate as defined in the standard library.

-------------------------------------------------------

module SSReflect where


open import Data.Empty
open import Data.Unit hiding (_≟_; _≤?_; _≤_)
open import Data.Product
open import Data.Bool hiding (_≟_)
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product
open import Relation.Nullary.Sum
import Data.Fin as F
import Data.List as L


-- The divisibility predicate.
dividesP : ℕ -> ℕ -> Set
dividesP m n = Σ _ (\(x : ℕ) -> x * m ≡ n)

-- Helper theorem
postulate mulr-alddl : ∀ x y a -> (x + y) * a ≡ x * a + y * a


module 1:Direct where

  divides-add : (a b c : ℕ) ->  dividesP a b  -> dividesP a c  ->
dividesP a (b + c)
  divides-add a b c (x , bax) (y , bay) = (x + y) , trans (mulr-alddl
x y a) (cong₂ _+_ bax bay)
  -- The proof offers no surprise.

  suc-lt : ∀ a b -> (a ≤ b) -> suc a ≤ suc b
  suc-lt a b p = s≤s p -- Note that, despite the proof being easy, we
                       -- still need to construct something.


module 2:UsingReflect where

  -- The reflection predicate
  data Ref (P : Set) : Bool -> Set where
    true : P -> Ref P true
    false : (P -> ⊥) -> Ref P false

  -- Helper to convert a witness of a proposition "P" to the
  -- corresponding boolean expression.
  unRef : ∀ {P b} -> Ref P b -> P -> T b
  unRef (true y) p = tt
  unRef (false y) p = y p


  postulate
    -- for divisibility we need the divisibility predicate as a boolean
    divides : ℕ -> ℕ -> Bool
    -- ... and show that it properly reflects dividesP.
    reflect : ∀ m n -> Ref (dividesP m n) (divides m n)

  -- From there we can go in the direction 'Predicate ~> Boolean is
true' easily:
  dividesR : ∀ {m n} -> dividesP m n -> T (divides m n)
  dividesR {m} {n} = unRef (reflect m n)

  -- Note that "T" corresponds to the coercion in Coq.

  divides-add : (a b c : ℕ) ->  T (divides a b)  -> T (divides a c)
-> T (divides a (b + c))
  divides-add a b c p q with divides a b | reflect a b | divides a c |
reflect a c
     -- we need to do a double "with" to satisfy the unifier.
  divides-add a b c p q | .true | true (x , bax) | .true | true (y , bay) =
     dividesR (((x + y) , trans (mulr-alddl x y a) (cong₂ _+_ bax bay)))
  divides-add a b c () q | .false | false y | .true | true y'
     -- Overhead: we need to write something for the "false" cases.
  divides-add a b c p () | t | w | .false | false y

  _<=_ : ℕ -> ℕ -> Bool
  zero <= n = true
  suc n <= zero = false
  suc n <= suc n' = n <= n'

  suc-lt : ∀ a b -> T (a <= b) -> T (suc a <= suc b)
  suc-lt a b p with a <= b
  suc-lt a b p | true = tt -- Note that the result is computed, we
                           -- need not do anything here. (As I
                           -- understand it, this is the big advantage
                           -- of small-scale reflection)
  suc-lt a b () | false


module 3:UsingDec where
  -- Here we can re-use Dec from the standard library, and all the
  -- goodies coming with it.

  -- We need only one function that does the job of 'divides' and
  -- 'reflect' at once:
  postulate dividesD : (m n : ℕ) -> Dec (dividesP m n)

  -- Note that "True" corresponds to the coercion in Coq.
  divides-add : (a b c : ℕ) ->  True (dividesD a b)  -> True (dividesD
a c)  -> True (dividesD a (b + c))
  divides-add a b c p  q with dividesD a b | dividesD a c
   -- a single 'with' is sufficient here.
  divides-add a b c p q | yes (x , bax) | yes (y , bay)
     = fromWitness ((x + y) , trans (mulr-alddl x y a) (cong₂ _+_ bax bay))
  divides-add a b c p () | s | no ¬p
  divides-add a b c () q | no ¬p | s

  suc-lt : ∀ a b -> True (a ≤? b) -> True (suc a ≤? suc b)
  suc-lt a b q with a ≤? b
  suc-lt a b _  | yes _ = tt -- computed!
  suc-lt a b () | no _


  -- Note: we can sometimes delegate the false-cases to the following
  -- helper function:
  dec :  ∀ {A : Set} -> ∀ {P : Set} -> {d : Dec P} -> True d -> (P -> A) -> A
  dec {A} {P} {yes p} _ k = k p
  dec {A} {P} {no _} () k

  divides-add' : (a b c : ℕ) ->  True (dividesD a b)  -> True
(dividesD a c)  -> True (dividesD a (b + c))
  divides-add' a b c p q = dec p (λ xx → dec q (λ yy → fromWitness
(1:Direct.divides-add a b c xx yy)))