Lemma lookup_env_cst_inv {Σ c k cst} :
  lookup_env Σ c = Some (ConstantDecl k cst) → c = k.

Definition atom t :=
  match t with
  | tConstruct _ _ _
  | tFix _ _
  | tCoFix _ _
  | tLambda _ _ _
  | tSort _
  | tProd _ _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isArityHead t :=
  match t with
  | tSort _
  | tProd _ _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isEvar t :=
  match t with
  | tEvar _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isFix t :=
  match t with
  | tFix _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isFixApp t :=
  match fst (decompose_app t) with
  | tFix _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isCoFix t :=
  match t with
  | tCoFix _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isConstruct t :=
  match t with
  | tConstruct _ _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isAssRel Γ x :=
  match x with
  | tRel i ⇒
    match option_map decl_body (nth_error Γ i) with
    | Some None ⇒ true
    | _ ⇒ false
    end
  | _ ⇒ false
  end.

Definition isAxiom Σ x :=
  match x with
  | tConst c u ⇒
    match lookup_env Σ c with
    | Some (ConstantDecl _ {| cst_body := None |}) ⇒ true
    | _ ⇒ false
    end
  | _ ⇒ false
  end.

Definition isStuckFix t args :=
  match t with
  | tFix mfix idx ⇒
    match unfold_fix mfix idx with
    | Some (narg, fn) ⇒
      ~~ is_constructor narg args
    | None ⇒ false
    end
  | _ ⇒ false
  end.

Lemma atom_mkApps f l : atom (mkApps f l) → (l = []) ∧ atom f.

