2
$\begingroup$

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?

$\endgroup$
1

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ I think the other half of the answer is that Agsy doesn't have any way to deal with the variables it wants to use not being in scope. The solution is to bring them into scope via either the s<s constructors' implicit arguments or by un-dotting the dot patterns and filling in the _s. $\endgroup$
    – James Wood
    Mar 15 at 9:54
  • $\begingroup$ @JamesWood I think the implicits are introduced in the pattern s<s {m} {n} m<n instead of the prior dotted patterns, but yeah you can also undot them $\endgroup$
    – ice1000
    Mar 15 at 15:32
  • 1
    $\begingroup$ In a sense, dot patterns can never introduce variables, but they sometimes are the most convenient or clearest place to introduce variables (after undotting). $\endgroup$
    – James Wood
    Mar 15 at 16:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.