Stream: Beginner Questions

Topic: Arbitrary number of variables

Chris_Y (Jul 04 2023 at 11:30):

Hi everyone, I wonder if there's any way to define an arbitrary (but fixed) number of variables that satisfy certain properties?

For instance, if I want to write "There exist m consecutive odd numbers in the interval I", where m is a fixed natural number, what would be the most efficient way to write it down?

Thank you!

Manuel Eberl (Jul 04 2023 at 12:09):

Typically you'd do that by fixing a set/multiset/list of numbers of size $m$. If they have to be distinct, a set; otherwise a list or a multiset, whichever is more convenient.

Manuel Eberl (Jul 04 2023 at 12:10):

An alternative to lists that is sometimes nicer is to just fix the number $m$ and treat the variables as a function $f$ of type nat ⇒ real (assuming you want real numbers) with the idea that you only care about the first $m$ values of that function, i.e. your "variables" are simply $f(0), \ldots, f(m-1)$.

Chris_Y (Jul 04 2023 at 14:45):

Great ideas! Thank you so much!

Kevin Lee (Jul 05 2023 at 13:53):

Following from this, I have shown that there exists 2m consecutive integers in the interval I

have "∃ s::int list. (∀ i∈{1..2*m-1}. s ! i = s ! (i-1) + (1::int)) ∧ (∀ i∈{0..2*m-1}. s ! i ∈ I)"

and I want to show that there exists m consecutive odd numbers in the interval I. What's the best way to do this?

Assuming the first element of s is odd, I tried
define l::"int list" where "l = map (λx. s! (nat (2*x))) [0 .. m-1]"
then to show "∀ i∈{1..m-1}. l! i = l! (i-1) + (2::int)" but I'm failing to even prove easy statements like "odd (l ! 0)" with "l ! 0 = s ! 0" and "odd (s ! 0)".

Jan van Brügge (Jul 05 2023 at 15:41):

Probably because the equality is the wrong way around. simp and similar methods do not use symmetry of equality because that would very quickly lead to endless loops. If you flip the equality either directly with the sym theorem or by stating the goal the other way, the proof should work

Wolfgang Jeltsch (Jul 05 2023 at 18:28):

You can also flip the sides of equalities with the symmetric attribute: equality_fact [symmetric].

Last updated: Dec 21 2024 at 16:20 UTC