------------------------------------------------------------------------
-- The Agda standard library
--
-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Data.Fin.Base using (Fin)
open import Data.Nat.Base using ()
open import Data.Vec.Base as Vec using (Vec; allFin)
open import Function.Base using (id; _⟨_⟩_)
open import Function.Bundles using (module Equivalence)
open import Level using (Level)
open import Relation.Binary
import Relation.Binary.PropositionalEquality.Core as P

-- 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.Base using (_×_; _,_; proj₁; proj₂)
import Relation.Binary.Reasoning.Setoid 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 : Set e} 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 solve which does not require that the normal form
-- equality is proved for an arbitrary environment.

solve₁ :  n (f : N-ary n (Expr n) (Expr n × Expr n)) 
         ∀ⁿ n (curryⁿ λ ρ 
                  proj₁ (close n f) ⇓⟧ ρ   proj₂ (close n f) ⇓⟧ ρ 
                  proj₁ (close n f)   ρ   proj₂ (close n f)   ρ)
solve₁ n f =
  Equivalence.from (uncurry-∀ⁿ n) λ ρ 
    P.subst id (P.sym (left-inverse  _  _  _  _  _) ρ))
      (prove ρ (proj₁ (close n f)) (proj₂ (close n f)))

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

infix 4 _⊜_

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