------------------------------------------------------------------------
-- The Agda standard library
--
-- A solver for equations over monoids
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Monoid)
import Algebra.Solver.Monoid.Expression as Expression
module Algebra.Solver.Monoid.Solver {a c ℓ} (M : Monoid c ℓ)
(open Monoid M using (rawMonoid; setoid; _≈_))
(open Expression rawMonoid using (Expr; Env; var; ⟦_⟧; NormalAPI))
(N : NormalAPI a) where
open import Data.Maybe.Base as Maybe
using (Maybe; From-just; from-just)
open import Data.Nat.Base using (ℕ)
open import Function.Base using (_∘_; _$_)
open import Relation.Binary.Consequences using (dec⇒weaklyDec)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
import Relation.Binary.Reflection as Reflection
open NormalAPI N
private
variable
n : ℕ
module
R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct
------------------------------------------------------------------------
-- Proof procedures
-- Re-export the existing solver machinery from `Reflection`
open R public
using (solve; _⊜_)
-- We can also give a sound, but not necessarily complete, procedure
-- for determining if two expressions have the same semantics.
prove′ : ∀ e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)
where
open import Relation.Binary.Reasoning.Setoid setoid
lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
lemma eq ρ = R.prove ρ e₁ e₂ $ begin
⟦ normalise e₁ ⟧⇓ ρ ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
⟦ normalise e₂ ⟧⇓ ρ ∎
-- This procedure can then be combined with from-just.
prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
prove _ e₁ e₂ = from-just $ prove′ e₁ e₂
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4