Library OSMutexAcceptProof

Require Import ucert.
Require Import OSMutex_common.
Open Scope code_scope.

Theorem OSMutexAccepteRight:
  forall vl p r,
    Some p = BuildPreA´ os_api OSMutexAccept mutexaccapi vl ->
    Some r = BuildRetA´ os_api OSMutexAccept mutexaccapi vl ->
    exists t d1 d2 s,
      os_api OSMutexAccept = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.
  Require Import mathlib.
  Ltac if_invert := let HH := fresh in
                    match goal with
                      | |- (if ?e then true else false) = false => cut (e = false); [intro HH; rewrite HH; reflexivity| idtac]
                      | |- (if ?e then true else false) = true => cut (e = true); [intro HH; rewrite HH; reflexivity| idtac]
                    end.