Quinn (Jan 24 2022 at 11:30): 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?
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.
Paolo Giarrusso (Jan 24 2022 at 12:16):do you mean you wrote Lemma 0lt29 : 0 < 29. ... and invoke those, rather than ltac:(lia)?
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?
Quinn (Jan 24 2022 at 15:26):yes, you are aren't you :D I just tried it and it worked.
Quinn (Jan 24 2022 at 15:28):as far as I know it doesn't help me reasoning about unknown n
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 ?
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?
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.
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).
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: Apr 19 2024 at 18:01 UTC