Require Import Nat Bool List.

From PCF Require Import PCF.

Inductive value : form → Prop :=
  | v_abs :
      ∀ t,
        is_closed (f_abs t) →
        value (f_abs t)

  | v_star :
      value (f_star)
  | v_nat :
      ∀ n,
        value (f_nat n)

  | v_pair : ∀ t s,
      is_closed t →
      is_closed s →
      value (f_pair t s)

  | v_inl : ∀ t,
      is_closed t →
      value (f_inl t)
  | v_inr : ∀ t,
      is_closed t →
      value (f_inr t).

Inductive bigCBN : form → form → Prop :=
  | bigCBN_value :
      ∀ v,
        value v →
        bigCBN v v
  

  | bigCBN_app :
      ∀ p p' q r,
        bigCBN p (f_abs p') →
        bigCBN (subst p' 0 q) r →
        bigCBN (f_app p q) r

  | bigCBN_fst :
      ∀ t p q r,
        bigCBN t (f_pair p q) →
        bigCBN p r →
        bigCBN (f_fst t) r
  | bigCBN_snd :
      ∀ t p q r,
        bigCBN t (f_pair p q) →
        bigCBN q r →
        bigCBN (f_snd t) r

  | bigCBN_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_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_fix :
      ∀ f A r,
        bigCBN (f_app f (f_app (f_fix A) f)) r →
        bigCBN (f_app (f_fix A) f) 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_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).

Theorem bigCBN_reduces_to_value :
  ∀ p v,
    bigCBN p v →
    value v.
Proof.
  induction 1 as
  [v H1
  |p p' q r H1 IH1 H2 IH2

  |t p q r H1 IH1 H2 IH2
  |t p q r H1 IH1 H2 IH2

  |b b' p r q H1 IH1 H2 IH2
  |b b' p r q H1 IH1 H2 IH2

  |f A r H1 IH1

  |b p r q H1 IH1 H2 IH2
  |b p r q H1 IH1 H2 IH2

  |n1 n2 m p q H1 IH1 H2 IH2 H3
  |n1 n2 m p q H1 IH1 H2 IH2 H3
  |n1 n2 m p q H1 IH1 H2 IH2 H3
  ];
  eauto using bigCBN, value; destruct m; constructor; reflexivity.
Qed.

Theorem bigCBN_bool :
  ∀ b,
    bigCBN (f_bool b) (f_bool b).
Proof.
  intros [|]; do 2 constructor; reflexivity.
Qed.