I'm new to agda and trying to prove that 5 is prime :).
I'm now trying to dismiss that 2 is a divisor of 5. I have:
p1 : k * 2 ≡ 5
p2 : k ≤ 5
I would now hope that pattern matching like:
case (p2 ,′ p1 ) of λ where ()
would typecheck as there's 6 terms fulfilling p2 and none of them fulfills p1. Doesn't seem like the computational budget should get exceeded so quickly, no?
Is there a way to make it work? How else can i continue with p1 and p2 and in general: how to prove 5 is prime or that 2 does not divide it?
Let's try defining the following:
goal : ∀ k → (k ≤ 5) × (k * 2 ≡ 5) → ⊥
If we simply bind all the variables, we have
Goal: ⊥
y : k * 2 ≡ 5
x : k ≤ 5
k : ℕ
While we can see that this is absurd, Agda cannot: each of the premises is possible in isolation, and Agda is not going to try checking every possible value of k because it wouldn't know when to stop. So we have to guide it by making the appropriate case split ourselves. Let's see what happens if we split on k once:
goal (suc k) (x , y) = {! !}
Now Agda was able to discard the zero case as absurd, because in that case we have y : zero ≡ suc (suc (suc (suc (suc zero)))), which is impossible. We are left with the suc k case, which is still not immediately absurd. Let's split on k two more times:
goal (suc (suc zero)) (x , y) = {! !}
goal (suc (suc (suc k))) (x , y) = {! !}
Now Agda can see that both of these cases are absurd, because in the first one we have y : 4 ≡ 5 and in the second one we have y : 6 + k * 2 ≡ 5, which reduces to suc (k * 2) ≡ zero. We can't just discard both cases though, because Agda needs to know it should make those splits. Thus the simplest definition that works is
goal : ∀ k → (k ≤ 5) × (k * 2 ≡ 5) → ⊥
goal 2 ()
Agda will create a case tree that includes 2 and see that each case is absurd (this would work with a higher number as well). Note that we have not used the k ≤ 5 argument.
A more principled approach would be to use proof by reflection: for example, if you can prove that divisibility of natural numbers is decidable, then the proof doubles as an effective decision procedure for divisibility. You can then ask Agda whether 2 divides 5 and extract a proof from the (negative) answer.