Section Measure.

  Context {cf : checker_flags}.

  Context (flags : RedFlags.t).
  Context (Σ : global_env_ext).

  Definition R_aux Γ :=
    dlexprod (cored Σ Γ) (@posR).

  Definition R Γ u v :=
    R_aux Γ (zip u ; stack_pos (fst u) (snd u))
            (zip v ; stack_pos (fst v) (snd v)).

  Lemma cored_wellformed :
    ∀ {Γ u v},
      ∥ wf Σ ∥ → wellformed Σ Γ u →
      cored (fst Σ) Γ v u →
      wellformed Σ Γ v.

  Lemma red_wellformed :
    ∀ {Γ u v},
      ∥ wf Σ ∥ → wellformed Σ Γ u →
      ∥ red (fst Σ) Γ u v ∥ →
      wellformed Σ Γ v.

  Corollary R_Acc_aux :
    ∀ Γ t p,
      wf Σ → wellformed Σ Γ t →
      Acc (R_aux Γ) (t ; p).


  Corollary R_Acc :
    ∀ Γ t,
      wf Σ → wellformed Σ Γ (zip t) →
      Acc (R Γ) t.

  Lemma R_positionR :
    ∀ Γ t1 t2 (p1 : pos t1) (p2 : pos t2),
      t1 = t2 →
      positionR (` p1) (` p2) →
      R_aux Γ (t1 ; p1) (t2 ; p2).

  Definition Req Γ t t' :=
    t = t' ∨ R Γ t t'.

  Lemma Rtrans :
    ∀ Γ u v w,
      R Γ u v →
      R Γ v w →
      R Γ u w.

  Lemma Req_trans :
    ∀ {Γ}, transitive (Req Γ).

  Lemma R_to_Req :
    ∀ {Γ u v},
      R Γ u v →
      Req Γ u v.

  Instance Req_refl : ∀ Γ, Reflexive (Req Γ).

  Lemma R_Req_R :
    ∀ {Γ u v w},
      R Γ u v →
      Req Γ v w →
      R Γ u w.

End Measure.

