From 2a0e057f9e3d27b6110f529884d29eb625b0dbaf Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Fri, 3 May 2024 19:19:36 -0400 Subject: [PATCH] Finish PER transitivity (#49) --- theories/Core/Semantic/PERLemmas.v | 134 ++++++++++++++++++++++++----- 1 file changed, 113 insertions(+), 21 deletions(-) diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v index 74ac6b05..e6a7196a 100644 --- a/theories/Core/Semantic/PERLemmas.v +++ b/theories/Core/Semantic/PERLemmas.v @@ -118,6 +118,22 @@ Proof. intros. eauto using per_univ_elem_right_irrel_gen. Qed. +Ltac per_univ_elem_right_irrel_rewrite := + repeat match goal with + | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R1 }} |- _ => + mark H2 + | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ => + assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; mark H2 + end; unmark_all. + +Ltac functional_per_univ_elem_rewrite_clear := + repeat match goal with + | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ => + clear H2 + | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ => + assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; clear H2 + end. + Lemma per_univ_elem_sym : forall i A B R, per_univ_elem i A B R -> exists R', per_univ_elem i B A R' /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R' }}). @@ -162,24 +178,100 @@ Proof. + intros; split; mauto. Qed. -(* Lemma per_univ_elem_trans : forall i A1 A2 R1, *) -(* per_univ_elem i A1 A2 R1 -> *) -(* forall A3 R2, *) -(* per_univ_elem i A2 A3 R2 -> *) -(* exists R3, per_univ_elem i A1 A3 R3 /\ (forall a1 a2 a3, R1 a1 a2 -> R2 a2 a3 -> R3 a1 a3). *) -(* Proof. *) -(* induction 1 using per_univ_elem_ind; intros ? ? HT2; *) -(* invert_per_univ_elem HT2. *) -(* - exists (per_univ j'0). *) -(* split. *) -(* + apply per_univ_elem_core_univ'; trivial. *) -(* + intros. unfold per_univ in *. *) -(* destruct H0, H2. *) -(* destruct (H1 _ _ _ H0 _ _ H2) as [? [? ?]]. *) -(* eauto. *) -(* - exists per_nat. *) -(* split... *) -(* + mauto. *) -(* + eapply per_nat_trans. *) -(* - specialize (IHper_univ_elem _ _ equiv_a_a'). *) -(* destruct IHper_univ_elem as [in_rel3 [? ?]]. *) +Lemma per_univ_elem_left_irrel : forall i A B R A' R', + per_univ_elem i A B R -> + per_univ_elem i A' B R' -> + R = R'. +Proof. + intros * [? []]%per_univ_elem_sym [? []]%per_univ_elem_sym. + per_univ_elem_right_irrel_rewrite. + extensionality a. + extensionality b. + specialize (H0 a b). + specialize (H2 a b). + apply propositional_extensionality; firstorder. +Qed. + +Ltac per_univ_elem_left_irrel_rewrite := + repeat match goal with + | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ => + mark H2 + | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ => + assert (R2 = R1) by (eapply per_univ_elem_left_irrel; eassumption); subst; mark H2 + end; unmark_all. + +Ltac per_univ_elem_irrel_rewrite := functional_per_univ_elem_rewrite_clear; per_univ_elem_right_irrel_rewrite; per_univ_elem_left_irrel_rewrite. + +Lemma per_univ_elem_trans : forall i A1 A2 R1, + per_univ_elem i A1 A2 R1 -> + forall A3 R2, + per_univ_elem i A2 A3 R2 -> + exists R3, per_univ_elem i A1 A3 R3 /\ (forall a1 a2 a3, R1 a1 a2 -> R2 a2 a3 -> R3 a1 a3). +Proof with solve [mauto]. + induction 1 using per_univ_elem_ind; intros * HT2; + invert_per_univ_elem HT2; clear HT2. + - exists (per_univ j'0). + split; mauto. + intros. + destruct H0, H2. + destruct (H1 _ _ _ H0 _ _ H2) as [? [? ?]]. + econstructor... + - exists per_nat. + split; try econstructor... + - rename R2 into elem_rel0. + destruct (IHper_univ_elem _ _ equiv_a_a') as [in_rel3 [? in_rel_trans]]. + per_univ_elem_irrel_rewrite. + pose proof (per_univ_elem_sym _ _ _ _ H) as [in_rel' [? in_rel_sym]]. + specialize (IHper_univ_elem _ _ H3) as [in_rel'' [? _]]. + per_univ_elem_irrel_rewrite. + rename in_rel0 into in_rel. + assert (in_rel_refl : forall c c', in_rel c c' -> in_rel c' c'). + { + intros. + assert (equiv_c'_c : in_rel c' c) by (destruct in_rel_sym with c c'; mauto)... + } + assert (forall (c c' : domain) (equiv_c_c' : in_rel c c'), + exists R3, + rel_mod_eval + (fun (x y : domain) (R : relation domain) => + per_univ_elem i x y R) + B d{{{ p ↦ c }}} B'0 d{{{ p'0 ↦ c' }}} R3 + /\ (forall c'' (equiv_c_c'' : in_rel c c'') (equiv_c''_c' : in_rel c'' c') b0 b1 b2, + out_rel _ _ equiv_c_c'' b0 b1 -> out_rel0 _ _ equiv_c''_c' b1 b2 -> R3 b0 b2)). + { + intros. + assert (equiv_c'_c' : in_rel c' c') by mauto. + destruct (H0 _ _ equiv_c_c') as [? ? ? ? []]. + destruct (H7 _ _ equiv_c'_c') as []. + functional_eval_rewrite_clear. + destruct (H10 _ _ H13) as [R []]. + exists R. + split. + - econstructor... + - intros. + specialize (H0 _ _ equiv_c_c'') as [? ? ? ? []]. + specialize (H7 _ _ equiv_c''_c') as []. + functional_eval_rewrite_clear. + specialize (H19 _ _ H21) as [R' []]. + per_univ_elem_irrel_rewrite. + eapply H7... + } + repeat setoid_rewrite dep_functional_choice_equiv in H5. + destruct H5 as [out_rel3 ?]. + exists (fun f f' => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel3 c c' equiv_c_c') f c f' c'). + split. + + per_univ_elem_econstructor; mauto. + intros. + specialize (H5 _ _ equiv_c_c') as []... + + intros. + assert (equiv_c'_c' : in_rel c' c') by mauto. + rewrite H1 in H6. + rewrite H8 in H9. + specialize (H6 _ _ equiv_c_c') as []. + specialize (H9 _ _ equiv_c'_c') as []. + functional_eval_rewrite_clear. + specialize (H5 _ _ equiv_c_c') as []. + econstructor... + - exists per_ne. + split; try per_univ_elem_econstructor... +Qed.