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.

Local Open Scope logic_base.
Local Open Scope syntax.

Section Sound.

Context {L: Language}
        {minL: MinimunLanguage L}
        {MD: Model}
        {SM: Semantics L MD}
        {tminSM: TrivialMinimunSemantics L MD SM}.

Lemma sound_modus_ponens:
  forall x y m,
    m |= (x --> y) -> m |= x -> m |= y.
Proof.
(* Goal: forall (x y z : @expr L) (m : @model MD), @satisfies L MD SM m (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  intros.
(* Goal: @satisfies L MD SM m y *)
  rewrite sat_impp in H.
(* Goal: @satisfies L MD SM m y *)
  apply H; auto.
Qed.

Lemma sound_axiom1:
  forall x y m,
    m |= x --> y --> x.
Proof.
(* Goal: forall (x y z : @expr L) (m : @model MD), @satisfies L MD SM m (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  rewrite !sat_impp.
(* Goal: forall (_ : @satisfies L MD SM m x) (_ : @satisfies L MD SM m y), @satisfies L MD SM m x *)
  intros ? ?; auto.
Qed.

Lemma sound_axiom2:
  forall x y z m,
    m |= (x --> y --> z) --> (x --> y) --> (x --> z).
Proof.
(* Goal: forall (x y z : @expr L) (m : @model MD), @satisfies L MD SM m (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  intros.
(* Goal: @satisfies L MD SM m (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  rewrite !sat_impp.
(* Goal: forall (_ : forall (_ : @satisfies L MD SM m x) (_ : @satisfies L MD SM m y), @satisfies L MD SM m z) (_ : forall _ : @satisfies L MD SM m x, @satisfies L MD SM m y) (_ : @satisfies L MD SM m x), @satisfies L MD SM m z *)
  intros ? ? ?.
(* Goal: @satisfies L MD SM m z *)
  specialize (H H1).
(* Goal: @satisfies L MD SM m z *)
  specialize (H0 H1).
(* Goal: @satisfies L MD SM m z *)
  auto.
Qed.

End Sound.
