Cubical reflection machinery and Solvers for Paths

marcinjangrzybowski commented 2 months ago

For this to work, it requires following PR's merged to Agda https://github.com/agda/agda/pull/7287, https://github.com/agda/agda/pull/6629 (here is my branch incorporating thosoe changes into latest version of agda) detaills of the issue adrressed by thosoe PRs, are explained in Agda issue 7288

Solvers for Cubical Terms

This is the main goal of the PR, all the other modules are used by those solvers.

features:

applying groupoid laws
functoriallity of cong (congFunct generalised for arbitrary many arguments , both explicit and impllicit)
- all the laws are aplied recursively for subterms as necessary
- in single solution, solver will deal with as many diferent types in subterms as necessary, each one from arbitraty universe level.
- handling paths defined as free variables, abstract defs, HITs, constructors, ua , build with funExt or as subfaces and diagonalls of higer dimensional cubes
- Interval expressions involving (i ∨ ~ i , i ∧ ~ i , etc ... ) are interpolated as necessary into "non degenerated forms" (also in higher dimensions)

there are two solvers implemented, with overlaping functinality, but slightly different limitations:

`Cubical.Tactics.PathSolver.NSolver` (examples) (tests)

This solver, besides fillng squares, is able to prove coherences up to arbitrary dimension. (by coherences I mean that it is able to prove pentagon identity, but not Eckmann-Hilton cube) One of the limitation is that it treats every cubical cell as seperate path, thus failing in goals analogus to cong₂Funct

`Cubical.Tactics.PathSolver.MonoidalSolver` (examples)

This solver applies generalised version of cong₂Funct, but does not provide coherences, it can be used only to fill squares. (Monoidal nomenclature comes from the idea that n-cong is treated as functor from path in n-prod, there is surely better name for this, but this was my first intuition)

Visualisation of example solutions of simple goals:

module _ {ℓ} (A : Type ℓ) {x y z w v : A} {x : A} (p : x ≡ y) (q q' : y ≡ z) (r : z ≡ w) (s : w ≡ v) where

 ex1 : (q ∙ sym q' ∙ q) ∙ (sym q ∙∙ q' ∙∙ r)  ≡
        sym p ∙ p ∙ q ∙ r ∙ s ∙ sym s
 ex1 = solvePaths

 
 ex2 : Square
         (q ∙ sym q' ∙ q)
         (q ∙ r ∙ s ∙ sym s)
         (sym p ∙ p)
         (sym q ∙∙ q' ∙∙ r)
 ex2 = solvePaths

Helper modules

Utilities for handling dimensions and faces `Cubical.Tactics.Reflection.Dimensions.agda`

This module elaborates on handling interval expressions and face expressions (FExpr) in reflected syntax.
Abstract representations for interval expressions (IExpr) and operations like disjunction (∨'), conjunction (∧'), and negation (~') , allows for more agresive normalisation ( i ∨ i => i)
Utilities for converting between IExpr and FExpr, functions for adding interval dimensions to contexts, various operations for specyfic transformations face expressions.
Interpollating between "degenerated?" Interval expression, and equivalent, simple form : (i ∧ ~ i) => i0

Specialised Term Representation `Cubical.Tactics.Reflection.CuTerm.agda`

This module introduces a representation for cubical terms, focusing particularly on compositions and higher-dimensional constructs. The CuTerm' includes specialized constructors like hco' for hcomps and cell' for cells, enabling a more nuanced manipulation of terms. Partial elements , and abstrations over Interval variables are also abstracted away.

Rendering and Conversion: Functions for converting CuTerm' into Agda's reflected R.Term and vice versa, facilitating reflection-based manipulations.
Normalization and Evaluation: Utilities like cuEval and normaliseCells provide mechanisms for evaluating and normalizing terms within the CuTerm' representation, essential for solver operations and macro utility functions.
Code Generation & Pretty Printer: A codeGen utility for translating CuTerm' representations back into Agda code, useful for debugging and macro-generated code validation, thera are also macros for inspecting cubical terms, and generating normalised terms (currently, cubical terms cannot be reliably given using C-u C-u C-c C-m), this provides workaround.

demo-pp

Macros for Handling Cubical Terms `Cubical.Tactics.PathSolver.Macro.agda`. (examples)

some of the utills used by folders are wrapped into seperate macros.

here is demo of macro for convinient composition code generation:

macro-demo

Syntactic sugar via Instances + monad transformers

For long I was avoiding introducing all this transformers machinery to my code, eventualy when I submited, it imensly improved redability/maintability/ease of developement of the code in this PR.

Modules: Cubical.Reflection.Sugar.agda, including submodules Base and Instances.
- Design Assumption: Created with a focus on utility and ease of macro writing. Formal reasoning about their categorical nature was not a goal. Purposufully put this into Reflection module, to make it clear that this is NOT formalisation of the concept.
- Content:
  - Definitions for RawMonad, RawApplicative, RawMonadTransformer, and IdentityFunctor.
  - Instances for common types like Maybe, List, and Sum, operators for combining monads, traversal and maps realying on RawMonad instances
- Independence: The Base submodule does not depend in any way on cubical library.

External integrations

Additionally, machinery form PR allows for integration with external tools that operate on Agda's AST, with the focus of terms including interatively nested hcomps: (integration code is not part of the PR, link are for external files)

Dedekind Solver: Developed by Max Dore (https://github.com/maxdore/dedekind)

Dedekind.agda

CubeViz2 Visualizer: My tool for visualizing cubical terms. https://github.com/marcinjangrzybowski/cubeViz2

CubeViz2Export.agda

Cartesian Experiment

as demonstration of utility of cubical reflection machinery I included macro transforming terms to a equivalent form where all interval expressions are either i0, i1, or a single interval variable (This transformation excludes the implicit φ argument of hcomp, which is effectively a face expression), crudely mimicking transpillation to Cartesian cubical theory (I think?)

marcinjangrzybowski commented 2 months ago

@felixwellen this is PR we discussed earlier I prepared code for initiall round of review by providing comments, and refactoring modules into sane strucutre, before doing full code cleanup (nice names for all lemmas, nice foormatting) I would like to get some initial aproval of general idea.

felixwellen commented 2 months ago

This is awesome :-) Pending a suitable release of agda and reviewing/polishing of your changes, this should be merged. We should also look on the type checking time - if there is a big increase, I think we should come up with a workaround.

marcinjangrzybowski commented 2 months ago

I am thinking on providing Lightweigh and Havy (basic/extended?) version of tests/examples, and exclude them from default CI run (either by using existing check-except option in Everythings.hs or adding other mechanism - will share proof of concept of that)

felixwellen commented 2 months ago

I think one important point is, that we won't slow down the agda ci (so whatever they use to check if cubical still checks with agda should not get worse).

agda / cubical