Library MetaCoq.PCUIC.PCUICParallelReduction

Lemma size_lift n k t : size (lift n k t) = size t.



Lemma All_pair {A} (P Q : A → Type) l :
  All (fun x ⇒ P x × Q x)%type l <~> (All P l × All Q l).

Definition on_local_decl (P : context → term → Type)
           (Γ : context) (t : term) (T : option term) :=
  match T with
  | Some T ⇒ (P Γ t × P Γ T)%type
  | None ⇒ P Γ t
  end.

Lemma term_forall_ctx_list_ind :
  ∀ (P : context → term → Type),

    (∀ Γ (n : nat), P Γ (tRel n)) →
    (∀ Γ (i : ident), P Γ (tVar i)) →
    (∀ Γ (n : nat) (l : list term), All (P Γ) l → P Γ (tEvar n l)) →
    (∀ Γ s, P Γ (tSort s)) →
    (∀ Γ (n : name) (t : term), P Γ t → ∀ t0 : term, P (vass n t :: Γ) t0 → P Γ (tProd n t t0)) →
    (∀ Γ (n : name) (t : term), P Γ t → ∀ t0 : term, P (vass n t :: Γ) t0 → P Γ (tLambda n t t0)) →
    (∀ Γ (n : name) (t : term),
        P Γ t → ∀ t0 : term, P Γ t0 → ∀ t1 : term, P (vdef n t t0 :: Γ) t1 → P Γ (tLetIn n t t0 t1)) →
    (∀ Γ (t u : term), P Γ t → P Γ u → P Γ (tApp t u)) →
    (∀ Γ (s : String.string) (u : list Level.t), P Γ (tConst s u)) →
    (∀ Γ (i : inductive) (u : list Level.t), P Γ (tInd i u)) →
    (∀ Γ (i : inductive) (n : nat) (u : list Level.t), P Γ (tConstruct i n u)) →
    (∀ Γ (p : inductive × nat) (t : term),
        P Γ t → ∀ t0 : term, P Γ t0 → ∀ l : list (nat × term),
            tCaseBrsProp (P Γ) l → P Γ (tCase p t t0 l)) →
    (∀ Γ (s : projection) (t : term), P Γ t → P Γ (tProj s t)) →
    (∀ Γ (m : mfixpoint term) (n : nat),
        All_local_env (on_local_decl (fun Γ' t ⇒ P (Γ ,,, Γ') t)) (fix_context m) →
        tFixProp (P Γ) (P (Γ ,,, fix_context m)) m → P Γ (tFix m n)) →
    (∀ Γ (m : mfixpoint term) (n : nat),
        All_local_env (on_local_decl (fun Γ' t ⇒ P (Γ ,,, Γ') t)) (fix_context m) →
        tFixProp (P Γ) (P (Γ ,,, fix_context m)) m → P Γ (tCoFix m n)) →
    ∀ Γ (t : term), P Γ t.

Lemma simpl_subst' :
  ∀ N M n p k, k = List.length N → p ≤ n → subst N p (lift0 (k + n) M) = lift0 n M.

Lemma All2_app {A} {P : A → A → Type} {l l' r r'} :
  All2 P l l' → All2 P r r' →
  All2 P (l ++ r) (l' ++ r').

