Salvatore Francesco Rossetta (Apr 15 2024 at 10:02): Salvatore Francesco Rossetta (Apr 15 2024 at 10:02):Is there any lemma similar to this?
lemma max_eqI:
assumes
"l ! x = Max(set l)" and
"l' ! x > l ! x" and
"x ≠ y" and
"l ! y ≥ l' ! y"
shows "Max (set l') = l' ! x"
you're missing quantifiers in the lemma statement, also, generally you will need to assume x <= length l and similarly for y
Salvatore Francesco Rossetta (Apr 15 2024 at 10:18):Something like this?
lemma max_eqI:
assumes
"x ≤ length l" and
"finite (set l)" and
"length l = length l'" and
"l ! x = Max(set l)" and
"l' ! x > l ! x" and
"∀y ≠ x. y ≤ length l ⟹ l ! y ≥ l' ! y"
shows "l' ! x = Max (set l')"
this looks fine, although you don't need the finite (set l) assumption
In addition, I made a typo earlier, you probably want x < length l rather than <=
edit: one more problem, your quantifier over y isn't binding correctly. if you look at the statement in Isabelle you will notice that y is not colored green i.e., it's a free variable
Yong Kiam (Apr 15 2024 at 11:17):returning to your original question: no I don't think there's something like this in the library, but it should not be a difficult exercise to prove this from the usual intros for Max
Salvatore Francesco Rossetta (Apr 15 2024 at 12:54):Yong Kiam said:
this looks fine, although you don't need the
finite (set l)assumptionIn addition, I made a typo earlier, you probably want
x < length lrather than<=edit: one more problem, your quantifier over
yisn't binding correctly. if you look at the statement in Isabelle you will notice thatyis not coloredgreeni.e., it's a free variable
How do I bind correctly y? I never used quantifiers in assms
Mathias Fleury (Apr 15 2024 at 14:01):Compare the colors in
term "⋀y. y ≤ length l ⟹ l ! y ≥ l' ! y"
term "∀y. y ≤ length l ⟹ l ! y ≥ l' ! y"
term "∀y. y ≤ length l ⟶ l ! y ≥ l' ! y"
(green = bound, blue = free)
Yong Kiam (Apr 15 2024 at 14:03):alternatively: add parens
Mathias Fleury (Apr 15 2024 at 14:37):Yeah with parentheses you get error messages:
term "∀y. (y ≤ length l ⟹ l ! y ≥ l' ! y)"
You cannot use meta implication (⟹) underneath HOL a HOL quantifier (∀).
Manuel Eberl (Apr 15 2024 at 14:46):Basically, use meta quantifiers and meta implication whenever possible.
Manuel Eberl (Apr 15 2024 at 14:47):HOL quantifiers and implication are necessary when you have quantifiers or implication nested inside something else, e.g. something like ∃x. ∀y. P x y or filter (λx. ∀y. P y ⟶ Q x y). Here you cannot replace the ∀ and ⟶ with meta quantifiers/meta implication because they occur inside other HOL constants.
Manuel Eberl (Apr 15 2024 at 14:48):In principle you can also just always use HOL quantifiers and HOL implication everywhere and ignore the meta stuff entirely. But that will make your theorems a bit more awkward to use later because you cannot instantiate them as easily.
Salvatore Francesco Rossetta (Apr 15 2024 at 16:38):I did it in the end, but what if I want to prove this now? Is there any useful lemma?
lemma filter_size_is_one_helper:
fixes
fv::"rat list"
assumes
"x < length fv" and
"m = Max(set fv)" and
"fv ! x = m" and
"⋀y. y ≠ x ⟹ y < length fv ⟹ fv ! y < m"
shows "length (filter (λx. fv ! x = m) ps) = 1"
what is ps?
Mathias Fleury (Apr 15 2024 at 16:53):ah any list okay
Mathias Fleury (Apr 15 2024 at 16:54):but then the lemma is wrong
Mathias Fleury (Apr 15 2024 at 16:54):Nitpicking formula...
Nitpick found a potentially spurious counterexample:
Free variables:
fv = [0]
m = 0
ps = []
x = 0
My best guess is that you are trying to do:
lemma filter_size_is_one_helper:
fixes
fv::"'a :: linorder list"
assumes
"x < length fv" and
"m = Max(set fv)" and
"fv ! x = m" and
strict_le: "⋀y. y ≠ x ⟹ y < length fv ⟹ fv ! y < m"
shows "length (filter (λx. fv ! x = m) [0..<length fv]) = 1"
proof -
have le: ‹[0..<length fv] = ([0..<x] @ [x] @ [Suc x ..< length fv])›
using ‹fv ! x = m›
by (metis append_Cons assms(1) leI le_add_diff_inverse less_imp_le_nat not_less_zero
self_append_conv2 upt_add_eq_append upt_rec)
show ‹length (filter (λx. fv ! x = m) [0..<length fv]) = 1›
using strict_le assms(1,3) unfolding le by (force simp: filter_empty_conv)
qed
Mathias Fleury said:
My best guess is that you are trying to do:
lemma filter_size_is_one_helper: fixes fv::"'a :: linorder list" assumes "x < length fv" and "m = Max(set fv)" and "fv ! x = m" and strict_le: "⋀y. y ≠ x ⟹ y < length fv ⟹ fv ! y < m" shows "length (filter (λx. fv ! x = m) [0..<length fv]) = 1" proof - have le: ‹[0..<length fv] = ([0..<x] @ [x] @ [Suc x ..< length fv])› using ‹fv ! x = m› by (metis append_Cons assms(1) leI le_add_diff_inverse less_imp_le_nat not_less_zero self_append_conv2 upt_add_eq_append upt_rec) show ‹length (filter (λx. fv ! x = m) [0..<length fv]) = 1› using strict_le assms(1,3) unfolding le by (force simp: filter_empty_conv) qed
Sorry, my actual aim is to do something similar to the lemma you wrote, like this
lemma filter_size_is_one_helper_2:
fixes
fv::"'a :: linorder list"
assumes
"index ps x < length fv" and
"index ps x < length ps" and
"length ps = length fv" and
"x ∈ set ps" and
"m = Max(set fv)" and
"fv ! index ps x = m" and
strict_le: "⋀y. y ≠ index ps x ⟹ y < length fv ⟹ fv ! y < m"
shows "length (filter (λx. fv ! (index ps x) = m) ps) = 1"
So filtering one list using indexes of another list (ps) of the same length. I then added some assumptions to use the lemma you wrote in my case but i am missing something, i think
Salvatore Francesco Rossetta (Apr 16 2024 at 09:57):I am trying to adapt, I managed to write the first step, but in showing the thesis it fails.
lemma filter_size_is_one_helper_my_case:
fixes
fv::"'a :: linorder list"
assumes
"index ps x < length fv" and
"index ps x < length ps" and
"length ps = length fv" and
"x ∈ set ps" and
"m = Max(set fv)" and
"fv ! index ps x = m" and
"ps ! index ps x = x" and
strict_le: "⋀y. index ps y < length ps ⟹ y ∈ set ps ⟹index ps y ≠ index ps x ⟹ index ps y < length fv ⟹ fv ! index ps y < m"
shows "length (filter (λx. fv ! (index ps x) = m) [0..<length ps]) = 1"
proof -
have le: ‹[0..<length ps] = ([0..<index ps x] @ [index ps x] @ [Suc (index ps x) ..< length fv])›
using ‹fv ! index ps x = m›
by (metis Cons_eq_appendI assms(2) assms(3) eq_Nil_appendI le_add2 le_add_same_cancel2 less_imp_add_positive upt_add_eq_append upt_conv_Cons)
show ‹length (filter (λx. fv ! (index ps x) = m) [0..<length ps]) = 1›
using strict_le assms unfolding le by (force simp: filter_empty_conv)
qed
What is missing?
Mathias Fleury (Apr 16 2024 at 10:05):Replace force by auto, look at the goal that do not work and think how you would prove things by hand
Mathias Fleury (Apr 16 2024 at 10:05):this will tell you what is missing
Last updated: May 06 2024 at 08:19 UTC