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!

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!

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

(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)

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).

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!

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)

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

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

and of course the final color_correct still eludes me :)

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.

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`

).

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!

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

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

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

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

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

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

Not sure what you mean

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

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 _ _)`

.

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

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

Last updated: Sep 23 2023 at 06:01 UTC