Library CatSem.ULC.ULC_terms
Require Export CatSem.ULC.ULC_syntax.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Automatic Introduction.
Definition ULC_Y_h (V : TT) : ULC (V*) :=
Abs (App (Var (Some (None)))
(App (Var None)
(Var None))).
Definition ULC_Y (V : TT) : ULC V :=
Abs (App (ULC_Y_h _ ) (ULC_Y_h _ )).
Definition ULC_theta_h (V : TT) : ULC V :=
Abs(
Abs(
App
(Var None)
(App
(App
(Var (Some None))
(Var (Some None)))
(Var None))
)).
Definition ULC_theta (V : TT) : ULC V :=
App (ULC_theta_h V) (ULC_theta_h V).
Definition ULC_fix (V : TT) : ULC V :=
Abs (
App
(Abs
(App
(Var (Some None))
(App
(Var None)
(Var None))
))
(Abs
(App
(Var (Some None))
(App
(Var None)
(Var None))
))
).
Fixpoint ULC_Nat (n : nat) (V : TT) :
ULC V :=
match n with
| 0 => Abs (Abs (Var None))
| S n' =>
Abs(
Abs (
App
(Var (Some None))
(App
(App
(ULC_Nat n' _ )
(Var (Some None)))
(Var (None)))))
end.
Lemma ulc_nats_rename n :
forall (V W : TT) (f : V ---> W),
ULC_Nat n W = ULC_Nat n V //- f.
Proof.
induction n.
simpl.
intros.
unfold lift.
simpl.
auto.
simpl.
intros.
apply f_equal.
apply f_equal.
apply f_equal.
rewrite <- IHn.
auto.
Qed.
Lemma ulc_nats_subst n :
forall (V W : TT)
(f : V ---> ULC W),
ULC_Nat n W = ULC_Nat n V >>= f.
Proof.
induction n.
reflexivity.
simpl.
intros.
rewrite <- (IHn (V * *)).
reflexivity.
Qed.
Fixpoint pow n V (T : ULC V) : ULC V:=
match n return ULC V with
| 0 => Abs (Var None)
| S n' => Abs
(App
(inj T)
(App
(inj (pow n' T))
(Var (None))))
end.
Fixpoint ULC_nat_skel n V
(f : ULC V* )
(y : ULC V * * ) :
ULC V * * :=
match n with
| 0 => y
| S n' => App (inj f) (ULC_nat_skel n' f y)
end.
Definition ULC_nat_sk n V : ULC V* * :=
ULC_nat_skel n (Var None) (Var None).
Definition ULC_N n V : ULC V :=
Abs (Abs (ULC_nat_sk n V)).
Lemma ULC_nat_skel_rename_lift n V W
(f : V* ---> W*) a b :
ULC_nat_skel n a b //- (^f) =
ULC_nat_skel n (a//-f) (b//-^f).
Proof.
induction n.
reflexivity.
intros;
simpl in *.
apply App_eq;
auto.
unfold inj.
repeat rewrite rename_rename.
fin.
Qed.
Lemma ULC_nat_skel_rename_some n V
a b :
ULC_nat_skel n a b //- (Some (A:=V * *)) =
ULC_nat_skel n (inj a) (b //- Some (A:= V * * )).
Proof.
simpl.
intros.
induction n.
reflexivity.
simpl.
apply App_eq.
auto.
simpl.
auto.
Qed.
Lemma ULC_N_skel_subst_shift n V W
(f : V* ---> ULC W*) a b :
ULC_nat_skel n a b >>= (_shift f) =
ULC_nat_skel n (a>>= f) (b>>=(_shift f)).
Proof.
induction n.
reflexivity.
intros;
simpl in *.
apply App_eq;
auto.
unfold inj;
simpl.
rewrite rename_subst.
rewrite subst_rename.
fin.
Qed.
Lemma ULC_N_skel_substar n V (M : ULC (V* * ))
(a : ULC (V* * ))
(b:ULC V * * * ) :
inj (ULC_nat_skel n (a) b [*:= M]) =
( ULC_nat_skel n a ((inj (b[*:= M])))).
Proof.
induction n.
reflexivity.
simpl;
intros.
rewrite <- IHn.
unfold inj;
simpl.
apply App_eq;
auto.
rewrite subst_rename.
rewrite rename_subst.
simpl.
rewrite lift_rename.
auto.
Qed.
Lemma ULC_N_sk_rename n V W (f : V ---> W) :
ULC_nat_sk n V //- ^(^f) = ULC_nat_sk n _ .
Proof.
induction n.
reflexivity.
intros;
simpl in *.
apply App_eq.
auto.
rewrite IHn.
auto.
Qed.
Lemma ULC_N_sk_subst n V W (f : V ---> ULC W) :
ULC_nat_sk n V >>= _shift (_shift f) =
ULC_nat_sk n W .
Proof.
induction n.
reflexivity.
simpl.
intros.
rewrite IHn.
unfold inj.
simpl.
reflexivity.
Qed.
Lemma ULC_N_subst n V W (f : V ---> ULC W) :
ULC_N n V >>= f = ULC_N n W.
Proof.
simpl.
intros.
rewrite ULC_N_sk_subst.
auto.
Qed.
Lemma pow_rename (n: nat) (V W : TT)(f : V ---> W) T :
pow n T //- f = pow n (T //- f).
Proof.
induction n.
reflexivity.
intros;
simpl.
apply f_equal.
apply App_eq.
unfold inj; simpl.
repeat rewrite rename_rename;
fin.
apply App_eq.
unfold inj; simpl.
rewrite <- IHn.
repeat rewrite rename_rename;
fin.
fin.
Qed.
Lemma pow_subst (n: nat) (V W : TT)(f : V ---> ULC W) T :
pow n T >>= f = pow n (T >>= f).
Proof.
induction n.
reflexivity.
simpl.
intros.
apply f_equal.
apply App_eq.
unfold inj.
rewrite rename_subst.
rewrite subst_rename.
fin.
apply App_eq.
unfold inj.
rewrite <- IHn.
rewrite rename_subst.
rewrite subst_rename.
fin.
auto.
Qed.
Definition ULC_Nat_alt n V : ULC V :=
Abs (pow n (Var None)).
plus = \n.\m.\f.\x. n(f) (m(f)x)
SUCC := \nfx.f (n f x)
Definition ULCsucc V : ULC V :=
Abs (
Abs (
Abs (
App
(Var (Some None))
(App
(App
(Var (Some (Some None)))
(Var (Some None))
)
(Var None)
)))).
Abs (
Abs (
Abs (
App
(Var (Some None))
(App
(App
(Var (Some (Some None)))
(Var (Some None))
)
(Var None)
)))).
if then else = \a.\b.\c. a(b)(c)
Definition ULC_cond (V : TT) :=
Abs (V:=V)
( Abs (V:= V*)
( Abs (V:=V * * )
(
App (V:= V * * * )
(App (V:= V * * * )
(Var (V:= V * * * )
(Some (Some None)))
(Var (Some None)
))
(Var None)
)
)
)
.
Definition ULC_omega (V : TT) :=
Abs (V:= V)
( App (Var (None)) (Var (None))).
Definition ULC_True V : ULC V :=
Abs (Abs (Var (Some (None)))).
Definition ULC_False V : ULC V :=
Abs (Abs (Var (None))).
Definition ULC_zero (V : TT) :=
Abs (
App
(App
(Var (None (A:=V) ))
(Abs (ULC_False _)))
(ULC_True _ )).
Definition ULC_T V f : ULC V :=
Abs (
Abs (
App
(Var (None))
(App
(Var (Some(None)))
(inj (inj f))))
).
Lemma T_rename (V W : TT) (g : V ---> W) f :
ULC_T f //- g = ULC_T (f//-g).
Proof.
simpl.
unfold ULC_T.
intros.
repeat apply f_equal.
unfold inj;
simpl.
repeat rewrite rename_rename.
apply rename_eq.
simpl.
auto.
Qed.
Definition ULC_pred (V : TT) : ULC V :=
Abs (
Abs (
Abs (
App
(App
(App
(Var (Some(Some(None))))
(ULC_T (Var (Some (None))))
)
(Abs (Var (Some (None)))))
(Abs (Var (None)))
))).
Definition ULC_pred_alt (V : TT) : ULC V :=
Abs (
Abs (
Abs (
App
(App
(App
(Var (Some(Some (None))))
(Abs (
Abs (
App
(Var (None))
(App
(Var (Some (None)))
(Var (Some (Some (Some (None)))))
)))))
(Abs (Var (Some(None )))))
(Abs (Var (None)))
))).
Lemma ULC_pred_alt_correct V :
ULC_pred_alt V = ULC_pred V.
Proof.
reflexivity.
Qed.