Frex

Frex is an extensible library of algebraic solver built around the
concept of a FRee EXtension from universal algebra.

This module imports the core defintions and concepts.

Reexports

import public Data.Setoid
import public Data.Finite
import public Frex.Signature
import public Frex.Algebra
import public Frex.Presentation
import public Frex.Axiom
import public Frex.Model
import public Frex.Powers
import public Frex.Free
import public Frex.Coproduct
import public Frex.Frex
import public Frex.Frex.Construction
import public Frex.Free.Construction.ByFrex
import public Frex.Lemma
import public Data.Fun.Nary

Definitions

extEnv : (ext : Extension a x) -> Either (cast a) x ~> cast (ext .Model): Totality: total
Visibility: public export
extensionLemma : (h : ext1 ~> ext2) -> (Either (cast a) x ~~> ext2 .Model) .rel ((h .H) .H . extEnv ext1) (extEnv ext2): Totality: total
Visibility: public export
frexEnv : (frex : Frex a x) -> Either (cast a) x ~> cast ((frex .Data) .Model): Totality: total
Visibility: public export
frexify : ext1 ~> ext2 -> (eq : (Term (pres .signature) (Either (U a) (U x)), Term (pres .signature) (Either (U a) (U x)))) -> (ext1 .Model) .rel ((ext1 .Model) .Sem (fst eq) ((extEnv ext1) .H)) ((ext1 .Model) .Sem (snd eq) ((extEnv ext1) .H)) -> (ext2 .Model) .rel ((ext2 .Model) .Sem (fst eq) ((extEnv ext2) .H)) ((ext2 .Model) .Sem (snd eq) ((extEnv ext2) .H)): Totality: total
Visibility: public export
solveVect : (frex : Frex a (irrelevantCast (Fin n))) -> (env : Vect n (U a)) -> (eq : (Term (pres .signature) (Either (U a) (Fin n)), Term (pres .signature) (Either (U a) (Fin n)))) -> ((frex .Data) .Model) .rel (frex .Sem (fst eq) ((frexEnv frex) .H)) (frex .Sem (snd eq) ((frexEnv frex) .H)) => a .rel (a .Sem (fst eq) (either (Delay id) (Delay (flip index env)))) (a .Sem (snd eq) (either (Delay id) (Delay (flip index env)))): Totality: total
Visibility: public export
solve : (n : Nat) -> (frex : Frex a (cast (Fin n))) -> PI n Hidden (U a) (\env => (eq : (Term (pres .signature) (Either (U a) (Fin n)), Term (pres .signature) (Either (U a) (Fin n)))) -> ((frex .Data) .Model) .rel (frex .Sem (fst eq) ((frexEnv frex) .H)) (frex .Sem (snd eq) ((frexEnv frex) .H)) => a .rel (a .Sem (fst eq) (either (Delay id) (Delay (flip index env)))) (a .Sem (snd eq) (either (Delay id) (Delay (flip index env))))): Totality: total
Visibility: public export
proveAux : (frex : Frex a (cast (Fin n))) -> (eq : (Term (pres .signature) (Either (U a) (Fin n)), Term (pres .signature) (Either (U a) (Fin n)))) -> {auto prf : ((frex .Data) .Model) .rel (frex .Sem (fst eq) ((frexEnv frex) .H)) (frex .Sem (snd eq) ((frexEnv frex) .H))} -> ((frex' .Data) .Model) .rel (((frex' .Data) .Model) .Sem (fst eq) (either (Delay ((((frex' .Data) .Embed) .H) .H)) (Delay (((frex' .Data) .Var) .H)))) (((frex' .Data) .Model) .Sem (snd eq) (either (Delay ((((frex' .Data) .Embed) .H) .H)) (Delay (((frex' .Data) .Var) .H)))): Totality: total
Visibility: public export
prove : (n : Nat) -> (frex : Frex a (cast (Fin n))) -> (eq : (Term (pres .signature) (Either (U a) (Fin n)), Term (pres .signature) (Either (U a) (Fin n)))) -> {auto prf : ((frex .Data) .Model) .rel (frex .Sem (fst eq) ((frexEnv frex) .H)) (frex .Sem (snd eq) ((frexEnv frex) .H))} -> ((frex' .Data) .Model) .rel (((frex' .Data) .Model) .Sem (fst eq) (either (Delay ((((frex' .Data) .Embed) .H) .H)) (Delay (((frex' .Data) .Var) .H)))) (((frex' .Data) .Model) .Sem (snd eq) (either (Delay ((((frex' .Data) .Embed) .H) .H)) (Delay (((frex' .Data) .Var) .H)))): Totality: total
Visibility: public export
.simplify : Frex a x -> x ~> cast a -> Term (pres .signature) (Either (U a) (U x)) -> U a: Totality: total
Visibility: public export
simplifyGeneral : (frex : Frex a x) -> (env : x ~> cast a) -> (t : Term (pres .signature) (Either (U a) (U x))) -> a .rel (a .Sem t ((extEnv (MkExtension a (id a) env)) .H)) (frex .simplify env t): Totality: total
Visibility: public export
simplifyVect : (frex : Frex a (irrelevantCast (Fin n))) -> (env : Vect n (U a)) -> (t : Term (pres .signature) (Either (U a) (Fin n))) -> a .rel (a .Sem t ((extEnv (MkExtension a (id a) (mate (flip index env)))) .H)) (frex .simplify (mate (flip index env)) t): Totality: total
Visibility: public export
simplify : (n : Nat) -> (frex : Frex a (cast (Fin n))) -> PI n Hidden (U a) (\env => (t : Term (pres .signature) (Either (U a) (Fin n))) -> a .rel (a .Sem t ((extEnv (MkExtension a (id a) (mate (flip index env)))) .H)) (frex .simplify (mate (flip index env)) t)): Totality: total
Visibility: public export