Library Eta
Require Import Untyped.
Require Import Subst.
Require Import Rels.
Require Import Relation_Operators.
Require Import Relation_Definitions.
Require Import Coq.Structures.Equalities.
Require Import Coq.Program.Equality.
Require Import Coq.Arith.Compare_dec.
Module Export Eta.
Require Import Subst.
Require Import Rels.
Require Import Relation_Operators.
Require Import Relation_Definitions.
Require Import Coq.Structures.Equalities.
Require Import Coq.Program.Equality.
Require Import Coq.Arith.Compare_dec.
Module Export Eta.
η-conversion
Inductive eta_prim : lterm → lterm → Prop :=
eta_base (f g: lterm): (f = shift 0 g) → eta_prim (Lam (App f (Var 0))) g.
We defined eta as the compatible closure of the primitive relation.
A couple of examples to make sure our definition works with at least
the basic cases:
Example ex1_eta : eta (\"x" ~> ((\"y" ~> `"y") $ `"x")) (\"x" ~> `"x").
apply clos_base. apply eta_base. unfold shift. auto.
Qed.
Example ex2_eta: eta (Lam (App (Lam (Lam (Var 1))) (Var 0))) (Lam (Lam (Var 1))).
Proof.
apply clos_base. apply eta_base. unfold shift. auto.
Qed.
Example ex3_eta: ¬ eta (Lam (App (Lam (Var 1)) (Var 0))) (Lam (Var 0)).
Proof.
unfold not. intros. inversion H.
inversion H0. discriminate.
inversion H2. inversion H3.
Qed.
We prove a couple of substitution lemmas regarding eta.
eta_prim is substitutive (as per Barendregt's definition)
Lemma eta_prim_substitutive:
∀ (M N L: lterm) (n: nat),
eta_prim M N → eta_prim (subst n L M) (subst n L N).
Proof.
intros.
assert (Sn_eq: n + 1 = S n). omega.
destruct H.
assert (HH: subst n L (Lam (App f (Var 0))) =
Lam (App (subst (S n) L f) (Var 0))).
simpl.
rewrite Sn_eq. auto.
rewrite HH.
apply eta_base.
unfold shift.
rewrite lift_lem2. simpl. rewrite H. rewrite Sn_eq.
unfold shift.
reflexivity. omega.
Qed.
Lemma eta_substitutive:
∀ (M N L: lterm) (n: nat),
eta M N → eta (subst n L M) (subst n L N).
Proof.
intros. generalize dependent n. generalize dependent L.
unfold eta.
induction H.
intros. apply clos_base. apply eta_prim_substitutive. assumption.
intros. apply clos_lam. apply IHclos_compat.
intros. apply clos_appl. apply IHclos_compat.
intros. apply clos_appr. apply IHclos_compat.
Qed.
Lemma eta_prim_lift_closed:
∀ M N, ∀ b k,
eta_prim M N → eta_prim (lift k b M) (lift k b N).
Proof.
intros.
generalize dependent b. generalize dependent k.
dependent induction H.
intros. rewrite H.
simpl.
case_eq (lt_dec 0 (b+1)).
intros.
unfold shift.
apply eta_base. unfold shift.
rewrite lift_lift_rev.
replace (b + 1 - 1) with b by omega. reflexivity.
omega.
intros. omega.
Qed.
Lemma eta_lift_closed:
∀ M N, ∀ b k,
eta M N → eta (lift k b M) (lift k b N).
Proof.
induction M.
intros.
inversion_clear H. inversion_clear H0.
intros.
inversion_clear H. apply eta_prim_lift_closed with (b := b) (k := k) in H0.
constructor. assumption.
simpl. apply clos_lam. apply IHM. assumption.
intros.
inversion_clear H. inversion_clear H0.
simpl. apply clos_appl. apply IHM1. assumption.
simpl. apply clos_appr. apply IHM2. assumption.
Qed.
Definition eta_star := clos_refl_trans lterm eta.
Definition eta_star_step := rt_step lterm eta.
Definition eta_star_refl := rt_refl lterm eta.
Definition eta_star_trans := rt_trans lterm eta.
Lemma eta_star_lam_closed:
∀ M N,
eta_star M N → eta_star (Lam M) (Lam N).
Proof.
intros.
dependent induction H.
constructor.
apply clos_lam in H. assumption. apply rt_refl.
apply rt_trans with (Lam y); assumption.
Qed.
Lemma eta_star_app_closed_l:
∀ M M' N,
eta_star M M' → eta_star (App M N) (App M' N).
Proof.
intros.
dependent induction H.
constructor. apply clos_appl. assumption.
apply rt_refl.
apply rt_trans with (App y N); assumption.
Qed.
Lemma eta_star_app_closed_r:
∀ M N N',
eta_star N N' → eta_star (App M N) (App M N').
Proof.
intros.
dependent induction H.
constructor. apply clos_appr. assumption.
apply rt_refl.
apply rt_trans with (App M y); assumption.
Qed.
Lemma eta_star_app_closed:
∀ M M' N N',
eta_star M M' → eta_star N N' → eta_star (App M N) (App M' N').
Proof.
intros ? ? ? ?. intros H1 H2.
apply rt_trans with (App M N').
apply eta_star_app_closed_r. assumption.
apply eta_star_app_closed_l. assumption.
Qed.
Additionally, eta_star is closed under lifting
Lemma eta_star_lift_closed:
∀ M N, ∀ k b,
eta_star M N → eta_star (lift k b M) (lift k b N).
Proof.
intros.
dependent induction H.
constructor. apply eta_lift_closed. assumption.
apply eta_star_refl.
apply eta_star_trans with (lift k b y).
assumption. assumption.
Qed.
Lemma eta_star_base_closed:
∀ M N N',
(M = shift 0 N) → eta_star N N' →
eta_star (Lam (App M (Var 0))) N'.
Proof.
intros.
rewrite H. clear H. clear M.
dependent induction H0.
apply rt_trans with (Lam (App (shift 0 y) (Var 0))).
apply eta_star_lam_closed. apply eta_star_app_closed.
apply eta_star_lift_closed. constructor. assumption.
apply rt_refl.
constructor. apply clos_base. apply eta_base. reflexivity.
constructor. apply clos_base. apply eta_base. reflexivity.
apply rt_trans with (Lam (App (shift 0 y) (Var 0))).
apply eta_star_lam_closed. apply eta_star_app_closed.
apply eta_star_lift_closed. assumption. apply rt_refl.
assumption.
Qed.
Parallel eta conversion
Inductive eta_par : lterm → lterm → Prop :=
| eta_par_var: ∀ n,
eta_par (Var n) (Var n)
| eta_par_lam: ∀ M M',
eta_par M M' → eta_par (Lam M) (Lam M')
| eta_par_app: ∀ M M' N N',
eta_par M M' → eta_par N N' → eta_par (App M N) (App M' N')
| eta_par_base: ∀ M N N',
(M = shift 0 N) → eta_par N N' →
eta_par (Lam (App M (Var 0))) N'.
Lemma eta_par_refl:
∀ t, eta_par t t.
Proof.
induction t.
constructor.
apply eta_par_lam.
assumption.
apply eta_par_app.
assumption. assumption.
Qed.
Parallel eta is closed under lifting
Lemma eta_par_lift_closed:
∀ M N, ∀ k b,
eta_par M N → eta_par (lift k b M) (lift k b N).
Proof.
intros.
generalize dependent k.
generalize dependent b.
dependent induction H.
intros. apply eta_par_refl.
simpl. intros. constructor. apply IHeta_par.
simpl. intros. constructor. apply IHeta_par1. apply IHeta_par2.
simpl. intros.
replace (b +1) with (S b) by omega. simpl.
unfold shift. replace (S b) with (b+1) by omega.
rewrite H.
apply eta_par_base with (lift k b N).
unfold shift. replace (S b) with (b+1) by omega.
rewrite lift_lift_rev. replace (b+1-1) with b by omega.
reflexivity. omega.
apply IHeta_par.
Qed.
eta_par is substitutive
Lemma eta_par_substitutive:
∀ (M N L: lterm) (n: nat),
eta_par M N → eta_par (subst n L M) (subst n L N).
Proof.
intros. generalize dependent n.
dependent induction H.
intros. apply eta_par_refl.
simpl. constructor. apply IHeta_par.
simpl. constructor. apply IHeta_par1. apply IHeta_par2.
intros.
simpl. replace (n+1) with (S n) by omega.
rewrite H. replace (S n) with (n+1) by omega.
rewrite <- lift_lem2.
apply eta_par_base with (subst n L N). reflexivity.
apply IHeta_par. omega.
Qed.
eta_par is fully closed under parallel substitution
Lemma eta_par_subst_closed:
∀ (M M' N N': lterm), ∀ n,
eta_par M M' → eta_par N N' → eta_par (subst n N M) (subst n N' M').
Proof.
intros. generalize dependent n.
dependent induction H. intros. simpl.
case_eq (nat_compare n n0).
intros.
apply eta_par_lift_closed. assumption.
intros. apply eta_par_refl.
intros. apply eta_par_refl.
intros. simpl. apply eta_par_lam. apply IHeta_par. assumption.
intros. simpl. apply eta_par_app. apply IHeta_par1. assumption.
apply IHeta_par2. assumption.
intros.
simpl. replace (n+1) with (S n) by omega. simpl.
rewrite H. simpl.
apply eta_par_base with (subst n N N0).
unfold shift. replace (S n) with (n+1) by omega.
rewrite lift_lem2. reflexivity.
omega.
apply IHeta_par. assumption.
Qed.
Lemma eta_imp_eta_par:
∀ M N, eta M N → eta_par M N.
Proof.
intros.
dependent induction H.
destruct H. apply eta_par_base with g. assumption.
apply eta_par_refl.
constructor. assumption.
constructor. assumption. apply eta_par_refl.
constructor. apply eta_par_refl. assumption.
Qed.
Lemma eta_par_imp_eta_star:
∀ M N,
eta_par M N → eta_star M N.
Proof.
intros.
dependent induction H.
apply rt_refl.
apply eta_star_lam_closed. assumption.
apply eta_star_app_closed; assumption.
apply eta_star_base_closed with N; assumption.
Qed.
The transitive closure of eta_par
Lemma eta_star_eq_closure_of_eta_par:
∀ M N,
eta_star M N ↔ eta_par_trans M N.
Proof.
split.
intros.
dependent induction H.
constructor. apply eta_imp_eta_par. assumption.
constructor. apply eta_par_refl.
apply t_trans with y; assumption.
intros.
dependent induction H.
apply eta_par_imp_eta_star. assumption.
apply rt_trans with y; assumption.
Qed.
Fixpoint lam_k (k: nat) (M: lterm) : lterm :=
match k with
| 0 ⇒ M
(*
Note: This should have probably been defined in a tail-recursive way, as:
(S n) ⇒ lam_k (App (shift 0 M) (Var 0))
since it is much easier to work with. However,
I realised this way too late, so left it this way in order to avoid
modifying existing proofs. Instead, an equivalence of these definitions
is proved in the lam_k_alt lemma.
*)
| (S n) ⇒ Lam (App (shift 0 (lam_k n M)) (Var 0))
end.
Lemma lam_k_alt:
∀ k, ∀ M,
lam_k (S k) M = lam_k k (Lam (App (shift 0 M) (Var 0))).
Proof.
induction k.
intros. simpl. reflexivity.
intros.
simpl. do 4 f_equal. rewrite <- IHk. simpl.
reflexivity.
Qed.
A trivial fact
This commutativity lemma which will be useful later.
Lemma shift_0_lam_commute:
∀ n, ∀ t,
shift 0 (lam_k n t) = (lam_k n (shift 0 t)).
Proof.
induction n.
(* n := 0 *)
simpl. reflexivity.
(* n := (S n) *)
intros. simpl. unfold shift. simpl.
f_equal. f_equal.
rewrite lift_fuse. simpl. rewrite <- IHn. unfold shift.
rewrite lift_fuse. simpl.
reflexivity. simpl. auto. simpl. auto.
Qed.
We now prove some basic properties about the relationship between eta
and lam_k. (This is Lemma 3.2 in the Takahashi paper.)
(* Lemma 3.2 (1) *)
Lemma eta_par_lam_k_var:
∀ M, ∀ n,
eta_par M (Var n) ↔ (∃ k, M = lam_k k (Var n)).
Proof.
intros. split.
(* -> *)
(* trivial induction on the definition of eta_par *)
intros.
dependent induction H.
∃ 0.
apply lam_k_zero.
destruct IHeta_par.
rewrite H.
∃ (S x). simpl. f_equal.
(* <- *)
intros.
(* clean up our hypothesis a bit *)
destruct H.
rewrite H.
clear H. clear M.
generalize dependent n.
generalize dependent x.
(* again, just perform simple induction on k *)
intro k.
induction k.
intros.
simpl.
apply eta_par_var.
intros.
simpl.
apply eta_par_base with (lam_k k (Var n)).
reflexivity.
apply IHk.
Qed.
(* Lemma 3.2 (2), the proof technique is essentially the same as for
eta_par_lam_k_var.
*)
Lemma eta_par_lam_k_app:
∀ M N_1 N_2,
eta_par M (App N_1 N_2)
↔
(∃ k, ∃ M_1 M_2,
(eta_par M_1 N_1) ∧ (eta_par M_2 N_2) ∧ M = lam_k k (App M_1 M_2)).
Proof.
split.
(* -> *)
intro.
dependent induction H.
∃ 0. simpl.
∃ M.
∃ N.
split.
assumption.
split.
assumption.
reflexivity.
destruct IHeta_par.
∃ (S x).
simpl.
destruct H as [M_1].
destruct H as [M_2].
∃ M_1.
∃ M_2.
split. destruct H.
assumption.
destruct H. destruct H1.
split. assumption.
apply f_equal.
f_equal. rewrite H2. reflexivity.
(* <- *)
intros.
destruct H as [k].
generalize dependent M.
generalize dependent N_1.
generalize dependent N_2.
induction k.
(* k := 0 *)
intros.
destruct H as [M_1].
destruct H as [M_2].
destruct H as [H1].
destruct H as [H2].
rewrite H.
simpl. apply eta_par_app. assumption. assumption.
(* k := (S k) *)
intros.
simpl in H.
destruct H as [M_1].
destruct H as [M_2].
destruct H as [H1].
destruct H as [H2].
rewrite H.
apply eta_par_base with (lam_k k (App M_1 M_2)).
reflexivity.
apply IHk.
∃ M_1.
∃ M_2.
split. assumption.
split. assumption.
reflexivity.
Qed.
(* Lemma 3.2 (3), the situation is again similar to the previous two
cases *)
Lemma eta_par_lam_k_lam:
∀ M N,
eta_par M (Lam N)
↔
(∃ k, ∃ M', (eta_par M' N) ∧ (M = lam_k k (Lam M'))).
Proof.
split.
(* -> *)
intro.
dependent induction H.
∃ 0. ∃ M.
split. assumption.
simpl. reflexivity.
destruct IHeta_par as [k].
destruct H as [M'].
destruct H as [H1].
∃ (S k).
∃ M'.
split. assumption.
simpl. rewrite H. f_equal.
(* <- *)
intros.
destruct H as [k].
generalize dependent M.
generalize dependent N.
induction k.
(* k := 0 *)
intros. destruct H as [M'].
destruct H as [H1].
rewrite H.
simpl. apply eta_par_lam. assumption.
(* k := (S k) *)
intros.
destruct H as [M'].
destruct H as [H1].
rewrite H.
simpl.
apply eta_par_base with (lam_k k (Lam M')).
reflexivity.
apply IHk.
∃ M'.
split. assumption.
reflexivity.
Qed.
Finally, we include this simple lemma which will be useful later.