Require Export Sequent.
Set Implicit Arguments.
Unset Strict Implicit.
Section LProperties.
Variable Atoms : Set.

Fixpoint addToEnd (Atoms : Set) (T1 T2 : Term Atoms) {struct T1} :
 Term Atoms :=
  match T1 with
  | OneForm f ⇒ Comma (OneForm f) T2
  | Comma L M ⇒ Comma L (addToEnd M T2)
  end.

Definition addToEndL :
  ∀ T1 T2 T3 : Term Atoms,
  addToEnd T1 (addToEnd T2 T3) = addToEnd (addToEnd T1 T2) T3.
 intros T1 T2 T3.
 elim T1.
 simpl in |- ×.
 auto.
 intros t H t0 H0.
 simpl in |- ×.
 rewrite H0.
 reflexivity.
Defined.

Definition addToEndCom :
  ∀ (T1 T2 : Term Atoms) (F : Form Atoms),
  addToEnd T1 T2 = OneForm F → False.
 intros T1 T2 F.
 elim T1.
 simpl in |- ×.
 intros f H.
 discriminate H.
 simpl in |- ×.
 intros t H t0 H0 H1.
 discriminate H1.
Defined.

Fixpoint convertTree (Atoms : Set) (T : Term Atoms) {struct T} :
 Term Atoms :=
  match T with
  | OneForm f ⇒ OneForm f
  | Comma T1 T2 ⇒ addToEnd (convertTree T1) (convertTree T2)
  end.

Definition replaceConvert :
  ∀ T1 T2 T3 T4 : Term Atoms,
  replace T1 T2 T3 T4 →
  convertTree T3 = convertTree T4 → convertTree T1 = convertTree T2.
 simple induction 1.
 auto.
 intros G1 G2 D F1 F2 r H0 H1.
 simpl in |- ×.
 elim (H0 H1).
 auto.
 intros G1 G2 D F1 F2 r H0 H1.
 simpl in |- ×.
 elim (H0 H1).
 auto.
Defined.

Inductive LGeneralization (Atoms : Set) : Term Atoms → Term Atoms → Set :=
  | sameTerm : ∀ T : Term Atoms, LGeneralization T T
  | termL :
      ∀ T1 T2 G1 G2 T' : Term Atoms,
      LGeneralization T1 T2 →
      L_Sequent G1 G2 → replace T2 T' G1 G2 → LGeneralization T1 T'.

Definition LGenTransitive :
  ∀ T1 T2 T3 : Term Atoms,
  LGeneralization T2 T3 → LGeneralization T1 T2 → LGeneralization T1 T3.
 simple induction 1.
 auto.
 intros T0 T4 G1 G2; intros.
 apply termL with T4 G1 G2; auto.
Defined.

Definition replaceSym :
  ∀ T1 T2 T3 T4 : Term Atoms, replace T1 T2 T3 T4 → replace T2 T1 T4 T3.
 simple induction 1.
 constructor 1.
 intros.
 apply replaceLeft; auto.
 intros.
 apply replaceRight; auto.
Defined.

Definition LSequenTSym :
  ∀ T1 T2 : Term Atoms, L_Sequent T1 T2 → L_Sequent T2 T1.
 simple induction 1.
 intros; constructor 2.
 intros; constructor 1.
Defined.

Definition LGenSymetrique :
  ∀ T1 T2 : Term Atoms, LGeneralization T1 T2 → LGeneralization T2 T1.
 simple induction 1.
 constructor 1.
 intros.
 eapply LGenTransitive.
 eauto.
 eapply termL.
 constructor 1.
 eapply LSequenTSym; eauto.
 apply replaceSym; assumption.
Defined.

Definition LGenMonoLeft :
  ∀ T1 T2 T : Term Atoms,
  LGeneralization T1 T2 → LGeneralization (Comma T T1) (Comma T T2).
 simple induction 1.
 constructor 1.
 intros.
 eapply termL.
 eauto.
 eauto.
 apply replaceRight; assumption.
Defined.

Definition LGenMonoRight :
  ∀ T1 T2 T : Term Atoms,
  LGeneralization T1 T2 → LGeneralization (Comma T1 T) (Comma T2 T).
 simple induction 1.
 constructor 1.
 intros.
 eapply termL.
 eauto.
 eauto.
 apply replaceLeft; assumption.
Defined.

Definition LGenMono :
  ∀ T1 T2 T3 T4 : Term Atoms,
  LGeneralization T1 T2 →
  LGeneralization T3 T4 → LGeneralization (Comma T1 T3) (Comma T2 T4).
 intros T1 T2 T3 T4; intros.
 apply LGenTransitive with (Comma T1 T4).
 apply LGenMonoRight; auto.
 apply LGenMonoLeft; auto.
Defined.

Definition LGenAddToEnd :
  ∀ T1 T2 : Term Atoms, LGeneralization (addToEnd T1 T2) (Comma T1 T2).

 intros T1 T2.
 elim T1.
 simpl in |- ×.
 constructor 1.
 intros t H t0 H0.
 simpl in |- ×.
 apply LGenTransitive with (Comma t (Comma t0 T2)).
 eapply termL; [ constructor 1 | idtac | constructor 1 ].
 constructor 1.
 apply LGenMonoLeft; auto.
Defined.

Definition LGenConvertT :
  ∀ T : Term Atoms, LGeneralization (convertTree T) T.
 intro T.
 elim T.
 simpl in |- ×.
 constructor 1.
 intros t H t0 H0.
 simpl in |- ×.
 apply LGenTransitive with (Comma (convertTree t) (convertTree t0)).
 apply LGenMono; auto.
 apply LGenAddToEnd.
Defined.

Definition eqFlattenTreeL :
  ∀ T1 T2 : Term Atoms,
  LGeneralization T1 T2 → convertTree T1 = convertTree T2.
 intros T1 T2 H.
 elim H.
 auto.
 intros T3 T4 G1 G2 T' l H0 l0 r.
 rewrite H0.
 eapply replaceConvert.
 eauto.
 elim l0.
 intros.
 simpl in |- ×.
 apply addToEndL.
 intros.
 simpl in |- ×.
 elim addToEndL.
 auto.
Defined.

Definition LgenEqFlattenTrees :
  ∀ T1 T2 : Term Atoms,
  convertTree T1 = convertTree T2 → LGeneralization T1 T2.
 intros T1 T2 H.
 eapply LGenTransitive.
 eapply LGenConvertT.
 rewrite <- H.
 apply LGenSymetrique.
 apply LGenConvertT.
Defined.

Section sequentsLogicL.
Require Export NaturalDeduction.

Definition LGenSequent :
  ∀ (T1 T2 : Term Atoms) (F : Form Atoms),
  LGeneralization T1 T2 →
  gentzenSequent L_Sequent T1 F → gentzenSequent L_Sequent T2 F.
 simple induction 1.
 auto.
 intros.
 eapply SequentExtension; eauto.
Defined.

Definition LNaturalDeduction :
  ∀ (T1 T2 : Term Atoms) (F : Form Atoms),
  LGeneralization T1 T2 →
  natDed L_Sequent T1 F → natDed L_Sequent T2 F.
simple induction 1.
 auto.
 intros.
 eapply NatExt; eauto.
Defined.

End sequentsLogicL.
End LProperties.