diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-25 17:45:27 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-25 17:45:27 +0100 |
| commit | 9c73520c5fe209cfd3d212b5891dfb8b677fb9d4 (patch) | |
| tree | 12310896d1af5710ad2d54b1a305b7571485d425 /src/Data/Term.idr | |
| parent | c305e99c3f0866d2aa4fb0431b06fc398663bd94 (diff) | |
Prove mgu has a unique factor.
Diffstat (limited to 'src/Data/Term.idr')
| -rw-r--r-- | src/Data/Term.idr | 26 |
1 files changed, 26 insertions, 0 deletions
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 |