@Paolo Giarrusso I have created a new thread as I worried that I was getting off topic.

Perhaps metaprogramming / plugins are not the right solution for me.

I will be a little more concrete, take the pigeonhole principle for maps f: 'I_n -> 'I_m, where we conclude that if m < n then there are x, y in 'I_n with x < y and f(x)=f(y). What would a "model proof" of this theorem look like? It has to deal with the difference between naturals and elements of 'I_n, perhaps conversion between functions and fintype maps, possibly manipulating negation / contrapositives (f is not injective -> there are x, y with x < y and f(x) = f(y)). I have written some pages of code about ordinal arithmetic in this vein and I am very unhappy with how verbose it is, but I don't know how to proceed. I will try to post my work on github soon and request constructive feedback from the community.

@Patrick Nicodemus it looks like you want to be using MathComp/SSReflect for the model lemma/proof? (In this case, the best place is MathComp users stream, I can move this topic there)

This topic was moved here from #Coq users > Best practices for automation in mathematical proofs by Karl Palmskog.

Last updated: Jul 25 2024 at 16:02 UTC