Skip to main content
Became Hot Network Question
edited tags
Link
ice1000
  • 6.3k
  • 10
  • 63
Source Link
tinlyx
  • 2.2k
  • 1
  • 7
  • 29

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

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?