Equality is hard.

In Agda, which is a dependently typed programming language, there are different notions of equality: judgemental equality, propositional equality, heterogeneous equality etc. Propositional equality is the most common one used in equality reasoning in Agda. Sometimes Heterogeneous equality is used to reason about the equality between two variables with different types. For instance, if we want to reason about xs equals to ys where xs has the type Vec T (n + m) and ys has the type Vec T (m + n), we need to use the notion of heterogenous equality, since in Agda, they have different types. In addition, if we can prove two variables are heterogeneously equal, we will still not be able to say they are propositionally equal --- these two kinds of equalities are conceptually different.

However, from a user perspective, when we say two things are equal, we have a uniformed conceptual understanding of the notion "equality". These different equalities in Agda sometimes makes the equality reasoning complicated. Moreover, with the feature REWRITE, which can rewrite propositional equalities as definitioanl eqaulities in to the compiler, it is possible to make a heterogenous equality into a propositional eqaulity, creating inconsistencies in the undertanding of eqaulity.

In my old project, I tried to use Agda to prove the correctness of a set of rewrite rules for program optimisation. Equality reasoning is important in this project since we want to prove the programs before and after appliying a rewrite rule produce same result. Both propositional equality and heterogeneous equality are used in this project. In addition, the proofs heavily rely on REWRITE to be simplified, otherwise the encoding can be too complicated to be reason about. There are there major problem with these proofs: 1) equalities are not proven under the same notion of equality, which creates a conceptual mismatch to what we want to say about these rewrite rules; 2) the usage of REWRITE is brutal, it does not pass the confluence check in the lastest version of Agda anymore; 3) there are rules that can be easily proven on paper, but they are unable to be proven in Agda, because of the overcomplicated encoding of lengths of arrays.

In this study, we attempt to reason about equalities of some of these complicated rewrite rules using cubical Agda, which has a uniformed understanding of equality --- it is a equivalence relation under the notion path. Hopefully, it can provide a more stable equality reasoning and a clearer understanding of the correctness of these rewrite rules.