option.v: Add option_guard_decide and option_guard_bool_decide

LGTM.

merged

mentioned in commit e0657da4

Thanks! However I still think we should adjust lookup_gset_to_gmap though, to keep users in the more widely-known parts of std++.

I don't have a strong preference. If you want to change it, we probably should use decide (not bool_decide) because it works with just destruct (for bool_decide you need case_bool_decide to get P and ¬ P) and do it consistently for similar map functions where mguard is used.

decide is harder to use though. bool_decide_True is an awfully useful lemma. In my experience one wants to use if bool_decide rather than if decide. I remember fighting with annoying occurrences of decide that I fixed by just using bool_decide instead.

I am not sure I understand your concern. Do you have a concrete example?

My example is: If you have if decide P then ... else ... in your goal, you can just do destruct (decide P) and get hypotheses H : P and H : ¬P. With if bool_decide P then ... else ... that does not work.

But what if decide P occurs in the goal and you already have a proof of P?

I guess you can use decide_True, but that was not possible when I had the problem (I forgot the context, but I guess it was not in an if). I remember reaching for decide_True_pi but then things were not actually PI and then I gave up and just changed everything to bool_decide. I have always used bool_decide since then and never regretted it. I don't see destruct as a big advantage given that we have case_bool_decide.

I guess you can use decide_True, but that was not possible when I had the problem

I am quite curious where that would happen.

You cannot use decide_True if you use the proof, i.e., use match decide P with left H => ..., but in that case bool_decide is not useful either since it gives no proof. Maybe you used decide P in Program which then implicitly made use of the proof?

Maybe you used decide P in Program which then implicitly made use of the proof?

Sadly I didn't write a note, I guess I was in a rush and just had to Get It Done (TM).

I think it's easier: with ssreflect rewrite, rewrite decide_True basically never works. I've mentioned it in https://mattermost.mpi-sws.org/iris/pl/99cykea83jbq7ea3wkxzafntwo with a testcase:

From iris.prelude Require Import prelude.

Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
  Succeed by rewrite ->decide_True.
  Fail rewrite decide_True.
  (* uglier variants — see https://gist.github.com/Blaisorblade/898115dd0be901d4ba5ca79df0aa2ffa *)

and others have the same experience: https://mattermost.mpi-sws.org/iris/pl/bw767z8c7pgfufgjc6murgaxcc.

It is also the case that rewriting on booleans is intrinsically easier.

with ssreflect rewrite

Oh, that would explain why things work fine inside std++ but I had issues elsewhere. Opened an issue to track / discuss this further (a closed MR is where issues go to die): #168

option.v: Add option_guard_decide and option_guard_bool_decide

Merge request reports

Activity