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

Definition isFixApp t :=
  match fst (decompose_app t) with
  | tFix _ _ ⇒ true
  | _ ⇒ 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_declarations).

  Inductive eval : term → term → Prop :=
  

  | eval_box a t t' :
      eval a tBox →
      eval t t' →
      eval (tApp a t) tBox

  

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

  

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

  

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

  

  | eval_iota_sing ind pars discr brs n f res :
      eval discr tBox →
      brs = [ (n,f) ] →
      eval (mkApps f (repeat tBox n)) res →
      eval (tCase (ind, pars) discr brs) 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_or_box narg args' →
      

      S narg = #|args| →
      
      Forall2 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) →
      
      Forall2 eval args args' →
      isStuckFix (tFix mfix idx) args' →
      eval (mkApps f args) (mkApps (tFix mfix idx) args')

  

  | red_cofix_case ip mfix idx args narg fn brs res :
      unfold_cofix mfix idx = Some (narg, fn) →
      eval (tCase ip (mkApps fn args) brs) res →
      eval (tCase ip (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_delta c decl body (isdecl : declared_constant Σ c decl) res :
      decl.(cst_body) = Some body →
      eval body res →
      eval (tConst c) res

  

  | eval_proj i pars arg discr args k res :
      eval discr (mkApps (tConstruct i k) args) →
      eval (List.nth (pars + arg) args tDummy) res →
      eval (tProj (i, pars, arg) discr) res

  

  | eval_proj_box i pars arg discr :
      eval discr tBox →
      eval (tProj (i, pars, arg) discr) tBox

  

  | eval_app_cong f f' a a' :
      eval f f' →
      ~~ (isLambda f' || isFixApp f' || isBox f') →
      eval a a' →
      eval (tApp f a) (tApp f' a')

  

  
  
  


  

  | eval_atom t : atom t → eval t t.


  Definition eval_evals_ind :
    ∀ P : term → term → Prop,
      (∀ a t t', eval a tBox → P a tBox → eval t t' → P t t' → eval (tApp a t) tBox → P (tApp a t) tBox ) →
      (∀ (f : term) (na : name) (b a a' res : term),
          eval f (tLambda na b) →
          P f (tLambda na b) → eval a a' → P a a' → eval (b {0 := a'}) res → P (b {0 := a'}) res → P (tApp f a) res) →
      (∀ (na : name) (b0 b0' b1 res : term),
          eval b0 b0' → P b0 b0' → eval (b1 {0 := b0'}) res → P (b1 {0 := b0'}) res → P (tLetIn na b0 b1) res) →
      (∀ (c : ident) (decl : constant_body) (body : term),
          declared_constant Σ c decl →
          ∀ (res : term),
            cst_body decl = Some body →
            eval body res → P body res → P (tConst c) res) →
      (∀ (ind : inductive) (pars : nat) (discr : term) (c : nat)
              (args : list term) (brs : list (nat × term)) (res : term),
          eval discr (mkApps (tConstruct ind c) args) →
          P discr (mkApps (tConstruct ind c) args) →
          eval (iota_red pars c args brs) res → P (iota_red pars c args brs) res → P (tCase (ind, pars) discr brs) res) →
      (∀ ind pars discr brs n f res,
          eval discr tBox → P discr tBox →
          brs = [(n, f)] →
          eval (mkApps f (repeat tBox n)) res → P (mkApps f (repeat tBox n)) res →
          eval (tCase (ind, pars) discr brs) res → P (tCase (ind, pars) discr brs) res
      ) →
      (∀ (i : inductive) (pars arg : nat) (discr : term) (args : list term) (k : nat)
              (a res : term),
          eval discr (mkApps (tConstruct i k) args) →
          P discr (mkApps (tConstruct i k) args) →
          eval (nth (pars + arg) args tDummy) res → P (nth (pars + arg) args tDummy) res → P (tProj (i, pars, arg) discr) res) →
      (∀ i pars arg discr,
          eval discr tBox → P discr tBox →
          eval (tProj (i, pars, arg) discr) tBox → P (tProj (i, pars, arg) discr) tBox
      ) →
      (∀ 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_or_box narg args' →
          S narg = #|args| →
          Forall2 eval args args' →
          Forall2 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) →
          Forall2 eval args args' →
          Forall2 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) (args : list term)
              (narg : nat) (fn : term) (brs : list (nat × term)) (res : term),
          unfold_cofix mfix idx = Some (narg, fn) →
          eval (tCase ip (mkApps fn args) brs) res →
          P (tCase ip (mkApps fn args) brs) res → P (tCase ip (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) →
      (∀ f11 f' a a' : term,
          eval f11 f' → P f11 f' → ~~ (isLambda f' || isFixApp f' || isBox f') → eval a a' → P a a' → P (tApp f11 a) (tApp 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.

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

  Lemma value_values_ind : ∀ P : term → Prop,
      (∀ t, atom t → P t) →
      (∀ t l, value_head t → Forall value l → Forall P l → P (mkApps t l)) →
      (∀ f args,
          Forall value args →
          Forall 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 ∧ Forall value l) ∨ (isStuckFix t l ∧ Forall value l).

  Lemma value_head_spec t :
    value_head t = (~~ (isLambda t || isFix t || isBox t)) && atom t.

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

  Lemma Forall_app_inv {A} (P : A → Prop) l l' : Forall P l → Forall P l' → Forall P (l ++ l').

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
























End Wcbv.