I have a sigma-based `fin`

sort of type, and I have a known `n`

, which is 29. Unvirtuously, I longhand wrote `Lemma klt29 : k < 29. Proof. lia. Qed.`

29 times, for each k.

I'd like to do something similar for a fixed but unknown `n`

. Do I have any options?

I have some ideas, but I can't make sense of the program description... you can't really write `k < 29`

for each `k`

.

do you mean you wrote `Lemma 0lt29 : 0 < 29. ...`

and invoke those, rather than `ltac:(lia)`

?

I wrote out `zerolt29 : 0 < 29. Proof. lia. Qed.`

, `onelt29 : 1 < 29. Proof. lia. Qed.`

.

Are you telling me I can pass around `ltac:(lia)`

as like the literal proof term that `lia`

generates?

yes, you are aren't you :D I just tried it and it worked.

as far as I know it doesn't help me reasoning about unknown `n`

Quinn said:

as far as I know it doesn't help me reasoning about unknown

`n`

There is little you can prove about an unknown `n`

, for instance it is not the case that `0 < n`

.

Do you mean that you want to generate these proofs for an arbitrary but concrete integer `n`

?

I'm using a `Parameter (n : nat)`

in a `Section`

, so the caller will later supply an `n`

. Can I write something where like these lemmas will be generated at that time?

But these lemmas will only work for `k < n`

. Like, you picked 29, so you know that you will need `0 < 29`

, ... `28 < 29`

. If I pick 15, then I will only be able to prove them up to 14. If you have some assumption that `k < n`

then I don't quite understand why you need all of these lemmas. And if you don't have such an assumption, then at some point you will try to prove `20 < 15`

and things won't work. If you just want that the user can at any moment show 10 < 14, then `ltac:(lia)`

seems appropriate. If you really want that a user has lemmas called `kltn`

for every `k < n`

for an arbitrary but concrete `n`

, then I think you need some kind of meta-programming.

I don't think you can write anything along these lines using a parameter of a section. What you might be able to do is write a meta-programming function in Ltac2 / MetaCoq / Elpi and call this function on a concrete numeral (e.g. `15`

, `27`

but not a variable or an open expression).

With a section parameter you can also generate a list of proofs, without metaprogramming — `seq 0 n`

generates a list of numbers less than `n`

.

Last updated: May 19 2024 at 16:02 UTC