From 59d61ee8a9082fca45604233b57b1d2209466f53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 28 Aug 2024 14:21:59 +0200 Subject: [PATCH] Fix admits --- theories/iSL/Environments.v | 22 ++++++++++++++++ theories/iSL/PropQuantifiers.v | 46 ++++++++++++++++++++-------------- 2 files changed, 49 insertions(+), 19 deletions(-) diff --git a/theories/iSL/Environments.v b/theories/iSL/Environments.v index 734e04e..572f2df 100755 --- a/theories/iSL/Environments.v +++ b/theories/iSL/Environments.v @@ -677,4 +677,26 @@ induction l as [| a l]. rewrite IHl. setoid_rewrite gmultiset_elements_singleton. trivial. Qed. +Lemma list_to_set_disj_env_add Δ v: ((list_to_set_disj Δ : env) • v : env) ≡ list_to_set_disj (v :: Δ). +Proof. ms. Qed. + +Lemma list_to_set_disj_rm Δ v: (list_to_set_disj Δ : env) ∖ {[v]} ≡ list_to_set_disj (rm v Δ). +Proof. +induction Δ as [|φ Δ]; simpl; [ms|]. +case form_eq_dec; intro; subst; [ms|]. +simpl. rewrite <- IHΔ. case (decide (v ∈ (list_to_set_disj Δ: env))). +- intro. rewrite union_difference_R by assumption. ms. +- intro. rewrite diff_not_in by auto with *. rewrite diff_not_in; auto with *. +Qed. + +Lemma gmultiset_elements_list_to_set_disj l: gmultiset_elements(list_to_set_disj l) ≡ₚ l. +Proof. +induction l as [| x l]; [ms|]. +rewrite Proper_elements; [|symmetry; apply list_to_set_disj_env_add]. +rewrite elements_env_add, IHl. trivial. +Qed. + +Lemma list_to_set_disj_open_boxes Δ: ((⊗ (list_to_set_disj Δ)) = list_to_set_disj (map open_box Δ)). +Proof. apply list_to_set_disj_perm, Permutation_map', gmultiset_elements_list_to_set_disj. Qed. + (* TODO: move in optimisations *) \ No newline at end of file diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v index 39ddbdc..841a098 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -362,26 +362,33 @@ Opaque make_disj. Opaque make_conj. (* TODO move *) -Lemma list_to_set_disj_rm Δ v: (list_to_set_disj Δ : env) ∖ {[v]} = list_to_set_disj (rm v Δ). -Proof. -Admitted. +Lemma list_to_set_disj_env_add Δ v: ((list_to_set_disj Δ : env) • v : env) ≡ list_to_set_disj (v :: Δ). +Proof. ms. Qed. -Lemma list_to_set_disj_env_add Δ v: ((list_to_set_disj Δ : env) • v : env)≡ list_to_set_disj (v :: Δ). +Lemma list_to_set_disj_rm Δ v: (list_to_set_disj Δ : env) ∖ {[v]} ≡ list_to_set_disj (rm v Δ). Proof. -Admitted. +induction Δ as [|φ Δ]; simpl; [ms|]. +case form_eq_dec; intro; subst; [ms|]. +simpl. rewrite <- IHΔ. case (decide (v ∈ (list_to_set_disj Δ: env))). +- intro. rewrite union_difference_R by assumption. ms. +- intro. rewrite diff_not_in by auto with *. rewrite diff_not_in; auto with *. +Qed. -Lemma list_to_set_disj_open_boxes Δ: ((⊗ (list_to_set_disj Δ)) ≡ list_to_set_disj (map open_box Δ)). +Lemma gmultiset_elements_list_to_set_disj l: gmultiset_elements(list_to_set_disj l) ≡ₚ l. Proof. -Admitted. +induction l as [| x l]; [ms|]. +rewrite Proper_elements; [|symmetry; apply list_to_set_disj_env_add]. +rewrite elements_env_add, IHl. trivial. +Qed. + +Lemma list_to_set_disj_open_boxes Δ: ((⊗ (list_to_set_disj Δ)) = list_to_set_disj (map open_box Δ)). +Proof. apply list_to_set_disj_perm, Permutation_map', gmultiset_elements_list_to_set_disj. Qed. -Local Ltac l_tac := +Local Ltac l_tac := repeat rewrite list_to_set_disj_open_boxes; rewrite (proper_Provable _ _ (list_to_set_disj_env_add _ _) _ _ eq_refl) || rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)) _ _ eq_refl) -|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (list_to_set_disj_open_boxes _)) _ _ eq_refl) || rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _))) _ _ eq_refl) -|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_open_boxes _))) _ _ eq_refl) -|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)))) _ _ eq_refl) -|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_open_boxes _)))) _ _ eq_refl). +|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)))) _ _ eq_refl). Lemma a_rule_env_spec (Δ : list form) θ ϕ Hin (EA0 : ∀ pe, (pe ≺· (Δ, ϕ)) → form * form) (HEA : forall Δ ϕ Hpe, (list_to_set_disj Δ ⊢ fst (EA0 (Δ, ϕ) Hpe)) * (list_to_set_disj Δ• snd(EA0 (Δ, ϕ) Hpe) ⊢ ϕ)) : @@ -391,7 +398,8 @@ assert (HE := λ Δ0 ϕ0 Hpe, fst (HEA Δ0 ϕ0 Hpe)). assert (HA := λ Δ0 ϕ0 Hpe, snd (HEA Δ0 ϕ0 Hpe)). clear HEA. assert(Hi : θ ∈ list_to_set_disj Δ) by now apply elem_of_list_to_set_disj. -destruct θ; exhibit Hi 1; rewrite list_to_set_disj_rm in *. +destruct θ; exhibit Hi 1; +rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_rm _ _))) _ _ eq_refl). - simpl; case decide; intro Hp. + subst. case_decide; subst; auto with proof. + exch 0... @@ -421,7 +429,7 @@ destruct θ; exhibit Hi 1; rewrite list_to_set_disj_rm in *. * apply AndL. exch 0. l_tac. apply weakening, HA. + exch 0. exch 0. simpl. apply AndL. exch 1; exch 0. apply ImpBox. * box_tac. box_tac. exch 0; exch 1; exch 0. apply weakening. exch 1; exch 0. - apply make_impl_sound_L. do 3 l_tac. apply ImpL. + apply make_impl_sound_L. do 2 l_tac. apply ImpL. -- auto with proof. -- apply HA. * exch 1; exch 0. apply weakening. exch 0. l_tac. auto with proof. @@ -447,7 +455,7 @@ split. { apply conjunction_R1. intros φ Hin. apply in_in_map in Hin. destruct Hin as (ψ&Hin&Heq). subst. assert(Hi : ψ ∈ list_to_set_disj Δ) by now apply elem_of_list_to_set_disj. -destruct ψ; unfold e_rule; exhibit Hi 0; rewrite list_to_set_disj_rm in *. +destruct ψ; unfold e_rule; exhibit Hi 0; rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (list_to_set_disj_rm _ _)) _ _ eq_refl). - case decide; intro; subst; simpl; auto using HE with proof. - auto with proof. - apply AndL. do 2 l_tac... @@ -471,10 +479,10 @@ destruct ψ; unfold e_rule; exhibit Hi 0; rewrite list_to_set_disj_rm in *. * exch 0. l_tac. auto with proof. + foldEA. apply make_impl_sound_R, ImpR. exch 0. apply ImpBox. -- box_tac. exch 0; exch 1; exch 0. apply make_impl_sound_L, ImpL. - ++ do 3 l_tac. apply weakening, HE. order_tac. - ++ do 3 l_tac. apply HA. order_tac. + ++ do 2 l_tac. apply weakening, HE. order_tac. + ++ do 2 l_tac. apply HA. order_tac. -- exch 0. l_tac. apply weakening, HE. order_tac. -- apply BoxR. apply weakening. box_tac. do 2 l_tac. apply HE. order_tac. +- apply BoxR. apply weakening. box_tac. l_tac. apply HE. order_tac. } (* A *) apply make_disj_sound_L, OrL. @@ -485,7 +493,7 @@ apply make_disj_sound_L, OrL. + case decide; intro; subst; [constructor 2|constructor 1]. + apply make_conj_sound_L, AndR; apply AndL; auto using HE with proof. + apply ImpR. exch 0. l_tac. apply make_impl_sound_L, ImpL; auto using HE, HA with proof. - + foldEA. apply BoxR. box_tac. exch 0. do 2 l_tac. apply make_impl_sound_L, ImpL. + + foldEA. apply BoxR. box_tac. exch 0. l_tac. apply make_impl_sound_L, ImpL. * apply weakening, HE. order_tac. * apply HA. order_tac. Qed.