From 93e6c2f957cc6fe1bf1cfbbe60067220396f844c Mon Sep 17 00:00:00 2001 From: Paulo Torrens Date: Mon, 25 Dec 2023 02:21:51 +0000 Subject: [PATCH] Finish proof that lift and substitution commmute --- theories/Substitution.v | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/theories/Substitution.v b/theories/Substitution.v index a8914d3..480c822 100644 --- a/theories/Substitution.v +++ b/theories/Substitution.v @@ -343,10 +343,44 @@ Section DeBruijn. do 2 rewrite traverse_var. now simplify decidable equality. (* Case: composition. *) - - admit. + - (* We just need to split the occurrences to use the hypotheses. *) + do 2 rewrite subst_lift_unfold. + replace j with ((j - k) + k) at 1 by lia. + rewrite <- subst_inst_lift. + unfold inst. + do 2 rewrite traverse_fun. + apply traverse_ext; simpl; intros l n ?. + destruct (le_gt_dec l n). + + remember (j - k + l) as m. + (* Will we be performing the substitution or...? *) + destruct (le_gt_dec m n). + * (* There's a long way to go, but these are fine. *) + rewrite traverse_var. + simplify decidable equality. + fold (lift_fun i) (lift i). + fold (inst s2). + rewrite IHs2 by lia. + f_equal; try lia. + do 2 rewrite <- traverse_var. + fold (inst s1). + rewrite IHs1 by lia. + f_equal; try lia. + unfold lift, lift_fun. + rewrite traverse_var. + (* Finally! *) + now simplify decidable equality. + * (* Just lifting for now. *) + do 2 rewrite traverse_var. + now simplify decidable equality. + + (* Nothing at all! *) + do 2 rewrite traverse_var. + now simplify decidable equality. (* Case: entering a binder. *) - - admit. - Admitted. + - (* We can just adjust the distance and use the inductive hypothesis. *) + do 2 rewrite subst_inst_lift. + rewrite IHs by lia. + f_equal; lia. + Qed. Lemma subst_comp_clos: forall s t k j x,