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}.

Context {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {sL: SeparationLanguage L} {SM: Semantics L MD} {R: Relation model} {po_R: PreOrder Krelation} {kiSM: KripkeIntuitionisticSemantics L MD (tt: @Kmodel MD (unit_kMD _)) SM} {kminSM: KripkeMinimunSemantics L MD (tt: @Kmodel MD (unit_kMD _)) SM} {kpSM: KripkePropositionalSemantics L MD (tt: @Kmodel MD (unit_kMD _)) SM}.

Lemma hoare_consequence_partial_sound: forall c P1 P2 Q1 Q2,
  valid (AllModel _) (P2 --> P1) ->
  valid (AllModel _) (Q1 --> Q2) ->
  triple_partial_valid P1 c Q1 ->
  triple_partial_valid P2 c Q2.
Proof.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: @triple_partial_valid L P MD BSS SM (@orp L pL P1 P2) c (@orp L pL Q1 Q2) *)
  unfold triple_partial_valid in *.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) P2) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  intros s ms ? ?.
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  specialize (H1 s ms).
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  specialize (H (KRIPKE: s) I).
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  rewrite sat_impp in H.
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  apply (H s) in H2; [| reflexivity].
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  specialize (H1 H2 H3); clear H2 H3.
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  destruct ms as [| | s']; auto.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s') Q2 *)
  specialize (H0 (KRIPKE: s') I).
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s') Q2 *)
  rewrite sat_impp in H0.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s') Q2 *)
  apply (H0 s'); auto.
(* Goal: @Krelation (@Kworlds MD (unit_kMD MD) tt) R s' s' *)
  reflexivity.
Qed.

Lemma hoare_consequence_total_sound: forall c P1 P2 Q1 Q2,
  valid (AllModel _) (P2 --> P1) ->
  valid (AllModel _) (Q1 --> Q2) ->
  triple_total_valid P1 c Q1 ->
  triple_total_valid P2 c Q2.
Proof.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: @triple_total_valid L P MD BSS SM (@orp L pL P1 P2) c (@orp L pL Q1 Q2) *)
  unfold triple_total_valid in *.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) P2) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  intros s ms ? ?.
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  specialize (H1 s ms).
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  specialize (H (KRIPKE: s) I).
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  rewrite sat_impp in H.
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  apply (H s) in H2; [| reflexivity].
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  specialize (H1 H2 H3); clear H2 H3.
(* Goal: match ms with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) Q2 end *)
  destruct ms as [| | s']; auto.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s') Q2 *)
  specialize (H0 (KRIPKE: s') I).
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s') Q2 *)
  rewrite sat_impp in H0.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s') Q2 *)
  apply (H0 s'); auto.
(* Goal: @Krelation (@Kworlds MD (unit_kMD MD) tt) R s' s' *)
  reflexivity.
Qed.

Lemma hoare_conjunction_partial_sound: forall c P1 P2 Q1 Q2,
    triple_partial_valid P1 c Q1 ->
    triple_partial_valid P2 c Q2 ->
    triple_partial_valid (P1 && P2) c (Q1 && Q2).
Proof.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: @triple_partial_valid L P MD BSS SM (@orp L pL P1 P2) c (@orp L pL Q1 Q2) *)
  unfold triple_partial_valid in *.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H0 s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => True | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@andp L pL Q1 Q2) end *)
  rewrite sat_andp in H1. destruct H1.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  apply H in H1; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@andp L pL Q1 Q2) end *)
  apply H0 in H3; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  destruct ms_post; auto.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt m) (@andp L pL Q1 Q2) *)
  apply sat_andp. split; assumption.
Qed.

Lemma hoare_conjuntion_total_sound: forall c P1 P2 Q1 Q2,
    triple_total_valid P1 c Q1 ->
    triple_total_valid P2 c Q2 ->
    triple_total_valid (P1 && P2) c (Q1 && Q2).
Proof.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: @triple_total_valid L P MD BSS SM (@orp L pL P1 P2) c (@orp L pL Q1 Q2) *)
  unfold triple_total_valid in *.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H0 s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  apply sat_andp in H1. destruct H1.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  apply H in H1; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@andp L pL Q1 Q2) end *)
  apply H0 in H3; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  destruct ms_post; auto.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt m) (@andp L pL Q1 Q2) *)
  apply sat_andp. split; assumption.
Qed.

Lemma hoare_disjunction_parial_sound: forall c P1 P2 Q1 Q2,
    triple_partial_valid P1 c Q1 ->
    triple_partial_valid P2 c Q2 ->
    triple_partial_valid (P1 || P2) c (Q1 || Q2).
Proof.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: @triple_partial_valid L P MD BSS SM (@orp L pL P1 P2) c (@orp L pL Q1 Q2) *)
  unfold triple_partial_valid in *.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H0 s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  rewrite sat_orp in H1. destruct H1.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  - apply H in H1; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
    destruct ms_post; auto.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt m) (@orp L pL Q1 Q2) *)
    apply sat_orp. left. assumption.
  - apply H0 in H1; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
    destruct ms_post; auto.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt m) (@orp L pL Q1 Q2) *)
    apply sat_orp. right. assumption.
Qed.

Lemma hoare_disjunction_total_sound: forall c P1 P2 Q1 Q2,
    triple_total_valid P1 c Q1 ->
    triple_total_valid P2 c Q2 ->
    triple_total_valid (P1 || P2) c (Q1 || Q2).
Proof.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: @triple_total_valid L P MD BSS SM (@orp L pL P1 P2) c (@orp L pL Q1 Q2) *)
  unfold triple_total_valid in *.
(* Goal: forall (s_pre : @model MD) (ms_post : MetaState (@model MD)) (_ : @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_pre) (@orp L pL P1 P2)) (_ : @access P (@model MD) BSS s_pre c ms_post), match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  intros.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  specialize (H0 s_pre ms_post).
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  rewrite sat_orp in H1. destruct H1.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
  - apply H in H1; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
    destruct ms_post; auto.
(* Goal: or (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m) Q1) (@satisfies L MD SM (@build_model MD (unit_kMD MD) tt m) Q2) *)
    rewrite sat_orp. left. assumption.
  - apply H0 in H1; auto.
(* Goal: match ms_post with | Error => False | NonTerminating => False | Terminating s_post => @satisfies L MD SM (@build_model MD (unit_kMD MD) tt s_post) (@orp L pL Q1 Q2) end *)
    destruct ms_post; auto.
(* Goal: @satisfies L MD SM (@build_model MD (unit_kMD MD) tt m) Q2 *)
    rewrite sat_orp. right. assumption.
Qed.

End soundness.
