From 9c73520c5fe209cfd3d212b5891dfb8b677fb9d4 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 25 Jul 2023 17:45:27 +0100
Subject: Prove mgu has a unique factor.

---
 src/Data/Term.idr | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

(limited to 'src/Data/Term.idr')

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 385b864..973ff3d 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -93,6 +93,32 @@ subComp :
   f . pure r .=. f . r
 subComp f r i = Refl
 
+export
+compCong2 :
+  {0 f1, f2 : Fin k -> Term sig n} ->
+  {0 g1, g2 : Fin j -> Term sig k} ->
+  f1 .=. f2 ->
+  g1 .=. g2 ->
+  f1 . g1 .=. f2 . g2
+compCong2 prf1 prf2 i = Calc $
+  |~ f1 <$> g1 i
+  ~~ f1 <$> g2 i ...(cong (f1 <$>) $ prf2 i)
+  ~~ f2 <$> g2 i ...(subExtensional prf1 (g2 i))
+
+compCongL :
+  {0 f1, f2 : Fin k -> Term sig n} ->
+  f1 .=. f2 ->
+  (0 g : Fin j -> Term sig k) ->
+  f1 . g .=. f2 . g
+compCongL prf g = compCong2 prf (\_ => Refl)
+
+compCongR :
+  (0 f : Fin k -> Term sig n) ->
+  {0 g1, g2 : Fin j -> Term sig k} ->
+  g1 .=. g2 ->
+  f . g1 .=. f . g2
+compCongR f prf = compCong2 (\_ => Refl) prf
+
 -- Injectivity -----------------------------------------------------------------
 
 export
-- 
cgit v1.2.3