6 Relations

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

We have seen one example of using a data definition to create a new datatype (and, briefly, a second example in the demo chapter, where we used polymorphic lists). Defined relations between datatype elements give us logical statements. We imported the equality relation to form our first theorems.

Equality is defined using the same datatype mechanism, but understanding the nuances of how this happens should be put off a while longer. Instead, we will consider relations that are simpler to explain. Relations can be among more than two elements, or just on a single element (for example, "being even").

The constructors of a datatype defining a relation (or more generally, providing evidence for some form of logical statement) can be seen as representing inference rules for that relation, in the same way as PLFA explained the constructors for the natural numbers using inference rules.

6.1 Defining relations

Our first example of the definition of a relation will be the "less than or equal to" relation, which Unicode conveniently lets us write as ≤. The definition is indexed by the two natural numbers being related.

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

The definition of ≤ in PLFA matches that in the Agda standard library. Interestingly enough, the definition in SF is different, to match the Coq standard library. The two definitions are equivalent. As a thought exercise, perhaps you can figure out another definition, and prove the equivalence of the two definitions.

PLFA presents the proof of 2 ≤ 4 in a stack by identifying the hypotheses of one rule with the conclusion of another. In general this will not result in a stack, but a tree, as there could be several hypotheses (but only one conclusion). The constructor-based proof can be viewed as a concise way of representing this tree. Proof trees are likely to show up in most conventional treatments of logic, so don’t be surprised if you see them elsewhere.

6.2 Implicit arguments

Implicit arguments are helpful in improving expressivity by reducing the amount of information the programmer has to provide to the typechecker. But sometimes the typechecker cannot infer the arguments, or we need to provide different ones than it might expect, so we need ways of providing them. PLFA demonstrates several, some of which show up during interaction, so now you will recognize them when you see them.

In this chapter, we start to see that pattern matching in Agda is sophisticated. It can detect cases that cannot happen and don’t need to be included. Refinement and case-split work well with it, generating patterns that are forced by details of the case. We may sometimes need to edit those generated patterns in subsequent developments, for example, to name an argument that was previously unused and replaced by an underscore.

The proof of 2 ≤ 4 can be derived by Agda just using the "refine" command without typing anything else, because with concrete arguments, there is only one possible choice for the constructor at each step. Later we will see how we can automate the repeated uses of "refine".

6.3 Inversion

The idea of inversion is important, but in practice we rarely need to use theorems like the two proved here. Instead we use the same interactive techniques used to prove these theorems to do the necessary transformations on the fly in the places we would apply the theorems.

Using m≤n as the name of a variable with type m ≤ n is a clever mnemonic, but it has its cost. If you try to type ≤ in Emacs with \le, and then type n, you will get the ≰ symbol. One way to avoid this is to add a space after ≤ appears and then delete it. There are other ways, but you still have to remember to do something.

6.4 Properties of relations

You may be familiar with some or all of these properties. We will be seeing many of these terms again, so please mentally bookmark this PLFA summary for future use.

6.5 Reflexivity

We can’t case-split on an implicit argument that is listed as "not in scope" in the context. We can move it into scope by adding it in curly braces in the pattern, and a quick way to do this is to try to case-split on it anyway.

6.6 Transitivity

The version without implicit arguments is a bit frustrating to develop interactively, as Agda creates dotted patterns with underscores within as one does case-splitting. We’ll talk about dotted patterns later; for the time being, you can ignore the dot. But manual editing is necessary, as well as bringing variables into scope. While we can avoid this work by using implicit arguments, we’ll later encounter situations where a certain amount of this is required.

6.7 Anti-symmetry

Using rewrite, we arrive at a different proof.

≤-antisym z≤n z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m)
  rewrite ≤-antisym m≤n n≤m = refl

6.8 Total

With consistent parallel construction, this section would be called "Totality", but perhaps that sounds too ominous. Agda functions must be total, but relations need not be. In fact, the empty relation is a perfectly good relation (and sometimes even useful).

This is the first section in PLFA to use a parameterized datatype. We saw one briefly in the demo chapter; our list datatype was parameterized by element type. The differences between parameterized and indexed datatypes, beyond the obvious ones shown in PLFA, are subtle, and the choice of which to use is made easier with experience.

This section also introduces the with clause, a concise way of doing case analysis on an arbitrary expression. As shown in PLFA, it is equivalent to the use of a helper function, which can be defined locally using where (this has the advantage of being able to use local context). A where block can be attached to any equation in a function definition. Later, we will see that rewrite is equivalent to a particular use of with.

The ellipsis (...) in a with clause is replacing the pattern up to the keyword with. Sometimes refinement will fill the pattern back in. There are reasons for doing this in complicated circumstances but for us this is mostly a nuisance. Once our development is done, we can go back and replace the ellipses, and we should, to improve readability.

One way to work interactively with with clauses is to write out the expression following it, then write the next line as:
... | r = ?
Here r stands for ’result’, and will be in scope in the hole, at which point one can split on it. This is the technique I will use in asciicasts.

Just as rewrite can use multiple equations separated by vertical bars, with can split on multiple expressions separated by vertical bars. We’ll see examples of this later.

If you find you have used a with clause on an expression e, given the result a name like r, and then completed the right-hand side without case-splitting on r, then you probably did not need to use the with clause, and your code will probably be cleaner if you just substitute e wherever you have used r on the right-hand side. I want to emphasize this point, because I see this more than I should in beginner code.

Sometimes you have a long expression e and you just want to give it a shorter name for convenience. In this case, it’s best to use a where clause, or Agda’s let form, which is described in the Agda documentation.

6.9 Monotonicity

Distributivity is a property of two operators, and is order-specific (for example, multiplication distributes over addition, but addition does not distribute over multiplication). Monotonicity is a property of an operator and an ordering.

An asciicast of the monotonicity theorems wouldn’t add much to the text in PLFA, so I have not provided one. The starter file has holes if you wish to practice interaction using these theorems.

6.10 Strict inequality

The standard library definition of strict inequality is simpler, and is based on non-strict inequality rather than a new datatype. This definition is in PLFA mainly to provide fodder for exercises, several of which you can do for credit.

6.11 Even and odd

This section is notable for the first uses of mutual recursion, both in defining datatypes and in proving theorems about them. We could define "odd" as "not even". But we haven’t defined negation yet (that is coming shortly), and even when we do, having a more positive definition can sometimes be more elegant, both conceptually and in terms of ease of use.

I have moved the Bin-predicates exercise into the Isomorphism file (and also tweaked it somewhat).