Stream: Coq users

Topic: Some help with Software Foundations VFA Colors.v


view this post on Zulip jco (Jun 17 2020 at 09:59):

Hello, I'm not sure if this is the right place...I'm new to zulip and not sure what should go where. The discourse seems pretty dead, otherwise I'd go there? Regardless, I'm trying to prove Sin_domain from Colors.v from software foundations...multiple proofs around Mdomain are really giving me trouble. Anyone have any pointers. I've spent a lot of time trying a lot of dead ends -_- I understand why the solutiosn aren't made available, but could someone perhaps share the solutions to just this module? I wouldn't distribute it more widely...

view this post on Zulip jco (Jun 17 2020 at 10:00):

The ever helpful Li-yao xia answered my stack overflow question https://stackoverflow.com/questions/62407248/looking-for-some-help-on-the-sin-domain-proof-from-software-foundations-color-v, but it hasn't quite got me going in the right direction. Every direction I take requires me to be able to split Mdomain in someway...I've tried stuff in that vein, but my proofs end up in dead ends. Thus I'm here...

view this post on Zulip jco (Jun 17 2020 at 10:01):

(if there's a better place for this sort of thing lpease let me know. self studying this stuff can be a lonely endeavor :( but this is the hardest wall I've hit in the first 3 modules...)

view this post on Zulip jco (Jun 17 2020 at 10:05):

I'm able to massage things so I have S.In n (Mdomain g), but if I directly apply fold_rec_bis or fold_rec_nodep, I have to prove S.In n S.empty, which of course is not true. I'm trying to figure out if there is a way to sort of "expand" the fold so that there is something other than empty...but all such avenues have failed. I think the key is that I don't know what ot od with the hypothesis value, since I don't really have anything I can do with things of the shape Mdomain (M.Node g1 o g2)

view this post on Zulip Kenji Maillard (Jun 17 2020 at 10:37):

Hi @jco, welcome to the Coq zulip! I don't think this is a bad place to ask such questions.
Can you explain to which predicate P you try to apply the induction principle fold_rec_bis that Li-yao pointed you to ?

view this post on Zulip jco (Jun 17 2020 at 10:42):

Thank you for your response, Kenji. Sure!

Proof.
split.
generalize dependent g.
induction n; intros.
-
destruct g.
inversion H.
(* at this point, the target has nothing foldable. *)
unfold M.In.
apply IHn.
(* now we have a fold *)
unfold Mdomain.
apply WP.fold_rec_bis.
intros.
assumption.
(* wants me to prove S.In n S.empty!)

view this post on Zulip jco (Jun 17 2020 at 10:43):

I have the following hypothesis which is sort of the issue I think, I have no clue how to reduce it:
S.In (n~1)%positive (Mdomain (M.Node g1 o g2))

view this post on Zulip jco (Jun 17 2020 at 10:43):

I have tried reduce it to the fold, but it's unclear how WP.fold_rec_bis can apply to the hypothesis in this way

view this post on Zulip jco (Jun 17 2020 at 10:45):

I've tried a lot of incantations, this is just one...but the fundamental issue has been that I don't really have anything I can do with the Mdomain (M.Node g1 o g2) in the hypothesis. I've tried unfolding the fold in all different ways, but couldn't really recover anything useful from it

view this post on Zulip jco (Jun 17 2020 at 10:48):

It's entirely possible that I'm tackling the induction incorrectly, I've tried some other things but this is the one that led me the furthest because at least I could use the induction hypothesis. bu tI haven't figured out how to "reduce" the head. it seems like it should be possible to break it doewn into a clear fold of g1 o and g2 and I've tried some incantations, but then was unable to connect it back to the inductive hypothesis

view this post on Zulip Kenji Maillard (Jun 17 2020 at 10:50):

I have the impression that the fold Li-Yao was referring to is the one underlying Mdomain: from the original goal, if you just intros A n g and unfold Mdomain you should get something like S.In n (M.fold (fun n _ s ⇒ S.add n s) g S.empty) ↔ M.In n g to which you might be able to apply WP.fold_rec_bis directly (Edit: you might need to generalize n).

view this post on Zulip jco (Jun 17 2020 at 10:53):

ah...trying this out it already looks more promising. SIGH

view this post on Zulip jco (Jun 17 2020 at 10:53):

I will explore it, but I think you are right that this is the right avenue

view this post on Zulip jco (Jun 17 2020 at 10:54):

thank you so so much, I've hit my head on these Mdomain proofs for like..10 hours -__-

view this post on Zulip jco (Jun 17 2020 at 11:15):

I just proved it!!! thank you!

view this post on Zulip jco (Jun 17 2020 at 11:16):

hopefully one day I will get better at this stuff!

view this post on Zulip Kenji Maillard (Jun 17 2020 at 11:19):

Great ! It's easy to get lost on technical details in a proof because "it looks obvious".

view this post on Zulip Li-yao (Jun 17 2020 at 16:00):

@jco Fun fact: that solution using that lemma is twice shorter than the current solution (non-available publicly, sadly), that Appel was complaining about in that comment.

view this post on Zulip jco (Jun 17 2020 at 16:17):

hah! yeah it's really sad that the solutions aren't available...I understand why, but it'd be so instructive! who cares if some cheating undergrads want to shoot their own knowledge in the foot, I say :P


Last updated: Feb 09 2023 at 00:03 UTC