Require Import Nat Bool List.

From PCF Require Import PCF.

Inductive value : form → Prop :=
  | v_bool :
      ∀ b,
        value (f_bool b)
  | v_nat :
      ∀ n,
        value (f_nat n)
  | v_star :
      value (f_star)
  | v_pair : ∀ t s,
      is_term t →
      is_term s →
      is_closed t →
      is_closed s →
      value (f_pair t s)
  | v_inl : ∀ t,
      is_term t →
      is_closed t →
      value (f_inl t)
  | v_inr : ∀ t,
      is_term t →
      is_closed t →
      value (f_inr t)
  | v_func :
      ∀ t,
        is_term t →
        is_closed (f_abs t) →
        value (f_abs t).

Inductive bigCBN : form → form → Prop :=
  | bigCBN_refl_nat :
      ∀ n,
        bigCBN (f_nat n) (f_nat n)
  | bigCBN_refl_bool :
      ∀ b,
        bigCBN (f_bool b) (f_bool b)
  | bigCBN_refl_star :
      bigCBN f_star f_star
  | bigCBN_refl_pair :
      ∀ t s,
        bigCBN (f_pair t s) (f_pair t s)
  | bigCBN_abs_refl :
      ∀ p,
        bigCBN (f_abs p) (f_abs p)
  | bigCBN_beta :
      ∀ p p' q r,
        bigCBN p (f_abs p') →
        bigCBN (subst p' 0 q) r →
        bigCBN (f_app p q) r
  | bigCBN_pair_fst :
      ∀ t p q r,
        bigCBN t (f_pair p q) →
        bigCBN p r →
        bigCBN (f_fst t) r
  | bigCBN_pair_snd :
      ∀ t p q r,
        bigCBN t (f_pair p q) →
        bigCBN q r →
        bigCBN (f_snd t) r
  | bigCBN_sum_case_inl :
      ∀ b b' p r q,
        bigCBN b (f_inl b') →
        bigCBN (subst p 0 b') r →
        bigCBN (f_case b p q) r
  | bigCBN_sum_case_inr :
      ∀ b b' p r q,
        bigCBN b (f_inr b') →
        bigCBN (subst q 0 b') r →
        bigCBN (f_case b p q) r
  | bigCBN_ite_true :
      ∀ b p r q,
        bigCBN b (f_bool true) →
        bigCBN p r →
        bigCBN (f_ite b p q) r
  | bigCBN_ite_false :
      ∀ b p r q,
        bigCBN b (f_bool false) →
        bigCBN q r →
        bigCBN (f_ite b p q) r
  | bigCBN_fix :
      ∀ f A r,
        bigCBN (f_app f (f_app (f_fix A) f)) r →
        bigCBN (f_app (f_fix A) f) r

  | bigCBN_leq :
      ∀ n1 n2 m p q,
        bigCBN p (f_nat n1) →
        bigCBN q (f_nat n2) →
        m = Nat.leb n1 n2 →
        bigCBN (f_leq p q) (f_bool m)
  | bigCBN_mul :
      ∀ n1 n2 m p q,
        bigCBN p (f_nat n1) →
        bigCBN q (f_nat n2) →
        m = n1 × n2 →
        bigCBN (f_mul p q) (f_nat m)
  | bigCBN_minus :
      ∀ n1 n2 m p q,
        bigCBN p (f_nat n1) →
        bigCBN q (f_nat n2) →
        m = n1 - n2 →
        bigCBN (f_minus p q) (f_nat m).