Definition All2_prop_eq Γ Γ' {A B} (f : A → term) (g : A → B) (rel : ∀ (Γ Γ' : context) (t t' : term), Type) :=
  All2 (on_Trel_eq (rel Γ Γ') f g).

Definition All2_prop Γ (rel : ∀ (Γ : context) (t t' : term), Type) :=
  All2 (rel Γ).


Lemma All2_All2_prop {P Q : context → context → term → term → Type} {par par'} {l l' : list term} :
  All2 (P par par') l l' →
  (∀ x y, P par par' x y → Q par par' x y) →
  All2 (Q par par') l l'.

Lemma All2_All2_prop_eq {A B} {P Q : context → context → term → term → Type} {par par'}
      {f : A → term} {g : A → B} {l l' : list A} :
  All2 (on_Trel_eq (P par par') f g) l l' →
  (∀ x y, P par par' x y → Q par par' x y) →
  All2_prop_eq par par' f g Q l l'.

Definition All2_prop2_eq Γ Γ' Γ2 Γ2' {A B} (f g : A → term) (h : A → B)
           (rel : ∀ (Γ Γ' : context) (t t' : term), Type) :=
  All2 (fun x y ⇒ on_Trel (rel Γ Γ') f x y × on_Trel_eq (rel Γ2 Γ2') g h x y)%type.

Definition All2_prop2 Γ Γ' {A} (f g : A → term)
           (rel : ∀ (Γ : context) (t t' : term), Type) :=
  All2 (fun x y ⇒ on_Trel (rel Γ) f x y × on_Trel (rel Γ') g x y)%type.

Lemma All2_All2_prop2_eq {A B} {P Q : context → context → term → term → Type} {par par' par2 par2'}
      {f g : A → term} {h : A → B} {l l' : list A} :
  All2_prop2_eq par par' par2 par2' f g h P l l' →
  (∀ par par' x y, P par par' x y → Q par par' x y) →
  All2_prop2_eq par par' par2 par2' f g h Q l l'.


Section All2_local_env.

  Definition on_decl (P : context → context → term → term → Type)
             (Γ Γ' : context) (b : option (term × term)) (t t' : term) :=
    match b with
    | Some (b, b') ⇒ (P Γ Γ' b b' × P Γ Γ' t t')%type
    | None ⇒ P Γ Γ' t t'
    end.

  Definition on_decls (P : term → term → Type) (d d' : context_decl) :=
    match d.(decl_body), d'.(decl_body) with
    | Some b, Some b' ⇒ (P b b' × P d.(decl_type) d'.(decl_type))%type
    | None, None ⇒ P d.(decl_type) d'.(decl_type)
    | _, _ ⇒ False
    end.

  Section All_local_2.
    Context (P : ∀ (Γ Γ' : context), option (term × term) → term → term → Type).

    Inductive All2_local_env : context → context → Type :=
    | localenv2_nil : All2_local_env [] []
    | localenv2_cons_abs Γ Γ' na na' t t' :
        All2_local_env Γ Γ' →
        P Γ Γ' None t t' →
        All2_local_env (Γ ,, vass na t) (Γ' ,, vass na' t')
    | localenv2_cons_def Γ Γ' na na' b b' t t' :
        All2_local_env Γ Γ' →
        P Γ Γ' (Some (b, b')) t t' →
        All2_local_env (Γ ,, vdef na b t) (Γ' ,, vdef na' b' t').
  End All_local_2.

  Definition on_decl_over (P : context → context → term → term → Type) Γ Γ' :=
    fun Δ Δ' ⇒ P (Γ ,,, Δ) (Γ' ,,, Δ').

  Definition All2_local_env_over P Γ Γ' := All2_local_env (on_decl (on_decl_over P Γ Γ')).

  Lemma All2_local_env_impl {P Q : context → context → term → term → Type} {par par'} :
    All2_local_env (on_decl P) par par' →
    (∀ par par' x y, P par par' x y → Q par par' x y) →
    All2_local_env (on_decl Q) par par'.

  Lemma All2_local_env_app_inv :
    ∀ P (Γ Γ' Γl Γr : context),
      All2_local_env (on_decl P) Γ Γl →
      All2_local_env (on_decl (on_decl_over P Γ Γl)) Γ' Γr →
      All2_local_env (on_decl P) (Γ ,,, Γ') (Γl ,,, Γr).

  Lemma All2_local_env_length {P l l'} : @All2_local_env P l l' → #|l| = #|l'|.



  Lemma All2_local_env_app':
    ∀ P (Γ Γ' Γ'' : context),
      All2_local_env (on_decl P) (Γ ,,, Γ') Γ'' →
      ∑ Γl Γr, (Γ'' = Γl ,,, Γr) ∧ #|Γ'| = #|Γr| ∧ #|Γ| = #|Γl|.

  Lemma app_inj_length_r {A} (l l' r r' : list A) :
    app l r = app l' r' → #|r| = #|r'| → l = l' ∧ r = r'.

  Lemma app_inj_length_l {A} (l l' r r' : list A) :
    app l r = app l' r' → #|l| = #|l'| → l = l' ∧ r = r'.

  Lemma All2_local_env_app_ex:
    ∀ P (Γ Γ' Γ'' : context),
      All2_local_env (on_decl P) (Γ ,,, Γ') Γ'' →
      ∑ Γl Γr, (Γ'' = Γl ,,, Γr) ×
      All2_local_env
        (on_decl P)
        Γ Γl × All2_local_env (on_decl (fun Δ Δ' ⇒ P (Γ ,,, Δ) (Γl ,,, Δ'))) Γ' Γr.

  Lemma All2_local_env_app :
    ∀ P (Γ Γ' Γl Γr : context),
      All2_local_env (on_decl P) (Γ ,,, Γ') (Γl ,,, Γr) →
      #|Γ| = #|Γl| →
      All2_local_env (on_decl P) Γ Γl × All2_local_env (on_decl (fun Δ Δ' ⇒ P (Γ ,,, Δ) (Γl ,,, Δ'))) Γ' Γr.

  Lemma nth_error_pred1_ctx {P} {Γ Δ} i body' :
    All2_local_env (on_decl P) Γ Δ →
    option_map decl_body (nth_error Δ i) = Some (Some body') →
    { body & (option_map decl_body (nth_error Γ i) = Some (Some body)) ×
             P (skipn (S i) Γ) (skipn (S i) Δ) body body' }%type.

  Lemma nth_error_pred1_ctx_l {P} {Γ Δ} i body :
    All2_local_env (on_decl P) Γ Δ →
    option_map decl_body (nth_error Γ i) = Some (Some body) →
    { body' & (option_map decl_body (nth_error Δ i) = Some (Some body')) ×
             P (skipn (S i) Γ) (skipn (S i) Δ) body body' }%type.

  Lemma All2_local_env_over_app P {Γ0 Δ Γ'' Δ''} :
    All2_local_env (on_decl P) Γ0 Δ →
    All2_local_env_over P Γ0 Δ Γ'' Δ'' →
    All2_local_env (on_decl P) (Γ0 ,,, Γ'') (Δ ,,, Δ'').

  Lemma All2_local_env_app_left {P Γ Γ' Δ Δ'} :
    All2_local_env (on_decl P) (Γ ,,, Δ) (Γ' ,,, Δ') → #|Γ| = #|Γ'| →
    All2_local_env (on_decl P) Γ Γ'.

End All2_local_env.

Section ParallelReduction.
  Context (Σ : global_env).

  Definition pred_atom t :=
    match t with
    | tVar _
    | tSort _
    | tInd _ _
    | tConstruct _ _ _ ⇒ true
    | _ ⇒ false
    end.

  Inductive pred1 (Γ Γ' : context) : term → term → Type :=
  

  | pred_beta na t0 t1 b0 b1 a0 a1 :
      pred1 Γ Γ' t0 t1 →
      pred1 (Γ ,, vass na t0) (Γ' ,, vass na t1) b0 b1 → pred1 Γ Γ' a0 a1 →
      pred1 Γ Γ' (tApp (tLambda na t0 b0) a0) (subst10 a1 b1)

  

  | pred_zeta na d0 d1 t0 t1 b0 b1 :
      pred1 Γ Γ' t0 t1 →
      pred1 Γ Γ' d0 d1 → pred1 (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1 →
      pred1 Γ Γ' (tLetIn na d0 t0 b0) (subst10 d1 b1)

  

  | pred_rel_def_unfold i body :
      All2_local_env (on_decl pred1) Γ Γ' →
      option_map decl_body (nth_error Γ' i) = Some (Some body) →
      pred1 Γ Γ' (tRel i) (lift0 (S i) body)

  | pred_rel_refl i :
      All2_local_env (on_decl pred1) Γ Γ' →
      pred1 Γ Γ' (tRel i) (tRel i)

  

  | pred_iota ind pars c u args0 args1 p brs0 brs1 :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2 (pred1 Γ Γ') args0 args1 →
      All2 (on_Trel_eq (pred1 Γ Γ') snd fst) brs0 brs1 →
      pred1 Γ Γ' (tCase (ind, pars) p (mkApps (tConstruct ind c u) args0) brs0)
            (iota_red pars c args1 brs1)

  

  | pred_fix mfix0 mfix1 idx args0 args1 narg fn :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
      All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                    dtype dbody (fun x ⇒ (dname x, rarg x)) pred1 mfix0 mfix1 →
      unfold_fix mfix1 idx = Some (narg, fn) →
      is_constructor narg args1 = true →
      All2 (pred1 Γ Γ') args0 args1 →
      pred1 Γ Γ' (mkApps (tFix mfix0 idx) args0) (mkApps fn args1)

  

  | pred_cofix_case ip p0 p1 mfix0 mfix1 idx args0 args1 narg fn brs0 brs1 :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
      All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                    dtype dbody (fun x ⇒ (dname x, rarg x)) pred1 mfix0 mfix1 →
      unfold_cofix mfix1 idx = Some (narg, fn) →
      All2 (pred1 Γ Γ') args0 args1 →
      pred1 Γ Γ' p0 p1 →
      All2 (on_Trel_eq (pred1 Γ Γ') snd fst) brs0 brs1 →
      pred1 Γ Γ' (tCase ip p0 (mkApps (tCoFix mfix0 idx) args0) brs0)
            (tCase ip p1 (mkApps fn args1) brs1)

  

  | pred_cofix_proj p mfix0 mfix1 idx args0 args1 narg fn :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
      All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                    dtype dbody (fun x ⇒ (dname x, rarg x)) pred1 mfix0 mfix1 →
      unfold_cofix mfix1 idx = Some (narg, fn) →
      All2 (pred1 Γ Γ') args0 args1 →
      pred1 Γ Γ' (tProj p (mkApps (tCoFix mfix0 idx) args0))
            (tProj p (mkApps fn args1))

  

  | pred_delta c decl body (isdecl : declared_constant Σ c decl) u :
      All2_local_env (on_decl pred1) Γ Γ' →
      decl.(cst_body) = Some body →
      pred1 Γ Γ' (tConst c u) (subst_instance_constr u body)

  | pred_const c u :
      All2_local_env (on_decl pred1) Γ Γ' →
      pred1 Γ Γ' (tConst c u) (tConst c u)

  

  | pred_proj i pars narg k u args0 args1 arg1 :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2 (pred1 Γ Γ') args0 args1 →
      nth_error args1 (pars + narg) = Some arg1 →
      pred1 Γ Γ' (tProj (i, pars, narg) (mkApps (tConstruct i k u) args0)) arg1

  

  | pred_abs na M M' N N' : pred1 Γ Γ' M M' → pred1 (Γ ,, vass na M) (Γ' ,, vass na M') N N' →
                            pred1 Γ Γ' (tLambda na M N) (tLambda na M' N')
  | pred_app M0 M1 N0 N1 :
      pred1 Γ Γ' M0 M1 →
      pred1 Γ Γ' N0 N1 →
      pred1 Γ Γ' (tApp M0 N0) (tApp M1 N1)
            

  | pred_letin na d0 d1 t0 t1 b0 b1 :
      pred1 Γ Γ' d0 d1 → pred1 Γ Γ' t0 t1 → pred1 (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1 →
      pred1 Γ Γ' (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1)

  | pred_case ind p0 p1 c0 c1 brs0 brs1 :
      pred1 Γ Γ' p0 p1 →
      pred1 Γ Γ' c0 c1 →
      All2 (on_Trel_eq (pred1 Γ Γ') snd fst) brs0 brs1 →
      pred1 Γ Γ' (tCase ind p0 c0 brs0) (tCase ind p1 c1 brs1)

  | pred_proj_congr p c c' :
      pred1 Γ Γ' c c' → pred1 Γ Γ' (tProj p c) (tProj p c')

  | pred_fix_congr mfix0 mfix1 idx :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
      All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                    dtype dbody (fun x ⇒ (dname x, rarg x)) pred1 mfix0 mfix1 →
      pred1 Γ Γ' (tFix mfix0 idx) (tFix mfix1 idx)

  | pred_cofix_congr mfix0 mfix1 idx :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
      All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                    dtype dbody (fun x ⇒ (dname x, rarg x)) pred1 mfix0 mfix1 →
      pred1 Γ Γ' (tCoFix mfix0 idx) (tCoFix mfix1 idx)

  | pred_prod na M0 M1 N0 N1 : pred1 Γ Γ' M0 M1 → pred1 (Γ ,, vass na M0) (Γ' ,, vass na M1) N0 N1 →
                               pred1 Γ Γ' (tProd na M0 N0) (tProd na M1 N1)

  | evar_pred ev l l' :
      All2_local_env (on_decl pred1) Γ Γ' →
      All2 (pred1 Γ Γ') l l' → pred1 Γ Γ' (tEvar ev l) (tEvar ev l')

  | pred_atom_refl t :
      All2_local_env (on_decl pred1) Γ Γ' →
      pred_atom t → pred1 Γ Γ' t t.

  Notation pred1_ctx Γ Γ' := (All2_local_env (on_decl pred1) Γ Γ').



  Definition extendP {P Q: context → context → term → term → Type}
             (aux : ∀ Γ Γ' t t', P Γ Γ' t t' → Q Γ Γ' t t') :
    (∀ Γ Γ' t t', P Γ Γ' t t' → (P Γ Γ' t t' × Q Γ Γ' t t')).




  Lemma pred1_ind_all_ctx :
    ∀ (P : ∀ (Γ Γ' : context) (t t0 : term), Type)
           (Pctx : ∀ (Γ Γ' : context), Type),
           
      let P' Γ Γ' x y := ((pred1 Γ Γ' x y) × P Γ Γ' x y)%type in
      (∀ Γ Γ', All2_local_env (on_decl pred1) Γ Γ' → All2_local_env (on_decl P) Γ Γ' → Pctx Γ Γ') →
      
      
      
      
      
      (∀ (Γ Γ' : context) (na : name) (t0 t1 b0 b1 a0 a1 : term),
          pred1 (Γ ,, vass na t0) (Γ' ,, vass na t1) b0 b1 → P (Γ ,, vass na t0) (Γ' ,, vass na t1) b0 b1 →
          pred1 Γ Γ' t0 t1 → P Γ Γ' t0 t1 →
          pred1 Γ Γ' a0 a1 → P Γ Γ' a0 a1 → P Γ Γ' (tApp (tLambda na t0 b0) a0) (b1 {0 := a1})) →
      (∀ (Γ Γ' : context) (na : name) (d0 d1 t0 t1 b0 b1 : term),
          pred1 Γ Γ' t0 t1 → P Γ Γ' t0 t1 →
          pred1 Γ Γ' d0 d1 → P Γ Γ' d0 d1 →
          pred1 (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1 →
          P (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1 → P Γ Γ' (tLetIn na d0 t0 b0) (b1 {0 := d1})) →
      (∀ (Γ Γ' : context) (i : nat) (body : term),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          option_map decl_body (nth_error Γ' i) = Some (Some body) →
          P Γ Γ' (tRel i) (lift0 (S i) body)) →
      (∀ (Γ Γ' : context) (i : nat),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          P Γ Γ' (tRel i) (tRel i)) →
      (∀ (Γ Γ' : context) (ind : inductive) (pars c : nat) (u : universe_instance) (args0 args1 : list term)
              (p : term) (brs0 brs1 : list (nat × term)),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2 (P' Γ Γ') args0 args1 →
          All2_prop_eq Γ Γ' snd fst P' brs0 brs1 →
          P Γ Γ' (tCase (ind, pars) p (mkApps (tConstruct ind c u) args0) brs0) (iota_red pars c args1 brs1)) →
      (∀ (Γ Γ' : context) (mfix0 mfix1 : mfixpoint term) (idx : nat) (args0 args1 : list term) (narg : nat) (fn : term),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_local_env (on_decl (on_decl_over P Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody
                        (fun x ⇒ (dname x, rarg x)) P' mfix0 mfix1 →
          unfold_fix mfix1 idx = Some (narg, fn) →
          is_constructor narg args1 = true →
          All2 (P' Γ Γ') args0 args1 →
          P Γ Γ' (mkApps (tFix mfix0 idx) args0) (mkApps fn args1)) →
      (∀ (Γ Γ' : context) (ip : inductive × nat) (p0 p1 : term) (mfix0 mfix1 : mfixpoint term) (idx : nat)
              (args0 args1 : list term) (narg : nat) (fn : term) (brs0 brs1 : list (nat × term)),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_local_env (on_decl (on_decl_over P Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody
                        (fun x ⇒ (dname x, rarg x)) P' mfix0 mfix1 →
          unfold_cofix mfix1 idx = Some (narg, fn) →
          All2 (P' Γ Γ') args0 args1 →
          pred1 Γ Γ' p0 p1 →
          P Γ Γ' p0 p1 →
          All2_prop_eq Γ Γ' snd fst P' brs0 brs1 →
          P Γ Γ' (tCase ip p0 (mkApps (tCoFix mfix0 idx) args0) brs0) (tCase ip p1 (mkApps fn args1) brs1)) →
      (∀ (Γ Γ' : context) (p : projection) (mfix0 mfix1 : mfixpoint term)
         (idx : nat) (args0 args1 : list term)
         (narg : nat) (fn : term),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_local_env (on_decl (on_decl_over P Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody
                        (fun x ⇒ (dname x, rarg x)) P' mfix0 mfix1 →
          unfold_cofix mfix1 idx = Some (narg, fn) →
          All2 (P' Γ Γ') args0 args1 →
          P Γ Γ' (tProj p (mkApps (tCoFix mfix0 idx) args0)) (tProj p (mkApps fn args1))) →
      (∀ (Γ Γ' : context) (c : ident) (decl : constant_body) (body : term),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          declared_constant Σ c decl →
          ∀ u : universe_instance, cst_body decl = Some body →
                                        P Γ Γ' (tConst c u) (subst_instance_constr u body)) →
      (∀ (Γ Γ' : context) (c : ident) (u : universe_instance),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          P Γ Γ' (tConst c u) (tConst c u)) →
      (∀ (Γ Γ' : context) (i : inductive) (pars narg : nat) (k : nat) (u : universe_instance)
              (args0 args1 : list term) (arg1 : term),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2 (pred1 Γ Γ') args0 args1 →
          All2 (P Γ Γ') args0 args1 →
          nth_error args1 (pars + narg) = Some arg1 →
          P Γ Γ' (tProj (i, pars, narg) (mkApps (tConstruct i k u) args0)) arg1) →
      (∀ (Γ Γ' : context) (na : name) (M M' N N' : term),
          pred1 Γ Γ' M M' →
          P Γ Γ' M M' → pred1 (Γ,, vass na M) (Γ' ,, vass na M') N N' →
          P (Γ,, vass na M) (Γ' ,, vass na M') N N' → P Γ Γ' (tLambda na M N) (tLambda na M' N')) →
      (∀ (Γ Γ' : context) (M0 M1 N0 N1 : term),
          pred1 Γ Γ' M0 M1 → P Γ Γ' M0 M1 → pred1 Γ Γ' N0 N1 →
          P Γ Γ' N0 N1 → P Γ Γ' (tApp M0 N0) (tApp M1 N1)) →
      (∀ (Γ Γ' : context) (na : name) (d0 d1 t0 t1 b0 b1 : term),
          pred1 Γ Γ' d0 d1 →
          P Γ Γ' d0 d1 →
          pred1 Γ Γ' t0 t1 →
          P Γ Γ' t0 t1 →
          pred1 (Γ,, vdef na d0 t0) (Γ',,vdef na d1 t1) b0 b1 →
          P (Γ,, vdef na d0 t0) (Γ',,vdef na d1 t1) b0 b1 → P Γ Γ' (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1)) →
      (∀ (Γ Γ' : context) (ind : inductive × nat) (p0 p1 c0 c1 : term) (brs0 brs1 : list (nat × term)),
          pred1 Γ Γ' p0 p1 →
          P Γ Γ' p0 p1 →
          pred1 Γ Γ' c0 c1 →
          P Γ Γ' c0 c1 → All2_prop_eq Γ Γ' snd fst P' brs0 brs1 →
          P Γ Γ' (tCase ind p0 c0 brs0) (tCase ind p1 c1 brs1)) →
      (∀ (Γ Γ' : context) (p : projection) (c c' : term), pred1 Γ Γ' c c' → P Γ Γ' c c' → P Γ Γ' (tProj p c) (tProj p c')) →

      (∀ (Γ Γ' : context) (mfix0 : mfixpoint term) (mfix1 : list (def term)) (idx : nat),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_local_env (on_decl (on_decl_over P Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                        dtype dbody (fun x ⇒ (dname x, rarg x)) P' mfix0 mfix1 →
          P Γ Γ' (tFix mfix0 idx) (tFix mfix1 idx)) →

      (∀ (Γ Γ' : context) (mfix0 : mfixpoint term) (mfix1 : list (def term)) (idx : nat),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2_local_env (on_decl (on_decl_over pred1 Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_local_env (on_decl (on_decl_over P Γ Γ')) (fix_context mfix0) (fix_context mfix1) →
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody (fun x ⇒ (dname x, rarg x)) P' mfix0 mfix1 →
          P Γ Γ' (tCoFix mfix0 idx) (tCoFix mfix1 idx)) →
      (∀ (Γ Γ' : context) (na : name) (M0 M1 N0 N1 : term),
          pred1 Γ Γ' M0 M1 →
          P Γ Γ' M0 M1 → pred1 (Γ,, vass na M0) (Γ' ,, vass na M1) N0 N1 →
          P (Γ,, vass na M0) (Γ' ,, vass na M1) N0 N1 → P Γ Γ' (tProd na M0 N0) (tProd na M1 N1)) →
      (∀ (Γ Γ' : context) (ev : nat) (l l' : list term),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          All2 (P' Γ Γ') l l' → P Γ Γ' (tEvar ev l) (tEvar ev l')) →
      (∀ (Γ Γ' : context) (t : term),
          All2_local_env (on_decl pred1) Γ Γ' →
          Pctx Γ Γ' →
          pred_atom t → P Γ Γ' t t) →
      ∀ (Γ Γ' : context) (t t0 : term), pred1 Γ Γ' t t0 → P Γ Γ' t t0.

  Lemma pred1_refl_gen Γ Γ' t : pred1_ctx Γ Γ' → pred1 Γ Γ' t t.

  Lemma pred1_ctx_refl Γ : pred1_ctx Γ Γ.

  Lemma pred1_refl Γ t : pred1 Γ Γ t t.

  Lemma pred1_pred1_ctx {Γ Δ t u} : pred1 Γ Δ t u → pred1_ctx Γ Δ.

  Lemma pred1_ctx_over_refl Γ Δ : All2_local_env (on_decl (on_decl_over pred1 Γ Γ)) Δ Δ.

End ParallelReduction.





Notation pred1_ctx Σ Γ Γ' := (All2_local_env (on_decl (pred1 Σ)) Γ Γ').







Lemma All2_local_env_over_refl {Σ Γ Δ Γ'} :
  pred1_ctx Σ Γ Δ → All2_local_env_over (pred1 Σ) Γ Δ Γ' Γ'.


Section ParallelWeakening.
  Context {cf : checker_flags}.


  Lemma All2_local_env_weaken_pred_ctx {Σ Γ0 Γ'0 Δ Δ' Γ'' Δ''} :
      #|Γ0| = #|Δ| →
  pred1_ctx Σ Γ0 Δ →
  All2_local_env_over (pred1 Σ) Γ0 Δ Γ'' Δ'' →
  All2_local_env
    (on_decl
       (fun (Γ Γ' : context) (t t0 : term) ⇒
        ∀ Γ1 Γ'1 : context,
        Γ = Γ1 ,,, Γ'1 →
        ∀ Δ0 Δ'0 : context,
        Γ' = Δ0 ,,, Δ'0 →
        #|Γ1| = #|Δ0| →
        ∀ Γ''0 Δ''0 : context,
        All2_local_env_over (pred1 Σ) Γ1 Δ0 Γ''0 Δ''0 →
        pred1 Σ (Γ1 ,,, Γ''0 ,,, lift_context #|Γ''0| 0 Γ'1) (Δ0 ,,, Δ''0 ,,, lift_context #|Δ''0| 0 Δ'0)
          (lift #|Γ''0| #|Γ'1| t) (lift #|Δ''0| #|Δ'0| t0))) (Γ0 ,,, Γ'0) (Δ ,,, Δ') →

  pred1_ctx Σ (Γ0 ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ'0) (Δ ,,, Δ'' ,,, lift_context #|Δ''| 0 Δ').

  Lemma All2_local_env_weaken_pred_ctx' {Σ Γ0 Γ'0 Δ Δ' Γ'' Δ''} ctx ctx' :
      #|Γ0| = #|Δ| → #|Γ0 ,,, Γ'0| = #|Δ ,,, Δ'| →
  pred1_ctx Σ Γ0 Δ →
  All2_local_env_over (pred1 Σ) Γ0 Δ Γ'' Δ'' →
  All2_local_env
    (on_decl
       (on_decl_over
          (fun (Γ Γ' : context) (t t0 : term) ⇒
           ∀ Γ1 Γ'1 : context,
           Γ = Γ1 ,,, Γ'1 →
           ∀ Δ0 Δ'0 : context,
           Γ' = Δ0 ,,, Δ'0 →
           #|Γ1| = #|Δ0| →
           ∀ Γ''0 Δ''0 : context,
           All2_local_env_over (pred1 Σ) Γ1 Δ0 Γ''0 Δ''0 →
           pred1 Σ (Γ1 ,,, Γ''0 ,,, lift_context #|Γ''0| 0 Γ'1) (Δ0 ,,, Δ''0 ,,, lift_context #|Δ''0| 0 Δ'0)
             (lift #|Γ''0| #|Γ'1| t) (lift #|Δ''0| #|Δ'0| t0)) (Γ0 ,,, Γ'0) (Δ ,,, Δ')))
    ctx ctx' →
  All2_local_env
    (on_decl
       (on_decl_over (pred1 Σ) (Γ0 ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ'0) (Δ ,,, Δ'' ,,, lift_context #|Δ''| 0 Δ')))
    (lift_context #|Γ''| #|Γ'0| ctx) (lift_context #|Δ''| #|Δ'| ctx').

  Lemma map_cofix_subst f mfix :
    (∀ n, tCoFix (map (map_def (f 0) (f #|mfix|)) mfix) n = f 0 (tCoFix mfix n)) →
    cofix_subst (map (map_def (f 0) (f #|mfix|)) mfix) =
    map (f 0) (cofix_subst mfix).

  Lemma map_fix_subst f mfix :
    (∀ n, tFix (map (map_def (f 0) (f #|mfix|)) mfix) n = f 0 (tFix mfix n)) →
    fix_subst (map (map_def (f 0) (f #|mfix|)) mfix) =
    map (f 0) (fix_subst mfix).

  Lemma weakening_pred1 Σ Γ Γ' Γ'' Δ Δ' Δ'' M N : wf Σ →
    pred1 Σ (Γ ,,, Γ') (Δ ,,, Δ') M N →
    #|Γ| = #|Δ| →
    All2_local_env_over (pred1 Σ) Γ Δ Γ'' Δ'' →
    pred1 Σ (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ')
          (Δ ,,, Δ'' ,,, lift_context #|Δ''| 0 Δ')
          (lift #|Γ''| #|Γ'| M) (lift #|Δ''| #|Δ'| N).

  Lemma weakening_pred1_pred1 Σ Γ Δ Γ' Δ' M N : wf Σ →
    All2_local_env_over (pred1 Σ) Γ Δ Γ' Δ' →
    pred1 Σ Γ Δ M N →
    pred1 Σ (Γ ,,, Γ') (Δ ,,, Δ') (lift0 #|Γ'| M) (lift0 #|Δ'| N).

  Lemma weakening_pred1_0 Σ Γ Δ Γ' M N : wf Σ →
    pred1 Σ Γ Δ M N →
    pred1 Σ (Γ ,,, Γ') (Δ ,,, Γ') (lift0 #|Γ'| M) (lift0 #|Γ'| N).

  Lemma All2_local_env_over_pred1_ctx Σ Γ Γ' Δ Δ' :
    #|Δ| = #|Δ'| →
    pred1_ctx Σ (Γ ,,, Δ) (Γ' ,,, Δ') →
    All2_local_env
      (on_decl (on_decl_over (pred1 Σ) Γ Γ')) Δ Δ'.

  Lemma nth_error_pred1_ctx_all_defs {P} {Γ Δ} :
    All2_local_env (on_decl P) Γ Δ →
    ∀ i body body', option_map decl_body (nth_error Γ i) = Some (Some body) →
              option_map decl_body (nth_error Δ i) = Some (Some body') →
              P (skipn (S i) Γ) (skipn (S i) Δ) body body'.

  Lemma All2_local_env_over_firstn_skipn:
    ∀ (Σ : global_env) (i : nat) (Δ' R : context),
      pred1_ctx Σ Δ' R →
      All2_local_env_over (pred1 Σ) (skipn i Δ') (skipn i R) (firstn i Δ') (firstn i R).

End ParallelWeakening.


Section ParallelSubstitution.
  Context {cf : checker_flags}.

  Inductive psubst Σ (Γ Γ' : context) : list term → list term → context → context → Type :=
  | psubst_empty : psubst Σ Γ Γ' [] [] [] []
  | psubst_vass Δ Δ' s s' na na' t t' T T' :
      psubst Σ Γ Γ' s s' Δ Δ' →
      pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') T T' →
      pred1 Σ Γ Γ' t t' →
      psubst Σ Γ Γ' (t :: s) (t' :: s') (Δ ,, vass na T) (Δ' ,, vass na' T')
  | psubst_vdef Δ Δ' s s' na na' t t' T T' :
      psubst Σ Γ Γ' s s' Δ Δ' →
      pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') T T' →
      pred1 Σ Γ Γ' (subst0 s t) (subst0 s' t') →
      psubst Σ Γ Γ' (subst0 s t :: s) (subst0 s' t' :: s') (Δ ,, vdef na t T) (Δ' ,, vdef na' t' T').

  Lemma psubst_length {Σ Γ Δ Γ' Δ' s s'} : psubst Σ Γ Δ s s' Γ' Δ' →
                                           #|s| = #|Γ'| ∧ #|s'| = #|Δ'| ∧ #|s| = #|s'|.

  Lemma psubst_length' {Σ Γ Δ Γ' Δ' s s'} : psubst Σ Γ Δ s s' Γ' Δ' → #|s'| = #|Γ'|.

  Lemma psubst_nth_error Σ Γ Δ Γ' Δ' s s' n t :
    psubst Σ Γ Δ s s' Γ' Δ' →
    nth_error s n = Some t →
    ∑ decl decl' t',
      (nth_error Γ' n = Some decl) ×
      (nth_error Δ' n = Some decl') ×
      (nth_error s' n = Some t') ×
    match decl_body decl, decl_body decl' with
    | Some d, Some d' ⇒
        let s2 := (skipn (S n) s) in
        let s2' := (skipn (S n) s') in
      let b := subst0 s2 d in
      let b' := subst0 s2' d' in
      psubst Σ Γ Δ s2 s2' (skipn (S n) Γ') (skipn (S n) Δ') ×
      (t = b) × (t' = b') × pred1 Σ Γ Δ t t'
    | None, None ⇒ pred1 Σ Γ Δ t t'
    | _, _ ⇒ False
    end.

  Lemma psubst_nth_error' Σ Γ Δ Γ' Δ' s s' n t :
    psubst Σ Γ Δ s s' Γ' Δ' →
    nth_error s n = Some t →
    ∑ t',
      (nth_error s' n = Some t') ×
      pred1 Σ Γ Δ t t'.

  Lemma psubst_nth_error_None Σ Γ Δ Γ' Δ' s s' n :
    psubst Σ Γ Δ s s' Γ' Δ' →
    nth_error s n = None →
    (nth_error Γ' n = None) × (nth_error Δ' n = None)* (nth_error s' n = None).

  Lemma subst_skipn' n s k t : k < n → (n - k) ≤ #|s| →
    lift0 k (subst0 (skipn (n - k) s) t) = subst s k (lift0 n t).

  Lemma split_app3 {A} (l l' l'' : list A) (l1 l1' l1'' : list A) :
    #|l| = #|l1| → #|l'| = #|l1'| →
        l ++ l' ++ l'' = l1 ++ l1' ++ l1'' →
        l = l1 ∧ l' = l1' ∧ l'' = l1''.

  Lemma All2_local_env_subst_ctx :
    ∀ (Σ : global_env) c c0 (Γ0 Δ : context)
    (Γ'0 : list context_decl) (Γ1 Δ1 : context) (Γ'1 : list context_decl) (s s' : list term),
      psubst Σ Γ0 Γ1 s s' Δ Δ1 →
      #|Γ'0| = #|Γ'1| →
      #|Γ0| = #|Γ1| →
      All2_local_env_over (pred1 Σ) Γ0 Γ1 Δ Δ1 →
     All2_local_env
      (on_decl
       (on_decl_over
          (fun (Γ Γ' : context) (t t0 : term) ⇒
           ∀ (Γ2 Δ0 : context) (Γ'2 : list context_decl),
           Γ = Γ2 ,,, Δ0 ,,, Γ'2 →
           ∀ (Γ3 Δ2 : context) (Γ'3 : list context_decl) (s0 s'0 : list term),
           psubst Σ Γ2 Γ3 s0 s'0 Δ0 Δ2 →
           Γ' = Γ3 ,,, Δ2 ,,, Γ'3 →
           #|Γ2| = #|Γ3| →
           #|Γ'2| = #|Γ'3| →
           All2_local_env_over (pred1 Σ) Γ2 Γ3 Δ0 Δ2 →
           pred1 Σ (Γ2 ,,, subst_context s0 0 Γ'2) (Γ3 ,,, subst_context s'0 0 Γ'3) (subst s0 #|Γ'2| t)
             (subst s'0 #|Γ'3| t0)) (Γ0 ,,, Δ ,,, Γ'0) (Γ1 ,,, Δ1 ,,, Γ'1))) c c0 →
  All2_local_env (on_decl (on_decl_over (pred1 Σ) (Γ0 ,,, subst_context s 0 Γ'0) (Γ1 ,,, subst_context s' 0 Γ'1)))
    (subst_context s #|Γ'0| c) (subst_context s' #|Γ'1| c0).