jco (Jun 17 2020 at 09:59): 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...
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...
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...)
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)
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 ?
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!)
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))
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
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
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
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).
jco (Jun 17 2020 at 10:53):ah...trying this out it already looks more promising. SIGH
jco (Jun 17 2020 at 10:53):I will explore it, but I think you are right that this is the right avenue
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 -__-
jco (Jun 17 2020 at 11:15):I just proved it!!! thank you!
jco (Jun 17 2020 at 11:16):hopefully one day I will get better at this stuff!
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".
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.
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: Apr 19 2024 at 16:01 UTC