Section Reduce.

  Context {cf : checker_flags}.

  Context (flags : RedFlags.t).

  Context (Σ : global_env_ext).
  Context (hΣ : ∥ wf Σ ∥).



  Definition inspect {A} (x : A) : { y : A | y = x } := exist x eq_refl.

  Definition Pr (t' : term × stack) π :=
    snd (decompose_stack π) = snd (decompose_stack (snd t')).

  Notation givePr := (_) (only parsing).

  Definition Pr' (t' : term × stack) :=
    isApp (fst t') = false ∧
    (RedFlags.beta flags → isLambda (fst t') → isStackApp (snd t') = false).

  Notation givePr' := (conj _ (fun β hl ⇒ _)) (only parsing).

  Notation rec reduce t π :=
    (let smaller := _ in
     let '(exist res (conj prf (conj h (conj h1 h2)))) := reduce t π smaller in
     exist res (conj (Req_trans _ _ _ _ _ (R_to_Req _ smaller)) (conj givePr givePr'))
    ) (only parsing).

  Notation give t π :=
    (exist (t,π) (conj _ (conj givePr givePr'))) (only parsing).

  Tactic Notation "zip" "fold" "in" hyp(h) :=
    lazymatch type of h with
    | context C[ zipc ?t ?π ] ⇒
      let C' := context C[ zip (t,π) ] in
      change C' in h
    end.

  Tactic Notation "zip" "fold" :=
    lazymatch goal with
    | |- context C[ zipc ?t ?π ] ⇒
      let C' := context C[ zip (t,π) ] in
      change C'
    end.

  Lemma Req_red :
    ∀ Γ x y,
      Req Σ Γ y x →
      ∥ red Σ Γ (zip x) (zip y) ∥.



  Obligation Tactic := obTac.

  Equations discr_construct (t : term) : Prop :=
    discr_construct (tConstruct ind n ui) := False ;
    discr_construct _ := True.

  Inductive construct_view : term → Set :=
  | view_construct : ∀ ind n ui, construct_view (tConstruct ind n ui)
  | view_other : ∀ t, discr_construct t → construct_view t.

  Equations construct_viewc t : construct_view t :=
    construct_viewc (tConstruct ind n ui) := view_construct ind n ui ;
    construct_viewc t := view_other t I.

  Equations red_discr (t : term) (π : stack) : Prop :=
    red_discr (tRel _) _ := False ;
    red_discr (tLetIn _ _ _ _) _ := False ;
    red_discr (tConst _ _) _ := False ;
    red_discr (tApp _ _) _ := False ;
    red_discr (tLambda _ _ _) (App _ _) := False ;
    red_discr (tFix _ _) _ := False ;
    red_discr (tCase _ _ _ _) _ := False ;
    red_discr (tProj _ _) _ := False ;
    red_discr _ _ := True.

  Inductive red_view : term → stack → Set :=
  | red_view_Rel c π : red_view (tRel c) π
  | red_view_LetIn A b B c π : red_view (tLetIn A b B c) π
  | red_view_Const c u π : red_view (tConst c u) π
  | red_view_App f a π : red_view (tApp f a) π
  | red_view_Lambda na A t a args : red_view (tLambda na A t) (App a args)
  | red_view_Fix mfix idx π : red_view (tFix mfix idx) π
  | red_view_Case ind par p c brs π : red_view (tCase (ind, par) p c brs) π
  | red_view_Proj p c π : red_view (tProj p c) π
  | red_view_other t π : red_discr t π → red_view t π.

  Equations red_viewc t π : red_view t π :=
    red_viewc (tRel c) π := red_view_Rel c π ;
    red_viewc (tLetIn A b B c) π := red_view_LetIn A b B c π ;
    red_viewc (tConst c u) π := red_view_Const c u π ;
    red_viewc (tApp f a) π := red_view_App f a π ;
    red_viewc (tLambda na A t) (App a args) := red_view_Lambda na A t a args ;
    red_viewc (tFix mfix idx) π := red_view_Fix mfix idx π ;
    red_viewc (tCase (ind, par) p c brs) π := red_view_Case ind par p c brs π ;
    red_viewc (tProj p c) π := red_view_Proj p c π ;
    red_viewc t π := red_view_other t π I.

  Equations discr_construct_cofix (t : term) : Prop :=
    discr_construct_cofix (tConstruct ind n ui) := False ;
    discr_construct_cofix (tCoFix mfix idx) := False ;
    discr_construct_cofix _ := True.

  Inductive construct_cofix_view : term → Set :=
  | ccview_construct : ∀ ind n ui, construct_cofix_view (tConstruct ind n ui)
  | ccview_cofix : ∀ mfix idx, construct_cofix_view (tCoFix mfix idx)
  | ccview_other : ∀ t, discr_construct_cofix t → construct_cofix_view t.

  Equations cc_viewc t : construct_cofix_view t :=
    cc_viewc (tConstruct ind n ui) := ccview_construct ind n ui ;
    cc_viewc (tCoFix mfix idx) := ccview_cofix mfix idx ;
    cc_viewc t := ccview_other t I.

  Equations _reduce_stack (Γ : context) (t : term) (π : stack)
            (h : wellformed Σ Γ (zip (t,π)))
            (reduce : ∀ t' π', R Σ Γ (t',π') (t,π) →
                               { t'' : term × stack | Req Σ Γ t'' (t',π') ∧ Pr t'' π' ∧ Pr' t'' })
    : { t' : term × stack | Req Σ Γ t' (t,π) ∧ Pr t' π ∧ Pr' t' } :=

    _reduce_stack Γ t π h reduce with red_viewc t π := {

    | red_view_Rel c π with RedFlags.zeta flags := {
      | true with inspect (nth_error (Γ ,,, stack_context π) c) := {
        | @exist None eq := False_rect _ _ ;
        | @exist (Some d) eq with inspect d.(decl_body) := {
          | @exist None _ := give (tRel c) π ;
          | @exist (Some b) H := rec reduce (lift0 (S c) b) π
          }
        } ;
      | false := give (tRel c) π
      } ;

    | red_view_LetIn A b B c π with RedFlags.zeta flags := {
      | true := rec reduce (subst10 b c) π ;
      | false := give (tLetIn A b B c) π
      } ;

    | red_view_Const c u π with RedFlags.delta flags := {
      | true with inspect (lookup_env (fst Σ) c) := {
        | @exist (Some (ConstantDecl _ {| cst_body := Some body |})) eq :=
          let body' := subst_instance_constr u body in
          rec reduce body' π ;
        | @exist (Some (InductiveDecl _ _)) eq := False_rect _ _ ;
        | @exist (Some _) eq := give (tConst c u) π ;
        | @exist None eq := False_rect _ _
        } ;
      | _ := give (tConst c u) π
      } ;

    | red_view_App f a π := rec reduce f (App a π) ;

    | red_view_Lambda na A t a args with inspect (RedFlags.beta flags) := {
      | @exist true eq1 := rec reduce (subst10 a t) args ;
      | @exist false eq1 := give (tLambda na A t) (App a args)
      } ;

    | red_view_Fix mfix idx π with RedFlags.fix_ flags := {
      | true with inspect (unfold_fix mfix idx) := {
        | @exist (Some (narg, fn)) eq1 with inspect (decompose_stack_at π narg) := {
          | @exist (Some (args, c, ρ)) eq2 with inspect (reduce c (Fix mfix idx args ρ) _) := {
            | @exist (@exist (t, ρ') prf) eq3 with construct_viewc t := {
              | view_construct ind n ui with inspect (decompose_stack ρ') := {
                | @exist (l, θ) eq4 :=
                  rec reduce fn (appstack args (App (mkApps (tConstruct ind n ui) l) ρ))
                } ;
              | view_other t ht := give (tFix mfix idx) π
              }
            } ;
          | _ := give (tFix mfix idx) π
          } ;
        | _ := give (tFix mfix idx) π
        } ;
      | false := give (tFix mfix idx) π
      } ;

    | red_view_Case ind par p c brs π with RedFlags.iota flags := {
      | true with inspect (reduce c (Case (ind, par) p brs π) _) := {
        | @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
          | @exist (args, ρ) prf' with cc_viewc t := {
            | ccview_construct ind' c' _ := rec reduce (iota_red par c' args brs) π ;
            | ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
              | @exist (Some (narg, fn)) eq' :=
                rec reduce (tCase (ind, par) p (mkApps fn args) brs) π ;
              | @exist None bot := False_rect _ _
              } ;
            | ccview_other t ht := give (tCase (ind, par) p (mkApps t args) brs) π
            }
          }
        } ;
      | false := give (tCase (ind, par) p c brs) π
      } ;

    | red_view_Proj (i, pars, narg) c π with RedFlags.iota flags := {
      | true with inspect (reduce c (Proj (i, pars, narg) π) _) := {
        | @exist (@exist (t,π') prf) eq with inspect (decompose_stack π') := {
          | @exist (args, ρ) prf' with cc_viewc t := {
            | ccview_construct ind' c' _
              with inspect (nth_error args (pars + narg)) := {
              | @exist (Some arg) eqa := rec reduce arg π ;
              | @exist None eqa := False_rect _ _
              } ;
            | ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
              | @exist (Some (narg, fn)) eq' :=
                rec reduce (tProj (i, pars, narg) (mkApps fn args)) π ;
              | @exist None bot := False_rect _ _
              } ;
            | ccview_other t ht := give (tProj (i, pars, narg) (mkApps t args)) π
            }
          }
        } ;
      | false := give (tProj (i, pars, narg) c) π
      } ;

    | red_view_other t π discr := give t π

    }.










Section Acc_sidecond_generator.
  Context {A : Type} {R : A → A → Prop} {P : A → Prop}.
  Variable Pimpl : ∀ x y, P x → R y x → P y.
  Fixpoint Acc_intro_generator n (acc : ∀ t, P t → Acc R t) : ∀ t, P t → Acc R t :=
    match n with
        | O ⇒ acc
        | S n ⇒ fun x Px ⇒
                   Acc_intro x (fun y Hy ⇒ Acc_intro_generator n (Acc_intro_generator n acc) y (Pimpl _ _ Px Hy))
    end.

End Acc_sidecond_generator.

  Lemma wellformed_R_pres Γ :
    ∀ x y : term × stack, wellformed Σ Γ (zip x) → R Σ Γ y x → wellformed Σ Γ (zip y).

  Equations reduce_stack_full (Γ : context) (t : term) (π : stack)
           (h : wellformed Σ Γ (zip (t,π))) : { t' : term × stack | Req Σ Γ t' (t, π) ∧ Pr t' π ∧ Pr' t' } :=
    reduce_stack_full Γ t π h :=
      Fix_F (R := R Σ Γ)
            (fun x ⇒ wellformed Σ Γ (zip x) → { t' : term × stack | Req Σ Γ t' x ∧ Pr t' (snd x) ∧ Pr' t' })
            (fun t' f ⇒ _) (x := (t, π)) _ _.

  Definition reduce_stack Γ t π h :=
    let '(exist ts _) := reduce_stack_full Γ t π h in ts.

  Lemma reduce_stack_Req :
    ∀ Γ t π h,
      Req Σ Γ (reduce_stack Γ t π h) (t, π).

  Theorem reduce_stack_sound :
    ∀ Γ t π h,
      ∥ red (fst Σ) Γ (zip (t, π)) (zip (reduce_stack Γ t π h)) ∥.

  Lemma reduce_stack_decompose :
    ∀ Γ t π h,
      snd (decompose_stack (snd (reduce_stack Γ t π h))) =
      snd (decompose_stack π).

  Lemma reduce_stack_context :
    ∀ Γ t π h,
      stack_context (snd (reduce_stack Γ t π h)) =
      stack_context π.

  Definition isred (t : term × stack) :=
    isApp (fst t) = false ∧
    (isLambda (fst t) → isStackApp (snd t) = false).

  Lemma reduce_stack_isred :
    ∀ Γ t π h,
      RedFlags.beta flags →
      isred (reduce_stack Γ t π h).

  Lemma reduce_stack_noApp :
    ∀ Γ t π h,
      isApp (fst (reduce_stack Γ t π h)) = false.

  Lemma reduce_stack_noLamApp :
    ∀ Γ t π h,
      RedFlags.beta flags →
      isLambda (fst (reduce_stack Γ t π h)) →
      isStackApp (snd (reduce_stack Γ t π h)) = false.

  Definition reduce_term Γ t (h : wellformed Σ Γ t) :=
    zip (reduce_stack Γ t ε h).

  Theorem reduce_term_sound :
    ∀ Γ t h,
      ∥ red (fst Σ) Γ t (reduce_term Γ t h) ∥.

  Lemma Ind_canonicity :
    ∀ Γ ind uni args t,
      Σ ;;; Γ |- t : mkApps (tInd ind uni) args →
      RedFlags.iota flags →
      let '(u,l) := decompose_app t in
      (isLambda u → l = []) →
      whnf flags Σ Γ u →
      discr_construct u →
      whne flags Σ Γ u.

  Scheme Acc_ind' := Induction for Acc Sort Prop.

  Lemma Fix_F_prop :
    ∀ A R P f (pred : ∀ x : A, P x → Prop) x hx,
      (∀ x aux, (∀ y hy, pred y (aux y hy)) → pred x (f x aux)) →
      pred x (@Fix_F A R P f x hx).

  Lemma reduce_stack_prop :
    ∀ Γ t π h (P : term × stack → term × stack → Prop),
      (∀ t π h aux,
          (∀ t' π' hR, P (t', π') (` (aux t' π' hR))) →
          P (t, π) (` (_reduce_stack Γ t π h aux))) →
      P (t, π) (reduce_stack Γ t π h).

  Lemma reduce_stack_whnf :
    ∀ Γ t π h,
      let '(u, ρ) := reduce_stack Γ t π h in
      whnf flags Σ (Γ ,,, stack_context ρ) (zipp u ρ).

  Lemma reduce_stack_whnf :
    ∀ Γ t π h,
      whnf flags Σ (Γ ,,, stack_context (snd (reduce_stack Γ t π h)))
           (fst (reduce_stack Γ t π h)).

End Reduce.