Require Import Coq.Logic.Classical_Prop.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.Semantics.Trivial.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.Semantics.Trivial.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.

Section Sound.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {MD: Model}
        {SM: Semantics L MD}
        {tminSM: TrivialMinimunSemantics L MD SM}
        {tpSM: TrivialPropositionalSemantics L MD SM}.

Lemma sound_andp_intros:
  forall x y m,
    m |= x --> y --> x && y.
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@andp L pL x y) y) *)
  rewrite !sat_impp, sat_andp.
(* Goal: forall (_ : @satisfies L MD SM m x) (_ : @satisfies L MD SM m y), and (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  simpl; intros ? ?.
(* Goal: forall _ : @satisfies L MD SM m y, or (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  auto.
Qed.

Lemma sound_andp_elim1:
  forall x y m,
    m |= x && y --> x.
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@andp L pL x y) y) *)
  rewrite !sat_impp, sat_andp.
(* Goal: forall _ : and (@satisfies L MD SM m x) (@satisfies L MD SM m y), @satisfies L MD SM m y *)
  intros [? ?].
(* Goal: forall _ : @satisfies L MD SM m y, or (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  auto.
Qed.

Lemma sound_andp_elim2:
  forall x y m,
    m |= x && y --> y.
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@andp L pL x y) y) *)
  rewrite !sat_impp, sat_andp.
(* Goal: forall _ : and (@satisfies L MD SM m x) (@satisfies L MD SM m y), @satisfies L MD SM m y *)
  intros [? ?].
(* Goal: forall _ : @satisfies L MD SM m y, or (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  auto.
Qed.

Lemma sound_orp_intros1:
  forall x y m,
    m |= x --> x || y.
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@impp L minL x z) (@impp L minL (@impp L minL y z) (@impp L minL (@orp L pL x y) z))) *)
  rewrite !sat_impp, sat_orp.
(* Goal: forall _ : @satisfies L MD SM m y, or (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  auto.
Qed.

Lemma sound_orp_intros2:
  forall x y m,
      m |= y --> x || y.
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@impp L minL x z) (@impp L minL (@impp L minL y z) (@impp L minL (@orp L pL x y) z))) *)
  rewrite !sat_impp, sat_orp.
(* Goal: forall _ : @satisfies L MD SM m y, or (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  auto.
Qed.

Lemma sound_orp_elim:
  forall x y z m,
    m |= (x --> z) --> (y --> z) --> (x || y --> z).
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@impp L minL x z) (@impp L minL (@impp L minL y z) (@impp L minL (@orp L pL x y) z))) *)
  rewrite !sat_impp, sat_orp.
(* Goal: forall _ : @satisfies L MD SM m y, or (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  tauto.
Qed.

Lemma sound_falsep_elim:
  forall x m,
    m |= FF --> x.
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@falsep L pL) x) *)
  rewrite sat_impp, sat_falsep.
(* Goal: forall _ : False, @satisfies L MD SM m x *)
  intros [].
Qed.

Lemma sound_excluded_middle:
  forall x m,
    m |= x || (x --> FF).
Proof.
(* Goal: forall (x : @expr L) (m : @model MD), @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  intros.
(* Goal: @satisfies L MD SM m (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  rewrite sat_orp, sat_impp, sat_falsep.
(* Goal: forall _ : @satisfies L MD SM m y, or (@satisfies L MD SM m x) (@satisfies L MD SM m y) *)
  tauto.
Qed.

End Sound.
