Library OSQAcceptProof

Require Import ucert.
Require Import OSQAcceptPure.
Require Import lab.


Ltac sep_lift_absdata H :=
  match type of H with
    | _ |= ?P =>
      match find_aop P with
        | none _ =>
          idtac 1 "no absop in the pre-condition"; fail 1
        | some ?a =>
          match find_absdata P absecblsid with
            | none _ =>
              idtac 2 "no HECBList in the pre-condition";
                fail 2
            | some ?b =>
              match find_absdata P abstcblsid with
                | none _ =>
                  idtac 3 "no HTCBList in the pre-condition"; fail 3
                | some ?c =>
                  match find_absdata P ostmid with
                    | none _ =>
                      idtac 4 "no HTime in the pre-condition"; fail 4
                    | some ?e =>
                      match find_absdata P curtid with
                        | none _ =>
                          idtac 5 "no HCurTCB in the pre-condition"; fail 5
                        | some ?f =>
                              sep lifts (a::b::c::e::f::nil) in H
                          end
                      end
              end
          end
      end
  end.

Ltac find_aisris´ Hp :=
  match Hp with
    | ?A ** ?B =>
      match find_aisris´ A with
        | some ?a => constr:(some a)
        | none ?a =>
          match find_aisris´ B with
            | some ?b => constr:(some (a + b)%nat)
            | none ?b => constr:(none (a + b)%nat)
          end
      end
    | A_isr_is_prop => constr:(some 1%nat)
    | _ => constr:(none 1%nat)
  end.

Ltac find_aisris Hp := let y := find_aisris´ Hp in
                       eval compute in y.

Ltac isr_is_prop_elim´:=
  match goal with
    | H:?s |= ?P |- ?s |= _ =>
      match find_aisr P with
        | none => idtac
        | some ?a =>
          match find_ais P with
            | none => idtac
            | some ?b =>
              match find_aisris P with
                | none => idtac
                | some ?c => sep lifts (a::b::c::nil)%nat in H;eapply elim_a_isr_is_prop in H;exact H
              end
          end
      end
  end.

Ltac isr_is_prop_elim:=eapply backward_rule1;[intros;isr_is_prop_elim´ | ].

Ltac isr_is_prop_add´:=
  match goal with
    | H:?s |= ?P |- ?s |= _ =>
      match find_aisr P with
        | none => idtac
        | some ?a =>
          match find_ais P with
            | none => idtac
            | some ?b =>
              sep lifts (a::b::nil)%nat in H;eapply add_a_isr_is_prop in H;exact H
          end
      end
  end.

Ltac isr_is_prop_add:=eapply backward_rule1;[intros;isr_is_prop_add´ | ].

Ltac sep_lift_absdata´ H :=
  match type of H with
    | _ |= ?P =>
      match find_aop P with
        | none _ =>
          idtac 1 "no absop in the pre-condition"; fail 1
        | some ?a =>
          match find_absdata P absecblsid with
            | none _ =>
              idtac 2 "no HECBList in the pre-condition";
                fail 2
            | some ?b =>
              match find_absdata P abstcblsid with
                | none _ =>
                  idtac 3 "no HTCBList in the pre-condition"; fail 3
                | some ?c =>
                  match find_absdata P ostmid with
                    | none _ =>
                      idtac 4 "no HTime in the pre-condition"; fail 4
                    | some ?e =>
                      match find_absdata P curtid with
                        | none _ =>
                          idtac 5 "no HCurTCB in the pre-condition"; fail 5
                        | some ?f =>
                          sep lifts (a::b::c::e::f::nil) in H
                      end
                  end
              end
          end
      end
    end.

Open Scope code_scope.

Lemma OSQAccProof :
  forall vl p r,
    Some p =
    BuildPreA´ os_api OSQAccept
               (qacc, (Tptr Tvoid, Tptr os_ucos_h.OS_EVENT :: nil)) vl ->
    Some r =
    BuildRetA´ os_api OSQAccept
               (qacc, (Tptr Tvoid, Tptr os_ucos_h.OS_EVENT :: nil)) vl ->
    exists t d1 d2 s,
      os_api OSQAccept = Some (t, d1, d2, s) /\
      {|OSQ_spec , GetHPrio, I, r, Afalse|}|- {{p}}s {{Afalse}}.

Close Scope code_scope.