How can I use agda2-mode to generate patterns when I expect to see an absurd pattern?

Question

For example, we're proving 2 + 2 != 5:

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

And I can manually prove it:

2+2≠5 : 2 + 2 ≡ 5 → ⊥
2+2≠5 (sns (sns ()))

But I want the pattern (sns (sns ())) to be generated (just like filling a hole). Are there any ways to achieve that?

I am using Emacs 25 with agda2-mode.

There is a somewhat similar [issue](https://github.com/agda/agda/issues/2069#issuecomment-330351186). With this feature you could probably write `2+2≠5 (snsN ())` where `snsN` generates an appropriate number of `sns`s. Not much of automation, though. — effectfully, Nov 07 '17 at 05:51

score 3 · Accepted Answer · answered Nov 07 '17 at 12:22

Ok, so let's say you start from this configuration:

2+2≠5 : 2 + 2 ≡ 5 → ⊥
2+2≠5 h = {!!}

In this case you can use emacs' keyboard macros because the sub-term generated by matching on h will also be named h. So using:

you've recorded the action of "moving to the first goal an matching on h". You can now keep pressing <f4> until you reach an absurd case.

This is awesome! If a better approach doesn't appear for a day I'll set your answer as accepted :D — ice1000, Nov 07 '17 at 12:44

1 Answers1