Skip to content

Commit 6b51b26

Browse files
bousmahawasselbousmahawassel
committed
proved confluence of beta-reduction (after rectifying the definition of beta-reduction
1 parent e4ca361 commit 6b51b26

2 files changed

Lines changed: 299 additions & 82 deletions

File tree

‎theories/LambdaCube/Operational.v‎

Lines changed: 241 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,251 @@
11
From Coq Require Import Utf8.
2+
From Coq Require Import Arith Lia.
23
From FormArith Require Import Base.
34
From FormArith.LambdaCube Require Import Term.
45

6+
Reserved Notation "t [≻] u" (at level 70).
7+
Reserved Notation "t ≻ u" (at level 70).
8+
Reserved Notation "t ≻+ u" (at level 70).
9+
Reserved Notation "t ≻* u" (at level 70).
10+
Reserved Notation "t ≅ u" (at level 70).
11+
512
Inductive head_step {n : nat} : term n → term n → Prop :=
613
| beta_red
714
(ty : term n)
815
(body : term (S n))
9-
(arg : term n) : head_step (App (Abs ty body) arg) (bind (bind_first arg) body).
16+
(arg : term n) : App (Abs ty body) arg [≻] bind (bind_first arg) body
17+
where "t [≻] u" := (head_step t u).
1018

1119
Inductive step {n : nat} : term n → term n → Prop :=
12-
| ctx_red (K : ctx n) (t u : term n) :
13-
head_step t u → step (fill K t) (fill K u).
20+
| ctx_red {k} (K : ctx n k) (t u : term k) :
21+
t [≻] u → fill K t ≻ fill K u
22+
where "t ≻ u" := (step t u).
23+
24+
Lemma step_under_context {n k} (K: ctx n k) t u : t ≻ u -> fill K t ≻ fill K u.
25+
Proof.
26+
destruct 1 as [K']. do 2 rewrite <- fill_fillK. constructor. assumption.
27+
Qed.
28+
29+
Inductive Rplus {A} (R: relation A) a b : Prop :=
30+
| add_last_R m : Rplus R a m -> R m b -> Rplus R a b
31+
| Rclot_plus : R a b -> Rplus R a b.
32+
33+
Notation "t ≻+ u" := (Rplus step t u).
34+
35+
Lemma Rplus_trans {A} (R: relation A) x y z : Rplus R x y -> Rplus R y z -> Rplus R x z.
36+
Proof.
37+
induction 2.
38+
- econstructor; eauto.
39+
- econstructor; eauto.
40+
Qed.
41+
42+
Lemma add_first {A} (R: relation A) x y z : R x y -> Rplus R y z -> Rplus R x z.
43+
induction 2.
44+
- econstructor; eauto.
45+
- econstructor; eauto. constructor. auto.
46+
Qed.
47+
48+
Inductive Rstar {A} (R: relation A) a : A -> Prop :=
49+
| Rstar_refl : Rstar R a a
50+
| Rclot_plus_star b : Rplus R a b -> Rstar R a b.
51+
52+
Notation "t ≻* u" := (Rstar step t u).
53+
54+
Lemma step_star_context {n k} (K: ctx n k) t u : t ≻* u -> fill K t ≻* fill K u.
55+
Proof.
56+
destruct 1; constructor. induction H.
57+
- econstructor; try eassumption. apply step_under_context. assumption.
58+
- constructor. apply step_under_context. assumption.
59+
Qed.
60+
61+
Lemma Rstar_trans {A} (R: relation A) x y z : Rstar R x y -> Rstar R y z -> Rstar R x z.
62+
Proof.
63+
destruct 1; auto.
64+
destruct 1.
65+
- constructor. assumption.
66+
- constructor. eapply Rplus_trans; eassumption.
67+
Qed.
68+
69+
Inductive Requiv {A} (R: relation A) a : A -> Prop :=
70+
| Rclot_plus_equiv b : Rplus R a b -> Requiv R a b
71+
| Rclot_plus_equiv_r b : Rplus R b a -> Requiv R a b
72+
| Requiv_refl : Requiv R a a.
73+
74+
Reserved Notation "t ⪼ u" (at level 70).
75+
Reserved Notation "t ⪼+ u" (at level 70).
76+
Reserved Notation "t ⪼* u" (at level 70).
77+
78+
Inductive par_step {n: nat} : term n -> term n -> Prop :=
79+
| par_step_var i : Var i ⪼ Var i
80+
| par_step_sort s : Srt s ⪼ Srt s
81+
| par_step_pi t1 t2 u1 u2 : t1 ⪼ u1 -> t2 ⪼ u2 -> Pi t1 t2 ⪼ Pi u1 u2
82+
| par_step_abs t1 t2 u1 u2 : t1 ⪼ u1 -> t2 ⪼ u2 -> Abs t1 t2 ⪼ Abs u1 u2
83+
| par_step_app t1 t2 u1 u2 : t1 ⪼ u1 -> t2 ⪼ u2 -> App t1 t2 ⪼ App u1 u2
84+
| par_step_redex T f arg f' arg' :
85+
f ⪼ f' -> arg ⪼ arg' -> App (Abs T f) arg ⪼ bind (bind_first arg') f'
86+
where "t ⪼ u" := (par_step t u).
87+
88+
Notation "t ⪼+ u" := (Rplus par_step t u).
89+
Notation "t ⪼* u" := (Rstar par_step t u).
90+
91+
Lemma par_refl {n} (t : term n) : t ⪼ t.
92+
Proof.
93+
induction t; constructor; assumption.
94+
Qed.
95+
96+
Fixpoint par_max {n} (t: term n) : term n :=
97+
match t with
98+
| App (Abs _ f) arg => bind (bind_first (par_max arg)) (par_max f)
99+
| Srt _ | Var _ => t
100+
| Pi A B => Pi (par_max A) (par_max B)
101+
| Abs T f => Abs (par_max T) (par_max f)
102+
| App a b => App (par_max a) (par_max b)
103+
end.
104+
105+
Lemma par_par_max {n} (t: term n) : t ⪼ par_max t.
106+
induction t; simpl; try solve [constructor; assumption].
107+
destruct t1; try solve [constructor; assumption].
108+
simpl in *. inversion_clear IHt1.
109+
constructor; assumption.
110+
Qed.
111+
112+
Lemma ren_preserves_par {n k} (σ: {i | i < n} -> {i | i < k}) t u :
113+
t ⪼ u -> ren σ t ⪼ ren σ u.
114+
Proof.
115+
induction 1 in k, σ |- *; simpl; try constructor; auto.
116+
rewrite ren_bind. specialize (IHpar_step1 _ (lift σ)). specialize (IHpar_step2 _ σ).
117+
enough (
118+
e : bind (ren σ ∘ bind_first arg') f' =
119+
bind (bind_first (ren σ arg')) (ren (lift σ) f')
120+
) by (rewrite e; constructor; assumption). clear. rewrite bind_ren.
121+
apply bind_ext.
122+
intro. unfold lift, bind_first. destruct (lt_dec _ _); simpl.
123+
- pose proof (proj2_sig (σ (exist _ (proj1_sig i) l))). simpl in *.
124+
destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity.
125+
- destruct (lt_dec _ _); try lia. reflexivity.
126+
Qed.
127+
128+
Lemma par_max_is_max {n} (t t': term n) : t ⪼ t' -> t' ⪼ par_max t.
129+
Proof.
130+
induction 1; simpl in *; try solve [constructor; assumption].
131+
- destruct t1; try solve [constructor; assumption].
132+
simpl in *. inversion H; subst; clear H. inversion_clear IHpar_step1.
133+
constructor; assumption.
134+
- revert IHpar_step1 IHpar_step2. clear. generalize (par_max f), (par_max arg). clear.
135+
rename f' into f, arg' into arg. intros f' arg' fred argred.
136+
cut (forall i, bind_first arg i ⪼ bind_first arg' i); swap 1 2.
137+
{ unfold bind_first. intro. destruct (lt_dec _ _); try assumption; constructor. }
138+
generalize (bind_first arg) as σ1, (bind_first arg') as σ2.
139+
clear arg arg' argred. generalize dependent n. fix IH 4.
140+
destruct 1; simpl.
141+
+ intros ? ? H. apply H.
142+
+ constructor.
143+
+ constructor; auto. apply IH; try assumption. unfold lift_bind.
144+
intro. destruct (lt_dec _ _); try solve [constructor].
145+
apply ren_preserves_par. apply H.
146+
+ constructor; auto. apply IH; try assumption. unfold lift_bind.
147+
intro. destruct (lt_dec _ _); try solve [constructor].
148+
apply ren_preserves_par. apply H.
149+
+ constructor; auto.
150+
+ intros. rewrite bind_comp.
151+
apply IH with (σ1 := lift_bind σ1) (σ2 := lift_bind σ2) in fred1 as IHf; swap 1 2.
152+
{ unfold lift_bind. intro. destruct (lt_dec _ _); try solve [constructor].
153+
apply ren_preserves_par. apply H. }
154+
apply IH with (σ1 := σ1) (σ2 := σ2) in fred2 as IHarg; try assumption.
155+
enough (
156+
e : bind (bind σ2 ∘ bind_first arg') f' =
157+
bind (bind_first (bind σ2 arg')) (bind (lift_bind σ2) f')
158+
) by (rewrite e; constructor; try assumption).
159+
rewrite bind_comp. apply bind_ext.
160+
intro. unfold lift_bind, bind_first at 1.
161+
destruct (lt_dec _ _).
162+
* simpl. rewrite bind_ren.
163+
generalize (σ2 (exist _ (proj1_sig i) l)).
164+
intro. clear. assert (forall i, (bind_first (bind σ2 arg') ∘ weaken) i = Var i).
165+
{ intro. unfold weaken. unfold bind_first. simpl. pose proof (proj2_sig i).
166+
destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. }
167+
revert H. generalize (bind_first (bind σ2 arg') ∘ weaken). clear.
168+
induction t; simpl; auto; intros; f_equal; auto; apply IHt2.
169+
-- unfold lift_bind. intro. destruct (lt_dec _ _).
170+
++ rewrite H. simpl. unfold weaken. f_equal. apply sig_lt_ext. reflexivity.
171+
++ f_equal. apply sig_lt_ext. pose proof (proj2_sig i). simpl in *. lia.
172+
-- unfold lift_bind. intro. destruct (lt_dec _ _).
173+
++ rewrite H. simpl. unfold weaken. f_equal. apply sig_lt_ext. reflexivity.
174+
++ f_equal. apply sig_lt_ext. pose proof (proj2_sig i). simpl in *. lia.
175+
* simpl. unfold bind_first. simpl. destruct (lt_dec n n); try lia. reflexivity.
176+
Qed.
177+
178+
Lemma diamond_par {n} (t u u': term n) : t ⪼ u -> t ⪼ u' -> exists v, u ⪼ v /\ u' ⪼ v.
179+
intros. exists (par_max t). split; apply par_max_is_max; assumption.
180+
Qed.
181+
182+
Lemma left_star_par_commute {n} (t u u': term n) : t ⪼* u -> t ⪼ u' -> exists v, u ⪼ v /\ u' ⪼* v.
183+
Proof.
184+
destruct 1. { intro. exists u'. intuition. constructor. }
185+
induction H in u' |- *.
186+
- intro redr. specialize (IHRplus _ redr) as IHu'. destruct IHu' as [x []].
187+
destruct (diamond_par m b x); try assumption. intuition. exists x0. intuition.
188+
destruct H2.
189+
+ do 2 constructor. assumption.
190+
+ constructor. econstructor; eassumption.
191+
- intro. destruct (diamond_par t b u'); try assumption. exists x. intuition. do 2 constructor.
192+
assumption.
193+
Qed.
194+
195+
Lemma confluence_par {n} (t u u': term n) : t ⪼* u -> t ⪼* u' -> exists v, u ⪼* v /\ u' ⪼* v.
196+
Proof.
197+
destruct 2. { eexists. intuition try eassumption. constructor. }
198+
induction H0; firstorder.
199+
- destruct (left_star_par_commute _ _ _ H3 H1). exists x0. intuition. constructor. destruct H2.
200+
+ constructor. assumption.
201+
+ econstructor; eassumption.
202+
- destruct (left_star_par_commute _ _ _ H H0). exists x. intuition. do 2 constructor. assumption.
203+
Qed.
204+
205+
Lemma step_incl_par {n} (t u: term n) : t ≻ u -> t ⪼ u.
206+
Proof.
207+
destruct 1.
208+
induction K; simpl; try solve [constructor; auto using par_refl].
209+
destruct H. constructor; apply par_refl.
210+
Qed.
211+
212+
Lemma step_star_incl_par_star {n} (t u: term n) : t ≻* u -> t ⪼* u.
213+
Proof.
214+
destruct 1; constructor.
215+
induction H.
216+
- econstructor; try eassumption. apply step_incl_par. assumption.
217+
- constructor. apply step_incl_par. assumption.
218+
Qed.
219+
220+
Lemma par_incl_step_star {n} (t u: term n) : t ⪼ u -> t ≻* u.
221+
induction 1; try solve [constructor].
222+
- eapply Rstar_trans.
223+
+ change (Pi t1 t2) with (fill (PiL Hole t2) t1). apply step_star_context. eassumption.
224+
+ simpl. change (Pi u1 ?x) with (fill (PiR u1 Hole) x). apply step_star_context. assumption.
225+
- eapply Rstar_trans.
226+
+ change (Abs t1 t2) with (fill (AbsL Hole t2) t1). apply step_star_context. eassumption.
227+
+ simpl. change (Abs u1 ?x) with (fill (AbsR u1 Hole) x). apply step_star_context. assumption.
228+
- eapply Rstar_trans.
229+
+ change (App t1 t2) with (fill (AppL Hole t2) t1). apply step_star_context. eassumption.
230+
+ simpl. change (App u1 ?x) with (fill (AppR u1 Hole) x). apply step_star_context. assumption.
231+
- apply Rstar_trans with (y := App (Abs T f') arg).
232+
+ change (App (Abs T ?x) ?y) with (fill (AppL (AbsR T Hole) y) x).
233+
apply step_star_context. assumption.
234+
+ apply Rstar_trans with (y := App (Abs T f') arg').
235+
* change (App ?x ?y) with (fill (AppR x Hole) y). apply step_star_context. assumption.
236+
* do 2 constructor. change (?x ≻ ?y) with (fill Hole x ≻ fill Hole y). do 2 constructor.
237+
Qed.
238+
239+
Lemma par_star_incl_step_star {n} (t u: term n) : t ⪼* u -> t ≻* u.
240+
Proof.
241+
destruct 1; [constructor |].
242+
induction H.
243+
- eapply Rstar_trans; try eassumption. apply par_incl_step_star. assumption.
244+
- apply par_incl_step_star. assumption.
245+
Qed.
246+
247+
Lemma confluence_step {n} (t u u': term n) : t ≻* u -> t ≻* u' -> exists v, u ≻* v /\ u' ≻* v.
248+
Proof.
249+
intros tl tr. apply step_star_incl_par_star in tl, tr.
250+
destruct (confluence_par _ _ _ tl tr) as [v]. exists v. intuition auto using par_star_incl_step_star.
251+
Qed.

0 commit comments

Comments
 (0)