Section Wcbv.
  Context (Σ : global_env) (Γ : context).

  Inductive eval : term → term → Type :=
  

  | eval_beta f na t b a a' l res :
      eval f (tLambda na t b) →
      eval a a' →
      eval (mkApps (subst10 a' b) l) res →
      eval (tApp f (a :: l)) res

  

  | eval_zeta na b0 b0' t b1 res :
      eval b0 b0' →
      eval (subst10 b0' b1) res →
      eval (tLetIn na b0 t b1) res

  

  | eval_rel_def i body res :
      option_map decl_body (nth_error Γ i) = Some (Some body) →
      eval (lift0 (S i) body) res →
      eval (tRel i) res

  | eval_rel_undef i :
      option_map decl_body (nth_error Γ i) = Some None →
      eval (tRel i) (tRel i)

  

  | eval_delta c decl body (isdecl : declared_constant Σ c decl) u res :
      decl.(cst_body) = Some body →
      eval (subst_instance_constr u body) res →
      eval (tConst c u) res

  

  | eval_axiom c decl (isdecl : declared_constant Σ c decl) u :
      decl.(cst_body) = None →
      eval (tConst c u) (tConst c u)

  

  | eval_iota ind pars discr c u args p brs res :
      eval discr (mkApps (tConstruct ind c u) args) →
      eval (iota_red pars c args brs) res →
      eval (tCase (ind, pars) p discr brs) res

  

  | eval_proj i pars arg discr args k u a res :
      eval discr (mkApps (tConstruct i k u) args) →
      nth_error args (pars + arg) = Some a →
      eval a res →
      eval (tProj (i, pars, arg) discr) res

  

  | eval_fix f mfix idx args args' narg fn res :
      eval f (tFix mfix idx) →
      unfold_fix mfix idx = Some (narg, fn) →
      
      is_constructor narg args' →
      

      S narg = #|args| →
      
      All2 eval args args' →
      eval (mkApps fn args') res →
      eval (mkApps f args) res

  

  | eval_fix_value f mfix idx args args' :
      eval f (tFix mfix idx) →
      
      All2 eval args args' →
      isStuckFix (tFix mfix idx) args' →
      eval (mkApps f args) (mkApps (tFix mfix idx) args')

  

  | red_cofix_case ip mfix idx p args narg fn brs res :
      unfold_cofix mfix idx = Some (narg, fn) →
      eval (tCase ip p (mkApps fn args) brs) res →
      eval (tCase ip p (mkApps (tCoFix mfix idx) args) brs) res

  

  | red_cofix_proj p mfix idx args narg fn res :
      unfold_cofix mfix idx = Some (narg, fn) →
      eval (tProj p (mkApps fn args)) res →
      eval (tProj p (mkApps (tCoFix mfix idx) args)) res

  

  | eval_app_cong f f' a a' :
      ~~ isApp f → ~~ is_empty a →
      eval f f' →
      ~~ (isLambda f' || isFixApp f' || isArityHead f') →
      All2 eval a a' →
      eval (tApp f a) (mkApps f' a')

  

  
  
  


  

  | eval_atom t : atom t → eval t t.

  Definition eval_evals_ind :
    ∀ P : term → term → Type,
      (∀ (f : term) (na : name) t b a a' l res,
          eval f (tLambda na t b) →
          P f (tLambda na t b) → eval a a' → P a a' →
          eval (mkApps (b {0 := a'}) l) res → P (mkApps (b {0 := a'}) l) res →
          P (tApp f (a :: l)) res) →
      (∀ (na : name) (b0 b0' t b1 res : term),
          eval b0 b0' → P b0 b0' → eval (b1 {0 := b0'}) res → P (b1 {0 := b0'}) res → P (tLetIn na b0 t b1) res) →
      (∀ (i : nat) (body res : term),
          option_map decl_body (nth_error Γ i) = Some (Some body) →
          eval ((lift0 (S i)) body) res → P ((lift0 (S i)) body) res → P (tRel i) res) →
      (∀ i : nat, option_map decl_body (nth_error Γ i) = Some None → P (tRel i) (tRel i)) →
      (∀ (c : ident) (decl : constant_body) (body : term),
          declared_constant Σ c decl →
          ∀ (u : universe_instance) (res : term),
            cst_body decl = Some body →
            eval (subst_instance_constr u body) res → P (subst_instance_constr u body) res → P (tConst c u) res) →
      (∀ (c : ident) (decl : constant_body),
          declared_constant Σ c decl → ∀ u : universe_instance, cst_body decl = None → P (tConst c u) (tConst c u)) →
      (∀ (ind : inductive) (pars : nat) (discr : term) (c : nat) (u : universe_instance)
              (args : list term) (p : term) (brs : list (nat × term)) (res : term),
          eval discr (mkApps (tConstruct ind c u) args) →
          P discr (mkApps (tConstruct ind c u) args) →
          eval (iota_red pars c args brs) res → P (iota_red pars c args brs) res → P (tCase (ind, pars) p discr brs) res) →
      (∀ (i : inductive) (pars arg : nat) (discr : term) (args : list term) (k : nat) (u : universe_instance)
              (a res : term),
          eval discr (mkApps (tConstruct i k u) args) →
          P discr (mkApps (tConstruct i k u) args) →
          nth_error args (pars + arg) = Some a → eval a res → P a res → P (tProj (i, pars, arg) discr) res) →
      (∀ f (mfix : mfixpoint term) (idx : nat) (args args' : list term) (narg : nat) (fn res : term),
          eval f (tFix mfix idx) →
          P f (tFix mfix idx) →
          unfold_fix mfix idx = Some (narg, fn) →
          is_constructor narg args' →
          S narg = #|args| →
          All2 eval args args' →
          All2 P args args' →
          eval (mkApps fn args') res → P (mkApps fn args') res → P (mkApps f args) res) →
      (∀ f (mfix : mfixpoint term) (idx : nat) (args args' : list term),
          eval f (tFix mfix idx) →
          P f (tFix mfix idx) →
          All2 eval args args' →
          All2 P args args' →
          isStuckFix (tFix mfix idx) args' → P (mkApps f args) (mkApps (tFix mfix idx) args')) →
      (∀ (ip : inductive × nat) (mfix : mfixpoint term) (idx : nat) (p : term) (args : list term)
              (narg : nat) (fn : term) (brs : list (nat × term)) (res : term),
          unfold_cofix mfix idx = Some (narg, fn) →
          eval (tCase ip p (mkApps fn args) brs) res →
          P (tCase ip p (mkApps fn args) brs) res → P (tCase ip p (mkApps (tCoFix mfix idx) args) brs) res) →
      (∀ (p : projection) (mfix : mfixpoint term) (idx : nat) (args : list term) (narg : nat) (fn res : term),
          unfold_cofix mfix idx = Some (narg, fn) →
          eval (tProj p (mkApps fn args)) res →
          P (tProj p (mkApps fn args)) res → P (tProj p (mkApps (tCoFix mfix idx) args)) res) →
      (∀ f f' a a',
          ~~ isApp f → ~~ is_empty a →
          eval f f' → P f f' →
          ~~ (isLambda f' || isFixApp f' || isArityHead f') →
          All2 eval a a' → All2 P a a' → P (tApp f a) (mkApps f' a')) →
      (∀ t : term, atom t → P t t) → ∀ t t0 : term, eval t t0 → P t t0.

  Definition value_head x :=
    isConstruct x || isCoFix x || isAssRel Γ x || isAxiom Σ x.


  Inductive value : term → Type :=
  | value_atom t : atom t → value t
  | value_app t l : value_head t → All value l → value (mkApps t l)
  | value_stuck_fix f args : All value args → isStuckFix f args → value (mkApps f args).

  Lemma value_values_ind : ∀ P : term → Type,
      (∀ t, atom t → P t) →
      (∀ t l, value_head t → All value l → All P l → P (mkApps t l)) →
      (∀ f args,
          All value args →
          All P args →
          isStuckFix f args →
          P (mkApps f args)) →
      ∀ t : term, value t → P t.

  Lemma value_head_nApp {t} : value_head t → ~~ isApp t.

  Lemma isStuckfix_nApp {t args} : isStuckFix t args → ~~ isApp t.

  Lemma atom_nApp {t} : atom t → ~~ isApp t.

  Lemma value_mkApps_inv t l :
    ~~ isApp t →
    value (mkApps t l) →
    ((l = []) × atom t) + (value_head t × All value l) + (isStuckFix t l × All value l).

  Lemma isFixApp_mkApps f args : ~~ isApp f → isFixApp (mkApps f args) = isFixApp f.

  Lemma eval_to_value e e' : eval e e' → value e'.

  Lemma value_head_spec t :
    implb (value_head t) (~~ (isLambda t || isFixApp t || isArityHead t)).

  Lemma value_head_final t :
    value_head t →
    ~~ (isLambda t || isFixApp t || isArityHead t) →
    eval t t.

  Lemma value_final e : value e → eval e e.






  Lemma eval_atom_inj t t' : atom t → eval t t' → t = t'.

  Lemma eval_LetIn {n b ty t v} :
    eval (tLetIn n b ty t) v →
    ∑ b',
      eval b b' × eval (t {0 := b'}) v.

  Lemma eval_Const {c u v} :
    eval (tConst c u) v →
    ∑ decl, declared_constant Σ c decl ×
                 match cst_body decl with
                 | Some body ⇒ eval (subst_instance_constr u body) v
                 | None ⇒ v = tConst c u
                 end.









Lemma All2_app_inv_l :
  ∀ A B R l1 l2 r,
    @All2 A B R (l1 ++ l2) r →
    ∑ r1 r2,
      (r = r1 ++ r2)%list ×
      All2 R l1 r1 ×
      All2 R l2 r2.

  Lemma eval_mkApps_cong f f' l l' :
    ~~ isApp f →
    eval f f' →
    value_head f' →
    All2 eval l l' →
    eval (mkApps f l) (mkApps f' l').

End Wcbv.

Conjecture closed_typed_wcbeval : ∀ {cf : checker_flags} (Σ : global_env_ext) t T,
    Σ ;;; [] |- t : T → ∑ u, eval (fst Σ) [] t u.

Tactic Notation "redt" uconstr(y) := eapply (transitivity (R:=red _ _) (y:=y)).