Library MetaCoq.Erasure.Prelim

Module PA := PCUICAst.
Module P := PCUICWcbvEval.


Lemma nth_error_app_inv X (x : X) n l1 l2 :
  nth_error (l1 ++ l2) n = Some x → (n < #|l1| ∧ nth_error l1 n = Some x) ∨ (n ≥ #|l1| ∧ nth_error l2 (n - List.length l1) = Some x).

Lemma monad_map_All2 (X Y : Type) (f : X → typing_result Y) (l1 : list X) (a1 : list Y) :
  monad_map f l1 = ret a1 → All2 (fun a b ⇒ f a = ret b) l1 a1.

Lemma monad_map_Forall2 (X Y : Type) (f : X → typing_result Y) (l1 : list X) (a1 : list Y) :
  monad_map f l1 = Checked a1 → Forall2 (fun a b ⇒ f a = Checked b) l1 a1.

Lemma monad_map_length X Y (f : X → typing_result Y) (l1 : list X) a :
  monad_map f l1 = Checked a → #|l1| = #|a|.

Lemma monad_map_app X Y (f : X → typing_result Y) (l1 l2 : list X) a1 a2 :
  monad_map f l1 = Checked a1 → monad_map f l2 = Checked a2 → monad_map f (l1 ++ l2) = Checked (a1 ++ a2)%list.

Lemma monad_map_app_invs X Y (f : X → typing_result Y) (l1 l2 : list X) a :
  monad_map f (l1 ++ l2) = Checked a → ∃ a1 a2, monad_map f l1 = Checked a1 ∧ monad_map f l2 = Checked a2 ∧ (a = a1 ++ a2)%list.

Lemma typing_spine_inv_app Σ x0 l x x1 :
  PCUICGeneration.typing_spine Σ [] x0 (l ++ [x]) x1 → { '(x2, x3) : _ & (PCUICGeneration.typing_spine Σ [] x0 l x2) × (Σ ;;; [] |- x : x3)}%type.

Lemma typing_spine_inv args arg a Σ x2 x3 :
  nth_error args (arg) = Some a →
  PCUICGeneration.typing_spine Σ [] x2 args x3 →
  {T & Σ;;; [] |- a : T}.

Theorem subject_reduction_eval : ∀ (Σ : PCUICAst.global_env_ext) Γ t u T,
  wf Σ → Σ ;;; Γ |- t : T → PCUICWcbvEval.eval Σ Γ t u → Σ ;;; Γ |- u : T.

Lemma typing_spine_eval:
  ∀ (Σ : global_env_ext) Γ (args args' : list PCUICAst.term) (X : All2 (PCUICWcbvEval.eval Σ Γ) args args') (bla : wf Σ)
    (T x x0 : PCUICAst.term) (t0 : typing_spine Σ Γ x args x0) (c : Σ;;; Γ |- x0 ≤ T) (x1 : PCUICAst.term)
    (c0 : Σ;;; Γ |- x1 ≤ x), isWfArity_or_Type Σ Γ T → typing_spine Σ Γ x1 args' T.

Lemma emkApps_snoc a l b :
  EAst.mkApps a (l ++ [b]) = EAst.tApp (EAst.mkApps a l) b.

Lemma mkApps_snoc a l b :
  PCUICAst.mkApps a (l ++ [b]) = PCUICAst.tApp (PCUICAst.mkApps a l) b.

Lemma mkAppBox_repeat n a :
  mkAppBox a n = EAst.mkApps a (repeat tBox n).

Lemma All2_right_triv {A B} {l : list A} {l' : list B} P :
  All P l' → #|l| = #|l'| → All2 (fun _ b ⇒ P b) l l'.

Lemma All_repeat {A} {n P} x :
  P x → @All A P (repeat x n).

Lemma Alli_impl {A} {P Q} (l : list A) {n} : Alli P n l → (∀ n x, P n x → Q n x) → Alli Q n l.

Lemma All2_map_left {A B C} (P : A → C → Type) l l' (f : B → A) :
  All2 (fun x y ⇒ P (f x) y) l l' → All2 P (map f l) l'.

Lemma All2_map_right {A B C} (P : A → C → Type) l l' (f : B → C) :
  All2 (fun x y ⇒ P x (f y)) l l' → All2 P l (map f l').

Lemma Forall2_Forall_right {A B} {P : A → B → Prop} {Q : B → Prop} {l l'} :
  Forall2 P l l' →
  (∀ x y, P x y → Q y) →
  Forall Q l'.

Lemma All2_from_nth_error A B L1 L2 (P : A → B → Type) :
  #|L1| = #|L2| →
                (∀ n x1 x2, n < #|L1| → nth_error L1 n = Some x1
                                      → nth_error L2 n = Some x2
                                      → P x1 x2) →
                All2 P L1 L2.

Lemma All2_nth_error {A B} {P : A → B → Type} {l l'} n t t' :
  All2 P l l' →
  nth_error l n = Some t →
  nth_error l' n = Some t' →
  P t t'.

Lemma All_In X (P : X → Type) (l : list X) x : All P l → In x l → squash (P x).

Lemma nth_error_skipn A l m n (a : A) :
  nth_error l (m + n) = Some a →
  nth_error (skipn m l) n = Some a.

Lemma decompose_app_rec_inv2 {t l' f l} :
  decompose_app_rec t l' = (f, l) →
  isApp f = false.

Module Ee := EWcbvEval.

Lemma fst_decompose_app_rec t l : fst (EAstUtils.decompose_app_rec t l) = fst (EAstUtils.decompose_app t).

Lemma value_app_inv L :
  Ee.value (EAst.mkApps tBox L) →
  L = nil.

Lemma fix_subst_nth mfix n :
  n < #|mfix| →
  nth_error (fix_subst mfix) n = Some (tFix mfix (#|mfix| - n - 1)).

Lemma efix_subst_nth mfix n :
  n < #|mfix| →
  nth_error (ETyping.fix_subst mfix) n = Some (EAst.tFix mfix (#|mfix| - n - 1)).

Lemma subslet_fix_subst `{cf : checker_flags} Σ mfix1 T n :
  wf Σ.1 →
  Σ ;;; [] |- tFix mfix1 n : T →
  
  subslet Σ [] (PCUICTyping.fix_subst mfix1) (PCUICLiftSubst.fix_context mfix1).

Inductive red_decls Σ Γ Γ' : ∀ (x y : PCUICAst.context_decl), Type :=
| conv_vass na na' T T' : isType Σ Γ' T' → red Σ Γ T T' →
                      red_decls Σ Γ Γ' (PCUICAst.vass na T) (PCUICAst.vass na' T')

| conv_vdef_type na na' b T T' : isType Σ Γ' T' → red Σ Γ T T' →
                             red_decls Σ Γ Γ' (PCUICAst.vdef na b T) (PCUICAst.vdef na' b T')

| conv_vdef_body na na' b b' T : isType Σ Γ' T →
                                 Σ ;;; Γ' |- b' : T → red Σ Γ b b' →
                                                  red_decls Σ Γ Γ' (PCUICAst.vdef na b T) (PCUICAst.vdef na' b' T).

Notation red_context Σ := (context_relation (red_decls Σ)).

Lemma conv_context_app (Σ : global_env_ext) (Γ1 Γ2 Γ1' : context) :
  wf Σ →
  wf_local Σ (Γ1 ,,, Γ2) →
  conv_context Σ Γ1 Γ1' → conv_context Σ (Γ1 ,,, Γ2) (Γ1' ,,, Γ2).