Stream: Coq users

Topic: generate proofs by for loop?


view this post on Zulip Quinn (Jan 24 2022 at 11:30):

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?

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:54):

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

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 12:16):

do you mean you wrote Lemma 0lt29 : 0 < 29. ... and invoke those, rather than ltac:(lia)?

view this post on Zulip Quinn (Jan 24 2022 at 15:25):

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?

view this post on Zulip Quinn (Jan 24 2022 at 15:26):

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

view this post on Zulip Quinn (Jan 24 2022 at 15:28):

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

view this post on Zulip Kenji Maillard (Jan 24 2022 at 15:38):

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 ?

view this post on Zulip Quinn (Jan 24 2022 at 15:43):

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?

view this post on Zulip Ana de Almeida Borges (Jan 24 2022 at 15:49):

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.

view this post on Zulip Kenji Maillard (Jan 24 2022 at 15:52):

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).

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 17:04):

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: Jan 29 2023 at 04:05 UTC