Replace `MGuard` with `MFail`
This MR implements MFail as described in #171. This replaces mguard with guard : P → {Decision P} → M P using mfail. As such I've replaced guard P; mx with _ ← guard P; mx in all lemmas. This MR further more replaces case_option_guard with a more general case_guard.
These changes are very much breaking changes.
Merge request reports
Activity
Resolved by Robbert KrebbersReplace
MFailwithMGuardDoesn't this do the opposite, replace
MGuardwithMFail?- Last reply by Adam
- Resolved by Robbert Krebbers
There is already a special notation for
_ ← guard P; Mwhich isguard P;; M. Maybe this MR should use it, it feels less cluttered. Sorry for the nitpickingEdited by Thibaut Pérami - Last reply by Adam
In my development I have a typeclass
MRaiseto raise an error with a specific value:Class MRaise (E : Type) (M : Type → Type) := mraise : ∀ {A}, E → M A. Global Arguments mraise {_ _ _ _} _ : assert. Global Instance: Params (@mraise) 4 := {}. Global Hint Mode MRaise ! ! : typeclass_instances.Then I define
mfailas raising unit:Definition mfail `{MRaise () M} {A} : M A := mraise ().I was about to propose that.
It is an interesting design decision whether we want to do that or we want to keep
MRaiseandMFailas two separate typeclasses. But I think both options should be considered.Edited by Thibaut PéramiForgot to ping: so @tperami @adamAndMath, what is your opinion about postponing this change?
I sadly probably won't be available to submit a
MRaiseMR for next 3 weeks. If you can wait until then, then we can take the decision between having justMRaise(and thusmfail = mraise ()), or having bothMRaiseandMFail. On the other hand if we decide we want both, then this MR and theMRaiseMR are totally independent and this can go ahead nowIf @adamAndMath does not mind, let's wait 3 weeks then.
It's in MR #501
Edited by Thibaut Pérami
941 941 End fin_to_set. 942 942 943 943 (** * Guard *) 944 Global Instance set_guard `{MonadSet M} : MGuard M := 945 λ P dec A x, match dec with left H => x H | _ => ∅ end. 944 Global Instance set_mfail `{MonadSet M} : MFail M := λ _, ∅. 946 945 947 946 Section set_monad_base. 948 947 Context `{MonadSet M}. 949 948 950 949 Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) : 951 (x ∈ guard P; X) ↔ P ∧ x ∈ X. 950 x ∈ (guard P;; X) ↔ P ∧ x ∈ X. I am not sure what you want the lemma to state, because
x ∈ guard P ↔ decide P = left x. To avoid talking about equality of proofs we'd need either proof irrelevance or, to forget the proof using either fmap or mbind. This is the main reason I've kept the binds. Could you clarify what you want the lemma to state?
411 destruct_decide (@decide P dec) as Hx 412 end. 413 Tactic Notation "case_option_guard" := 414 let H := fresh in case_option_guard as H. 415 400 416 401 Lemma option_guard_True {A} P `{Decision P} (mx : option A) : 417 P → mguard P (λ _, mx) = mx. 418 Proof. intros. by case_option_guard. Qed. 419 Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A) 420 (HP : P) : 421 mguard P f = f HP. 422 Proof. intros. case_option_guard; [|done]. f_equal; apply proof_irrel. Qed. 423 Lemma option_guard_False {A} P `{Decision P} (f : P → option A) : 424 ¬P → mguard P f = None. 425 Proof. intros. by case_option_guard. Qed. 402 P → (guard P;; mx) = mx. added 2 commits
401 (** * Tactics *) 402 Tactic Notation "case_option_guard" "as" ident(Hx) := 403 match goal with 404 | H : context C [@mguard option _ ?P ?dec] |- _ => 405 change (@mguard option _ P dec) with (λ A (f : P → option A), 406 match @decide P dec with left H' => f H' | _ => None end) in *; 407 destruct_decide (@decide P dec) as Hx 408 | |- context C [@mguard option _ ?P ?dec] => 409 change (@mguard option _ P dec) with (λ A (f : P → option A), 410 match @decide P dec with left H' => f H' | _ => None end) in *; 411 destruct_decide (@decide P dec) as Hx 412 end. 413 Tactic Notation "case_option_guard" := 414 let H := fresh in case_option_guard as H. 415 400 (** 391 (** 392 This lemma includes a bind, to avoid equalities of proofs. 393 A direct proof that `guard P = Some p` would require `decide P = left p`. 394 *) 391 (** This lemma includes a bind, to avoid equalities of proofs. We cannot have 392 [guard P = Some p ↔ P] unless [P] is proof irrelant. The best (but less usable) 393 self-contained alternative would be [guard P = Some p ↔ decide P = left p]. *) How about this?
changed this line in version 5 of the diff
mentioned in merge request !501 (closed)
mentioned in merge request adamAndMath/stdpp!1 (merged)
added 2 commits
mentioned in merge request !522 (merged)
This can be closed as it is being superseded by !522 (merged)
Edited by Thibaut Pérami
