Library OSMutexPostPart2

Require Import ucert.
Require Import ucert.
Require Import os_code_defs.
Require Import mathlib.
Require Import OSMutex_common.
Require Import lab.
Require Import gen_lemmas.
Open Scope code_scope.

Theorem MutexPostPart1: gen_MutexPostPart1.
    Ltac mew2 := match goal with
                   | |- (if _ then true else false) = true => rewrite ifE
                   | |- (_ <=? _ = true) => apply Zle_imp_le_bool
                   | |- (_ <= _ ) => apply Zle_bool_imp_le
                 end.
    Require Import hoare_assign.
Require Import aux_for_hoare_lemmas.
Ltac hoare_assign_array´ :=
  let s := fresh in
  let H := fresh in
  match goal with
    | |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (earrayelem (evar ?x) _) _) {{ _ }} =>
      match find_lvararray P x with
        | some ?m =>
          match find_aop P with
            | none _ => fail 1
            | some ?n =>
              hoare lifts (n::m::nil)%list pre;
                eapply assign_rule_array_aop;
                [ intro s; split; intro H; exact H
                | symbolic execution
                | symbolic execution
                | intuition auto
                | idtac
                | apply assign_type_match_true; simpl; auto
                | idtac ]
          end
        | none _ =>
          match find_dom_lenv P with
            | (none _, _) => fail 2
            | (some ?m, Some ?ls) =>
              let ret1 := constr:(var_notin_dom x ls) in
              let ret2 := (eval compute in ret1) in
              match ret2 with
                | true =>
                  match find_aop P with
                    | none _ => fail 1
                    | some ?n =>
                      match find_gvararray P x with
                        | none _ => fail 3
                        | some ?o =>
                          hoare lifts (n::m::o::nil)%list pre;
                            eapply assign_rule_array_g_aop;
                            [ intro s; split; intro H; exact H
                            | simpl; auto
                            | symbolic execution
                            | symbolic execution
                            | intuition auto
                            | idtac
                            | apply assign_type_match_true; simpl; auto
                            | idtac ]
                      end
                  end
                | false => fail
              end
          end
      end
    | |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (earrayelem _ _) _) {{ _ }} =>
      eapply assign_rule_ptr_array_aop;
        [ symbolic execution;try solve [eauto | simpl;eauto]
        | intro s;split;intro H;
          [
            match goal with
              | H´ : ?s |= ?P |- ?s |= Aarray ?l _ _ ** _ =>
                 match find_ptrarray P l with
                   | (some ?n) => sep lift n in H´; try exact H´
                   | _ => fail 4
                 end
            end
          | match goal with
              | H´: ?s |= Aarray ?l _ _ ** _ |- ?s |= ?P =>
                match find_ptrarray P l with
                  | (some ?n) => sep lift n ; try exact H´
                  | _ => fail 4
                end
            end
          ]
        | symbolic execution
        | symbolic execution
        | intuition auto
        | intuition auto
        | simpl
        | simpl;auto
        | simpl
        ]
  end.
    Require Import OSMutexPostPart3.
    Require Import OSMutexPostPart2_0.