Skip to content

I'm trying to formalize System-T #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
timmykill wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

I'm trying to formalize System-T #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d11e7e0
tried (failed) to prove strong normalization for System-T
Dec 5, 2024
1368801
added beta reduction of n, still stuck on the strong normalization
Dec 6, 2024
6d614e4
proved church rosser for system-T
Dec 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
233 changes: 191 additions & 42 deletions theories/SimplyTypedLambdaCalculus/ChurchRosser.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,38 @@ Inductive par_red: term -> term -> Prop :=
App (Lam s) t >=> s'.[t'/]

| ParRed_Var (v: var): (Var v) >=> (Var v)


| ParRed_0 : Const_0 >=> Const_0

| ParRed_S (n n' : term):
n >=> n'
-> Const_S n >=> Const_S n'

| ParRed_App (s s' t t': term) :
s >=> s' ->
t >=> t' ->
App s t >=> App s' t'

| ParRed_Lam (t t': term) :
t >=> t' ->
Lam t >=> Lam t'

| ParRed_R (t0 t0' tn tn' n n' : term) :
t0 >=> t0'
-> tn >=> tn'
-> n >=> n'
-> Rec t0 tn n >=> Rec t0' tn' n'

| ParRed_R0 (t0 t0' tn : term) :
t0 >=> t0'
-> Rec t0 tn Const_0 >=> t0'

| ParRed_RN (t0 t0' tn tn' n n' : term) :
t0 >=> t0'
-> tn >=> tn'
-> n >=> n'
-> Rec t0 tn (Const_S n) >=> App (App tn' n') (Rec t0' tn' n')

where "t >=> t'" := (par_red t t').

Notation "R *" := (clos_refl_trans _ R)
Expand All @@ -43,6 +66,17 @@ Fixpoint par_red_max_reduction (t: term): term :=
| App (Lam t) u => (par_red_max_reduction t).[(par_red_max_reduction u)/]
| App t u => App (par_red_max_reduction t) (par_red_max_reduction u)
| Lam t => Lam (par_red_max_reduction t)
| Const_0 => Const_0
| Const_S n => Const_S (par_red_max_reduction n)
| Rec t0 tn (Const_S n) =>
App (App (par_red_max_reduction tn) (par_red_max_reduction n))
(Rec (par_red_max_reduction t0)
(par_red_max_reduction tn)
(par_red_max_reduction n))
| Rec t0 tn Const_0 => par_red_max_reduction t0
| Rec t0 tn n => (Rec (par_red_max_reduction t0)
(par_red_max_reduction tn)
(par_red_max_reduction n))
end.

Definition replace_lambda (f: term -> term) (s u: term): term :=
Expand All @@ -60,6 +94,9 @@ Proof.
- apply ParRed_App; assumption.
- apply ParRed_Lam.
assumption.
- constructor.
- constructor. assumption.
- apply ParRed_R; assumption.
Qed.

Lemma beta_star_refl (t: term):
Expand Down Expand Up @@ -110,6 +147,12 @@ Proof.
- apply ParRed_App; [ apply par_red_refl | assumption ].
- apply ParRed_Lam.
assumption.
- constructor. assumption.
- constructor. apply par_red_refl.
- constructor; apply par_red_refl.
- constructor; [assumption | apply par_red_refl .. ].
- constructor; [apply par_red_refl | assumption | apply par_red_refl].
- constructor; [apply par_red_refl .. | assumption ].
Qed.

Lemma par_red_subst (t t': term) (sigma: var -> term):
Expand All @@ -120,19 +163,33 @@ Proof.
revert sigma.
induction H as [
s s' t t' par_red_s_s' IHs par_red_t_t' IHt
| v
| | | t t' H IH
| s s' t t' par_red_s_s' IHs par_red_t_t' IHt
| s s' par_red_s_s' IHs
| t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
| t0 t0' ts H IH
| t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
]; intros sigma.
- asimpl.
pose proof (ParRed_Subst s.[up sigma] s'.[up sigma] t.[sigma] t'.[sigma]) as H.
asimpl in H.
apply H; [ apply IHs | apply IHt ].
- apply par_red_refl.
- apply par_red_refl.
- constructor. apply IH.
- apply ParRed_App; [ apply IHs | apply IHt ].
- apply ParRed_Lam.
asimpl.
apply IHs.
- specialize (IH1 sigma).
specialize (IH2 sigma).
specialize (IH3 sigma).
constructor; assumption.
- constructor. apply IH.
- specialize (IH1 sigma).
specialize (IH2 sigma).
specialize (IH3 sigma).
constructor; assumption.
Qed.

Lemma par_red_subst_up_equivalence (sigma sigma': var -> term):
Expand All @@ -155,9 +212,12 @@ Proof.
revert sigma sigma' Hv.
induction H as [
s s' t t' _ IHs _ IHt
| v
| | | n n' H IH
| s s' t t' _ IHs _ IHt
| s s' _ IHs
| t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
| t0 t0' ts H IH
| t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
]; intros sigma sigma' Hv.
- asimpl.
pose proof (ParRed_Subst s.[up sigma] s'.[up sigma'] t.[sigma] t'.[sigma']) as H.
Expand All @@ -168,10 +228,10 @@ Proof.
assumption.
+ apply IHt.
assumption.
- asimpl.
apply Hv.
- asimpl.
apply ParRed_App.
- asimpl. apply Hv.
- asimpl. constructor.
- asimpl. constructor. apply IH. apply Hv.
- apply ParRed_App.
+ apply IHs.
assumption.
+ apply IHt.
Expand All @@ -181,6 +241,15 @@ Proof.
apply IHs.
apply par_red_subst_up_equivalence.
assumption.
- specialize (IH1 sigma sigma' Hv).
specialize (IH2 sigma sigma' Hv).
specialize (IH3 sigma sigma' Hv).
asimpl. constructor; assumption.
- asimpl. constructor. apply IH. apply Hv.
- specialize (IH1 sigma sigma' Hv).
specialize (IH2 sigma sigma' Hv).
specialize (IH3 sigma sigma' Hv).
asimpl. constructor; assumption.
Qed.

Lemma beta_star_app_r (s s' t: term):
Expand Down Expand Up @@ -233,34 +302,96 @@ Proof.
assumption.
Qed.

(* TODO: generalize
Inductive sub_term: term -> term -> Prop :=
| Sub_app1 (t1 t2: term) : sub_term t1 (App t1 t2)
| Sub_app2 (t1 t2: term) : sub_term t2 (App t1 t2)
| Sub_lam (t: term) : sub_term t (Lam t)
| Sub_S (s : term) : sub_term s (Const_S s)
| Sub_R0 (t0 ts n: term) : sub_term t0 (Rec t0 ts n)
| Sub_RS (t0 ts n: term) : sub_term ts (Rec t0 ts n)
| Sub_RN (t0 ts n: term) : sub_term n (Rec t0 ts n).
*)

Lemma beta_star_lam (s s': term):
s ~>* s' ->
Lam s ~>* Lam s'.
Proof.
intros beta_star_s_s'.
induction beta_star_s_s' as [ s s' H | x | x y z IHxy IHAppxy IHyz IHAppyz ].
- induction H; apply rt_step, Beta_Lam.
+ apply Beta_Subst.
assumption.
+ apply Beta_AppL.
assumption.
+ apply Beta_AppR.
assumption.
+ apply Beta_Lam.
assumption.
- induction H; apply rt_step, Beta_Lam; constructor; assumption.
- apply rt_refl.
- apply rt_trans with (y := Lam y); assumption.
Qed.
Qed.

Lemma beta_star_const (s s': term):
s ~>* s' ->
Const_S s ~>* Const_S s'.
Proof.
intros beta_star_s_s'.
induction beta_star_s_s' as [ s s' H | x | x y z IHxy IHAppxy IHyz IHAppyz ].
- induction H; apply rt_step; constructor; constructor; assumption.
- apply rt_refl.
- apply rt_trans with (y := Const_S y); assumption.
Qed.

Lemma beta_star_R0 (t0 t0' tn n: term):
t0 ~>* t0' ->
Rec t0 tn n ~>* Rec t0' tn n.
Proof.
intros H.
induction H.
* apply rt_step. constructor. assumption.
* apply rt_refl.
* apply rt_trans with (y := Rec y tn n); assumption.
Qed.

Lemma beta_star_RS (t0 tn tn' n: term):
tn ~>* tn' ->
Rec t0 tn n ~>* Rec t0 tn' n.
Proof.
intros H.
induction H as [ | | ? y ].
* apply rt_step. constructor. assumption.
* apply rt_refl.
* apply rt_trans with (y := Rec t0 y n); assumption.
Qed.

Lemma beta_star_RN (t0 tn n n': term):
n ~>* n' ->
Rec t0 tn n ~>* Rec t0 tn n'.
Proof.
intros H.
induction H as [ | | ? y ].
* apply rt_step. constructor. assumption.
* apply rt_refl.
* apply rt_trans with (y := Rec t0 tn y); assumption.
Qed.

Lemma beta_star_R (t0 t0' tn tn' n n': term):
t0 ~>* t0' ->
tn ~>* tn' ->
n ~>* n' ->
Rec t0 tn n ~>* Rec t0' tn' n'.
Proof.
intros.
apply rt_trans with (y := Rec t0' tn' n); [| apply beta_star_RN; assumption].
apply rt_trans with (y := Rec t0' tn n); [| apply beta_star_RS; assumption].
apply beta_star_R0; assumption.
Qed.

Lemma par_red_to_beta_star (s t : term):
s >=> t -> s ~>* t.
Proof.
intros H.
induction H as [
s s' t t' _ beta_star_s_s' _ beta_star_t_t'
| v
| | | n n' H IH
| s s' t t' _ beta_star_s_s' _ beta_star_t_t'
| s s' _ beta_star_s_s'
| t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
| t0 t0' ts H IH
| t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
].
- apply rt_trans with (y := App (Lam s') t).
+ apply beta_star_app.
Expand All @@ -273,9 +404,18 @@ Proof.
apply Beta_Subst.
reflexivity.
- apply rt_refl.
- apply rt_refl.
- apply beta_star_const. assumption.
- apply beta_star_app; assumption.
- apply beta_star_lam.
assumption.
- apply beta_star_R; assumption.
- apply rt_trans with (y := Rec t0' ts Const_0).
* apply beta_star_R0. assumption.
* apply rt_step. constructor.
- apply rt_trans with (y := Rec t0' tn' (Const_S n')).
* apply beta_star_R; [ | | apply beta_star_const]; assumption.
* apply rt_step. constructor.
Qed.

Lemma beta_star_equiv_par_red_star (s t: term):
Expand All @@ -302,23 +442,16 @@ Lemma lam_match : forall (s u : term) (f : term -> term),
((replace_lambda f s u) = u /\ ~exists s', s = Lam s').
Proof.
intros s u f.
destruct s as [ n | s1 s2 | s ].
- right.
split.
+ simpl.
reflexivity.
+ intros [ t eq_t ].
discriminate.
- right.
destruct s as [ | | s | | | ].
3:{
simpl.
split.
+ reflexivity.
+ intros [ t eq_t ].
discriminate.
- simpl.
left.
exists s.
split; reflexivity.
}
all: right.
all: simpl.
all: split; [reflexivity | intros [ ? ? ]; discriminate].
Qed.

Lemma max_par_red (t t': term):
Expand All @@ -327,9 +460,9 @@ Proof.
intros Ht.
induction Ht as [
s s' t t' _ IHs _ IHt
| v
| | |
| s s' t t' par_red_s_s' IHs _ IHt
| s s' _ IHs
| s s' _ IHs | | |
]; asimpl.
- apply par_red_subst_par_red.
+ intros v.
Expand All @@ -339,22 +472,38 @@ Proof.
* asimpl.
apply par_red_refl.
+ assumption.
- apply par_red_refl.
- constructor.
- constructor.
- constructor; assumption.
- set (f := fun s' => (par_red_max_reduction s').[par_red_max_reduction t/]).
destruct (lam_match s (App (par_red_max_reduction s) (par_red_max_reduction t)) f) as [ [ u [ H1 H2 ] ] | [ H1 H2 ] ]; subst.
+ inversion par_red_s_s'; subst.
inversion IHs; subst.
apply ParRed_Subst; assumption.
+ destruct s as [ n | s1 s2 | s ]; simpl in IHs.
* simpl.
apply ParRed_App; assumption.
* apply ParRed_App; assumption.
* exfalso.
+ destruct s as [ n | s1 s2 | s | | | ]; simpl in IHs.
3:{
exfalso.
apply H2.
exists s.
reflexivity.
- apply ParRed_Lam.
assumption.
}
all: simpl in *; constructor; assumption.
- constructor; assumption.
- destruct n.
+ simpl in *; constructor; assumption.
+ simpl in *; constructor; assumption.
+ simpl in *; constructor; assumption.
+ inversion Ht3; subst.
apply ParRed_R0.
assumption.
+ inversion Ht3; subst.
apply ParRed_RN; [ assumption .. | ].
inversion IHHt3; subst; assumption.
+ simpl in *; constructor; assumption.
- assumption.
- constructor.
+ constructor; assumption.
+ constructor; assumption.
Qed.

Lemma local_confluence_par_red: local_confluence par_red.
Expand Down
Loading