achlipala/frap

Insufficient tactic of `model_check_done` in FrapWithoutSets.v.

Closed this issue · 3 comments

foreverbell commented

Hi, I am trying to solve pset5 (producer-consumer formal verification) of 6.887 with transition system abstraction and model checking.

Looks like the tactic model_check_done in FrapWithoutSets.v is insufficient to directly prove the abstracted transition system via model_check_infer.

I make some hacks to change the tactic

 Ltac model_check_done :=
    apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].

into

 Ltac model_check_done :=
    apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; apply sets_equal; simplify; propositional ].

And then model_check_infer could just work.

My Coq (8.6) code for pset5 is here (deleted to avoid cheater). It takes about 1 minute to execute. You can just focus on L210 to L213. If I use the above hacks, L211 to L213 can be omitted.

As I am a really Coq novice, I don't understand some details of your Coq Ltac magic, can you figure out more details to check if it is a bug? Thanks.

achlipala commented

Thanks for your interest in the book! First, to avoid creating a resource for students to cheat on this assignment in the future, could you please remove this solution and any others for our exercises from publicly accessible URLs? I've already saved your file for my own reference.

foreverbell commented

Aha, done.

achlipala commented

Thanks. I just pushed a different small change that also fixes your problem, based on what I thought was the more fundamental issue with the FRAP tactics.