Proving a type empty in Agda

Question

I am trying to prove 2*3!=5 in agda. To do this I will define a function with a signature 2 * 3 ≡ 5 → ⊥.

making use of my definition of multiplication

data _*_≡_ : ℕ → ℕ → ℕ → Set where
  base : ∀ {n} → 0 * n ≡ 0
  succ : ∀ {n m k j} → m * n ≡ j → j + n ≡ k → suc m * n ≡ k

I have proven

1*3≡3 : 1 * 3 ≡ 3
1*3≡3 = (succ base) znn

and

3+3≡5 : 3 + 3 ≡ 5 → ⊥
3+3≡5 (sns (sns (sns ())))

But when I try to prove:

m235 : 2 * 3 ≡ 5 → ⊥
m235 ( ( succ  1*3≡3 ) ( x ) ) = ( 3+3≡5 x )

the compiler spits out this error about x

.j != (suc 2) of type ℕ
when checking that the expression x has type 3 + 3 ≡ 5

Sorry if this is a stupid question. Thanks in advance.

Answer 1

First of all, you forgot to include the definition of _+_≡_. I assume it's as follows:

data _+_≡_ : ℕ → ℕ → ℕ → Set where
  znn : ∀ {n} → 0 + n ≡ n
  sns : ∀ {n m k} → n + m ≡ k → suc n + m ≡ suc k

Next, your problem is not with finding the correct syntax, but you have to figure out how you can conclude from a value of type 2 * 3 ≡ 5. With the pattern matching you have done, you can ask Agda what values are available in the context, by replacing the right-hand-side with a ?, calling C-c C-l to compile and using C-c C-, to ask for the context:

m235 : 2 * 3 ≡ 5 → ⊥
m235 ( ( succ  1*3≡3 ) ( x ) ) = ?

Agda will say:

Goal : ⊥
-----------------------------
x     : .j + 3 ≡ 5
1*3≡3 : 1 * 3 ≡ .j
.j    : ℕ

That is: you are looking to prove bottom (i.e. an inconsistency from the assumptions) and you have 3 values available in the context. You have a proof of type 1 * 3 ≡ .j, for an unknown number .j as well as a proof of type .j + 3 ≡ 5. You seem to assume that Agda can automatically notice that j must be 3, but this is too difficult for it: it will only conclude things here from unification, not perform actual reasoning itself. So the solution is to help Agda understand why .j must be 3. You can do this by further pattern matching on the proof of type 1 * 3 ≡ .j:

m235 : 2 * 3 ≡ 5 → ⊥
m235 ((succ (succ base znn)) sum) = ?

Now the context looks as follows:

Goal: ⊥
————————————————————————————————————————————————————————————
x : 3 + 3 ≡ 5

You can now finish by combining the proof x of type 3 + 3 ≡ 5 with your previous proof that such a proof cannot exist:

m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ (succ base znn) x) = 3+3≡5 x

---

UPDATE: I missed it in my first reading, but there is a misunderstanding in the question that I missed and failed to explain. The error is in the following code:

m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ  1*3≡3 x) = 3+3≡5 x

The misunderstanding here is that the variable name 1*3≡3 in the left-hand side of this clause does NOT refer to the previously defined value by the same name. Rather, it introduces a fresh new variable which is known by Agda to have the same type, but whose value is not known by it.

What you were expecting can be achieved by using the "pattern synonyms" feature that was introduced in Agda 2.3.2: see the release notes:

pattern 1*3≡3 = (succ base) znn

m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ  1*3≡3 x) = 3+3≡5 x

Only pattern synonyms are expanded in patterns, other values aren't.