------------------------------------------------------------------------
-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

open import Data.Fin
open import Function
open import Data.Nat
open import Data.Vec as Vec
open import Level
open import Relation.Binary

-- Think of the parameters as follows:
--
-- * Expr:    A representation of code.
-- * var:     The Expr type should support a notion of variables.
-- * ⟦_⟧:     Computes the semantics of an expression. Takes an
--            environment mapping variables to something.
-- * ⟦_⇓⟧:    Computes the semantics of the normal form of the
--            expression.
-- * correct: Normalisation preserves the semantics.
--
-- Given these parameters two "tactics" are returned, prove and solve.
--
-- For an example of the use of this module, see Algebra.RingSolver.

module Relation.Binary.Reflection
         {e a s}
         {Expr :   Set e} {A : Set a}
         (Sem : Setoid a s)
         (var :  {n}  Fin n  Expr n)
         (⟦_⟧ ⟦_⇓⟧ :  {n}  Expr n  Vec A n  Setoid.Carrier Sem)
         (correct :  {n} (e : Expr n) ρ 
                     e ⇓⟧ ρ  Setoid._≈_ Sem   e  ρ)
         where

open import Data.Vec.N-ary
open import Data.Product
import Relation.Binary.EqReasoning as Eq

open Setoid Sem
open Eq Sem

-- If two normalised expressions are semantically equal, then their
-- non-normalised forms are also equal.

prove :  {n} (ρ : Vec A n) e₁ e₂ 
         e₁ ⇓⟧ ρ   e₂ ⇓⟧ ρ 
         e₁   ρ   e₂   ρ
prove ρ e₁ e₂ hyp = begin
   e₁   ρ ≈⟨ sym (correct e₁ ρ) 
   e₁ ⇓⟧ ρ ≈⟨ hyp 
   e₂ ⇓⟧ ρ ≈⟨ correct e₂ ρ 
   e₂   ρ 

-- Applies the function to all possible "variables".

close :  {A} n  N-ary n (Expr n) A  A
close n f = f $ⁿ Vec.map var (allFin n)

-- A variant of prove which should in many cases be easier to use,
-- because variables and environments are handled in a less explicit
-- way.
--
-- If the type signature of solve is a bit daunting, then it may be
-- helpful to instantiate n with a small natural number and normalise
-- the remainder of the type.

solve :  n (f : N-ary n (Expr n) (Expr n × Expr n)) 
  Eqʰ n _≈_ (curryⁿ  proj₁ (close n f) ⇓⟧) (curryⁿ  proj₂ (close n f) ⇓⟧) 
  Eq  n _≈_ (curryⁿ  proj₁ (close n f)  ) (curryⁿ  proj₂ (close n f)  )
solve n f hyp =
  curryⁿ-cong  proj₁ (close n f)   proj₂ (close n f) 
     ρ  prove ρ (proj₁ (close n f)) (proj₂ (close n f))
             (curryⁿ-cong⁻¹  proj₁ (close n f) ⇓⟧  proj₂ (close n f) ⇓⟧
                            (Eqʰ-to-Eq n hyp) ρ))

-- A variant of _,_ which is intended to make uses of solve look a
-- bit nicer.

infix 4 _⊜_

_⊜_ :  {n}  Expr n  Expr n  Expr n × Expr n
_⊜_ = _,_