I’ve been working on a relatively large Agda project for a few months now, and I’d like to think that I’ve become quite proficient. Recently, I came up with a little trick to help simplify some of my proofs, and it seems like this trick might have broader applications.

In my head, I call this trick ‘Deeply Embedded Expressions’. Before I introduce it, let me explain the part of my work that motivated developing the trick.

Proofs about Map Operations

A part of my Agda project is the formalization of simple key-value maps. I model key-value maps as lists of key-value pairs. On top of this, I implement two operations: join and meet, which in my code are denoted using and . When “joining” two maps, you create a new map that has the keys from both input ones. If a key is only present in one of the input maps, then the new “joined” map has the same value for that key as the original. On the other hand, if the key is present in both maps, then its value in the new map is the result of “joining” the original values. The “meet” operation is similar, except instead of taking keys from either map, the result only has keys that were present in both maps, “meeting” their values. In a way, “join” and “meet” are similar to set union and intersection — but they also operate on the values in the map.

Given these operations, I need to prove certain properties of these operation. The most inconvenient to prove is probably associativity:

From Map.agda, line 752
752
⊔-assoc :  (m₁ m₂ m₃ : Map)  ((m₁  m₂)  m₃)  (m₁  (m₂  m₃))

This property is, in turn, proven using two ‘subset’ relations on maps, defined in the usual way.

From Map.agda, line 755
755
        ⊔-assoc₁ : ((m₁  m₂)  m₃)  (m₁  (m₂  m₃))
From Map.agda, line 774
774
        ⊔-assoc₂ : (m₁  (m₂  m₃))  ((m₁  m₂)  m₃)

The reason this property is so inconvenient to prove is that there are a lot of cases to consider. That’s because your claim, in words, is something like:

Suppose a key-value pair k , v is present in (m₁ ⊔ m₂) ⊔ m₃. Show that k , v is also in m₁ ⊔ (m₂ ⊔ m₃).

The only thing you can really do with k , v is figure out how it got into the three-way union map: did it come from m₁, m₂, or m₃, or perhaps several of them? The essence of the proof boils down to repeated uses of the fact that for a key to be in the union, it must be in at least one of the two maps. You end up with witnesses, repeated application of the same lemmas, lots of let-expressions or where clauses. It’s relatively tedious and, what’s more frustrating, driven entirely by the structure of the map operations. It seems like one shouldn’t have to mimic that structure using boilerplate lemmas. So I started looking at other ways.

Case Analysis using GADTs

A “proof by cases” in a dependently typed language like Agda usually brings to mind pattern matching. So, here’s an idea: what if for each expression involving and , we had some kind of data type, and that data type had exactly as many inhabitants as there are cases to analyze? A data type corresponding to m₁ ⊔ m₂ might have three cases, and the one for (m₁ ⊔ m₂) ⊔ m₃ might have seven. Each case would contain the information necessary to perform the proof.

A data type whose “shape” depends on an expression in the way I described above is said to be indexed by that expression. In Agda, GADTs are used to create indexed types. My initial attempt was something like this:

data Provenance (k : A) : B  Map  Set (a ⊔ℓ b) where
    single :  {v : B} {m : Map}  (k , v)  m  Provenance k v m
    in₁ :  {v : B} {m₁ m₂ : Expr}  Provenance k v e₁  ¬ k ∈k m₂  Provenance k v (e₁  e₂)
    in₂ :  {v : B} {m₁ m₂ : Expr}  ¬ k ∈k m₁  Provenance k v m₂  Provenance k v (e₁  e₂)
    bothᵘ :  {v₁ v₂ : B} {m₁ m₂ : Expr}  Provenance k v₁ m₁  Provenance k v₂ m₂  Provenance k (v₁  v₂) (e₁  e₂)
    bothⁱ :  {v₁ v₂ : B} {m₁ m₂ : Expr}  Provenance k v₁ m₁  Provenance k v₂ m₂  Provenance k (v₁  v₂) (e₁  e₂)

I was planning on a proof of associativity (in one direction) that looked something like the following — pattern matching on cases from the new Provenance type.

⊔-assoc₁ : ((m₁  m₂)  m₃)  (m₁  (m₂  m₃))
⊔-assoc₁ k v k,v∈m₁₂m₃
    with get-Provenance k,v∈m₁₂m₃
...   | in k∉km₁₂ (single v∈m₃) = ...
...   | in (in k∉km₁ (single v∈m₂)) k∉km₃ = ...
...   | bothᵘ (in k∉km₁ (single {v₂} v₂∈m₂)) (single {v₃} v₃∈m₃) = ...
...   | in (in (single v₁∈m₁) k∉km₂) k∉km₃ = ...
...   | bothᵘ (in (single {v₁} v₁∈m₁) k∉km₂) (single {v₃} v₃∈m₃) = ...
...   | in (bothᵘ (single {v₁} v₁∈m₁) (single {v₂} v₂∈m₂)) k∉ke₃ = ...
...   | bothᵘ (bothᵘ (single {v₁} v₁∈m₁) (single {v₂} v₂∈m₂)) (single {v₃} v₃∈m₃) = ...

However, this doesn’t work. Agda has trouble figuring out which cases of the Provenance GADT are allowed, in which aren’t. Is m₁ ⊔ m a single map, fit for the single case, or should it be broken up into more cases like in₁ and in₂? In general, is some expression of type Map the “bottom” of our recursion, or should it be analyzed further?

