Require Import sc_term. 
Require Import sc_red.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Omega.

Open Scope SC_scope.


Fixpoint flat M l {struct M} := match M with
 | x ## h => x ## (h@l)
 | t · h  => t · (h@l)
 | _ => match l with 
   | [[]] => M
   | _   => M  · l
   end
end.


Reserved Notation " s  ⇒  t" (at level 80,  no associativity).
Reserved Notation " l  ⇒' g" (at level 80,  no associativity).

Inductive R_par : Term -> Term -> Prop :=
 | Sort_par : forall s, !s ⇒ !s
 | Bcons_par: forall A u u' v v' l l',  u ⇒ u' -> v ⇒ v' -> l ⇒' l' ->
      ((λ[A],u) · (v ::: l)) ⇒ ((u' [ ← v']) · l')
 | La_par : forall A A' u u',  A ⇒ A' -> u ⇒ u'->  (λ[A],u)  ⇒ (λ[A'],u')
 | Pi_par : forall A A' B B',  A ⇒ A' -> B ⇒ B'->  (Π(A),B)  ⇒ (Π(A'),B')
 | App_par : forall u u' l l', u ⇒ u' -> l ⇒' l' -> u · l ⇒ u' · l'
 | App2_par : forall x l l', l ⇒' l' -> x ## l ⇒ x ## l'
 | App3_par : forall u u' l l', u ⇒ u' -> l ⇒' l' -> u · l ⇒ (flat u' l')
where "s  ⇒ t" := (R_par s t) 
with R_par_list : Term_List -> Term_List -> Prop :=
  | R_list_nil : [[]] ⇒' [[]]
  | R_list_cons : forall t t' l l', t ⇒ t' -> l ⇒' l' -> t ::: l ⇒' t' ::: l'
where "l ⇒' g" := (R_par_list l g). 

Hint Constructors R_par R_par_list.

Scheme R_par_ind' := Induction for R_par Sort Prop
      with R_par_list_ind' := Induction for R_par_list Sort Prop.

Combined Scheme Rpar_ind' from R_par_ind',  R_par_list_ind'.


Lemma R_par_refl : (forall s , s ⇒ s) /\ ( forall l, l ⇒' l).
apply term_ind; intros; intuition.
Qed.

Hint Resolve (proj1 R_par_refl) (proj2 R_par_refl).

Lemma flat_nil : forall t, flat t [[]] = t.
induction t; simpl; intuition.
rewrite append_nil. trivial.
rewrite append_nil. trivial.
Qed.

Lemma R_par_nil : forall t t', t ⇒ t' -> t· [[]] ⇒ t'.
intros. replace t' with (flat t' [[]]).
constructor. trivial. trivial.
apply flat_nil.
Qed.

Lemma Rp_append : forall l1 l1' l2 l2', l1⇒' l1' -> l2 ⇒' l2' -> l1@l2 ⇒' l1'@l2'.
induction l1; simpl; intros.
inversion H; subst; clear H. simpl; trivial.
inversion H; subst; clear H.
simpl; intuition.
Qed.

Lemma flat_lift : forall t l n m, (flat t l) ↑ n # m  = flat (t↑ n # m) (l↑↑ n # m).
induction t; intros; simpl.
destruct le_gt_dec. simpl. rewrite append_lift; trivial.
rewrite append_lift; trivial.

destruct l; trivial.

rewrite append_lift; trivial.

destruct l; trivial.
destruct l; trivial.
Qed.

Theorem  Rp0_lift: forall a b , a ⇒ b -> forall n m, a ↑ n # m ⇒ b ↑ n # m
 with    Rp0_list_lift : forall l l' , l ⇒' l' -> forall n m , l ↑↑ n # m ⇒' l' ↑↑ n # m.
induction 1; intros.
constructor.
simpl.
destruct substP1. change m with (0+m). rewrite H2.
constructor. apply IHR_par1.  apply IHR_par2. intuition.

simpl; constructor. apply IHR_par1. apply IHR_par2.
simpl; constructor. apply IHR_par1. apply IHR_par2.
simpl; constructor. apply IHR_par. intuition.
simpl. destruct (le_gt_dec m x). constructor; intuition.
constructor; intuition.

rewrite flat_lift. simpl. intuition.

induction 1; intros.
constructor.
simpl. constructor; intuition.
Qed.

Lemma flat_subst : forall t l x n, (flat t l)[x←n] = flat (t[x←n]) (l [[x←n]]).
induction t; intros; simpl.
destruct lt_eq_lt_dec as [ [] | ].
simpl. rewrite append_subst; trivial.
simpl. rewrite append_subst; trivial.
rewrite append_subst; trivial.

destruct l; trivial.

rewrite append_subst; trivial.

destruct l; trivial.
destruct l; trivial.
Qed.



Lemma Rp1: (forall m n n' x, n ⇒ n' -> m[x←n] ⇒ m[x←n'])
      /\   (forall l n n' x , n ⇒ n' -> l [[ x ← n ]] ⇒' l [[ x ← n' ]]).
apply term_ind; intros.
(**)
simpl. destruct (lt_eq_lt_dec v x). destruct s.
constructor. intuition.
constructor. apply Rp0_lift. trivial. intuition.
constructor. intuition.
simpl; trivial.
simpl. constructor. intuition. intuition.
simpl. constructor. intuition. intuition.
simpl. constructor. intuition. intuition.

simpl. trivial.
simpl. constructor. intuition. intuition.
Qed.


Lemma Rp1_subst: (forall m m' , m ⇒ m' -> forall n n' x, n ⇒ n' -> m[x←n] ⇒ m'[x←n'])/\
   (forall l l', l ⇒' l' -> forall  n n' x , n ⇒ n' -> l [[ x ← n ]] ⇒' l' [[ x ← n' ]]).
