Stream: Coq users

Topic: Software Foundations - Colors.v - color_correct

jco (Jun 18 2020 at 14:17):

With some help from @Li-yao, I was able to figure out a number of proofs that had gotten me stuck. Learning about the existence of WP.fold_rec_bis was really cool! I feel like I'm getting better at reasoning about folds, but now I'm pretty struck. This is a hard module! Or I'm just terrible at this stuff :( Regardless, I'm failing to find a good "line of attack" for this final proof.

The proof: forall palette g, no_selfloop g -> undirected g -> coloring_ok palette g (color palette g).

Messing around this for a while, it seems like the key proof is M.find i (color palette g) = Some ci -> S.In ci palette

An alternate statement I was able to cook up with S.Subset (color_of (color palette g)) (palette). This is another one of those proofs that seems obvious, but the proof is nontrivial! In this case, I'm not quite sure how to deal with color...it itself is a fold_right, but the pieces of that fold right get pretty complex pretty quickly (not complete to understand, but complex to reason about in Coq). This is sort of a theme in general, though maybe it just comes with experience...computationally "complex" functions (like color and especially things like select and select_terminates) seem quite difficult to prove things about. I guess ultimately that's the beauty of induction, I'm just sort of not seeing how to "pierce the veil" (pun intended). Would appreciate any pointers on this problem and sort of how to look at these in general. Maybe it's just a lack of experience. I've found the proofs in Color.v much harder than the other modules of VFA!

jco (Jun 18 2020 at 14:19):

I should add that for the proof of M.find i (color palette g) = Some ci -> S.In ci palette I've done a lot of exploration but don't really have much to show for it. Induction on palette and g don't really reduce the problem in an obvious way. It seems like we need to show that the computation from color will always return a result in palette...but I'm not sure how to do that in coq. I just wish I had more to show!

jco (Jun 18 2020 at 14:22):

There's another proof "in_colors_of_1" which is S.In i s -> M.find i f = Some c -> S.In c (colors_of f s), and colors_of seems a bit nicer to work with as far as a recursion, bu tI still just have no great way to link the palettes to each other

jco (Jun 18 2020 at 14:23):

(sorry for all the babbling, I just am trying to say that I've spent a decent amount of time on this...maybe 3 hours? I usually wait until I feel like I'm not making any progress with my unfoldings and proof attempts and explorations for 2-3 hours before I ask a question)

Donald Sebastian Leung (Jun 18 2020 at 15:36):

Don't worry, you're definitely not the only one who found the Color.v chapter difficult. I've been able to complete every single exercise in VFA except color_correct (actually, I'm bad with graphs and didn't really understand the content in Color.v at all but somehow managed to brute-force every lemma/theorem in that chapter except the very final one).

jco (Jun 18 2020 at 15:37):

Donald Sebastian Leung said:

Don't worry, you're definitely not the only one who found the Color.v chapter difficult. I've been able to complete every single exercise in VFA except color_correct (actually, I'm bad with graphs and didn't really understand the content in Color.v at all but somehow managed to brute-force every lemma/theorem in that chapter except the very final one).

that...really helps, thanks for sharing. I'm really passionate about getting better at proof assistants...but it's much more brain bending than python!

Li-yao (Jun 18 2020 at 15:39):

This chapter is particularly hard because you have to learn to navigate the lack of documentation around FSets, and the whole thing could maybe use more text (but it's certainly nontrivial to signpost things sufficiently)

jco (Jun 18 2020 at 15:52):

I definitely do not blame the writers, this stuff is hard to get right and on the whole, software foundations has been one of the best learning experiences of my life

jco (Jun 18 2020 at 15:53):

that said, the jump in difficulty with the colors module was real! I feel like I've learned a ton though, though a lot of the graph traversal stuff eludes me. That's why I'm particular curious about the Sin_domain proof without the fold_rec_bis, for example

jco (Jun 18 2020 at 15:56):

and of course the final color_correct still eludes me :)

Li-yao (Jun 18 2020 at 15:58):

A proof of M.find i (color palette g) = Some ci -> S.In ci palette would have to look at where the color algorithm adds colors to the result map and check that they come from palette. This happens inside the color1 function. In particular, this property is entirely independent of the last argument of fold_right in color, where g occurs.

Li-yao (Jun 18 2020 at 16:01):

That property that the set of colors is a subset of palette is actually an invariant of the fold_right (it holds at every step), so you can look for an induction principle for that (similar to the one discussed before for M.fold).

jco (Jun 18 2020 at 16:02):

Li-yao said:

A proof of M.find i (color palette g) = Some ci -> S.In ci palette would have to look at where the color algorithm adds colors to the result map and check that they come from palette. This happens inside the color1 function. In particular, this property is entirely independent of the last argument of fold_right in color, where g occurs.

this makes sense and I will focus my effort on trying to see what I can prove about that part of things!

jco (Jun 18 2020 at 16:03):

Li-yao said:

That property that the set of colors is a subset of palette is actually an invariant of the fold_right (it holds at every step), so you can look for an induction principle for that (similar to the one discussed before for M.fold).

this is the original direction I was thinking with the subset stuff, but I couldn't see a way to reason about invariants with fold_right. I'm not sure how the fold_rec_bis came about...I guess I could try to implement something like it

jco (Jun 18 2020 at 16:03):

fold_right does have a bunch of stuff, but it seems like it's all about equivalences

jco (Jun 18 2020 at 16:04):

I spent a bunch of time looking at "Search fold_right" trying to find something that would let me reason about the invariant like was possible for M.fold because that would be perfect

jco (Jun 18 2020 at 16:05):

hmm, taking another look, I wonder if fold_right_commutes2 might do it..

jco (Jun 18 2020 at 16:06):

though that would be if I wanted to show that Subset (singleton ci) palette I guess, as it still doesn't allow one to maintain an invariant

Li-yao (Jun 18 2020 at 16:10):

hmm it's a bit perplexing that there's no such lemma, but actually it is subsumed by induction on lists.

jco (Jun 18 2020 at 16:11):

Not sure what you mean

jco (Jun 18 2020 at 16:13):

I guess I'm not sure where fold_rec_bis came from. Is it autogenerated by coq or implemented by people? I guess I could implement something like it for fold_right or fold-left, or...I'm not sure how to connect to lists. The Fold_right in this case is operating on lists I believe

Li-yao (Jun 18 2020 at 16:18):

So you want to prove P (color palette g) (for some P), which after unfold-ing is P (fold_right (color1 palette g) (M.empty _) (select ...)), and as I mentioned earlier, it doesn't matter what the last argument (select ...) is, so you can do induction (select _ _).

jco (Jun 18 2020 at 16:25):

Yeah that makes sense. Cool I think this is probably enough fuel for me to bump into something that makes sense!

jco (Jun 19 2020 at 14:04):

I was able to crack the proof :D Thanks again!!!!!!

Last updated: Apr 18 2024 at 07:02 UTC