The above hints at what’s wrong. The mistake here is requiring Agda to infer the shape of our “join” and “meet” expressions from arbitrary terms. The set of expressions that we want to reason about is much more restricted – each expression will always be of three components: “meet”, “join”, and base-case maps being combined using these operations.

Defining an Expression Data Type

If you’re like me, and have spent years of your life around programming language theory and domain specific languages (DSLs), the last sentence of the previous section may be ringing a bell. In fact, it’s eerily similar to how we describe recursive grammars:

An expression of interest is either,

  • A map
  • The “join” of two expressions
  • The “meet” of two expressions

Mathematically, we might write this as follows:

e::=m(maps)ee(join)ee(meet) \begin{array}{rcll} e & ::= & m & \text{(maps)} \\ & | & e \sqcup e & \text{(join)} \\ & | & e \sqcap e & \text{(meet)} \end{array}

And in Agda,

From Map.agda, lines 543 through 546
543
544
545
546
data Expr : Set (a ⊔ℓ b) where
    `_ : Map  Expr
    _∪_ : Expr  Expr  Expr
    _∩_ : Expr  Expr  Expr

In the code, I used the set union and intersection operators to avoid overloading the and more than they already are.

We have just defined a very small expression language. In computer science, a language is called deeply embedded if a data type (or class hierarchy, or other ’explicit’ representation) is defined for its syntax in the host language (Agda, in our case). This is in contrast to a shallow embedding, in which expressions in the (new) language are just expressions in the host language.

In this sense, our Expr is deeply embedded — we defined new container for it, and _∪_ is a distinct entity from _⊔_. Our first attempt was a shallow embedding. That fell through because the Agda language is much broader than our expression language, which makes case analysis very difficult.

An obvious thing to do with an expression is to evaluate it. This will be important for our proofs, because it will establish a connection between expressions (created via Expr) and actual Agda objects that we need to reason about at the end of the day. The notation e\llbracket e \rrbracket is commonly used in PL circles for evaluation (it comes from Denotational Semantics ). Thus, my Agda evaluation function is written as follows:

From Map.agda, lines 586 through 589
586
587
588
589
⟦_⟧ : Expr -> Map
 ` m  = m
 e₁  e₂  =  e₁    e₂ 
 e₁  e₂  =  e₁    e₂ 

On top of this, here is my actual implementation of the Provenance data type. This time, it’s indexed by expressions in Expr, which makes it much easier to pattern match on instances:

From Map.agda, lines 591 through 596
591
592
593
594
595
596
data Provenance (k : A) : B  Expr  Set (a ⊔ℓ b) where
    single :  {v : B} {m : Map}  (k , v)  m  Provenance k v (` m)
    in₁ :  {v : B} {e₁ e₂ : Expr}  Provenance k v e₁  ¬ k ∈k  e₂   Provenance k v (e₁  e₂)
    in₂ :  {v : B} {e₁ e₂ : Expr}  ¬ k ∈k  e₁   Provenance k v e₂  Provenance k v (e₁  e₂)
    bothᵘ :  {v₁ v₂ : B} {e₁ e₂ : Expr}  Provenance k v₁ e₁  Provenance k v₂ e₂  Provenance k (v₁ ⊔₂ v₂) (e₁  e₂)
    bothⁱ :  {v₁ v₂ : B} {e₁ e₂ : Expr}  Provenance k v₁ e₁  Provenance k v₂ e₂  Provenance k (v₁ ⊓₂ v₂) (e₁  e₂)

Note that we have to use the evaluation function to be able to use operators such as . That’s because these are still defined on maps, and not expressions.

With this, I was able to write my proof in the way that I had hoped. It has the exact form of my previous sketch-of-proof.

(click here to see the full example, including each case’s implementation)
From Map.agda, lines 755 through 773
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
        ⊔-assoc₁ : ((m₁  m₂)  m₃)  (m₁  (m₂  m₃))
        ⊔-assoc₁ k v k,v∈m₁₂m₃
            with Expr-Provenance-≡ (((` m₁)  (` m₂))  (` m₃)) k,v∈m₁₂m₃
        ...   | in k∉ke₁₂ (single {v₃} v₃∈e₃) =
                let (k∉ke₁ , k∉ke₂) = I⊔.∉-union-∉-either {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
                in (v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
        ...   | in (in k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ =
                (v₂ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
        ...   | bothᵘ (in k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
                (v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁  (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
        ...   | in (in (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ =
                (v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ v₁∈e₁ (I⊔.union-preserves-∉ k∉ke₂ k∉ke₃)))
        ...   | bothᵘ (in (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) =
                (v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
        ...   | in (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃ =
                (v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
        ...   | bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
                (v₁ ⊔₂ (v₂ ⊔₂ v₃) , (⊔₂-assoc v₁ v₂ v₃ , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))

The General Trick

So far, I’ve presented a problem I faced in my Agda proof and a solution for that problem. However, it may not be clear how useful the trick is beyond this narrow case that I’ve encountered. The way I see it, the “deeply embedded expression” trick is applicable whenever you have data that is constructed from some fixed set of cases, and when proofs about that data need to follow the structure of these cases. Thus, examples include:

There are some pretty clear commonalities about examples above, which are the ingredients to this trick:

Conclusion

I’ll be the first to admit that this trick is quite situational, and may not be as far-reaching as the “Is Something” pattern I wrote about before, which seems to occur far more in the wild. However, there have now been two times when I personally reached for this trick, which seems to suggest that it may be useful to someone else.

I hope you’ve found this useful. Happy (dependently typed) programming!