Module semantics

From Coq Require Import Classical.


Definition var: Type := nat.

Lemma var_eq: forall (v1 v2: var), {v1=v2} + {v1<>v2}.

Parameter const: Type.
Parameters zero one: const.

Inductive term: Type :=
  | Var: var -> term
  | Const: const -> term
  | Fun: var -> term -> term
  | App: term -> term -> term.

Fixpoint subst (x: var) (b: term) (a: term) {struct a}: term :=
  match a with
  | Var y => if var_eq x y then b else Var y
  | Const n => Const n
  | Fun y a1 => Fun y (if var_eq x y then a1 else subst x b a1)
  | App a1 a2 => App (subst x b a1) (subst x b a2)
  end.

Inductive isvalue: term -> Prop :=
  | isvalue_const: forall c,
      isvalue (Const c)
  | isvalue_fun: forall x a,
      isvalue (Fun x a).


Inductive eval: term -> term -> Prop :=
  | eval_const: forall c,
      eval (Const c) (Const c)
  | eval_fun: forall x a,
      eval (Fun x a) (Fun x a)
  | eval_app: forall a b x c vb v,
      eval a (Fun x c) ->
      eval b vb ->
      eval (subst x vb c) v ->
      eval (App a b) v.

Lemma eval_isvalue:
  forall a b, eval a b -> isvalue b.

Lemma eval_deterministic:
  forall a v, eval a v -> forall v', eval a v' -> v' = v.

Definition vx: var := 0.
Definition delta := Fun vx (App (Var vx) (Var vx)).
Definition omega := App delta delta.

Lemma not_eval_omega:
  forall v, ~(eval omega v).

CoInductive evalinf: term -> Prop :=
  | evalinf_app_l: forall a b,
      evalinf a ->
      evalinf (App a b)
  | evalinf_app_r: forall a b va,
      eval a va ->
      evalinf b ->
      evalinf (App a b)
  | evalinf_app_f: forall a b x c vb,
      eval a (Fun x c) ->
      eval b vb ->
      evalinf (subst x vb c) ->
      evalinf (App a b).

CoFixpoint evalinf_omega_1: evalinf omega :=
  let eval_delta : eval delta delta :=
    (eval_fun vx (App (Var vx) (Var vx))) in
  evalinf_app_f delta delta vx (App (Var vx) (Var vx)) delta
    eval_delta
    eval_delta
    evalinf_omega_1.

Lemma evalinf_omega: evalinf omega.

Lemma eval_evalinf_exclusive:
  forall a v, eval a v -> evalinf a -> False.

CoInductive coeval: term -> term -> Prop :=
  | coeval_const: forall c,
      coeval (Const c) (Const c)
  | coeval_fun: forall x a,
      coeval (Fun x a) (Fun x a)
  | coeval_app: forall a b x c vb v,
      coeval a (Fun x c) ->
      coeval b vb ->
      coeval (subst x vb c) v ->
      coeval (App a b) v.

Lemma eval_coeval:
  forall a v, eval a v -> coeval a v.

Lemma coeval_omega: forall v, coeval omega v.

Lemma coeval_noteval_evalinf:
  forall a v, coeval a v -> ~(eval a v) -> evalinf a.

Lemma coeval_eval_or_evalinf:
  forall a v, coeval a v -> eval a v \/ evalinf a.

Lemma not_evalinf_coeval:
  ~(forall a, evalinf a -> exists v, coeval a v).

Lemma eval_coeval_deterministic:
  forall a v, eval a v -> forall v', coeval a v' -> v' = v.

Lemma coeval_zerofun_omega:
  forall v, coeval (App (Fun vx (Const zero)) omega) v -> v = Const zero.


Inductive red1: term -> term -> Prop :=
  | red1_beta: forall x a v,
      isvalue v ->
      red1 (App (Fun x a) v) (subst x v a)
  | red1_app_l: forall a1 a2 b,
      red1 a1 a2 ->
      red1 (App a1 b) (App a2 b)
  | red1_app_r: forall v b1 b2,
      isvalue v ->
      red1 b1 b2 ->
      red1 (App v b1) (App v b2).

Definition notred (a: term) : Prop := forall b, ~(red1 a b).

Lemma value_notred:
  forall a, isvalue a -> notred a.

Lemma red1_deterministic:
  forall a b, red1 a b -> forall c, red1 a c -> c = b.

Inductive red: term -> term -> Prop :=
  | red_refl: forall a,
      red a a
  | red_step: forall a b c,
      red1 a b -> red b c -> red a c.

Lemma red_one: forall a b, red1 a b -> red a b.

Lemma red_trans: forall a b c, red a b -> red b c -> red a c.

CoInductive redinf: term -> Prop :=
  | redinf_intro: forall a b,
      red1 a b -> redinf b -> redinf a.

CoInductive cored: term -> term -> Prop :=
  | cored_refl: forall a,
      cored a a
  | cored_step: forall a b c,
      red1 a b -> cored b c -> cored a c.

Lemma cored_trans:
  forall a b c, cored a b -> cored b c -> cored a c.

Lemma red_cored:
  forall a b, red a b -> cored a b.

Lemma redinf_cored:
  forall a b, redinf a -> cored a b.

Lemma cored_notred_redinf:
  forall a b, cored a b -> ~(red a b) -> redinf a.

Lemma cored_red_or_redinf:
  forall a b, cored a b <-> red a b \/ redinf a.


Lemma red_app_l:
   forall a1 a2 b, red a1 a2 -> red (App a1 b) (App a2 b).

Lemma red_app_r:
   forall v a1 a2 , isvalue v -> red a1 a2 -> red (App v a1) (App v a2).

Lemma eval_red:
  forall a v, eval a v -> red a v.

Lemma eval_value:
  forall v, isvalue v -> eval v v.

Lemma red1_eval:
  forall a b, red1 a b -> forall v, eval b v -> eval a v.

Lemma red_eval:
  forall a v, red a v -> isvalue v -> eval a v.

Lemma infinite_progress_redinf:
  forall a,
  (forall b, red a b -> exists c, red1 b c) ->
  redinf a.

Lemma red_or_redinf:
  forall a,
  (exists b, red a b /\ notred b) \/ redinf a.

Lemma evalinf_red1:
  forall a, evalinf a -> exists b, red1 a b /\ evalinf b.

Lemma evalinf_redinf:
  forall a, evalinf a -> redinf a.

Lemma redinf_app_l:
  forall a a', red a a' ->
  forall b, redinf (App a b) -> redinf (App a' b).

Lemma redinf_app_r:
  forall b b', red b b' ->
  forall a, isvalue a -> redinf (App a b) -> redinf (App a b').

Lemma redinf_evalinf:
  forall a, redinf a -> evalinf a.

Lemma coeval_value:
  forall a v, isvalue a -> coeval a v -> a = v.

Lemma coeval_value_or_red1:
  forall a v, coeval a v ->
  isvalue a \/ exists b, red1 a b /\ coeval b v.

Lemma coeval_cored:
  forall a v, coeval a v -> cored a v.

Lemma not_cored_coeval:
  ~(forall a b, cored a b -> isvalue b -> coeval a b).