Set Implicit Arguments. Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A. Inductive var : Type := | varN : nat -> var. Inductive ty : Type := | tyN : ty (* nat *) | tyF : ty -> ty -> ty. (* function type *) Inductive tm : Type := | tmO : tm (* zero *) | tmS : tm -> tm (* successor *) | tmC : tm -> tm -> tm -> tm (* case *) | tmV : var -> tm (* variable *) | tmL : var -> ty -> tm -> tm (* lambda *) | tmA : tm -> tm -> tm (* application *) | tmF : tm -> tm. (* fix *) Module Example. (* fix f x y => match x with 0 => y | S x' => S (f x' y) end *) Definition f : var := varN 0. Definition x : var := varN 1. Definition y : var := varN 2. Definition x' : var := varN 3. Definition pcf_add : tm := tmF (tmL f (tyF tyN (tyF tyN tyN)) (tmL x tyN (tmL y tyN (tmC (tmV x) (tmV y) (tmL x' tyN (tmS (tmA (tmA (tmV f) (tmV x')) (tmV y)))))))). End Example. Inductive free (x : var) : tm -> Prop := | freeS t : free x t -> free x (tmS t) | freeC t t1 t2 : free x t \/ free x t1 \/ free x t2 -> free x (tmC t t1 t2) | freeV : free x (tmV x) | freeL y T t : x<>y -> free x t -> free x (tmL y T t) | freeA t1 t2 : free x t1 \/ free x t2 -> free x (tmA t1 t2) | freeF t : free x t -> free x (tmF t). Fixpoint eq_nat (x y : nat) : bool := match x, y with | 0, 0 => true | S x', S y' => eq_nat x' y' | _, _ => false end. Definition eq_var (x y : var) : bool := match x, y with varN x', varN y' => eq_nat x' y' end. Lemma eq_var_correct x y : eq_var x y = true <-> x = y. Proof. destruct x, y ; simpl ; split. revert n0 ; induction n ; intros n0 A ; destruct n0 ; inv A. reflexivity. apply IHn in H0 ; inv H0 ; reflexivity. revert n0 ; induction n ; intros n0 A ; destruct n0 ; inv A. reflexivity. firstorder. Qed. Fixpoint freeb (x : var) (t : tm) : bool := match t with | tmO => false | tmS t' => freeb x t' | tmC t0 t1 t2 => orb (freeb x t0) (orb (freeb x t1) (freeb x t2)) | tmV y => eq_var x y | tmL y _ t' => if eq_var x y then false else freeb x t' | tmA t1 t2 => orb (freeb x t1) (freeb x t2) | tmF t' => freeb x t' end. Fixpoint subst (t : tm) (x : var) (s : tm) : tm := match t with | tmO => t | tmS t' => tmS (subst t' x s) | tmC t0 t1 t2 => tmC (subst t0 x s) (subst t1 x s) (subst t2 x s) | tmV y => if eq_var x y then s else t | tmL y T t' => if eq_var x y then t else tmL y T (subst t' x s) | tmA t1 t2 => tmA (subst t1 x s) (subst t2 x s) | tmF t' => tmF (subst t' x s) end. Inductive nvalue : tm -> Prop := | nvalueO : nvalue tmO | nvalueS t : nvalue t -> nvalue (tmS t). Inductive value : tm -> Prop := | valueN t : nvalue t -> value t | valueL x T t : value (tmL x T t). Inductive step : tm -> tm -> Prop := | stepCO t1 t2 : step (tmC tmO t1 t2) t1 | stepCS t t1 t2 : nvalue t -> step (tmC (tmS t) t1 t2) t2 | stepA x T t s : value s -> step (tmA (tmL x T t) s) (subst t x s) | stepF x T t : step (tmF (tmL x T t)) (subst t x (tmF (tmL x T t))) | stepDS t t' : step t t' -> step (tmS t) (tmS t') | stepDC t t' t1 t2 : step t t' -> step (tmC t t1 t2) (tmC t' t1 t2) | stepDA t1 t1' t2 : step t1 t1' -> step (tmA t1 t2) (tmA t1' t2) | stepDAR x T t t2 t2' : step t2 t2' -> step (tmA (tmL x T t) t2) (tmA (tmL x T t) t2'). Inductive sem : tm -> tm -> Prop := | semV v : value v -> sem v v | semS t u : sem t u -> nvalue u -> sem (tmS t) (tmS u) | semCO t t1 t2 v : sem t tmO -> sem t1 v -> sem (tmC t t1 t2) v | semCS t t1 t2 u v : sem t (tmS u) -> sem (tmA t2 u) v -> sem (tmC t t1 t2) v | semA t1 t2 x T t v2 v : sem t1 (tmL x T t) -> sem t2 v2 -> sem (subst t x v2) v -> sem (tmA t1 t2) v | semF x T t v : sem (subst t x (tmF (tmL x T t))) v -> sem (tmF (tmL x T t)) v. Goal forall t t', sem t t' -> value t'. Proof. intros t t' A. induction A ; auto using value, nvalue. Qed.