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...
The ever helpful Liyao xia answered my stack overflow question https://stackoverflow.com/questions/62407248/lookingforsomehelponthesindomainprooffromsoftwarefoundationscolorv, 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...
(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...)
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)
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 Liyao pointed you to ?
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))
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
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
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
I have the impression that the fold LiYao 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
).
ah...trying this out it already looks more promising. SIGH
I will explore it, but I think you are right that this is the right avenue
thank you so so much, I've hit my head on these Mdomain proofs for like..10 hours __
I just proved it!!! thank you!
hopefully one day I will get better at this stuff!
Great ! It's easy to get lost on technical details in a proof because "it looks obvious".
@jco Fun fact: that solution using that lemma is twice shorter than the current solution (nonavailable publicly, sadly), that Appel was complaining about in that comment.
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