apply Rpar_ind'; intros.
apply Rp1. trivial.
(**)
simpl. destruct subst_travers as (HH & ?).
rewrite HH. constructor;intuition. replace (S x) with (x+1) by intuition. intuition.
(**)
simpl. constructor; intuition.
simpl; constructor;intuition.
simpl; constructor;intuition.
simpl. destruct (lt_eq_lt_dec x x0). destruct s.
constructor; intuition.
constructor. apply Rp0_lift; trivial. intuition.
constructor; intuition.

rewrite flat_subst. simpl. intuition.

simpl. trivial.
simpl. constructor; intuition.
Qed.

Lemma Rp2 : forall A b m, λ[A],b ⇒ m -> exists A', exists b', m = λ[A'],b' /\ A ⇒ A' /\ b ⇒ b'.
intros.
inversion H; subst; clear H.
exists A'; exists u'; intuition.
Qed.

Lemma Rp3 : forall t l m, t::: l ⇒' m -> exists t', exists l', m = t' ::: l' /\ t ⇒ t' /\ l ⇒' l'.
intros.
inversion H; subst; clear H.
exists t'; exists l'; intuition.
Qed.

Lemma double_flat : forall u l l', flat (flat u l) l' = flat u (l@l').
induction u; intros; simpl.
rewrite append_assoc. trivial.
destruct l; intuition.
rewrite append_assoc. trivial.
destruct l; simpl; intuition.
destruct l; simpl; intuition.
Qed.

Lemma flat_R_par : forall t t' , t ⇒ t' -> forall l l', l ⇒' l' -> (flat t l) ⇒ (flat t' l').
induction 1; intros; simpl; intuition.
destruct H; intuition.
constructor. trivial. trivial. apply Rp_append.
trivial. intuition.
destruct H1; intuition.
destruct H1; intuition.
constructor. trivial. apply Rp_append. intuition. intuition.
constructor. apply Rp_append; trivial.
rewrite double_flat. constructor. trivial. apply Rp_append. intuition. intuition.
Qed.



Lemma R_par_confl  : (forall s t , s ⇒ t -> forall t', s ⇒ t' -> exists s',  t ⇒ s' /\ t' ⇒ s') /\
  (forall l l', l ⇒' l'-> forall l'', l ⇒' l'' -> exists k, l' ⇒' k /\ l'' ⇒' k).
apply Rpar_ind'; simpl; intros.
inversion H; subst; clear H.
exists !s; intuition.
(**)
inversion H2; subst; clear H2.
destruct (H u'0 H8) as (u'' & ? & ?).
destruct (H0 v'0 H9) as (v'' & ?& ?).
destruct (H1 l'0 H10) as (l'' & ? & ?).
exists ( u'' [ ← v''] · l''); split; intuition.
constructor; intuition. apply Rp1_subst; trivial.
constructor; intuition. apply Rp1_subst; trivial.
apply Rp2 in H5; apply Rp3 in H7.
destruct H5 as (A' & b' & h); destruct H7 as (t' & k' & h'); intuition. subst.
destruct (H b' H7) as (u'' & ? & ?).
destruct (H0 t' H3) as (v'' & ?& ?).
destruct (H1 k' H8) as (l'' & ? & ?).
exists ( u'' [ ← v''] · l''); split; intuition.
constructor; intuition. apply Rp1_subst; trivial.

apply Rp2 in H5; apply Rp3 in H7.
destruct H5 as (A' & b' & h); destruct H7 as (t' & k' & h'); intuition. subst.
simpl.
destruct (H b' H7) as (u'' & ? & ?).
destruct (H0 t' H3) as (v'' & ?& ?).
destruct (H1 k' H8) as (l'' & ? & ?).
exists ( u'' [ ← v''] · l''); split; intuition.
constructor; intuition. apply Rp1_subst; trivial.
(**)
apply Rp2 in H1. destruct H1 as (A0 & b0 & h); intuition. subst.
destruct (H A0 H3) as(A'' & ? & ?).
destruct (H0 b0 H4) as (u'' & ?& ?).
exists (λ[A''],u''); intuition.
(**)
inversion H1; subst; clear H1.
destruct (H A'0 H4) as(A'' & ? & ?).
destruct (H0 B'0 H6) as (B'' & ?& ?).
exists (Π(A''),B''); intuition.
(**)
inversion H1; subst; clear H1.
apply Rp2 in r; apply Rp3 in r0.
destruct r as (A' & b' & h); destruct r0 as (t' & k' &h'); intuition. subst.
destruct (H (λ[A],u'0)) as (u'' & ? & ?). constructor. intuition. trivial.
apply Rp2 in H1; apply Rp2 in H3. destruct H1 as (AA & u1 & h); destruct H3 as (AA2 & u2 & h'); intuition.
rewrite H1 in H6; injection H6; intros; subst; clear H6.
destruct (H0 (v':::l'0)) as (L & ?& ?). intuition.
apply Rp3 in H1; apply Rp3 in H6. destruct H1 as (T1 & L1 & h); destruct H6 as (T2 & L2 & h'); intuition. 
rewrite H1 in H11; injection H11; intros; subst; clear H11.
exists ( u2 [ ← T2] · L2); intuition. constructor; trivial. apply Rp1_subst; trivial.

destruct (H u'0 H4) as (u'' & ? &?). destruct (H0 l'0 H6) as (l'' & ?& ?).
exists (u'' · l''); intuition.

destruct (H u'0 H4) as (u'' & ? &?). destruct (H0 l'0 H6) as (l'' & ?& ?).
exists (flat u'' l''); intuition. apply flat_R_par; trivial.
(**)
inversion H0; subst; clear H0.
destruct (H l'0 H4) as (l'' & ?& ?).
exists (x ## l''); intuition.
(**)
inversion H1; subst; clear H1.
apply Rp3 in r0 as (v'' & l''0 & -> & ? & ?). apply Rp2 in r as (A'' & u0'' & -> & ?& ?).
simpl.
destruct (H (λ[A''],u'0)) as (L & ?& ?).
constructor. trivial. trivial. apply Rp2 in H8 as (? & Qu & ? & ? & ?).
apply Rp2 in H9 as (? & ? & ? & ? & ?). subst. injection H9; intros; subst; clear H9.
destruct (H0 (v':::l'0)) as (? & ? & ?). constructor; intuition.
apply Rp3 in H8 as ( Qv & QL & ?& ? & ?).
apply Rp3 in H9 as ( ? & ? & ?& ? & ?). subst. injection H9; intros; subst; clear H9.
exists ( x1 [ ← x2] ·  x3); intuition.
 constructor. apply Rp1_subst; trivial. trivial.

destruct (H u'0 H4) as (u'' & ?& ?). destruct (H0 l'0 H6) as (l'' & ?& ?).
exists (flat u'' l''); intuition. apply flat_R_par; trivial.

destruct (H u'0 H4) as (u'' & ?& ?). destruct (H0 l'0 H6) as (l'' & ?& ?).
exists (flat u'' l''); intuition. apply flat_R_par; trivial.  apply flat_R_par; trivial.
(**)
exists l''; intuition.
(**)
apply Rp3 in H1. destruct H1 as (u & k & h); intuition. subst.
destruct (H u H3) as (t'' & ? & ?). destruct (H0 k H4 ) as (l'' & ?& ?).
exists (t'' ::: l''); intuition.
Qed.



Reserved Notation " s ⇒⇒ t" (at level 80,  no associativity).
Reserved Notation " l ⇒⇒' g" (at level 80,  no associativity).

Inductive R_par_RT : Term -> Term -> Prop :=
  | R_par_RT_refl : forall s, s ⇒⇒ s
  | R_par_RT_trans : forall s t u , s ⇒ t -> t ⇒⇒ u -> s ⇒⇒ u
where "s ⇒⇒ t" := (R_par_RT s t) : SC_scope.


Inductive R_par_RT_List : Term_List -> Term_List -> Prop :=
  | R_par_RT_List_refl : forall l , l ⇒⇒' l
  | R_par_RT_List_trans : forall l l' l'' , l ⇒' l' -> l' ⇒⇒' l'' -> l ⇒⇒' l''
where "l ⇒⇒' g" := (R_par_RT_List l g) : SC_scope.

Hint Constructors R_par_RT R_par_RT_List.

Lemma R_par_RT_trans2 : forall s t u, s ⇒⇒ t -> t ⇒⇒ u -> s ⇒⇒ u.
intros s t u H; generalize u; clear u; induction H; intros; intuition.
apply R_par_RT_trans with t; trivial.
apply IHR_par_RT; trivial.
Qed.

Lemma R_par_RT_List_trans2 : forall j k l , j ⇒⇒' k -> k ⇒⇒' l -> j ⇒⇒' l.
intros j k l H; generalize l; clear l; induction H; intros; intuition.
apply R_par_RT_List_trans with l'; trivial.
apply IHR_par_RT_List; trivial.
Qed.


Lemma R_par_RT_onestep : forall i j , i ⇒ j -> i ⇒⇒ j.
intros.
apply R_par_RT_trans with j; trivial.
Qed.

Lemma R_par_RT_List_onestep : forall i j , i ⇒' j -> i ⇒⇒' j.
intros.
apply R_par_RT_List_trans with j; trivial.
Qed.

Hint Resolve R_par_RT_trans2 R_par_RT_onestep R_par_RT_List_trans2 R_par_RT_onestep.


Lemma RBx_to_flat : forall u l,  u · l ▹▹ flat u l.
induction u; intros; simpl; intuition.
destruct l; intuition.
destruct l; intuition.
destruct l; intuition.
Qed.

Lemma RBx_append : forall l l' l'', l ▹' l' -> l@l'' ▹' l'@l''.
intros. revert l''.
induction H; intros.
simpl. constructor. trivial.
simpl. constructor. intuition.
Qed.

Lemma RBx_RT_append : forall l l' k k', l ▹▹' l' -> k ▹▹' k' -> l@k ▹▹' l'@k'.
 assert (forall l l' , l ▹▹' l' -> forall k, l@k ▹▹' l'@k).
induction 1; intros. trivial. apply RBx_RT_List_trans2 with l'@k.
apply RBx_RT_List_onestep. apply RBx_append. trivial.
intuition.
intros. apply RBx_RT_List_trans2 with (l'@k).
eauto. clear H0 l H.
revert k k' H1.
induction l'; intros; simpl; trivial.
apply RBx_RT_cons. trivial. intuition.
Qed.


Lemma RBx_RT_List_Nil : forall l, [[]] ▹▹' l -> l = [[]].
intros. inversion H; subst; clear H. trivial.
inversion H0.
Qed.

Lemma RBx_RT_List_Cons : forall u k l , u::: k ▹▹' l -> exists v , exists k', l = v ::: k' /\ u ▹▹ v /\ k ▹▹' k'.
intros. remember (u:::k) as L.
revert u k HeqL.
induction H; intros; subst.
exists u; exists  k; intuition.
inversion H; subst; clear H.
destruct (IHRBx_RT_List t' k) as (w & ll & -> & ? &?); trivial.
exists w; exists ll; intuition. eauto.
destruct (IHRBx_RT_List u l'0) as (w &ll & -> & ? &?); trivial.
exists w ; exists ll; intuition. eauto.
Qed.


Lemma flat_RBx : forall t t' , t ▹  t' -> forall l l', l ▹▹' l' -> (flat t l) ▹▹ (flat t' l').
assert (forall t t' , t ▹  t' -> forall l , (flat t l) ▹▹ (flat t' l)).
induction 1; intros; simpl ; intuition. apply RBx_to_flat. 
rewrite <- append_assoc.
apply RBx_RT_CVar. trivial. trivial.
rewrite <- append_assoc.
apply RBx_RT_CTerm. trivial. trivial. trivial.
destruct l; intuition.
destruct l; intuition.
apply RBx_RT_App; intuition. apply RBx_RT_append; intuition. apply RBx_RT_List_onestep; trivial.
apply RBx_RT_Var. apply RBx_RT_append. apply RBx_RT_List_onestep; trivial. trivial.
destruct l; intuition.
destruct l; intuition.
intros.
apply RBx_RT_trans2 with (flat t' l); intuition.
clear t H0 H.
destruct t'; simpl; intuition.
apply RBx_RT_Var. apply RBx_RT_append. trivial. trivial.
destruct l. apply RBx_RT_List_Nil in H1; subst; trivial.
apply RBx_RT_List_Cons in H1 as (t' & k & -> & ?& ?). eauto.
apply RBx_RT_App. trivial. apply RBx_RT_append; trivial.

destruct l. apply RBx_RT_List_Nil in H1; subst; trivial.
apply RBx_RT_List_Cons in H1 as (t' & k & -> & ?& ?). eauto.
destruct l. apply RBx_RT_List_Nil in H1; subst; trivial.
apply RBx_RT_List_Cons in H1 as (t' & k & -> & ?& ?). eauto.
Qed.

Lemma flat_RBx_RT : forall t t' , t ▹▹  t' -> forall l l', l ▹▹' l' -> (flat t l) ▹▹ (flat t' l').
induction 1; intros.
destruct s; simpl. apply RBx_RT_Var; intuition. apply RBx_RT_append; trivial.
destruct l. apply RBx_RT_List_Nil in H; subst; trivial.
apply RBx_RT_List_Cons in H as (t' & k & -> & ?& ?). eauto.
apply RBx_RT_App; intuition. apply RBx_RT_append; trivial.
destruct l. apply RBx_RT_List_Nil in H; subst; trivial.
apply RBx_RT_List_Cons in H as (t' & k & -> & ?& ?). eauto.
destruct l. apply RBx_RT_List_Nil in H; subst; trivial.
apply RBx_RT_List_Cons in H as (t' & k & -> & ?& ?). eauto.
apply RBx_RT_trans2 with (flat t l').
apply flat_RBx; trivial.
intuition.
Qed.


 
Lemma Betas_Betap_closure : (forall x y , x ⇒ y -> x  ▹▹  y) /\
  (forall x y , x ⇒' y -> x  ▹▹'  y).
apply Rpar_ind'; intros; intuition.
apply RBx_RT_trans2 with (u [ ← v] · l). intuition. apply RBx_RT_App; trivial. 
apply RBx_RT_trans2 with (u [ ← v']). intuition. intuition.
apply RBx_RT_trans2 with (flat u l). apply RBx_to_flat. apply flat_RBx_RT.
trivial. trivial.
Qed.

Lemma Betas_Betaps_closure : forall x y , 
  x ⇒⇒  y -> x ▹▹  y.
induction 1; eauto.
apply Betas_Betap_closure in H. eauto.
Qed.

Lemma Betas_Betaps_List_closure : forall x y , 
  x ⇒⇒'  y -> x ▹▹'  y.
induction 1; eauto.
apply Betas_Betap_closure in H. eauto.
Qed.

Lemma Betap_Beta_closure : (forall x y, x ▹ y -> x ⇒ y) /\
 (forall x y, x ▹' y -> x ⇒' y).
apply R_ind'; intros; intuition. 
apply R_par_nil. apply R_par_refl.
replace (x ## l @ l') with (flat (x## l ) l').
apply App3_par. apply R_par_refl. apply R_par_refl. simpl; trivial.
replace (t · l @ l') with (flat (t  ·  l ) l').
apply App3_par. apply R_par_refl. apply R_par_refl. simpl; trivial.
Qed.

Lemma Betaps_Beta_closure :forall x y, x ▹ y -> x ⇒⇒ y.
intros. apply Betap_Beta_closure in H. apply R_par_RT_onestep; trivial.
Qed.

Lemma Betaps_Beta_List_closure :forall x y, x ▹' y -> x ⇒⇒' y.
intros. apply Betap_Beta_closure in H. apply R_par_RT_List_onestep; trivial.
Qed.

Lemma Betaps_Betas_closure : forall x y , x ▹▹ y -> x ⇒⇒ y.
induction 1. constructor; apply R_par_refl.
apply Betap_Beta_closure in H; eauto.
Qed.

Lemma Betaps_Betas_List_closure : forall x y , x ▹▹' y -> x ⇒⇒' y.
induction 1. constructor; apply R_par_refl.
apply Betap_Beta_closure in H; eauto.
Qed.

Lemma sub_diamond_Betaps : 
(   forall x y z, x ⇒ y -> x ⇒ z -> (exists t, y ⇒ t /\ z ⇒ t) )
 -> forall x y z , x ⇒ y -> x ⇒⇒ z ->(exists t, y ⇒⇒ t /\ z ⇒ t).
intros.
revert y H0. induction H1; eauto. 
intros.
destruct (H s t  y H0 H2) as (x1 & ?& ?).
destruct (IHR_par_RT x1 H3) as (x2 & ? & ?).
exists x2; eauto.
Qed.


Lemma diamond_Betaps : 
(   forall x y z, x ⇒ y -> x ⇒ z -> (exists t, y ⇒ t /\ z ⇒ t) )
 ->
  forall  x y z, x ⇒⇒ y -> x ⇒⇒ z -> (exists t,y ⇒⇒ t /\ z ⇒⇒ t) .
intros. 
revert z H1.
induction H0; intros; eauto.
destruct (sub_diamond_Betaps H s t z  H0 H2) as (Z & ? & ?).
destruct (IHR_par_RT  Z H3) as (ZZ & ?& ?). 
exists ZZ;eauto.
Qed.


(* from all this => Beta* is confluent \o/
 a hand written proof is in Barendregt 
TODO : finish for the list
*)
Lemma Betas_diamond: 
  forall x y z, x ▹▹ y -> x ▹▹ z -> (exists t, y ▹▹ t /\ z ▹▹ t).
intros.
destruct diamond_Betaps with   x y z. intros.
eapply R_par_confl. apply H1. trivial. apply Betaps_Betas_closure; trivial.
apply Betaps_Betas_closure; trivial.
exists x0; intuition. 
apply Betas_Betaps_closure; trivial.
apply Betas_Betaps_closure; trivial.
Qed.