1
------------------------------------------------------------------------
2
-- Helpers intended to ease the development of "tactics" which use
4
------------------------------------------------------------------------
6
{-# OPTIONS --universe-polymorphism #-}
9
open import Data.Function
11
open import Data.Vec as Vec
13
open import Relation.Binary
15
-- Think of the parameters as follows:
17
-- * Expr: A representation of code.
18
-- * var: The Expr type should support a notion of variables.
19
-- * ⟦_⟧: Computes the semantics of an expression. Takes an
20
-- environment mapping variables to something.
21
-- * ⟦_⇓⟧: Computes the semantics of the normal form of the
23
-- * correct: Normalisation preserves the semantics.
25
-- Given these parameters two "tactics" are returned, prove and solve.
27
-- For an example of the use of this module, see Algebra.RingSolver.
29
module Relation.Binary.Reflection
31
{Expr : ℕ → Set e} {A : Set a}
33
(var : ∀ {n} → Fin n → Expr n)
34
(⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Setoid.Carrier Sem)
35
(correct : ∀ {n} (e : Expr n) ρ →
36
⟦ e ⇓⟧ ρ ⟨ Setoid._≈_ Sem ⟩ ⟦ e ⟧ ρ)
39
open import Data.Vec.N-ary
40
open import Data.Product
41
import Relation.Binary.EqReasoning as Eq
46
-- If two normalised expressions are semantically equal, then their
47
-- non-normalised forms are also equal.
49
prove : ∀ {n} (ρ : Vec A n) e₁ e₂ →
50
⟦ e₁ ⇓⟧ ρ ≈ ⟦ e₂ ⇓⟧ ρ →
52
prove ρ e₁ e₂ hyp = begin
53
⟦ e₁ ⟧ ρ ≈⟨ sym (correct e₁ ρ) ⟩
55
⟦ e₂ ⇓⟧ ρ ≈⟨ correct e₂ ρ ⟩
58
-- Applies the function to all possible "variables".
60
close : ∀ {A} n → N-ary n (Expr n) A → A
61
close n f = f $ⁿ Vec.map var (allFin n)
63
-- A variant of prove which should in many cases be easier to use,
64
-- because variables and environments are handled in a less explicit
67
-- If the type signature of solve is a bit daunting, then it may be
68
-- helpful to instantiate n with a small natural number and normalise
69
-- the remainder of the type.
71
solve : ∀ n (f : N-ary n (Expr n) (Expr n × Expr n)) →
72
Eqʰ n _≈_ (curryⁿ ⟦ proj₁ (close n f) ⇓⟧) (curryⁿ ⟦ proj₂ (close n f) ⇓⟧) →
73
Eq n _≈_ (curryⁿ ⟦ proj₁ (close n f) ⟧) (curryⁿ ⟦ proj₂ (close n f) ⟧)
75
curryⁿ-cong ⟦ proj₁ (close n f) ⟧ ⟦ proj₂ (close n f) ⟧
76
(λ ρ → prove ρ (proj₁ (close n f)) (proj₂ (close n f))
77
(curryⁿ-cong⁻¹ ⟦ proj₁ (close n f) ⇓⟧ ⟦ proj₂ (close n f) ⇓⟧
80
-- A variant of _,_ which is intended to make uses of solve look a
85
_⊜_ : ∀ {n} → Expr n → Expr n → Expr n × Expr n
added
removed
src/Relation/Binary/Reflection.agda
