Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.Semantics.Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.Semantics.Kripke.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Semantics.FlatSemantics.
Require Import Logic.HoareLogic.ImperativeLanguage.
Require Import Logic.HoareLogic.ProgramState.
Require Import Logic.HoareLogic.BigStepSemantics.
Require Import Logic.HoareLogic.HoareTriple_BigStepSemantics.

Local Open Scope logic_base.
Local Open Scope syntax.
Local Open Scope kripke_model.
Import PropositionalLanguageNotation.
Import SeparationLogicNotation.
Import KripkeModelSingleNotation.
Import KripkeModelNotation_Intuitionistic.

Section soundness.

Existing Instance unit_kMD.

Context {P: ProgrammingLanguage}
        {MD: Model}
        {BSS: BigStepSemantics P model}
        {J: Join model}
        {R: Relation model}
        {po_R: PreOrder Krelation}
        {SA_BSS: SABigStepSemantics P model BSS}.

Context {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {SL: SeparationLanguage L} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD tt SM} {fsSM: FlatSemantics.SeparatingSemantics L MD tt SM}.

Lemma hoare_frame_partial_sound: forall c P Q F,
  triple_partial_valid P c Q ->
  triple_partial_valid (P * F) c (Q * F).
Proof.
(* Goal: forall (c : @cmd P) (P0 Q F : @expr L) (_ : @triple_total_valid L P MD BSS SM P0 c Q), @triple_total_valid L P MD BSS SM (@sepcon L SL P0 F) c (@sepcon L SL Q F) *)
  intros.
(* Goal: @triple_total_valid L P MD BSS SM (@sepcon L SL P0 F) c (@sepcon L SL Q F) *)
  unfold triple_partial_valid in *.
(* Goal: @triple_total_valid L P MD BSS SM (@sepcon L SL P0 F) c (@sepcon L SL Q F) *)
  intros m' _n' ? ?.
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  rewrite FlatSemantics.sat_sepcon in H0.
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  destruct H0 as [m [mf [? [? ?]]]].
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  assert (SAFE: safe m c) by exact (H m Error H2).
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  destruct (frame_property _ _ _ _ _ H0 H1) as [_n [nf [? [? ?]]]].
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  destruct _n' as [| | n'].
  + inversion H5; subst.
(* Goal: False *)
    revert H6; apply SAFE.
  + auto.
  + rewrite FlatSemantics.sat_sepcon.
(* Goal: @ex (@Kworlds MD (unit_kMD MD) tt) (fun m1 : @Kworlds MD (unit_kMD MD) tt => @ex (@Kworlds MD (unit_kMD MD) tt) (fun m2 : @Kworlds MD (unit_kMD MD) tt => and (@join (@Kworlds MD (unit_kMD MD) tt) J m1 m2 n') (and (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m1) Q) (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m2) F)))) *)
    inversion H5; subst.
(* Goal: False *)
    - exfalso; revert H6; apply SAFE.
    - rename x into n.
(* Goal: @ex (@Kworlds MD (unit_kMD MD) tt) (fun m1 : @Kworlds MD (unit_kMD MD) tt => @ex (@Kworlds MD (unit_kMD MD) tt) (fun m2 : @Kworlds MD (unit_kMD MD) tt => and (@join (@Kworlds MD (unit_kMD MD) tt) J m1 m2 n') (and (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m1) Q) (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m2) F)))) *)
      exists n, nf.
(* Goal: True *)
      split; [| split]; auto.
      * apply (H m _ H2 H6).
(* Goal: True *)
      * eapply sat_mono; eauto.
Qed.

Lemma hoare_frame_total_sound: forall c P Q F,
  triple_total_valid P c Q ->
  triple_total_valid (P * F) c (Q * F).
Proof.
(* Goal: forall (c : @cmd P) (P0 Q F : @expr L) (_ : @triple_total_valid L P MD BSS SM P0 c Q), @triple_total_valid L P MD BSS SM (@sepcon L SL P0 F) c (@sepcon L SL Q F) *)
  intros.
(* Goal: @triple_total_valid L P MD BSS SM (@sepcon L SL P0 F) c (@sepcon L SL Q F) *)
  unfold triple_partial_valid in *.
(* Goal: @triple_total_valid L P MD BSS SM (@sepcon L SL P0 F) c (@sepcon L SL Q F) *)
  intros m' _n' ? ?.
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  rewrite FlatSemantics.sat_sepcon in H0.
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  destruct H0 as [m [mf [? [? ?]]]].
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  assert (SAFE: safe m c) by exact (H m Error H2).
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  assert (TERM: term_norm m c) by exact (conj (H m Error H2) (H m NonTerminating H2)).
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  destruct (frame_property _ _ _ _ _ H0 H1) as [_n [nf [? [? ?]]]].
(* Goal: match _n' with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@sepcon L SL Q F) end *)
  destruct _n' as [| | n'].
  + inversion H5; subst.
(* Goal: False *)
    revert H6; apply SAFE.
  + inversion H5; subst.
(* Goal: False *)
    - revert H6; apply SAFE.
    - revert H6; apply TERM.
  + rewrite FlatSemantics.sat_sepcon.
(* Goal: @ex (@Kworlds MD (unit_kMD MD) tt) (fun m1 : @Kworlds MD (unit_kMD MD) tt => @ex (@Kworlds MD (unit_kMD MD) tt) (fun m2 : @Kworlds MD (unit_kMD MD) tt => and (@join (@Kworlds MD (unit_kMD MD) tt) J m1 m2 n') (and (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m1) Q) (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m2) F)))) *)
    inversion H5; subst.
(* Goal: False *)
    - exfalso; revert H6; apply SAFE.
    - rename x into n.
(* Goal: @ex (@Kworlds MD (unit_kMD MD) tt) (fun m1 : @Kworlds MD (unit_kMD MD) tt => @ex (@Kworlds MD (unit_kMD MD) tt) (fun m2 : @Kworlds MD (unit_kMD MD) tt => and (@join (@Kworlds MD (unit_kMD MD) tt) J m1 m2 n') (and (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m1) Q) (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m2) F)))) *)
      exists n, nf.
(* Goal: True *)
      split; [| split]; auto.
      * apply (H m _ H2 H6).
(* Goal: True *)
      * eapply sat_mono; eauto.
Qed.

End soundness.
