Library hoare_lemmas

Require Import Coq.Bool.IfProp.
Require Import Coq.Logic.Classical_Prop.
Require Import Recdef.
Require Import Coq.Init.Wf.
Require Import Coq.Arith.Wf_nat.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import inferules.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import memdata.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import hoare_conseq.
Require Import Integers.
Require Import baseTac.
Require Import LibTactics.
Require Import val.
Require Import derivedrules.
Require Import BaseAsrtDef.
Require Import simulation.
Require Import aux_for_hoare_lemmas.
Set Implicit Arguments.

Lemma sep_aconj_r_aistrue_to_astar :
  forall P e t v,
    P ==> Rv e @ t == v ->
    P //\\ Aistrue e ==> P ** [| v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef |].

Lemma sep_aconj_r_aisfalse_to_astar :
  forall P e t v,
    P ==> Rv e @ t == v ->
    P //\\ Aisfalse e ==> P ** [| v = Vint32 Int.zero \/ v = Vnull |].

Theorem aisfalse_prop_ptr :
  forall s P e v,
    s |= P ->
    s |= Aisfalse e ->
    (P ==> Rv e @ Tnull== v) ->
    s |= [| v= Vnull |] ** P.

Theorem if_rule´ :
  forall Spec I r ri p q1 q2 e tp s1 s2 sc,
    {| Spec, sc, I, r, ri |}|- {{ p //\\ Aistrue e }} s1 {{ q1 }} ->
                           {| Spec, sc, I, r, ri |}|- {{ p //\\ Aisfalse e }} s2 {{ q2 }} ->
                                                  p ==> EX v : val, Rv e @ tp == v ->
                                                                    {| Spec, sc, I, r, ri |}|- {{ p }} sif e s1 s2 {{ q1 \\// q2 }}.

Theorem while_rule´ :
  forall Spec I r ri p q e s tp sc,
    {| Spec, sc, I, r, ri |}|- {{ p //\\ Aistrue e }} s {{ p }} ->
                           p ==> EX v : val, Rv e @ tp == v ->
                                             p //\\ Aisfalse e ==> q ->
                                             {| Spec, sc, I, r, ri |}|-{{ p }} swhile e s {{ q }}.

Theorem if_rule2 :
  forall Spec I r ri p q1 q2 e tp s1 s2 v sc,
    p ==> Rv e @ tp == v ->
    {| Spec, sc, I, r, ri |}|- {{ p ** [| v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef |] }} s1 {{ q1 }} ->
                          {| Spec, sc, I, r, ri |}|- {{ p ** [| v = Vint32 Int.zero \/ v = Vnull |] }} s2 {{ q2 }} ->
                                                {| Spec, sc, I, r, ri |}|- {{ p }} sif e s1 s2 {{ q1 \\// q2 }}.

Theorem if_rule2´ :
  forall Spec I r ri p q1 q2 e tp s1 s2 v sc,
    p ==> Rv e @ tp == v ->
    {| Spec, sc, I, r, ri |}|- {{ p ** [| v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef |] }} s1 {{ q1 }} ->
                          {| Spec, sc, I, r, ri |}|- {{ p ** [| v = Vint32 Int.zero \/ v = Vnull |] }} s2 {{ q2 }} ->
                                                {| Spec, sc, I, r, ri |}|- {{ p }} sif e s1 s2 {{ q1 ** [| v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef |] \\// q2 ** [| v = Vint32 Int.zero \/ v = Vnull |] }}.

Theorem aconj_aisture_rule :
  forall Spec I r ri s P e t v Q sc,
    P ==> Rv e @ t == v ->
    {| Spec, sc, I, r, ri |}|- {{ P ** [| v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef |] }} s {{ Q }} ->
                          {| Spec, sc, I, r, ri |}|- {{ P //\\ Aistrue e }} s {{ Q }}.

Theorem aconj_aisfalse_rule :
  forall Spec I r ri s P e t v Q sc,
    P ==> Rv e @ t == v ->
    {| Spec, sc, I, r, ri |}|- {{ P ** [| v = Vint32 Int.zero \/ v = Vnull |] }} s {{ Q }} ->
                          {| Spec, sc, I, r, ri |}|-{{ P //\\ Aisfalse e }} s {{ Q }}.

Theorem list_reverse_prop1 :
  forall (t:Type) (a:t) l1 l2,
    (List.rev (a::l1) ++ l2)%list = (List.rev l1 ++ a::l2)%list.

Theorem list_reverse_prop2 :
  forall (t:Type) (l1 l2:list t),
    List.rev l1 = l2 -> l1 = List.rev l2.

Theorem pair_prop :
  forall {A B:Type} (x:A * B),
    (fst x, snd x) = x.

Hint Rewrite (@pair_prop block int) (@pair_prop int (list val)) List.app_nil_r List.rev_involutive List.rev_app_distr list_reverse_prop1 List.app_assoc_reverse : listprop.


Theorem Alvarenv_cancel :
  forall x t v1 v2 P Q,
    P ==> Q ->
    v1 = v2 ->
    L& x @ t == v1 ** P ==> L& x @ t == v2 ** Q.

Theorem Agvarenv_cancel :
  forall x t v1 v2 P Q,
    P ==> Q ->
    v1 = v2 ->
    G& x @ t == v1 ** P ==> G& x @ t == v2 ** Q.

Theorem Aptrmapsto_cancel :
  forall l t v1 v2 P Q,
    P ==> Q ->
    v1 = v2 ->
    PV l @ t |-> v1 ** P ==> PV l @ t |-> v2 ** Q.