Yiming Xu (Feb 08 2025 at 19:56): Yiming Xu (Feb 08 2025 at 19:56):I use zip lists to store values that are in correspondence, say, I can have
"for all x1 y1. (x1,y1) in set (zip xl yl) ==> P x1 y1"
and now I also have
"for all x1 z1. (x1,z1) in set (zip xl zl) ==> Q x1 z1"
and I want to pick a tuple (x,y,z) so I get P x y and Q x z.
But I cannot rely on the nth element function to do that, since there are duplicated values.
I tried zip all these three together, by considering "(zip xl (yl zl))". If I have "(x,y) in zip xl yl", then I have an n such that "(x,y) = zip xl yl ! n", and I can then pick the n-th element of "(zip xl (yl zl))". But sledgehammer does not seem to work well on this.
Any suggestions on how to deal with this sort of things?
Yiming Xu (Feb 08 2025 at 20:12):By "sledgehammer not working well" I refer to
I defined:
define ZL where "ZL ≡ zip ul (zip ul' (zip phil fl'))"
define phi0 where "phi0 ≡ fst (snd (snd (ZL ! j)))"
and ask sledgehammer to prove "phi0 = phil ! j", it gives me nothing. (I did not miss any assumption on the lengths of the lists.)
Mathias Fleury (Feb 08 2025 at 20:33):But I cannot rely on the nth element function to do that, since there are duplicated values.
?
nth is just the nth element. The 5th element of [1,1,1,1,1,.....,1] is 1. Duplication have no importance
Mathias Fleury (Feb 08 2025 at 20:48):I am not sure what you want. From what I understand it is this:
lemma
assumes ‹∀ x1 y1. (x1,y1)∈ set (zip xl yl) ⟶ P x1 y1›
‹∀ x1 z1. (x1,z1) ∈ set (zip xl zl) ⟶ Q x1 z1›
‹x ∈ set xl›
‹length xl = length yl›
‹length xl = length zl›
shows ‹∃n. x = xl ! n ∧ (x, yl ! n) ∈ set (zip xl yl) ∧ P x (yl ! n) ∧ (x, zl ! n) ∈ set (zip xl zl) ∧ Q x (zl ! n)› (is ‹∃n. ?R n›)
proof -
obtain n where n: ‹x = xl ! n› ‹n < length xl›
using assms(3) unfolding in_set_conv_nth
by auto
moreover have ‹Q (xl ! n) (zl ! n)›
using assms n
by (metis in_set_zip prod.sel(1) prod.sel(2))
ultimately have ‹?R n›
using assms
by (metis in_set_zip prod.sel(1) prod.sel(2))
then show ?thesis by blast
qed
Yes. The lemma is what I mean. The annoying thing is that I need it for four lists. It is then obvious from your proof that such a proof is not supposed to be automatic...
Yiming Xu (Feb 08 2025 at 21:03):Mathias Fleury said:
But I cannot rely on the nth element function to do that, since there are duplicated values.
?
nth is just the nth element. The 5th element of [1,1,1,1,1,.....,1] is 1. Duplication have no importance
I mean I cannot rely on the fact that (x,y) = zip xl yl ! i to pick the i-th element of zip xl zl to get the effect. That is because we have duplicates.
Mathias Fleury (Feb 08 2025 at 21:07):So this is what you want, going from the element in the zip to the element in the original list
lemma
assumes "(u, u') ∈ set (zip ul ul')"
obtains i where "u' = ul' ! i" "u = ul ! i" "i < length ul" "i < length ul'"
using assms
by (metis in_set_zip prod.sel(1) prod.sel(2))
?
Yiming Xu (Feb 08 2025 at 21:12):I believe that s not enough since what I have is:
(x,y) in set zip xl yl --> P x y
(y,z) in set zip yl zl --> Q y z
(z,e) in set zip zl el --> R z e
and I have (x,y) fixed, want a z and a e such that P x y and Q y z and R z e.
Yiming Xu (Feb 08 2025 at 21:13):Oh just discovered I need 5 lists involved...
Mathias Fleury (Feb 08 2025 at 21:14):Yeah but this is wrong
Yiming Xu (Feb 08 2025 at 21:15):Why cannot we zip all the lists together, and look for a tuple that has the given pair?
Mathias Fleury (Feb 08 2025 at 21:16):Ah no wait transitive stuff
Mathias Fleury (Feb 08 2025 at 21:17):xl = [1, 1, 1]
yl = [1, 1, 1]
zl = [1, 2, 3]
Q y z <--> z = 3
x = 1
y = 1
Ah right you vary the position of x
Yiming Xu (Feb 08 2025 at 21:17):take big zip of 5 lists is quite brute force and I think maybe I need this... (But I really do not want to use it by hand)
lemma fst_zip :
assumes "length l1 = length l2"
and "n < length l1"
shows
"fst (zip l1 l2 ! n) = l1 ! n"
using assms(1) assms(2) by force
lemma snd_zip :
assumes "length l1 = length l2"
and "n < length l1"
shows
"snd (zip l1 l2 ! n) = l2 ! n" using assms
by simp
Mathias Fleury (Feb 08 2025 at 21:22):Earlier you had:
"for all x1 z1. (x1,z1) in set (zip xl zl) ==> Q x1 z1"
This is a typo for zip yl zl?
Yiming Xu (Feb 08 2025 at 21:23):Do you mean"for all x1 z1. (x1,z1) in set (zip yl zl) ==> Q x1 z1"?
Yiming Xu (Feb 08 2025 at 21:24):I do not mean that.
Yiming Xu (Feb 08 2025 at 21:25):I should figure out the precise abstraction of the thm I need.
Yiming Xu (Feb 08 2025 at 21:25):If some of the relations are symmetric the order of list does not matter, otherwise it may do.
Mathias Fleury (Feb 08 2025 at 21:26):Yiming Xu said:
I use zip lists to store values that are in correspondence, say, I can have
"for all x1 y1. (x1,y1) in set (zip xl yl) ==> P x1 y1"and now I also have
"for all x1 z1. (x1,z1) in set (zip xl zl) ==> Q x1 z1"
Yiming Xu (Feb 08 2025 at 21:29):This is an over-simplification. Let me be more careful and write it out.
Mathias Fleury (Feb 08 2025 at 21:29):lemma H:
assumes ‹∀ x1 y1. (x1,y1)∈ set (zip xl yl) ⟶ P x1 y1›
‹∀ x1 z1. (x1,z1) ∈ set (zip yl zl) ⟶ Q x1 z1›
‹(x, y) ∈ set (zip xl yl)›
‹length yl = length zl›
shows "∃z. (y, z) ∈ set (zip yl zl) ∧Q y z"
using assms
by (meson in_set_impl_in_set_zip1 in_set_zipE)
lemma H2:
assumes ‹∀ x1 y1. (x1,y1)∈ set (zip xl yl) ⟶ P x1 y1›
‹∀ x1 z1. (x1,z1) ∈ set (zip yl zl) ⟶ Q x1 z1›
‹∀ x1 z1. (x1,z1) ∈ set (zip zl el) ⟶ R x1 z1›
‹(x, y) ∈ set (zip xl yl)›
‹length yl = length zl›
‹length zl = length el›
shows "∃z e. (y, z) ∈ set (zip yl zl) ∧ Q y z ∧ (z, e) ∈ set (zip zl el) ∧ R z e"
using assms H[OF assms(1,2,4,5)] H[OF assms(2,3) _ assms(6)]
by blast
lemma H3:
assumes ‹∀ x1 y1. (x1,y1)∈ set (zip xl yl) ⟶ P x1 y1›
‹∀ x1 z1. (x1,z1) ∈ set (zip yl zl) ⟶ Q x1 z1›
‹∀ x1 z1. (x1,z1) ∈ set (zip zl el) ⟶ R x1 z1›
‹∀ x1 z1. (x1,z1) ∈ set (zip el fl) ⟶ S x1 z1›
‹(x, y) ∈ set (zip xl yl)›
‹length yl = length zl›
‹length zl = length el›
‹length el = length fl›
shows "∃z e f. (y, z) ∈ set (zip yl zl) ∧ Q y z ∧ (z, e) ∈ set (zip zl el) ∧ R z e
∧ (e, f) ∈ set (zip el fl) ∧ S e f"
using assms H[OF assms(1,2,5,6)] H[OF assms(2,3) _ assms(7)]
H[OF assms(3,4) _ assms(8)]
by blast
having to instantiate H is a pain, but it works
Mathias Fleury (Feb 08 2025 at 21:31):(the length part is important, nitpick told me so!)
Yiming Xu (Feb 08 2025 at 21:35):Thanks and I am impressed with how hard it is. I just have done some investigation and found out that I have 4 lists, and 4 relations, instead of 4 lists and 3 relations.
Yiming Xu (Feb 08 2025 at 21:36):I will try out your technology first and think about it works for that case.
Yiming Xu (Feb 08 2025 at 22:09):I think I want :
lemma foo:
assumes
"⋀u phi. (u,phi) ∈ set (zip us phis) ==> P u phi"
and
"⋀v psi. (v,psi) ∈ set (zip vs psis) ==> Q v psi"
and
"⋀(phi::'a) psi::'a. (phi,psi) ∈ set (zip phis psis) ==> E phi psi "
and
"(u,v) ∈ set (zip us vs)"
and "equiv UNIV {(x,y). E x y}"
and "length us = length vs"
and "length us = length phis"
and "length vs = length psis"
and "length psis = length phis"
shows
"∃phi psi. P u phi ∧ Q v psi ∧ E phi psi" using assms nitpick
which is solved by sledgehammer.
Balazs Toth (Feb 10 2025 at 09:07):I'm not sure if this helps you, but there is the list_all2 which is like a zip that apply the predicate pairwise on the lists. (and it returns false if the list don't have the same length)
Last updated: Mar 09 2025 at 12:28 UTC