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.