Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

Question

I am trying to prove the transitivity of <. But I got stuck as the proof found by Auto (C-c C-a in Emacs) causes an error. Also, I couldn't understand some of the new variables generated during the proof. The start point is:

<-trans : ∀ (m n p : ℕ)
  → m < n
  → n < p
  -----------
  → m < p
<-trans m n p m<n n<p = {}0

I proceeded by case analyzing the proof m<n. This gives:

-- ...
<-trans .zero .(suc _) p z<s n<p = {}0
<-trans .(suc _) .(suc _) p (s<s m<n) n<p = {}1

The new pattern terms such as .zero .(suc _) on the LHS looks strange. I don't understand why they are needed in place of the regular zero and (suc n). And they don't seem to appear when displaying the associated goal. For example, C-c C-, on {}1 gives:

Goal: suc m < p
————————————————————————————————————————————————————————————
n<p : suc n < p
m<n : m < n
n   : ℕ   (not in scope)
m   : ℕ   (not in scope)
p   : ℕ

(Note that m and n are indicated as "not in scope", while the dot-patterns do not show up).

Further cases analysis on this hole and n<p turns the equation to:

-- ...
<-trans .(suc _) .(suc _) .(suc _) (s<s m<n) (s<s n<p) = {}1

, and there is a new not-in-scope variables n_1 in the context:

Goal: suc m < suc n
————————————————————————————————————————————————————————————
n<p : n₁ < n
n   : ℕ   (not in scope)
m<n : m < n₁
n₁  : ℕ   (not in scope)
m   : ℕ   (not in scope)

A bigger issue is that the Auto-generated proof (C-c C-a) doesn't type check:

-- ...
<-trans .(suc _) .(suc _) .(suc _) (s<s m<n) (s<s n<p) = s<s (<-trans m n₁ n m<n n<p)

When loaded (C-c C-l), the above proof generates an error about m in the Auto solution is not in scope:

m at ...Relations.agda:177,71-72
when scope checking m

Could someone help explain why are these dot-patterns and not-in-scope variables necessary, and how to solve the issue?

Moreover, is there a way to instruct Agda (2.6.3) and Emacs (29.1, Ubuntu 22.04) to avoid generating these dot-patterns?

Answer 1

Dotted patterns are also known as inaccessible patterns. My understanding is that the matched bindings are inaccessible, because they are generated from index unification. That's why they are marked with a dot, because the type checker will need to treat them as expressions instead of patterns.

A regular pattern needs to be linear (all bindings appear exactly once) and no function calls will be allowed. Then, you'll see the magic of dotted patterns. Here's an illustrative example:

open import Agda.Builtin.Nat

data F : Nat → Set where
  con : ∀ a → F (a + a)

test : ∀ a → F a → Nat
test .(x + x) (con x) = 0

The pattern con x makes sure that the type of this pattern is F (x + x) according to the type of con, and this says the a must be x + x, so we write x + x there as a hint. The feature is explained in docs.

Nowadays, thanks to the developers (I think primarily Jesper Cockx and Andreas Abel), the Agda LHS elaborator can infer dotted patterns automatically, so you don't have to mark it with a dot anymore if it's also a valid pattern, like in your case. However, if you want to put expressions there, you will need the dot, like if you remove the dot above and Agda 2.6.5-9e4afb1 will still complain about it.

When loaded (C-c C-l), the above proof generates an error about m in the Auto solution is not in scope:

Try replacing it with an underscore _ if it can be inferred during type checking, or use an implicit pattern (see related docs) to extract it from the LHS.