Set Implicit Arguments.
Unset Strict Implicit.

Section CTL_def.



 Inductive Form (Atoms : Set) : Set :=
   | At : Atoms -> Form Atoms
   | Slash : Form Atoms -> Form Atoms -> Form Atoms
   | Dot : Form Atoms -> Form Atoms -> Form Atoms
   | Backslash : Form Atoms -> Form Atoms -> Form Atoms.


 Definition arrow_extension :=
   forall Atoms : Set, Form Atoms -> Form Atoms -> Set.

 Definition add_extension (E1 E2 : arrow_extension) : arrow_extension :=
   fun At A B => (E1 At A B + E2 At A B)%type.

 Definition extends (X X' : arrow_extension) :=
   forall (At : Set) (A B : Form At), X At A B -> X' At A B.

 Definition no_extend : forall X : arrow_extension, extends X X.
  unfold extends in |- *; auto.
 Defined.

 Definition add_extend_l :
   forall X X' : arrow_extension, extends X (add_extension X X').
  intros; unfold add_extension, extends in |- *.
  left; auto.
 Qed.

 Definition add_extend_r :
   forall X X' : arrow_extension, extends X' (add_extension X X').
  intros; unfold add_extension, extends in |- *.
  right; auto.
 Qed.

 Definition extends_trans :
   forall X Y Z : arrow_extension, extends X Y -> extends Y Z -> extends X Z.
 intros X Y Z.
 unfold extends in |- *; auto.
 Defined.

Inductive NL (Atoms : Set) (A B : Form Atoms) : Set :=.

Inductive NLP (Atoms : Set) : Form Atoms -> Form Atoms -> Set :=
    Comm_intro : forall A B : Form Atoms, NLP (Dot A B) (Dot B A).

Inductive L (Atoms : Set) : Form Atoms -> Form Atoms -> Set :=
  | L_lr : forall A B C : Form Atoms, L (Dot A (Dot B C)) (Dot (Dot A B) C)
  | L_rl : forall A B C : Form Atoms, L (Dot (Dot A B) C) (Dot A (Dot B C)).

Definition LP : arrow_extension := add_extension NLP L.

Lemma NL_X : forall X : arrow_extension, extends NL X.
Proof.
  unfold extends in |- *; simple induction 1.
Qed.

Hint Resolve NL_X: ctl.

Lemma NLP_LP : extends NLP LP.
Proof.
 unfold extends, LP in |- *; left; assumption.
Qed.

Lemma L_LP : extends L LP.
Proof.
 unfold extends, LP in |- *; right; assumption.
Qed.

Variable Atoms : Set.

Section arrow_def.
 Variable X : arrow_extension.

 Inductive arrow (Atoms : Set) : Form Atoms -> Form Atoms -> Set :=
   | one : forall A : Form Atoms, arrow A A
   | comp : forall A B C : Form Atoms, arrow A B -> arrow B C -> arrow A C
   | beta :
       forall A B C : Form Atoms, arrow (Dot A B) C -> arrow A (Slash C B)
   | beta' :
       forall A B C : Form Atoms, arrow A (Slash C B) -> arrow (Dot A B) C
   | gamma :
       forall A B C : Form Atoms,
       arrow (Dot A B) C -> arrow B (Backslash A C)
   | gamma' :
       forall A B C : Form Atoms,
       arrow B (Backslash A C) -> arrow (Dot A B) C
   | arrow_plus : forall A B : Form Atoms, X A B -> arrow A B.

 Hint Resolve one comp beta gamma arrow_plus: ctl.


 Definition Dot_mono_right :
   forall A B B' : Form Atoms, arrow B' B -> arrow (Dot A B') (Dot A B).
  intros A B B' H.
  apply gamma'.
  apply comp with B.
  assumption.
  apply gamma.
  apply one.
 Defined.

 Definition Dot_mono_left :
   forall A B A' : Form Atoms, arrow A' A -> arrow (Dot A' B) (Dot A B).
  intros A B A' H.
  apply beta'.
  apply comp with A; auto.
  apply beta.
  apply one.
 Defined.

 Definition Dot_mono :
   forall A B C D : Form Atoms,
   arrow A C -> arrow B D -> arrow (Dot A B) (Dot C D).
 intros A B C D H H0.
 apply comp with (Dot C B).
 apply Dot_mono_left.
 assumption.
 apply Dot_mono_right; assumption.
Defined.

 Definition Slash_mono_left :
   forall C B C' : Form Atoms, arrow C' C -> arrow (Slash C' B) (Slash C B).
  intros C B C' H.
  apply beta.
  apply comp with C'.
  apply beta'.
  apply one.
  auto.
 Defined.

 Definition Slash_antimono_right :
   forall C B B' : Form Atoms, arrow B' B -> arrow (Slash C B) (Slash C B').
  intros C B B' H.
  apply beta; apply gamma'.
  apply comp with B.
  assumption.
  apply gamma.
  apply beta'.
  apply one.
 Defined.

 Definition Backslash_antimono_left :
   forall A C A' : Form Atoms,
   arrow A A' -> arrow (Backslash A' C) (Backslash A C).
  intros A C A' H.
  apply gamma.
  apply beta'.
  apply comp with A'.
  assumption.
  apply beta.
  apply gamma'.
  apply one.
 Defined.

 Definition Backslash_mono_right :
   forall A C C' : Form Atoms,
   arrow C' C -> arrow (Backslash A C') (Backslash A C).
  intros A C C' H.
  apply gamma.
  apply comp with C'.
  apply beta'.
  apply beta.
  apply gamma'.
  apply one.
  assumption.
 Defined.

End arrow_def.

Hint Resolve one comp beta gamma arrow_plus: ctl.

Definition mono_X :
  forall X X' : arrow_extension,
  extends X X' -> forall A B : Form Atoms, arrow X A B -> arrow X' A B.
 simple induction 2.
 apply one.
 intros.
 eapply comp.
 eauto.
 auto.
 intros.
 apply beta.
 assumption.
 intros.
 apply beta'.
 auto.
 intros.
 apply gamma.
 assumption.
 intros.
 apply gamma'; assumption.
 intros; constructor 7.
 auto.
Defined.

Section weaken.

 Inductive weak (A : Set) : Prop :=
     weak_intro : forall a : A, weak A.


  Lemma weak_one :
   forall (X : arrow_extension) (A : Form Atoms), weak (arrow X A A).
 Proof.
  intros; split.
  apply one.
 Qed.

 Hint Resolve weak_one: ctl.

 Lemma weak_comp :
  forall (X : arrow_extension) (A B C : Form Atoms),
  weak (arrow X A B) -> weak (arrow X B C) -> weak (arrow X A C).
 Proof.
  intros X A B C H H0.
  case H; case H0.
  split.
  apply comp with B; auto.
 Qed.

 Hint Resolve weak_comp: ctl.

 Lemma weak_beta :
  forall (X : arrow_extension) (A B C : Form Atoms),
  weak (arrow X (Dot A B) C) -> weak (arrow X A (Slash C B)).
 Proof.
  intros X A B C H.
  case H.
  split.
  apply beta; auto.
 Qed.

 Hint Resolve weak_beta: ctl.

 Lemma weak_beta' :
  forall (X : arrow_extension) (A B C : Form Atoms),
  weak (arrow X A (Slash C B)) -> weak (arrow X (Dot A B) C).
 Proof.
  intros X A B C H.
  case H.
  split.
  apply beta'; auto.
 Qed.

 Lemma weak_gamma :
  forall (X : arrow_extension) (A B C : Form Atoms),
  weak (arrow X (Dot A B) C) -> weak (arrow X B (Backslash A C)).
 Proof.
  intros X A B C H.
  case H.
  split.
  apply gamma; auto.
 Qed.

 Hint Resolve weak_gamma: ctl.

 Lemma weak_gamma' :
  forall (X : arrow_extension) (A B C : Form Atoms),
  weak (arrow X B (Backslash A C)) -> weak (arrow X (Dot A B) C).
 Proof.
  intros X A B C H.
  case H.
  split.
  apply gamma'; auto.
 Qed.

 Lemma weak_arrow_plus :
  forall (X : arrow_extension) (A B : Form Atoms),
  X _ A B -> weak (arrow X A B).
 Proof.
  split.
  apply arrow_plus; auto.
 Qed.

 Hint Resolve weak_gamma: ctl.

 Lemma weak_Dot_mono :
  forall (A B C D : Form Atoms) (X : arrow_extension),
  weak (arrow X A C) ->
  weak (arrow X B D) -> weak (arrow X (Dot A B) (Dot C D)).
 Proof.
 intros A B C D X H H0.
 case H.
 case H0.
 intros.
 split.
 apply Dot_mono; auto.
Qed.

 Lemma weak_Dot_mono_right :
  forall (X : arrow_extension) (A B B' : Form Atoms),
  weak (arrow X B' B) -> weak (arrow X (Dot A B') (Dot A B)).
 Proof.
  intros X A B B' H.
  case H.
  split.
  apply Dot_mono_right; auto.
 Qed.

 Lemma weak_Dot_mono_left :
  forall (X : arrow_extension) (A B A' : Form Atoms),
  weak (arrow X A' A) -> weak (arrow X (Dot A' B) (Dot A B)).
 Proof.
  intros X A B A' H.
  case H; split.
  apply Dot_mono_left; auto.
 Qed.

 Lemma weak_Slash_mono_left :
  forall (X : arrow_extension) (C B C' : Form Atoms),
  weak (arrow X C' C) -> weak (arrow X (Slash C' B) (Slash C B)).
 Proof.
  intros X C B C' H.
  case H; split.
  apply Slash_mono_left; auto.
 Qed.

 Lemma weak_Slash_antimono_right :
  forall (X : arrow_extension) (C B B' : Form Atoms),
  weak (arrow X B' B) -> weak (arrow X (Slash C B) (Slash C B')).
 Proof.
  intros X C B B' H.
  case H; split.
  apply Slash_antimono_right; auto.
 Qed.

 Lemma weak_Backslash_antimono_left :
  forall (X : arrow_extension) (A C A' : Form Atoms),
  weak (arrow X A A') -> weak (arrow X (Backslash A' C) (Backslash A C)).
 Proof.
  intros X A C A' H.
  case H; split.
  apply Backslash_antimono_left; auto.
 Qed.

 Lemma weak_Backslash_mono_right :
  forall (X : arrow_extension) (A C C' : Form Atoms),
  weak (arrow X C' C) -> weak (arrow X (Backslash A C') (Backslash A C)).
 Proof.
  intros X A C C' H.
  case H; split.
  apply Backslash_mono_right; auto.
 Qed.

End weaken.


 Definition pi :
   forall X : arrow_extension,
   extends NLP X -> forall A B : Form Atoms, arrow X (Dot A B) (Dot B A).
  intros X H A B.
  apply arrow_plus.
  apply H.
  split.
 Defined.

 Definition pi_NLP : forall A B : Form Atoms, arrow NLP (Dot A B) (Dot B A).
  apply pi.
  apply no_extend.
 Defined.

 Definition pi_LP : forall A B : Form Atoms, arrow LP (Dot A B) (Dot B A).
  apply pi.
  unfold LP in |- *.
  apply add_extend_l.
 Defined.

 Definition alpha :
   forall X : arrow_extension,
   extends L X ->
   forall A B C : Form Atoms, arrow X (Dot A (Dot B C)) (Dot (Dot A B) C).
  intros X H A B C.
  apply arrow_plus.
  apply H.
  left.
 Defined.

 Definition alpha_L :
   forall A B C : Form Atoms, arrow L (Dot A (Dot B C)) (Dot (Dot A B) C).
  apply alpha.
  apply no_extend.
 Defined.


 Definition alpha_LP :
   forall A B C : Form Atoms, arrow LP (Dot A (Dot B C)) (Dot (Dot A B) C).
  apply alpha.
  unfold LP in |- *; apply add_extend_r.
 Defined.

 Definition alpha' :
   forall X : arrow_extension,
   (forall A B : Form Atoms, L A B -> X _ A B) ->
   forall A B C : Form Atoms, arrow X (Dot (Dot A B) C) (Dot A (Dot B C)).
  intros X H A B C.
  apply arrow_plus.
  apply H.
  right.
 Defined.

 Definition alpha'_L :
   forall A B C : Form Atoms, arrow L (Dot (Dot A B) C) (Dot A (Dot B C)).
  apply alpha'.
  auto.
 Defined.


 Definition alpha'_LP :
   forall A B C : Form Atoms, arrow LP (Dot (Dot A B) C) (Dot A (Dot B C)).
  apply alpha'.
  unfold LP, add_extension in |- *; auto.
 Defined.

End CTL_def.

Implicit Arguments Dot [Atoms].
Implicit Arguments Slash [Atoms].
Implicit Arguments Backslash [Atoms].

Hint Resolve one comp beta gamma arrow_plus: ctl.

Hint Resolve weak_one weak_comp weak_beta weak_gamma: ctl.

Hint Resolve NL_X L_LP NLP_LP: ctl.