From 7227a6307c422fe0727c01645b7de2d31cd37a49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Tue, 27 Aug 2024 22:03:22 +0200 Subject: [PATCH 1/6] Use list instead of multiset when building propositional quantifiers. Definitions only, soundness proof to go. --- theories/iSL/Cut.v | 23 +-- theories/iSL/Environments.v | 75 +++++----- theories/iSL/Order.v | 249 +++++++++++++++++++-------------- theories/iSL/PropQuantifiers.v | 131 ++++++++--------- theories/iSL/Simp.v | 7 +- 5 files changed, 262 insertions(+), 223 deletions(-) diff --git a/theories/iSL/Cut.v b/theories/iSL/Cut.v index 523ab03..a992a1c 100644 --- a/theories/iSL/Cut.v +++ b/theories/iSL/Cut.v @@ -1,13 +1,14 @@ Require Import ISL.Formulas ISL.Sequents ISL.Order. Require Import ISL.SequentProps . +Local Hint Rewrite elements_env_add : order. + + (* From "A New Calculus for Intuitionistic Strong Löb Logic" *) Theorem additive_cut Γ φ ψ : Γ ⊢ φ -> Γ • φ ⊢ ψ -> Γ ⊢ ψ. -Proof. (* -Ltac order_tac := try (apply le_S_n; etransitivity; [|exact HW]); apply Nat.le_succ_l; -match goal with |- env_weight .order_tac. *) +Proof. remember (weight φ) as w. assert(Hw : weight φ ≤ w) by lia. clear Heqw. revert φ Hw ψ Γ. induction w; intros φ Hw; [pose (weight_pos φ); lia|]. @@ -15,7 +16,7 @@ intros ψ Γ. remember (Γ, ψ) as pe. replace Γ with pe.1 by now subst. replace ψ with pe.2 by now subst. clear Heqpe Γ ψ. revert pe. -refine (@well_founded_induction _ _ wf_pointed_order _ _). +refine (@well_founded_induction _ _ wf_pointed_env_ms_order _ _). intros (Γ &ψ). simpl. intro IHW'. assert (IHW := fun Γ0 => fun ψ0 => IHW' (Γ0, ψ0)). simpl in IHW. clear IHW'. intros HPφ HPψ. Ltac otac Heq := subst; repeat rewrite env_replace in Heq by trivial; repeat rewrite env_add_remove by trivial; order_tac; rewrite Heq; order_tac. @@ -23,7 +24,7 @@ destruct HPφ; simpl in Hw. - now apply contraction. - apply ExFalso. - apply AndL_rev in HPψ. do 2 apply IHw in HPψ; trivial; try lia; apply weakening; assumption. -- apply AndL. apply IHW; auto with proof. order_tac. +- apply AndL. apply IHW; auto with proof. order_tac. - apply OrL_rev in HPψ; apply (IHw φ); [lia| |]; tauto. - apply OrL_rev in HPψ; apply (IHw ψ0); [lia| |]; tauto. - apply OrL; apply IHW; auto with proof. @@ -41,7 +42,7 @@ destruct HPφ; simpl in Hw. + forward. auto with proof. + apply AndR. * rw (symmetry Heq) 0. apply IHW. - -- order_tac. + -- unfold pointed_env_ms_order. order_tac. -- now apply ImpR. -- peapply HPψ1. * rw (symmetry Heq) 0. apply IHW. @@ -49,7 +50,7 @@ destruct HPφ; simpl in Hw. -- apply ImpR. box_tac. peapply HPφ. -- peapply HPψ2. + forward. apply AndL. apply IHW. - * otac Heq. + * unfold pointed_env_ms_order. otac Heq. * apply AndL_rev. backward. rw (symmetry Heq) 0. apply ImpR, HPφ. * backward. peapply HPψ. + apply OrR1, IHW. @@ -157,7 +158,7 @@ destruct HPφ; simpl in Hw. * (* (V-f ) *) intro Hneq. forward. apply ImpBox. -- apply IHW. - ++ otac Heq. + ++ otac Heq. rewrite elements_open_boxes. otac Heq. ++ apply ImpR_rev, open_boxes_R, ImpR. apply ImpLBox_prev with φ1. exch 0. apply weakening. backward. rw (symmetry Heq) 0. apply ImpR, HPφ. @@ -170,7 +171,7 @@ destruct HPφ; simpl in Hw. ++ exch 0. rw (symmetry (difference_singleton _ _ Hin0)) 1. exact HPψ2. + subst. rw (symmetry Heq) 0. rewrite open_boxes_add in HPψ. simpl in HPψ. apply BoxR. apply IHW. - * otac Heq. (* todo: count rhs twice *) + * otac Heq. rewrite elements_open_boxes. otac Heq. * apply open_boxes_R, weakening, ImpR, HPφ. * exch 0. exact HPψ. - apply ImpLVar. eapply IHW; eauto. @@ -269,7 +270,7 @@ destruct HPφ; simpl in Hw. forward. apply ImpBox. * (* π0 *) apply IHW. - -- otac Heq. + -- otac Heq. rewrite elements_open_boxes. otac Heq. -- apply ImpLBox_prev with (φ1 := φ1). exch 0. apply weakening. apply open_boxes_R. backward. rw (symmetry Heq) 0. apply BoxR, HPφ. @@ -294,7 +295,7 @@ destruct HPφ; simpl in Hw. + (* (VIII-c) *) subst. rw (symmetry Heq) 0. rewrite open_boxes_add in HPψ. simpl in HPψ. apply BoxR. apply IHW. - * otac Heq. (* todo: count rhs twice *) + * otac Heq. rewrite elements_open_boxes. otac Heq. * apply open_boxes_R, weakening, BoxR, HPφ. * apply (IHw φ). -- lia. diff --git a/theories/iSL/Environments.v b/theories/iSL/Environments.v index e0994af..8cfffd1 100755 --- a/theories/iSL/Environments.v +++ b/theories/iSL/Environments.v @@ -45,9 +45,16 @@ Global Instance proper_disj_union : Proper ((≡@{env}) ==> (≡@{env}) ==> (≡ Proof. intros Γ Γ' Heq Δ Δ' Heq'. ms. Qed. - Global Notation "Γ • φ" := (disj_union Γ (base.singletonMS φ)) (at level 105, φ at level 85, left associativity). +Lemma elements_env_add (Γ : env) φ : elements(Γ • φ) ≡ₚ φ :: elements Γ. +Proof. +rewrite (gmultiset_elements_disj_union Γ). +setoid_rewrite (gmultiset_elements_singleton φ). +symmetry. apply Permutation_cons_append. +Qed. + + (** * Multiset utilities *) Lemma multeq_meq (M N: env) : (forall x, multiplicity x M = multiplicity x N) -> M ≡ N. @@ -325,21 +332,21 @@ Qed. (* a dependent map on lists, with knowledge that we are on that list *) (* should work with any set-like type *) -Program Fixpoint in_map_aux {A : Type} (Γ : env) (f : forall φ, (φ ∈ Γ) -> A) - Γ' (HΓ' : Γ' ⊆ elements Γ) : list A:= +Program Fixpoint in_map_aux {A : Type} (Γ : list form) (f : forall φ, (φ ∈ Γ) -> A) + Γ' (HΓ' : Γ' ⊆ Γ) : list A:= match Γ' with | [] => [] | a::Γ' => f a _ :: in_map_aux Γ f Γ' _ end. Next Obligation. -intros. apply gmultiset_elem_of_elements. auto with *. +intros. auto with *. Qed. Next Obligation. auto with *. Qed. -Definition in_map {A : Type} (Γ : env) +Definition in_map {A : Type} (Γ : list form) (f : forall φ, (φ ∈ Γ) -> A) : list A := - in_map_aux Γ f (elements Γ) (reflexivity _). + in_map_aux Γ f Γ (reflexivity _). (* This generalises to any type. decidability of equality over this type is necessary for a result in "Type" *) @@ -348,7 +355,7 @@ Lemma in_in_map {A : Type} {HD : forall a b : A, Decision (a = b)} ψ ∈ (in_map Γ f) -> {ψ0 & {Hin | ψ = f ψ0 Hin}}. Proof. unfold in_map. -assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ), ψ ∈ in_map_aux Γ f Γ' HΓ' +assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ Γ), ψ ∈ in_map_aux Γ f Γ' HΓ' → {ψ0 & {Hin : ψ0 ∈ Γ | ψ = f ψ0 Hin}}); [|apply Hcut]. induction Γ'; simpl; intros HΓ' Hin. - contradict Hin. auto. now rewrite elem_of_nil. @@ -369,7 +376,7 @@ Lemma in_map_in {A : Type} {HD : forall a b : A, Decision (a = b)} {Hin' | f ψ0 Hin' ∈ (in_map Γ f)}. Proof. unfold in_map. -assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ) ψ0 (Hin : In ψ0 Γ'), +assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ Γ) ψ0 (Hin : In ψ0 Γ'), {Hin' | f ψ0 Hin' ∈ in_map_aux Γ f Γ' HΓ'}). - induction Γ'; simpl; intros HΓ' ψ' Hin'; [auto with *|]. case (decide (ψ' = a)). @@ -378,12 +385,12 @@ assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ) ψ0 (Hin : In ψ0 Γ'), pose (Hincl := (in_map_aux_obligation_2 Γ (a :: Γ') HΓ' a Γ' eq_refl)). destruct (IHΓ' Hincl ψ' Hin'') as [Hin0 Hprop]. eexists. right. apply Hprop. -- destruct (Hcut (elements Γ) (reflexivity (elements Γ)) ψ0) as [Hin' Hprop]. - + now apply elem_of_list_In, gmultiset_elem_of_elements. +- destruct (Hcut Γ (reflexivity Γ) ψ0) as [Hin' Hprop]. + + auto. now apply elem_of_list_In. + exists Hin'. exact Hprop. Qed. -Lemma in_map_empty A f : @in_map A ∅ f = []. +Lemma in_map_empty A f : @in_map A [] f = []. Proof. auto with *. Qed. Lemma in_map_ext {A} Δ f g: @@ -461,7 +468,6 @@ Proof. apply Hinsert, IH; multiset_solver. Qed. - Lemma difference_include (θ θ' : form) (Δ : env) : (θ' ∈ Δ) -> θ ∈ Δ ∖ {[θ']} -> θ ∈ Δ. @@ -472,6 +478,11 @@ rewrite gmultiset_disj_union_difference with (X := {[θ']}). - now apply gmultiset_singleton_subseteq_l. Qed. +Lemma remove_include (θ θ' : form) (Δ : list form) : + (θ' ∈ Δ) -> + θ ∈ remove form_eq_dec θ' Δ -> θ ∈ Δ. +Proof. intros Hin' Hin. eapply elem_of_list_In, in_remove, elem_of_list_In, Hin. Qed. + (* technical lemma : one can constructively find whether an environment contains an element satisfying a decidable property *) @@ -577,6 +588,13 @@ Proof. intros Hx Hφ. apply elem_of_open_boxes in Hφ. destruct Hφ as [Hφ|Hφ]; eauto. Qed. +Lemma occurs_in_map_open_box x φ Δ : occurs_in x φ -> φ ∈ (map open_box Δ) -> exists θ, θ ∈ Δ /\ occurs_in x θ. +Proof. +intros Hx Hφ. apply elem_of_list_In, in_map_iff in Hφ. +destruct Hφ as [ψ [Hφ Hin]]; subst. +exists ψ. split. now apply elem_of_list_In. destruct ψ; trivial. +Qed. + Global Hint Rewrite open_boxes_disj_union : proof. @@ -634,27 +652,18 @@ Global Hint Rewrite open_boxes_singleton : proof. Global Hint Resolve open_boxes_spec' : proof. Global Hint Resolve open_boxes_spec : proof. +Global Instance Proper_elements : Proper ((≡) ==> (≡ₚ)) ((λ Γ : env, elements Γ)). +Proof. +intros Γ Δ Heq; apply AntiSymm_instance_0; apply gmultiset_elements_submseteq; ms. +Qed. -Ltac vars_tac := -intros; subst; -repeat match goal with -| HE : context [occurs_in ?x (?E _ _)], H : occurs_in ?x (?E _ _) |- _ => - apply HE in H -end; -intuition; -repeat match goal with | H : exists x, _ |- _ => destruct H end; -intuition; -simpl in *; in_tac; try (split; [tauto || auto with *|]); simpl in *; -try match goal with -| H : occurs_in _ (?a ⇢ (?b ⇢ ?c)) |- _ => apply occurs_in_make_impl2 in H -| H : occurs_in _ (?a ⇢ ?b) |- _ => apply occurs_in_make_impl in H -|H1 : ?x0 ∈ (⊗ ?Δ), H2 : occurs_in ?x ?x0 |- _ => - apply (occurs_in_open_boxes _ _ _ H2) in H1 -end; -repeat match goal with | H : exists x, _ |- _ => destruct H end; intuition; -try multimatch goal with -| H : ?θ0 ∈ ?Δ0 |- context [exists θ, θ ∈ ?Δ /\ occurs_in ?x θ] => - solve[try right; exists θ0; split; [eauto using difference_include|simpl; tauto]; eauto] end. - +Lemma elements_open_boxes Γ: elements (⊗ Γ) ≡ₚ map open_box (elements Γ). +Proof. +unfold open_boxes. remember (elements Γ) as l. clear Γ Heql. +induction l as [| a l]. +- ms. +- simpl. setoid_rewrite gmultiset_elements_disj_union. + rewrite IHl. setoid_rewrite gmultiset_elements_singleton. trivial. +Qed. (* TODO: move in optimisations *) \ No newline at end of file diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v index a928b3e..55f3ee2 100644 --- a/theories/iSL/Order.v +++ b/theories/iSL/Order.v @@ -1,50 +1,57 @@ Require Export ISL.Environments. (* Note 3 or 4 would suffice for IPC ; iSL requires 5 *) -Definition env_weight (Γ : env) := list_sum (map (fun x => 5^ weight x) (elements Γ)). +Definition env_weight (Γ : list form) := list_sum (map (fun x => 5^ weight x) Γ). -Lemma env_weight_disj_union Γ Δ : env_weight (disj_union Γ Δ) = env_weight Γ + env_weight Δ. +Lemma env_weight_disj_union Γ Δ : env_weight (Γ ++ Δ) = env_weight Γ + env_weight Δ. Proof. -unfold env_weight. -assert (Heq := gmultiset_elements_disj_union Γ Δ). -apply (Permutation_map (λ x : form, 5 ^ weight x)) in Heq. -apply Permutation_list_sum in Heq. -rewrite map_app, list_sum_app in Heq. exact Heq. +unfold env_weight. now rewrite map_app, list_sum_app. Qed. +(* TODO: dirty hack *) +Local Notation "Δ '•' φ" := (cons φ Δ). + Lemma env_weight_add Γ φ : env_weight (Γ • φ) = env_weight Γ + (5 ^ weight φ). Proof. -rewrite env_weight_disj_union. unfold env_weight at 2. -setoid_rewrite gmultiset_elements_singleton. simpl. lia. +unfold env_weight. simpl. lia. Qed. Global Hint Rewrite env_weight_add : order. -Definition env_order := ltof env env_weight. +Definition env_order := ltof (list form) env_weight. Infix "≺" := env_order (at level 150). -Lemma env_weight_singleton (φ : form) : env_weight {[ φ ]} = 5 ^ weight φ. +Lemma env_weight_singleton (φ : form) : env_weight [ φ ] = 5 ^ weight φ. Proof. -unfold env_weight, ltof. -replace (elements {[ φ ]}) with [φ]. simpl. lia. now rewrite <- gmultiset_elements_singleton. +unfold env_weight, ltof. simpl. lia. Qed. -Lemma env_order_singleton (φ ψ : form) : weight φ < weight ψ -> {[+ φ +]}≺ {[+ ψ +]}. +Lemma env_order_singleton (φ ψ : form) : weight φ < weight ψ -> [φ ] ≺ [ ψ ]. Proof. intro Hw. unfold env_order, ltof. do 2 rewrite env_weight_singleton. apply Nat.pow_lt_mono_r. lia. trivial. Qed. -Local Notation "Δ ≼ Δ'" := ((Δ ≺ Δ') \/ Δ = Δ') (at level 150). +Definition env_order_refl Δ Δ' := (Δ ≺ Δ') \/ Δ ≡ₚ Δ'. + +Local Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150). -Lemma env_le_weight Δ Δ' : (Δ' ≼ Δ) -> env_weight Δ' ≤ env_weight Δ. +Global Instance Proper_env_weight: Proper ((≡ₚ) ==> (=)) env_weight. Proof. +intros Γ Δ Heq. unfold env_weight. now rewrite Heq. +Qed. + + +Global Instance Proper_env_order_refl_env_weight: + Proper ((env_order_refl) ==> le) env_weight. +Proof. +intros Γ Δ. unfold env_order. intros [Hle | Heq]. - auto with *. -- subst; trivial. +- now rewrite Heq. Qed. -Global Hint Resolve env_le_weight : order. +Global Hint Resolve Proper_env_order_refl_env_weight : order. Global Hint Unfold form_order : mset. @@ -59,7 +66,10 @@ Defined. (* We introduce a notion of "pointed" environment, which is simply * a pair (Δ, φ), where Δ is an environment and φ is a formula, * not necessarily an element of Δ. *) -Definition pointed_env := (env * form)%type. +Definition pointed_env := (list form * form)%type. + + + (* The order on pointed environments is given by considering the * environment order on the sum of Δ and {φ}. *) @@ -70,23 +80,37 @@ Definition pointed_env_order (pe1 : pointed_env) (pe2 : pointed_env) := Lemma wf_pointed_order : well_founded pointed_env_order. Proof. apply well_founded_ltof. Qed. +Definition pointed_env_ms_order (Γφ Δψ : env * form) := + pointed_env_order (elements Γφ.1, Γφ.2) (elements Δψ.1, Δψ.2). + +Lemma wf_pointed_env_ms_order : well_founded pointed_env_ms_order. +Proof. apply well_founded_ltof. Qed. + Infix "≺·" := pointed_env_order (at level 150). -Lemma env_order_equiv_right_compat {Δ Δ' Δ'' : env}: - Δ' ≡ Δ'' -> +Lemma env_order_equiv_right_compat {Δ Δ' Δ'' }: + Δ' ≡ₚ Δ'' -> (Δ ≺ Δ'') -> Δ ≺ Δ'. -Proof. ms. Qed. +Proof. +unfold equiv, env_order, ltof, env_weight. intro Heq. rewrite Heq. trivial. +Qed. -Lemma env_order_equiv_left_compat {Δ Δ' Δ'' : env}: - Δ ≡ Δ'' -> +Lemma env_order_equiv_left_compat {Δ Δ' Δ'' }: + Δ ≡ₚ Δ'' -> (Δ'' ≺ Δ') -> Δ ≺ Δ'. -Proof. ms. Qed. +Proof. unfold equiv, env_order, ltof, env_weight. intro Heq. rewrite Heq. trivial. Qed. -Global Instance Proper_env_order : Proper ((≡@{env}) ==> (≡@{env}) ==> (fun x y => x <-> y)) env_order. -Proof. intros Δ1 Δ2 H12 Δ3 Δ4 H34; ms. Qed. +Global Instance Proper_env_order : Proper ((≡ₚ) ==> (≡ₚ) ==> (fun x y => x <-> y)) env_order. +Proof. intros Δ1 Δ2 H12 Δ3 Δ4 H34; unfold equiv, env_order, ltof, env_weight. rewrite H12, H34. tauto. Qed. + +Global Instance Proper_env_order_refl : Proper ((≡ₚ) ==> (≡ₚ) ==> (fun x y => x <-> y)) env_order_refl. +Proof. +intros Δ1 Δ2 H12 Δ3 Δ4 H34; unfold equiv, env_order, ltof, env_weight, env_order_refl. +now rewrite H12, H34. +Qed. Lemma env_order_1 Δ φ1 φ : weight φ1 < weight φ -> Δ • φ1 ≺ Δ • φ. Proof. @@ -104,6 +128,12 @@ Qed. Global Hint Resolve env_order_compat : order. +Lemma env_order_compat' Δ Δ' φ1 φ : weight φ1 ≤ weight φ -> (Δ' ≺ Δ) -> Δ' • φ1 ≺ Δ • φ. +Proof. +intros. unfold env_order, ltof. repeat rewrite env_weight_add. +apply Nat.add_lt_le_mono; auto with *. now apply Nat.pow_le_mono_r. +Qed. + Lemma env_order_add_compat Δ Δ' φ : (Δ ≺ Δ') -> (Δ • φ) ≺ (Δ' • φ). Proof. unfold env_order, ltof. do 2 rewrite env_weight_add. lia. @@ -111,31 +141,26 @@ Qed. (* TODO: this is just a special case *) Lemma env_order_disj_union_compat_left Δ Δ' Δ'': - (Δ ≺ Δ'') -> Δ ⊎ Δ' ≺ Δ'' ⊎ Δ'. + (Δ ≺ Δ'') -> Δ ++ Δ' ≺ Δ'' ++ Δ'. Proof. unfold env_order, ltof. intro. do 2 rewrite env_weight_disj_union. lia. Qed. Lemma env_order_disj_union_compat_right Δ Δ' Δ'': - (Δ ≺ Δ'') -> Δ' ⊎ Δ ≺ Δ' ⊎ Δ''. + (Δ ≺ Δ'') -> Δ' ++ Δ ≺ Δ' ++ Δ''. Proof. -intro H. eapply (Proper_env_order _ (Δ ⊎ Δ') _ _ (Δ'' ⊎ Δ')) . ms. -now apply env_order_disj_union_compat_left. -Unshelve. ms. +unfold env_order, ltof. repeat rewrite env_weight_disj_union. lia. Qed. Lemma env_order_disj_union_compat Δ Δ' Δ'' Δ''': - (Δ ≺ Δ'') -> (Δ' ≺ Δ''') -> Δ ⊎ Δ' ≺ Δ'' ⊎ Δ'''. + (Δ ≺ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''. Proof. -intros H1 H2. -transitivity (Δ ⊎ Δ'''). -- now apply env_order_disj_union_compat_right. -- now apply env_order_disj_union_compat_left. +unfold env_order, ltof. repeat rewrite env_weight_disj_union. lia. Qed. - +Hint Unfold env_order_refl : order. Lemma env_order_disj_union_compat_strong_right Δ Δ' Δ'' Δ''': - (Δ ≺ Δ'') -> (Δ' ≼ Δ''') -> Δ ⊎ Δ' ≺ Δ'' ⊎ Δ'''. + (Δ ≺ Δ'') -> (Δ' ≼ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''. Proof. intros H1 H2. destruct H2 as [Hlt|Heq]. @@ -144,36 +169,32 @@ destruct H2 as [Hlt|Heq]. Qed. Lemma env_order_disj_union_compat_strong_left Δ Δ' Δ'' Δ''': - (Δ ≼ Δ'') -> (Δ' ≺ Δ''') -> Δ ⊎ Δ' ≺ Δ'' ⊎ Δ'''. + (Δ ≼ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''. Proof. -intros H1 H2. +intros H1 H2. destruct H1 as [Hlt|Heq]. - unfold env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. - rewrite Heq. now apply env_order_disj_union_compat_right. Qed. -Lemma open_boxes_env_order Δ : (⊗Δ) ≼ Δ. +Lemma weight_open_box φ : weight (⊙ φ) ≤ weight φ. +Proof. destruct φ; simpl; lia. Qed. + +Lemma open_boxes_env_order Δ : (map open_box Δ) ≼ Δ. Proof. -induction Δ as [|φ Δ] using gmultiset_rec. -- right. autorewrite with proof. auto. -- destruct IHΔ as [Hlt | Heq]. - + left. autorewrite with proof. - apply env_order_disj_union_compat_strong_left; trivial. - destruct φ; simpl; try ms. left. - apply env_order_singleton. simpl. lia. - + rewrite open_boxes_disj_union, open_boxes_singleton, Heq. - case_eq (is_box φ); intro Hbox; simpl. - * left. apply env_order_disj_union_compat_strong_right; [|ms]. - destruct φ; simpl in *; try inversion Hbox. - apply env_order_singleton. simpl. lia. - * right. destruct φ; simpl in *; ms. +induction Δ as [|φ Δ]. +- right. trivial. +- destruct IHΔ as [Hlt | Heq]; simpl. + + left. apply env_order_compat'; trivial. apply weight_open_box. + + rewrite Heq. auto with order. destruct φ; simpl; try auto with order. + left. auto with order. Qed. Global Hint Resolve open_boxes_env_order : order. Lemma env_order_0 Δ φ: Δ ≺ Δ • φ. Proof. -unfold env_order, ltof. rewrite env_weight_disj_union, env_weight_singleton. +unfold env_order, ltof. rewrite env_weight_add. apply Nat.lt_add_pos_r. transitivity (5 ^ 0). simpl. lia. apply Nat.pow_lt_mono_r. lia. apply weight_pos. Qed. @@ -193,7 +214,7 @@ Lemma env_order_2 Δ Δ' φ1 φ2 φ: weight φ1 < weight φ -> weight φ2 < wei Proof. intros Hw1 Hw2 Hor. unfold env_order, ltof. repeat rewrite env_weight_add. -apply env_le_weight in Hor. +apply Proper_env_order_refl_env_weight in Hor. replace (weight φ) with (S (pred (weight φ))) by lia. apply Nat.lt_le_pred in Hw1, Hw2. simpl. repeat rewrite Nat.add_assoc. @@ -210,7 +231,7 @@ Lemma env_order_3 Δ Δ' φ1 φ2 φ3 φ: Proof. intros Hw1 Hw2 Hw3 Hor. unfold env_order, ltof. repeat rewrite env_weight_add. -apply env_le_weight in Hor. +apply Proper_env_order_refl_env_weight in Hor. replace (weight φ) with (S (pred (weight φ))) by lia. apply Nat.lt_le_pred in Hw1, Hw2. simpl. repeat rewrite Nat.add_assoc. @@ -227,7 +248,7 @@ Lemma env_order_4 Δ Δ' φ1 φ2 φ3 φ4 φ: Proof. intros Hw1 Hw2 Hw3 Hw4 Hor. unfold env_order, ltof. repeat rewrite env_weight_add. -apply env_le_weight in Hor. +apply Proper_env_order_refl_env_weight in Hor. replace (weight φ) with (S (pred (weight φ))) by lia. apply Nat.lt_le_pred in Hw1, Hw2. simpl. repeat rewrite Nat.add_assoc. @@ -261,6 +282,7 @@ Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order. Ltac get_diff_form g := match g with | ?Γ ∖{[?φ]} => φ | _ (?Γ ∖{[?φ]}) => φ +| _ (remove _ ?φ _) => φ | ?Γ • _ => get_diff_form Γ end. @@ -271,64 +293,87 @@ end. Global Hint Rewrite open_boxes_remove : order. -Ltac prepare_order := -repeat (apply env_order_add_compat); -unfold pointed_env_order; subst; simpl; repeat rewrite open_boxes_add; try match goal with -| Δ := _ |- _ => subst Δ; try prepare_order -| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ => let ψ' := (get_diff_form Γ') in - apply (env_order_equiv_right_compat (difference_singleton Γ ψ' H)) -| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ • ?φ => let ψ' := (get_diff_form Γ') in - apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(difference_singleton Γ ψ' H))) -| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ • _ • _ => let ψ' := (get_diff_form Γ') in -apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))) -end. +Lemma remove_env_order Δ φ: remove form_eq_dec φ Δ ≼ Δ. +Proof. +induction Δ as [|ψ Δ]. +- simpl. right. auto. +- simpl. destruct form_eq_dec. + + subst. destruct IHΔ as [Hlt | Heq]. + * left. apply env_order_cancel_right, Hlt. + * rewrite Heq. auto with order. + + auto with order. +Qed. + +Global Hint Resolve remove_env_order : order. -(* -Lemma make_impl_weight φ ψ: weight (φ ⇢ ψ) <= weight (φ → ψ). +Lemma remove_In_env_order_refl Δ φ: In φ Δ -> remove form_eq_dec φ Δ • φ ≼ Δ. Proof. -assert (H := weight_pos ψ). -assert (H' := weight_pos φ). -revert φ H'; induction ψ; intros φ H'; -unfold make_impl; repeat destruct decide; simpl; try lia. -fold make_impl. -etransitivity. apply IHψ2. -- apply weight_pos. -- apply weight_pos. -- simpl. assert(HH := make_conj_weight lia. -revert (IHψ2 (ma) +induction Δ as [|ψ Δ]. +- intro Hf; contradict Hf. +- intros [Heq | Hin]. + + subst. simpl. destruct form_eq_dec; [|tauto]. auto with order. + + specialize (IHΔ Hin). simpl. case form_eq_dec as [Heq | Hneq]. + * subst. auto with order. + * rewrite (Permutation_swap ψ φ (remove form_eq_dec φ Δ)). auto with order. Qed. -Lemma make_impl_weight2 φ ψ θ: weight (φ ⇢ (ψ ⇢ θ)) <= weight (φ → (ψ → θ)). +Global Hint Resolve remove_In_env_order_refl : order. + +Lemma env_order_lt_le_trans Γ Γ' Γ'' : (Γ ≺ Γ') -> (Γ' ≼ Γ'') -> Γ ≺ Γ''. +Proof. intros Hlt [Hlt' | Heq]. transitivity Γ'; auto with order. now rewrite <- Heq. Qed. + +Lemma env_order_le_lt_trans Γ Γ' Γ'' : (Γ ≼ Γ') -> (Γ' ≺ Γ'') -> Γ ≺ Γ''. +Proof. intros [Hlt' | Heq] Hlt. transitivity Γ'; auto with order. now rewrite Heq. Qed. + +Lemma remove_In_env_order Δ φ: In φ Δ -> remove form_eq_dec φ Δ ≺ Δ. Proof. -pose (make_impl_weight ψ θ). -pose (make_impl_weight φ (ψ ⇢ θ)). -simpl in *. lia. +intro Hin. apply remove_In_env_order_refl in Hin. +eapply env_order_lt_le_trans; [|apply Hin]. auto with order. Qed. +Global Hint Resolve remove_In_env_order : order. -Global Hint Extern 5 (weight (?φ ⇢ ?ψ) < _) => (eapply Nat.le_lt_trans; [eapply make_impl_weight|]) : order. +Lemma elem_of_list_In_1 {A : Type}: ∀ (l : list A) (x : A), x ∈ l -> In x l. +Proof. apply elem_of_list_In. Qed. -Global Hint Extern 5 (weight (?φ ⇢ (?ψ ⇢ ?θ)) < _) => (eapply Nat.le_lt_trans; [eapply make_impl_weight2|]) : order. +Global Hint Resolve elem_of_list_In_1 : order. + + +Ltac prepare_order := +repeat (apply env_order_add_compat); +unfold pointed_env_order; subst; simpl; repeat rewrite open_boxes_add; try match goal with +| Δ := _ |- _ => subst Δ; try prepare_order +| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ => let ψ' := (get_diff_form Γ') in + apply (env_order_equiv_right_compat (difference_singleton Γ ψ' H)) || + (eapply env_order_lt_le_trans ; [| apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial]) +| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ • ?φ => let ψ' := (get_diff_form Γ') in + apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(difference_singleton Γ ψ' H))) +| H : ?ψ ∈ ?Γ |- ?Γ' ≺ ?Γ • _ • _ => let ψ' := (get_diff_form Γ') in +apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))) || +(eapply env_order_le_lt_trans; [| apply env_order_add_compat; +eapply env_order_lt_le_trans; [| (apply env_order_eq_add; apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial) ] ] ) +end. -*) (* ad hoc *) -Lemma openboxes_env_order Δ δ : (⊗ Δ) • δ • δ ≺ Δ • □ δ. +Lemma openboxes_env_order Δ δ : (map open_box Δ) • δ • δ ≺ Δ • □ δ. Proof. -induction Δ using gmultiset_rec. -- eapply @env_order_equiv_left_compat with (∅ • δ • δ). - + now rewrite open_boxes_empty. - + apply env_order_2; simpl; try lia. ms. -- apply (@env_order_equiv_right_compat _ _ (Δ • □ δ • x)); [ms|]. - eapply (@env_order_equiv_left_compat _ _ (⊗ Δ • δ • δ • ⊙ x)). - rewrite open_boxes_disj_union, open_boxes_singleton. ms. - case x; intros; simpl; try (solve[now apply env_order_add_compat]). - transitivity (Δ • □δ • f). - + auto with *. - + apply env_order_1. simpl. auto. +induction Δ as [|x Δ]. +- simpl. unfold env_order, ltof, env_weight. simpl. + repeat rewrite <- plus_n_O. apply Nat.add_lt_mono_l. + rewrite plus_n_O at 1. auto with *. +- apply (@env_order_equiv_right_compat _ _ (Δ • □ δ • x)). constructor. + simpl. + eapply (@env_order_equiv_left_compat _ _ (map open_box Δ • δ • δ • ⊙ x)). + + do 2 (rewrite (Permutation_swap δ (⊙ x)); apply Permutation_skip). trivial. + + case x; intros; simpl; try (solve[now apply env_order_add_compat]). + transitivity (Δ • □δ • f). + * auto with *. + * apply env_order_1. simpl. auto. Qed. Global Hint Resolve openboxes_env_order : order. -Ltac order_tac := prepare_order; auto 10 with order. + +Ltac order_tac := try unfold pointed_env_ms_order; prepare_order; repeat rewrite elements_env_add; auto 10 with order. diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v index 80099d7..1b6fe3f 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -30,19 +30,22 @@ Section PropQuantDefinition. is an implementation of Pitts' Table 5, together with a (mostly automatic) proof that the definition terminates*) +Local Notation "Δ '•' φ" := (cons φ Δ). (* solves the obligations of the following programs *) Obligation Tactic := intros; order_tac. +Notation "□⁻¹ Γ" := (map open_box Γ) (at level 75). + (** First, the implementation of the rules for calculating E. The names of the rules refer to the table in Pitts' paper. *) (** note the use of "lazy" conjunctions, disjunctions and implications *) -Program Definition e_rule {Δ : env} {ϕ : form} +Program Definition e_rule {Δ : list form } {ϕ : form} (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) (θ: form) (Hin : θ ∈ Δ) : form := let E Δ H := fst (EA0 (Δ, ϕ) H) in let A pe0 H := snd (EA0 pe0 H) in -let Δ' := Δ ∖ {[θ]} in +let Δ' := remove form_eq_dec θ Δ in match θ with | Bot => ⊥ (* E0 *) | Var q => @@ -66,19 +69,20 @@ match θ with | ((δ₁→ δ₂)→ δ₃) => (E (Δ'•(δ₂ → δ₃)) _⇢ A (Δ'•(δ₂ → δ₃), δ₁ → δ₂) _) ⇢ E (Δ'•δ₃) _ | Bot → _ => ⊤ -| □ φ => □(E ((⊗Δ') • φ ) _) (* very redundant ; identical for each box *) -| (□δ1 → δ2) => (□(E((⊗Δ') • δ2 • □δ1) _ ⇢ A((⊗Δ') • δ2 • □δ1, δ1) _)) ⇢ E(Δ' • δ2) _ +| □ φ => □(E ((□⁻¹ Δ') • φ ) _) (* very redundant ; identical for each box *) +| (□δ1 → δ2) => (□(E((□⁻¹ Δ') • δ2 • □δ1) _ ⇢ A((□⁻¹ Δ') • δ2 • □δ1, δ1) _)) ⇢ E(Δ' • δ2) _ end. + (** The implementation of the rules for defining A is separated into two pieces. Referring to Table 5 in Pitts, the definition a_rule_env handles A1-8 and A10, and the definition a_rule_form handles A9 and A11-13. *) -Program Definition a_rule_env {Δ : env} {ϕ : form} +Program Definition a_rule_env {Δ : list form} {ϕ : form} (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) (θ: form) (Hin : θ ∈ Δ) : form := let E Δ H := fst (EA0 (Δ, ϕ) H) in let A pe0 H := snd (EA0 pe0 H) in -let Δ' := Δ ∖ {[θ]} in +let Δ' := remove form_eq_dec θ Δ in match θ with | Var q => if decide (p = q) @@ -111,13 +115,13 @@ match θ with | Bot => ⊥ | Bot → _ => ⊥ | □δ => ⊥ -| ((□δ1) → δ2) => (□(E((⊗Δ')• δ2 • □δ1) _ ⇢ A((⊗Δ')• δ2 • □δ1, δ1) _)) ∧ A(Δ' • δ2, ϕ) _ +| ((□δ1) → δ2) => (□(E((□⁻¹ Δ')• δ2 • □δ1) _ ⇢ A((□⁻¹ Δ')• δ2 • □δ1, δ1) _)) ∧ A(Δ' • δ2, ϕ) _ (* using ⊼ here breaks congruence *) end. (* make sure that the proof obligations do not depend on EA0 *) Obligation Tactic := intros Δ ϕ _ _ _; intros; order_tac. -Program Definition a_rule_form {Δ : env} {ϕ : form} +Program Definition a_rule_form {Δ : list form} {ϕ : form} (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) : form := let E pe0 H := fst (EA0 pe0 H) in let A pe0 H := snd (EA0 pe0 H) in @@ -133,21 +137,21 @@ match ϕ with (* A13 *) | ϕ₁→ ϕ₂ => E (Δ•ϕ₁, ϕ₂) _ ⇢ A (Δ•ϕ₁, ϕ₂) _ | Bot => ⊥ -| □δ => □((E ((⊗Δ) • □δ, δ) _) ⇢ A((⊗Δ) • □δ, δ) _) +| □δ => □((E ((□⁻¹ Δ) • □δ, δ) _) ⇢ A((□⁻¹ Δ) • □δ, δ) _) end. Obligation Tactic := intros; order_tac. -Program Fixpoint EA (pe : env * form) {wf pointed_env_order pe} := +Program Fixpoint EA (pe : list form * form) {wf pointed_env_order pe} := let Δ := fst pe in (⋀ (in_map Δ (e_rule EA)), ⋁ (in_map Δ (a_rule_env EA)) ⊻ a_rule_form EA). Next Obligation. apply wf_pointed_order. Defined. -Definition E (pe : env * form) := (EA pe).1. -Definition A (pe : env * form) := (EA pe).2. +Definition E pe := (EA pe).1. +Definition A pe := (EA pe).2. -Definition Ef (ψ : form) := E ({[ψ]}, ⊥). -Definition Af (ψ : form) := A (∅, ψ). +Definition Ef (ψ : form) := E ([ψ], ⊥). +Definition Af (ψ : form) := A ([], ψ). (** Congruence lemmas: if we apply any of e_rule, a_rule_env, or a_rule_form @@ -244,34 +248,44 @@ Section VariablesCorrect. occurs in the E- and A-formulas, and that the E- and A-formulas contain no more variables than the original formula. *) +(* A general tactic for variable occurrences *) +Ltac vars_tac := +intros; subst; +repeat match goal with +| HE : context [occurs_in ?x (?E _ _)], H : occurs_in ?x (?E _ _) |- _ => + apply HE in H +end; +intuition; +repeat match goal with | H : exists x, _ |- _ => destruct H end; +intuition; +simpl in *; in_tac; try (split; [tauto || auto with *|]); simpl in *; +try match goal with +| H : occurs_in _ (?a ⇢ (?b ⇢ ?c)) |- _ => apply occurs_in_make_impl2 in H +| H : occurs_in _ (?a ⇢ ?b) |- _ => apply occurs_in_make_impl in H +| H : occurs_in _ (?a ⊻ ?b) |- _ => apply occurs_in_make_disj in H +| H : occurs_in _ (?a ⊼ ?b) |- _ => apply occurs_in_make_conj in H +|H1 : ?x0 ∈ (⊗ ?Δ), H2 : occurs_in ?x ?x0 |- _ => + apply (occurs_in_open_boxes _ _ _ H2) in H1 +|H1 : ?x0 ∈ (map open_box ?Δ), H2 : occurs_in ?x ?x0 |- _ => + apply (occurs_in_map_open_box _ _ _ H2) in H1 +end; repeat rewrite elem_of_cons in * ; intuition; subst; +repeat match goal with | H : exists x, _ |- _ => destruct H end; intuition; +try multimatch goal with +| H : ?θ0 ∈ ?Δ0 |- context [exists θ, θ ∈ ?Δ /\ occurs_in ?x θ] => + solve[try right; exists θ0; split; [eauto using remove_include|simpl; tauto]; eauto] end. + + (** *** (a) *) -Lemma e_rule_vars (Δ : env) (θ : form) (Hin : θ ∈ Δ) (ϕ : form) +Lemma e_rule_vars Δ (θ : form) (Hin : θ ∈ Δ) (ϕ : form) (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) x (HEA0 : ∀ pe Hpe, (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))) : occurs_in x (e_rule EA0 θ Hin) -> x ≠ p ∧ ∃ θ, θ ∈ Δ /\ occurs_in x θ. Proof. -destruct θ; unfold e_rule. -- case decide. - + simpl. intros Heq HF; subst. tauto. - + intros Hneq Hocc. vars_tac. subst; tauto. -- simpl. tauto. -- vars_tac. -- intro Hocc. apply occurs_in_make_disj in Hocc as [Hocc|Hocc]; vars_tac. -- destruct θ1; try solve[vars_tac]. - + case decide. - * intro; subst. case decide. - -- vars_tac. - -- simpl; tauto. - * intros Hneq Hocc. apply occurs_in_make_impl in Hocc as [Heq | Hocc]; vars_tac. - subst. tauto. - + intros Hocc. apply occurs_in_make_impl in Hocc. - destruct Hocc as [Hocc|Hocc]; [apply occurs_in_make_impl in Hocc as [Hocc|Hocc]|]; vars_tac; subst; tauto. - + intros Hocc. repeat (apply occurs_in_make_impl in Hocc; destruct Hocc as [Hocc|Hocc]); - simpl in Hocc; vars_tac. -- intuition; simpl in *; vars_tac. +destruct θ; unfold e_rule; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. +destruct θ1; repeat case decide; repeat vars_tac. Qed. @@ -284,31 +298,8 @@ Lemma a_rule_env_vars Δ θ Hin ϕ (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): occurs_in x (a_rule_env EA0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). Proof. -destruct θ; unfold a_rule_env. -- case decide. - + intro; subst. case decide; simpl; tauto. - + intros Hneq Hocc. vars_tac. -- simpl. tauto. -- intro Hocc. vars_tac. -- intros Hocc. apply occurs_in_make_conj in Hocc. - destruct Hocc as [Hocc|Hocc]; - apply occurs_in_make_impl in Hocc; vars_tac; vars_tac. -- destruct θ1; try solve[vars_tac]. - + case decide. - * intro; subst. case decide. - -- intros Hp Hocc. vars_tac. - -- simpl; tauto. - * intros Hneq Hocc. apply occurs_in_make_conj in Hocc. - destruct Hocc as [Heq | Hocc]; vars_tac. subst; tauto. - + intros Hocc. apply occurs_in_make_conj in Hocc. - destruct Hocc as [Hocc|Hocc]. - * apply occurs_in_make_impl in Hocc; vars_tac; vars_tac. - * vars_tac. - + intros Hocc. try apply occurs_in_make_conj in Hocc. - destruct Hocc as [Hocc|Hocc]. - * try apply occurs_in_make_conj in Hocc; vars_tac; vars_tac. - * vars_tac. -- simpl; tauto. +destruct θ; unfold a_rule_env; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. +destruct θ1; repeat case decide; repeat vars_tac. Qed. @@ -319,15 +310,7 @@ Lemma a_rule_form_vars Δ ϕ (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): occurs_in x (a_rule_form EA0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). Proof. -destruct ϕ. -- simpl. case decide; simpl; intros; subst; intuition; auto. -- tauto. -- simpl. intros Hocc; apply occurs_in_make_conj in Hocc as [Hocc|Hocc]; vars_tac. -- simpl. intros Hocc; apply occurs_in_make_disj in Hocc as [Hocc|Hocc]; vars_tac. -- simpl. intro Hocc. apply occurs_in_make_impl in Hocc. destruct Hocc; vars_tac; vars_tac. -- intro Hocc. replace (occurs_in x (□ ϕ)) with (occurs_in x ϕ) by trivial. - unfold a_rule_form in Hocc. (* apply occurs_in_make_impl in Hocc. *) - repeat vars_tac; eauto using occurs_in_open_boxes. +destruct ϕ; unfold a_rule_form; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. Qed. Proposition EA_vars Δ ϕ x: @@ -376,10 +359,9 @@ Section EntailmentCorrect. Hint Extern 5 (?a ≺ ?b) => order_tac : proof. Opaque make_disj. Opaque make_conj. - -Lemma a_rule_env_spec Δ θ ϕ Hin (EA0 : ∀ pe, (pe ≺· (Δ, ϕ)) → form * form) - (HEA : forall Δ ϕ Hpe, (Δ ⊢ fst (EA0 (Δ, ϕ) Hpe)) * (Δ• snd(EA0 (Δ, ϕ) Hpe) ⊢ ϕ)) : - (Δ•a_rule_env EA0 θ Hin ⊢ ϕ). +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) ⊢ ϕ)) : + (list_to_set_disj Δ•a_rule_env EA0 θ Hin ⊢ ϕ). Proof with (auto with proof). assert (HE := λ Δ0 ϕ0 Hpe, fst (HEA Δ0 ϕ0 Hpe)). assert (HA := λ Δ0 ϕ0 Hpe, snd (HEA Δ0 ϕ0 Hpe)). @@ -871,9 +853,10 @@ Qed. End PropQuantCorrect. End Correctness. +*) End UniformInterpolation. - +(* (** * Main uniform interpolation Theorem *) Open Scope type_scope. @@ -919,4 +902,4 @@ intros Hp φ Hvarsφ; repeat split. * peapply Hyp. * now rewrite E_of_empty. Qed. - +*) diff --git a/theories/iSL/Simp.v b/theories/iSL/Simp.v index 9241024..3126de4 100644 --- a/theories/iSL/Simp.v +++ b/theories/iSL/Simp.v @@ -529,9 +529,10 @@ Qed. Require Import ISL.PropQuantifiers. -Definition E_simplified (p: variable) (ψ: form) := simp (Ef p ψ). -Definition A_simplified (p: variable) (ψ: form) := simp (Af p ψ). +Definition E_simplified (p: variable) (ψ: form) := simp (E p ([ψ], ⊥)). +Definition A_simplified (p: variable) (ψ: form) := simp (Af p (ψ)). +(* Lemma bot_vars_incl V: vars_incl ⊥ V. Proof. intros x H; unfold In; induction V; auto. @@ -747,7 +748,7 @@ repeat split. apply Hef. * apply (simp_equiv (Af p φ)). Qed. - +*) Require Import String. From fe5a3ecf2b0941702d54ea29dea6496c422f4aef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 28 Aug 2024 00:17:13 +0200 Subject: [PATCH 2/6] Define a linear remove function on lists (to mimic multiset differnce with a singleton). Prove a_rule_env_spec as a poc. --- theories/iSL/Environments.v | 15 +++++- theories/iSL/Order.v | 16 +++---- theories/iSL/PropQuantifiers.v | 87 +++++++++++++++++++++------------- 3 files changed, 74 insertions(+), 44 deletions(-) diff --git a/theories/iSL/Environments.v b/theories/iSL/Environments.v index 8cfffd1..734e04e 100755 --- a/theories/iSL/Environments.v +++ b/theories/iSL/Environments.v @@ -478,10 +478,21 @@ rewrite gmultiset_disj_union_difference with (X := {[θ']}). - now apply gmultiset_singleton_subseteq_l. Qed. +Fixpoint rm x l := match l with +| h :: t => if form_eq_dec x h then t else h :: rm x t +| [] => [] +end. + +Lemma in_rm l x y: In x (rm y l) -> In x l. +Proof. +induction l; simpl. tauto. +destruct form_eq_dec. tauto. firstorder. +Qed. + Lemma remove_include (θ θ' : form) (Δ : list form) : (θ' ∈ Δ) -> - θ ∈ remove form_eq_dec θ' Δ -> θ ∈ Δ. -Proof. intros Hin' Hin. eapply elem_of_list_In, in_remove, elem_of_list_In, Hin. Qed. + θ ∈ rm θ' Δ -> θ ∈ Δ. +Proof. intros Hin' Hin. eapply elem_of_list_In, in_rm, elem_of_list_In, Hin. Qed. (* technical lemma : one can constructively find whether an environment contains diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v index 55f3ee2..b9eda55 100644 --- a/theories/iSL/Order.v +++ b/theories/iSL/Order.v @@ -282,7 +282,7 @@ Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order. Ltac get_diff_form g := match g with | ?Γ ∖{[?φ]} => φ | _ (?Γ ∖{[?φ]}) => φ -| _ (remove _ ?φ _) => φ +| _ (rm ?φ _) => φ | ?Γ • _ => get_diff_form Γ end. @@ -293,20 +293,16 @@ end. Global Hint Rewrite open_boxes_remove : order. -Lemma remove_env_order Δ φ: remove form_eq_dec φ Δ ≼ Δ. +Lemma remove_env_order Δ φ: rm φ Δ ≼ Δ. Proof. induction Δ as [|ψ Δ]. - simpl. right. auto. -- simpl. destruct form_eq_dec. - + subst. destruct IHΔ as [Hlt | Heq]. - * left. apply env_order_cancel_right, Hlt. - * rewrite Heq. auto with order. - + auto with order. +- simpl. destruct form_eq_dec; auto with order. Qed. Global Hint Resolve remove_env_order : order. -Lemma remove_In_env_order_refl Δ φ: In φ Δ -> remove form_eq_dec φ Δ • φ ≼ Δ. +Lemma remove_In_env_order_refl Δ φ: In φ Δ -> rm φ Δ • φ ≼ Δ. Proof. induction Δ as [|ψ Δ]. - intro Hf; contradict Hf. @@ -314,7 +310,7 @@ induction Δ as [|ψ Δ]. + subst. simpl. destruct form_eq_dec; [|tauto]. auto with order. + specialize (IHΔ Hin). simpl. case form_eq_dec as [Heq | Hneq]. * subst. auto with order. - * rewrite (Permutation_swap ψ φ (remove form_eq_dec φ Δ)). auto with order. + * rewrite (Permutation_swap ψ φ (rm φ Δ)). auto with order. Qed. Global Hint Resolve remove_In_env_order_refl : order. @@ -325,7 +321,7 @@ Proof. intros Hlt [Hlt' | Heq]. transitivity Γ'; auto with order. now rewrite < Lemma env_order_le_lt_trans Γ Γ' Γ'' : (Γ ≼ Γ') -> (Γ' ≺ Γ'') -> Γ ≺ Γ''. Proof. intros [Hlt' | Heq] Hlt. transitivity Γ'; auto with order. now rewrite Heq. Qed. -Lemma remove_In_env_order Δ φ: In φ Δ -> remove form_eq_dec φ Δ ≺ Δ. +Lemma remove_In_env_order Δ φ: In φ Δ -> rm φ Δ ≺ Δ. Proof. intro Hin. apply remove_In_env_order_refl in Hin. eapply env_order_lt_le_trans; [|apply Hin]. auto with order. diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v index 1b6fe3f..8ca6fb1 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -45,7 +45,7 @@ Program Definition e_rule {Δ : list form } {ϕ : form} (θ: form) (Hin : θ ∈ Δ) : form := let E Δ H := fst (EA0 (Δ, ϕ) H) in let A pe0 H := snd (EA0 pe0 H) in -let Δ' := remove form_eq_dec θ Δ in +let Δ' := rm θ Δ in match θ with | Bot => ⊥ (* E0 *) | Var q => @@ -78,11 +78,11 @@ end. Referring to Table 5 in Pitts, the definition a_rule_env handles A1-8 and A10, and the definition a_rule_form handles A9 and A11-13. *) Program Definition a_rule_env {Δ : list form} {ϕ : form} - (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) + (EA0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form * form) (θ: form) (Hin : θ ∈ Δ) : form := let E Δ H := fst (EA0 (Δ, ϕ) H) in let A pe0 H := snd (EA0 pe0 H) in -let Δ' := remove form_eq_dec θ Δ in +let Δ' := rm θ Δ in match θ with | Var q => if decide (p = q) @@ -119,6 +119,7 @@ match θ with (* using ⊼ here breaks congruence *) end. + (* make sure that the proof obligations do not depend on EA0 *) Obligation Tactic := intros Δ ϕ _ _ _; intros; order_tac. Program Definition a_rule_form {Δ : list form} {ϕ : form} @@ -283,7 +284,7 @@ Lemma e_rule_vars Δ (θ : form) (Hin : θ ∈ Δ) (ϕ : form) (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))) : occurs_in x (e_rule EA0 θ Hin) -> x ≠ p ∧ ∃ θ, θ ∈ Δ /\ occurs_in x θ. -Proof. +Proof. destruct θ; unfold e_rule; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. destruct θ1; repeat case decide; repeat vars_tac. Qed. @@ -297,7 +298,7 @@ Lemma a_rule_env_vars Δ θ Hin ϕ (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): occurs_in x (a_rule_env EA0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). -Proof. +Proof. destruct θ; unfold a_rule_env; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. destruct θ1; repeat case decide; repeat vars_tac. Qed. @@ -309,14 +310,14 @@ Lemma a_rule_form_vars Δ ϕ (occurs_in x (fst (EA0 pe Hpe)) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ (occurs_in x (snd (EA0 pe Hpe)) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): occurs_in x (a_rule_form EA0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). -Proof. +Proof. destruct ϕ; unfold a_rule_form; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. Qed. Proposition EA_vars Δ ϕ x: (occurs_in x (E (Δ, ϕ)) -> x <> p /\ ∃ θ, θ ∈ Δ /\ occurs_in x θ) /\ (occurs_in x (A (Δ, ϕ)) -> x <> p /\ (occurs_in x ϕ \/ (∃ θ, θ ∈ Δ /\ occurs_in x θ))). -Proof. +Proof. remember (Δ, ϕ) as pe. replace Δ with pe.1 by now subst. replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. revert pe. @@ -359,52 +360,74 @@ Section EntailmentCorrect. Hint Extern 5 (?a ≺ ?b) => order_tac : proof. 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. +Admitted. + +Lemma list_to_set_disj_open_boxes Δ: ((⊗ (list_to_set_disj Δ)) ≡ list_to_set_disj (map open_box Δ)). +Proof. +Admitted. + +Local Ltac l_tac := + 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 (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_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). + 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) ⊢ ϕ)) : - (list_to_set_disj Δ•a_rule_env EA0 θ Hin ⊢ ϕ). + (HEA : forall Δ ϕ Hpe, (list_to_set_disj Δ ⊢ fst (EA0 (Δ, ϕ) Hpe)) * (list_to_set_disj Δ• snd(EA0 (Δ, ϕ) Hpe) ⊢ ϕ)) : + (list_to_set_disj Δ • a_rule_env EA0 θ Hin ⊢ ϕ). Proof with (auto with proof). assert (HE := λ Δ0 ϕ0 Hpe, fst (HEA Δ0 ϕ0 Hpe)). assert (HA := λ Δ0 ϕ0 Hpe, snd (HEA Δ0 ϕ0 Hpe)). clear HEA. -destruct θ; exhibit Hin 1. +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 *. - simpl; case decide; intro Hp. + subst. case_decide; subst; auto with proof. + exch 0... - constructor 2. -- simpl; exch 0. apply AndL. exch 1; exch 0... +- simpl; exch 0. apply AndL. exch 1; exch 0. do 2 l_tac... - apply make_conj_sound_L. exch 0. apply OrL; exch 0. - + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L... (* uses imp_cut *) - + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L. auto with proof. + + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L. + l_tac. apply ImpL... + + apply AndL. l_tac. apply make_impl_sound_L. exch 0. apply make_impl_sound_L... - destruct θ1. + simpl; case decide; intro Hp. * subst. case decide. -- intros Hp. - assert(Hin' : (p → θ2) ∈ Δ ∖ {[Var p]}) - by (rewrite (gmultiset_disj_union_difference' _ _ Hp) in Hin; ms). - assert (Hin'' : Var p ∈ Δ ∖ {[p → θ2]}) by now apply in_difference. - exhibit Hin'' 2. exch 0; exch 1. apply ImpLVar. - exch 1. exch 0. peapply HA. rewrite <- difference_singleton by trivial. reflexivity. + assert (Hin'' : Var p ∈ (list_to_set_disj (rm (p → θ2) Δ) : env)). + (rewrite <- list_to_set_disj_rm; apply in_difference; try easy; now apply elem_of_list_to_set_disj). + exhibit Hin'' 2. exch 0; exch 1. apply ImpLVar. exch 0. backward. + rewrite env_add_remove. exch 0. l_tac... -- intro; constructor 2. * apply make_conj_sound_L. constructor 4. exch 0. exch 1. exch 0. apply ImpLVar. - exch 0. apply weakening. exch 0... + exch 0. exch 1. l_tac. apply weakening... + constructor 2. - + simpl; exch 0. apply ImpLAnd. apply make_impl_complete_L2. exch 0... - + simpl; exch 0. apply ImpLOr. exch 1. exch 0... + + simpl; exch 0. apply ImpLAnd. exch 0. l_tac... + + simpl; exch 0. apply ImpLOr. exch 1. l_tac. exch 0. l_tac... + apply make_conj_sound_L. exch 0. apply ImpLImp; exch 0. - * apply AndL. exch 0. apply make_impl_sound_L. exch 0... - * apply AndL. exch 0. apply weakening, HA. + * apply AndL. exch 0. apply make_impl_sound_L. l_tac. exch 0... + * 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. apply ImpL. + apply make_impl_sound_L. do 3 l_tac. apply ImpL. -- auto with proof. -- apply HA. - * exch 1; exch 0. apply weakening. exch 0. auto with proof. + * exch 1; exch 0. apply weakening. exch 0. l_tac. auto with proof. - auto with proof. Qed. Proposition entail_correct Δ ϕ : (Δ ⊢ E (Δ, ϕ)) * (Δ•A (Δ, ϕ) ⊢ ϕ). -Proof. +Proof. Admitted. remember (Δ, ϕ) as pe. replace Δ with pe.1 by now subst. replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. revert pe. @@ -475,7 +498,7 @@ Section PropQuantCorrect. (** E's second argument is mostly irrelevant and is only there for uniform treatment with A *) Lemma E_irr ϕ' Δ ϕ : E (Δ, ϕ) = E (Δ, ϕ'). -Proof. +Proof. remember ((Δ, ϕ) : pointed_env) as pe. replace Δ with pe.1 by now subst. replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. @@ -492,7 +515,7 @@ Qed. Lemma E_left {Γ} {θ} {Δ} {φ φ'} (Hin : φ ∈ Δ) : (Γ•e_rule (λ pe (_ : pe ≺· (Δ, φ')), EA pe) φ Hin) ⊢ θ -> Γ•E (Δ, φ') ⊢ θ. -Proof. +Proof. intro Hp. rewrite E_eq. destruct (@in_map_in _ _ _ (e_rule (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule]. eapply conjunction_L. @@ -503,7 +526,7 @@ Qed. Lemma A_right {Γ} {Δ} {φ φ'} (Hin : φ ∈ Δ) : Γ ⊢ a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe) φ Hin -> Γ ⊢ A (Δ, φ'). -Proof. intro Hp. rewrite A_eq. +Proof. intro Hp. rewrite A_eq. destruct (@in_map_in _ _ _ (a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule]. eapply make_disj_sound_R, OrR1, disjunction_R. - exact Hrule. @@ -514,7 +537,7 @@ Qed. Proposition pq_correct Γ Δ ϕ: (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> (Γ ⊎ Δ ⊢ ϕ) -> (¬ occurs_in p ϕ -> Γ•E (Δ, ϕ) ⊢ ϕ) * (Γ•E (Δ, ϕ) ⊢ A (Δ, ϕ)). -Proof. +Proof. (* we want to use an E rule *) Ltac Etac := foldEA; intros; match goal with | Hin : ?a ∈ ?Δ |- _•E (?Δ, _) ⊢ _=> apply (E_left Hin); unfold e_rule end. @@ -863,7 +886,7 @@ Open Scope type_scope. Lemma E_of_empty p φ : E p (∅, φ) = (Implies Bot Bot). -Proof. +Proof. rewrite E_eq. rewrite in_map_empty. now unfold conjunction, nodup, foldl. Qed. @@ -879,7 +902,7 @@ Theorem iSL_uniform_interpolation p V: p ∉ V -> * (vars_incl (Af p φ) V) * ({[Af p φ]} ⊢ φ) * (∀ θ, vars_incl θ V -> {[θ]} ⊢ φ -> {[θ]} ⊢ Af p φ). -Proof. +Proof. intros Hp φ Hvarsφ; repeat split. + intros x Hx. apply (EA_vars p _ ⊥ x) in Hx. From 9593473ede338be29902f06b4898486696857c54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 28 Aug 2024 13:26:21 +0200 Subject: [PATCH 3/6] Done using lists instead of multisets. x60 speedup in some cases --- theories/iSL/PropQuantifiers.v | 218 ++++++++++++++++++--------------- 1 file changed, 117 insertions(+), 101 deletions(-) diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v index 8ca6fb1..39ddbdc 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -377,7 +377,9 @@ Admitted. Local Ltac l_tac := 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). @@ -426,8 +428,8 @@ destruct θ; exhibit Hi 1; rewrite list_to_set_disj_rm in *. - auto with proof. Qed. -Proposition entail_correct Δ ϕ : (Δ ⊢ E (Δ, ϕ)) * (Δ•A (Δ, ϕ) ⊢ ϕ). -Proof. Admitted. +Proposition entail_correct Δ ϕ : (list_to_set_disj Δ ⊢ E (Δ, ϕ)) * (list_to_set_disj Δ•A (Δ, ϕ) ⊢ ϕ). +Proof with (auto with proof). remember (Δ, ϕ) as pe. replace Δ with pe.1 by now subst. replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. revert pe. @@ -444,32 +446,35 @@ split. { (* E *) apply conjunction_R1. intros φ Hin. apply in_in_map in Hin. destruct Hin as (ψ&Hin&Heq). subst. -destruct ψ; unfold e_rule; exhibit Hin 0. +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 *. - case decide; intro; subst; simpl; auto using HE with proof. - auto with proof. -- auto 3 with proof. +- apply AndL. do 2 l_tac... - apply make_disj_sound_R, OrL. - + apply OrR1, HE. order_tac. - + apply OrR2, HE. order_tac. + + l_tac. apply OrR1, HE. order_tac. + + l_tac. apply OrR2, HE. order_tac. - destruct ψ1; auto 3 using HE with proof. + case decide; intro Hp. * subst. case decide; intro Hp. - -- assert(Hin'' : Var p ∈ Δ ∖ {[p → ψ2]}) by (apply in_difference; trivial; discriminate). - exhibit Hin'' 1. apply ImpLVar. - peapply (HE (Δ ∖ {[p → ψ2]}•ψ2) ϕ). auto with proof. - rewrite <- difference_singleton; trivial. + -- assert(Hin'' : Var p ∈ (list_to_set_disj (rm (p → ψ2) Δ) : env)) + by (rewrite <- list_to_set_disj_rm; apply in_difference; try easy; now apply elem_of_list_to_set_disj). + exhibit Hin'' 1. apply ImpLVar. exch 0. backward. rewrite env_add_remove. + l_tac. apply HE... -- apply ImpR, ExFalso. - * apply make_impl_sound_R, ImpR. exch 0. apply ImpLVar. exch 0. apply weakening, HE. order_tac. - + remember (Δ ∖ {[(ψ1_1 → ψ1_2) → ψ2]}) as Δ'. - apply make_impl_sound_R, ImpR. apply make_impl_sound_L. exch 0. apply ImpLImp. - * exch 0. auto with proof. - * exch 0. auto with proof. + * apply make_impl_sound_R, ImpR. exch 0. apply ImpLVar. exch 0. + l_tac. apply weakening, HE. order_tac. + + apply ImpLAnd. l_tac... + + apply ImpLOr. do 2 l_tac... + + apply make_impl_sound_R, ImpR, make_impl_sound_L. exch 0. apply ImpLImp. + * exch 0. l_tac. auto with proof. + * 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. - ++ apply weakening, HE. order_tac. - ++ apply HA. order_tac. - -- exch 0; apply weakening, HE. order_tac. -- apply BoxR. apply weakening. box_tac. simpl. apply HE. order_tac. + ++ do 3 l_tac. apply weakening, HE. order_tac. + ++ do 3 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. } (* A *) apply make_disj_sound_L, OrL. @@ -479,8 +484,8 @@ apply make_disj_sound_L, OrL. - destruct ϕ; simpl; auto using HE with proof. + 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. apply make_impl_sound_L, ImpL; auto using HE, HA with proof. - + foldEA. apply BoxR. box_tac. exch 0. apply make_impl_sound_L, ImpL. + + 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. * apply weakening, HE. order_tac. * apply HA. order_tac. Qed. @@ -534,20 +539,24 @@ eapply make_disj_sound_R, OrR1, disjunction_R. Qed. -Proposition pq_correct Γ Δ ϕ: (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> (Γ ⊎ Δ ⊢ ϕ) -> - (¬ occurs_in p ϕ -> Γ•E (Δ, ϕ) ⊢ ϕ) * - (Γ•E (Δ, ϕ) ⊢ A (Δ, ϕ)). +Proposition pq_correct Γ Δ ϕ: + (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> + (Γ ⊎ list_to_set_disj Δ ⊢ ϕ) -> + (¬ occurs_in p ϕ -> Γ•E (Δ, ϕ) ⊢ ϕ) * (Γ•E (Δ, ϕ) ⊢ A (Δ, ϕ)). Proof. (* we want to use an E rule *) -Ltac Etac := foldEA; intros; match goal with | Hin : ?a ∈ ?Δ |- _•E (?Δ, _) ⊢ _=> apply (E_left Hin); unfold e_rule end. +Local Ltac Etac := foldEA; intros; match goal with +| Hin : ?a ∈ list_to_set_disj ?Δ |- _•E (?Δ, _) ⊢ _=> + apply (E_left (proj1 (elem_of_list_to_set_disj _ _) Hin)); unfold e_rule end. (* we want to use an A rule defined in a_rule_env *) -Ltac Atac := foldEA; match goal with | Hin : ?a ∈ ?Δ |- _ ⊢ A (?Δ, _) => apply (A_right Hin); unfold a_rule_env end. +Local Ltac Atac := foldEA; match goal with | Hin : ?a ∈ list_to_set_disj ?Δ |- _ ⊢ A (?Δ, _) => + apply (A_right (proj1 (elem_of_list_to_set_disj _ _) Hin)); unfold a_rule_env end. (* we want to use an A rule defined in a_rule_form *) -Ltac Atac' := foldEA; rewrite A_eq; apply make_disj_sound_R, OrR2; simpl. +Local Ltac Atac' := foldEA; rewrite A_eq; apply make_disj_sound_R, OrR2; simpl. -Ltac occ := simpl; tauto || +Local Ltac occ := simpl; tauto || match goal with | Hnin : ∀ φ0 : form, φ0 ∈ ?Γ → ¬ occurs_in p φ0 |- _ => @@ -563,33 +572,35 @@ match goal with try (now apply Hnin) end. -Ltac equiv_tac := +Local Ltac equiv_tac := multimatch goal with | Heq' : _•_ ≡ _ |- _ => fail | Heq' : _ ≡ _ |- _ ≡ _ => try (rewrite <- difference_singleton; trivial); - rewrite Heq'; + try rewrite Heq'; + repeat rewrite <- list_to_set_disj_env_add; + try rewrite <- list_to_set_disj_rm; try (rewrite union_difference_L by trivial); try (rewrite union_difference_R by trivial); try ms end. intros Hnin Hp. -remember (Γ ⊎ Δ) as Γ' eqn:HH. -assert (Heq: Γ' ≡ Γ ⊎ Δ) by ms. clear HH. +remember (Γ ⊎ list_to_set_disj Δ) as Γ' eqn:HH. +assert (Heq: Γ' ≡ Γ ⊎ list_to_set_disj Δ) by ms. clear HH. revert Heq. dependent induction Hp generalizing Γ Δ Hnin; intro Heq; try (apply env_add_inv in Heq; [|discriminate]); (* try and solve the easy case where the main formula is on the left *) try match goal with -| H : (?Γ0•?a•?b) ≡ Γ ⊎ Δ |- _ => idtac -| H : (?Γ0•?a) ≡ Γ ⊎ Δ |- _ => rename H into Heq; +| H : (?Γ0•?a•?b) ≡ Γ ⊎ list_to_set_disj Δ |- _ => idtac +| H : (?Γ0•?a) ≡ Γ ⊎ list_to_set_disj Δ |- _ => rename H into Heq; assert(Hin : a ∈ (Γ0•a)) by ms; rewrite Heq in Hin; pose(Heq' := Heq); apply env_add_inv' in Heq'; try (case (decide (a ∈ Γ)); intro Hin0; [split; intros; exhibit Hin0 1| - case (decide (a ∈ Δ)); intro Hin0'; + case (decide (a ∈ (list_to_set_disj Δ : env))); intro Hin0'; [|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto]]) end; simpl. @@ -616,7 +627,7 @@ end; simpl. - exch 0. apply AndL. exch 1; exch 0. apply IHHp; trivial. occ. equiv_tac. - exch 0. apply AndL. exch 1; exch 0. apply IHHp; trivial. occ. equiv_tac. - split. - + Etac. apply IHHp; auto. equiv_tac. + + Etac. foldEA. apply IHHp; auto. equiv_tac. + Atac. Etac. apply IHHp; auto. equiv_tac. (* OrR1 & OrR2 *) - split. @@ -638,13 +649,12 @@ end; simpl. + apply IHHp2. occ. equiv_tac. - split. + Etac. apply make_disj_sound_L, OrL; [apply IHHp1| apply IHHp2]; trivial; - rewrite Heq', union_difference_R by trivial; ms. + rewrite Heq', union_difference_R by trivial; equiv_tac. + Atac. apply weakening. apply make_conj_sound_R,AndR, make_impl_sound_R. * apply make_impl_sound_R, ImpR. apply IHHp1; [tauto|equiv_tac]. * apply ImpR. apply IHHp2; [tauto|equiv_tac]. (* ImpR *) -- destruct (IHHp Γ (Δ•φ)) as [IHa IHb]; [auto|ms|]. - split. +- destruct (IHHp Γ (φ :: Δ)) as [IHa IHb]; [auto|ms|]. split. + intro Hocc. apply ImpR. exch 0. erewrite E_irr. apply IHHp; auto. ms. equiv_tac. + Atac'. auto with proof. @@ -661,7 +671,7 @@ end; simpl. exhibit Hin0 1; exhibit Hin2 2; exch 0; exch 1; apply ImpLVar; exch 1; exch 0; (peapply IHHp; trivial; [occ|equiv_tac]). * assert(Hin0' : Var p0 ∈ (Γ0•Var p0•(p0 → φ))) by ms. rewrite Heq in Hin0'. - case (decide (Var p0 ∈ Δ)); intro Hp0; + case (decide (Var p0 ∈ (list_to_set_disj Δ: env))); intro Hp0; [|apply gmultiset_elem_of_disj_union in Hin0'; exfalso; tauto]. (* subcase 3: p0 ∈ Δ ; (p0 → φ) ∈ Γ *) split; try case decide; intros; subst. @@ -674,55 +684,43 @@ end; simpl. + intro. assert(Hin : (Var p0 → φ) ∈ (Γ0•Var p0•(p0 → φ))) by ms. rewrite Heq in Hin. - case (decide ((Var p0 → φ) ∈ Δ)); intro Hin0; + case (decide ((Var p0 → φ) ∈ (list_to_set_disj Δ : env))); intro Hin0; [|apply gmultiset_elem_of_disj_union in Hin; exfalso; tauto]. case (decide (Var p0 ∈ Γ)); intro Hin1. * (* subcase 2: p0 ∈ Γ ; (p0 → φ) ∈ Δ *) do 2 exhibit Hin1 1. split; [intro Hocc|]. -- Etac. case_decide; [auto with *|]. - apply make_impl_sound_L, ImpLVar. apply IHHp; trivial. occ. - rewrite Heq', union_difference_R, <- union_difference_L by trivial; ms. + apply make_impl_sound_L, ImpLVar. exch 0. backward. rewrite env_add_remove. + apply IHHp; trivial. equiv_tac. -- Etac. case_decide; [auto with *|]. apply make_impl_sound_L, ImpLVar. Atac. repeat case_decide; auto 2 with proof; [tauto| tauto|]. - apply make_conj_sound_R, AndR; auto 2 with proof. apply IHHp; [occ|]. - rewrite Heq', union_difference_R, <- union_difference_L by trivial; ms. - * assert(Hin': Var p0 ∈ Γ ⊎ Δ) by (rewrite <- Heq; ms). - apply gmultiset_elem_of_disj_union in Hin'. - case (decide (Var p0 ∈ Δ)); intro Hin1'; [|exfalso; tauto]. + apply make_conj_sound_R, AndR; auto 2 with proof. exch 0. backward. rewrite env_add_remove. + apply IHHp; [occ|]. equiv_tac. + * assert(Hin': Var p0 ∈ Γ ⊎ list_to_set_disj Δ) by (rewrite <- Heq; ms). + apply gmultiset_elem_of_disj_union in Hin'. + case (decide (Var p0 ∈ (list_to_set_disj Δ: env))); intro Hin1'; [|exfalso; tauto]. (* subcase 4: p0,(p0 → φ) ∈ Δ *) case (decide (p = p0)); intro. -- (* subsubcase p = p0 *) + apply elem_of_list_to_set_disj in Hin1'. subst. split; Etac; repeat rewrite decide_True by trivial. - ++ apply IHHp; [tauto|equiv_tac|trivial]. - ++ Atac. repeat rewrite decide_True by trivial. - apply IHHp; [tauto|equiv_tac]. + ++ clear Heq. apply IHHp; [tauto| equiv_tac |trivial]. + ++ Atac. repeat rewrite decide_True by trivial. clear Heq. + apply IHHp; [tauto|equiv_tac]. -- (* subsubcase p ≠ p0 *) - assert ((p0 → φ) ∈ (Δ ∖ {[Var p0]})) by (apply in_difference; trivial; discriminate). - assert((Γ0•Var p0•φ) ≡ (Γ•Var p0) ⊎ (Δ ∖ {[Var p0]} ∖ {[p0 → φ]}•φ)). { - rewrite (assoc disj_union). - apply equiv_disj_union_compat_r. - rewrite (comm disj_union Γ {[Var p0]}). - rewrite <- (assoc disj_union). - rewrite (comm disj_union {[Var p0]}). - apply equiv_disj_union_compat_r. - rewrite Heq''. - rewrite union_difference_R by trivial. - rewrite union_difference_R. ms. - apply in_difference. discriminate. trivial. - } (* not pretty *) split; [intro Hocc|]. ++ apply contraction. Etac. rewrite decide_False by trivial. exch 0. - assert((p0 → φ) ∈ Δ) by ms. Etac. rewrite decide_False by trivial. + assert((p0 → φ) ∈ list_to_set_disj Δ) by ms. Etac. rewrite decide_False by trivial. foldEA. apply make_impl_sound_L, ImpLVar. exch 0. apply weakening. apply IHHp; trivial. - rewrite Heq'. rewrite union_difference_R by trivial. ms. - ++ apply contraction. Etac. exch 0. - assert((p0 → φ) ∈ Δ) by ms. Etac; Atac. + rewrite Heq'. rewrite union_difference_R by trivial. equiv_tac. + ++ apply contraction. Etac. exch 0. + assert((p0 → φ) ∈ list_to_set_disj Δ) by ms. Etac; Atac. repeat rewrite decide_False by trivial. foldEA. apply make_conj_sound_R, AndR; auto 2 with proof. apply make_impl_sound_L. apply ImpLVar. exch 0. apply weakening. - apply IHHp. occ. rewrite Heq'. rewrite union_difference_R by trivial. ms. + apply IHHp. occ. rewrite Heq'. rewrite union_difference_R by trivial. equiv_tac. (* ImpLAnd *) - exch 0. apply ImpLAnd. exch 0. apply IHHp; trivial; [occ|equiv_tac]. - exch 0. apply ImpLAnd. exch 0. apply IHHp; trivial; [occ|equiv_tac]. @@ -743,9 +741,8 @@ end; simpl. simpl. apply Hnin in Hin0. simpl in *. tauto. + erewrite E_irr. apply IHHp2; [occ|equiv_tac|trivial]. - exch 0; apply ImpLImp; exch 0. - + assert(IH: (Γ0•(φ2 → φ3)) ≡ (Γ ∖ {[(φ1 → φ2) → φ3]}•(φ2 → φ3)) ⊎ Δ) by equiv_tac. - erewrite E_irr. apply IHHp1; [occ|equiv_tac| trivial]. - simpl. apply Hnin in Hin0. simpl in Hin0. tauto. + + erewrite E_irr. apply IHHp1; [occ|equiv_tac| trivial]. + simpl. apply Hnin in Hin0. simpl in Hin0. tauto. + apply IHHp2; [occ|equiv_tac]. - (* subcase 2: ((φ1 → φ2) → φ3) ∈ Δ *) split. @@ -761,17 +758,19 @@ end; simpl. rewrite (E_irr (φ1 → φ2)). apply IHHp1; [occ|equiv_tac]. -- apply IHHp2. occ. equiv_tac. - (* ImpBox, external *) - destruct (open_boxes_case Δ) as [[θ Hθ] | Hequiv]. + destruct (open_boxes_case (list_to_set_disj Δ)) as [[θ Hθ] | Hequiv]. + apply contraction. Etac. exch 1; exch 0; apply ImpBox. * box_tac. box_tac. exch 2; exch 1; exch 0. apply weakening. foldEA. erewrite E_irr with (ϕ' := φ1). - exch 1; exch 0. - apply IHHp1. - -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). + exch 1; exch 0. apply IHHp1. + -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. -- rewrite Heq'. assert(Hθ' := In_open_boxes _ _ Hθ). - simpl in *. repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union. - simpl. rewrite <- difference_singleton by trivial. + rewrite <- list_to_set_disj_env_add. + simpl in *. repeat rewrite open_boxes_remove by ms. + rewrite <- list_to_set_disj_open_boxes, open_boxes_disj_union, <- list_to_set_disj_rm. + rewrite open_boxes_remove by ms. simpl. + rewrite <- difference_singleton by trivial. assert((□ φ1 → φ2) ∈ ⊗Γ) by auto with proof. rewrite union_difference_L by trivial. ms. -- intro HF. apply (Hnin _ Hin0). simpl. tauto. * exch 0. apply weakening. exch 0. apply IHHp2; [occ|equiv_tac| trivial]. @@ -786,18 +785,20 @@ end; simpl. simpl. rewrite union_difference_L by trivial. ms. -- intro HF. apply (Hnin _ Hin0). simpl. tauto. * exch 0. apply IHHp2; [occ | rewrite Heq'; equiv_tac | trivial]. -- destruct (open_boxes_case Δ) as [[θ Hθ] | Hequiv]. +- destruct (open_boxes_case (list_to_set_disj Δ)) as [[θ Hθ] | Hequiv]. + apply contraction. Etac. exch 1; exch 0; apply ImpBox. * box_tac. box_tac. exch 2; exch 1; exch 0. apply weakening. foldEA. erewrite E_irr with (ϕ' := φ1). - exch 1; exch 0. - apply IHHp1. + exch 1; exch 0. apply IHHp1. -- occ. intro HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. -- rewrite Heq'. assert(Hθ' := In_open_boxes _ _ Hin0). + rewrite <- list_to_set_disj_env_add. repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union. - simpl. rewrite union_difference_L by trivial. - rewrite <- difference_singleton by auto with proof. ms. + simpl. rewrite union_difference_L by trivial. + rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm. + rewrite open_boxes_remove by ms. simpl. + rewrite <- difference_singleton by auto with proof. ms. -- intro HF. apply (Hnin _ Hin0). simpl. tauto. * exch 0. apply weakening. exch 0. apply IHHp2 ; [occ|equiv_tac]. + erewrite E_irr with (ϕ' := φ1). @@ -819,8 +820,10 @@ end; simpl. ++ intros φ0 Hin1 HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. ++ rewrite Heq'. - repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union. - simpl. rewrite union_difference_R by auto with proof. ms. + repeat rewrite open_boxes_remove by ms. + repeat rewrite <- list_to_set_disj_env_add. + rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm, open_boxes_disj_union. + simpl. rewrite union_difference_R by auto with proof. rewrite open_boxes_remove by ms. ms. -- apply IHHp2. occ. equiv_tac. trivial. + foldEA. Atac. apply AndR. * apply make_impl_sound_L, ImpBox. @@ -829,13 +832,19 @@ end; simpl. apply IHHp1. ++ intros φ0 Hin1 HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. - ++ rewrite Heq', union_difference_R, open_boxes_disj_union, open_boxes_remove by trivial. ms. + ++ rewrite Heq', union_difference_R, open_boxes_disj_union, open_boxes_remove by trivial. + repeat rewrite <- list_to_set_disj_env_add. + rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm. + rewrite open_boxes_remove by ms. ms. -- apply BoxR. box_tac. do 2 apply weakening. apply make_impl_sound_R, ImpR. foldEA. erewrite E_irr with (ϕ' := φ1) by ms. apply IHHp1. ++ intros φ0 Hin1 HF. destruct (occurs_in_open_boxes _ _ _ HF Hin1) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. - ++ rewrite Heq', union_difference_R, open_boxes_disj_union, open_boxes_remove by trivial. ms. + ++ rewrite Heq', union_difference_R, open_boxes_disj_union, open_boxes_remove by trivial. + repeat rewrite <- list_to_set_disj_env_add. + rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm. + rewrite open_boxes_remove by ms. ms. * foldEA. apply make_impl_sound_L, ImpBox. ++ do 2 apply weakening. apply make_impl_sound_R, ImpR. erewrite E_irr with (ϕ' := φ1). @@ -844,10 +853,14 @@ end; simpl. apply (Hnin θ0); ms. ** rewrite Heq'. repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union. - simpl. rewrite union_difference_R. ms. auto with proof. + simpl. rewrite union_difference_R. + repeat rewrite <- list_to_set_disj_env_add. + rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm. + rewrite open_boxes_remove by ms. ms. + auto with proof. ++ apply IHHp2; [occ|equiv_tac]. - split. - + intro Hocc. destruct (open_boxes_case Δ) as [[θ Hθ] | Hequiv]. + + intro Hocc. destruct (open_boxes_case (list_to_set_disj Δ)) as [[θ Hθ] | Hequiv]. * Etac. foldEA. apply BoxR. box_tac. exch 0. erewrite E_irr with (ϕ' := φ); apply IHHp. -- intros φ0 Hφ0 HF. apply gmultiset_elem_of_disj_union in Hφ0. @@ -855,7 +868,10 @@ end; simpl. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. -- rewrite Heq. repeat rewrite open_boxes_remove by ms. rewrite open_boxes_disj_union. - simpl. auto with proof. rewrite <- difference_singleton by auto with proof. ms. + repeat rewrite <- list_to_set_disj_env_add. + rewrite <- list_to_set_disj_open_boxes, <- list_to_set_disj_rm. + rewrite open_boxes_remove by ms. simpl. + rewrite <- difference_singleton by auto with proof. ms. -- trivial. * apply BoxR. box_tac. exch 0. apply open_box_L. erewrite E_irr with (ϕ' := φ). @@ -870,22 +886,24 @@ end; simpl. apply IHHp. * intros φ0 Hφ0 HF. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. - * rewrite Heq, open_boxes_disj_union. ms. + * rewrite Heq, open_boxes_disj_union. + rewrite <- list_to_set_disj_env_add, <- list_to_set_disj_open_boxes. + ms. Qed. End PropQuantCorrect. End Correctness. -*) + End UniformInterpolation. -(* + (** * Main uniform interpolation Theorem *) Open Scope type_scope. -Lemma E_of_empty p φ : E p (∅, φ) = (Implies Bot Bot). +Lemma E_of_empty p φ : E p ([], φ) = (Implies Bot Bot). Proof. rewrite E_eq. rewrite in_map_empty. now unfold conjunction, nodup, foldl. Qed. @@ -904,13 +922,12 @@ Theorem iSL_uniform_interpolation p V: p ∉ V -> * (∀ θ, vars_incl θ V -> {[θ]} ⊢ φ -> {[θ]} ⊢ Af p φ). Proof. intros Hp φ Hvarsφ; repeat split. - + intros x Hx. apply (EA_vars p _ ⊥ x) in Hx. - destruct Hx as [Hneq [θ [Hθ Hocc]]]. apply gmultiset_elem_of_singleton in Hθ. subst. + destruct Hx as [Hneq [θ [Hθ Hocc]]]. apply elem_of_list_singleton in Hθ. subst. apply Hvarsφ in Hocc. destruct Hocc; subst; tauto. - + apply entail_correct. + + replace {[φ]} with (list_to_set_disj [φ] : env). apply entail_correct. simpl. ms. + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp. unfold Ef. rewrite E_irr with (ϕ' := ψ). - * peapply (pq_correct p ∅ {[φ]} ψ). + * peapply (pq_correct p ∅ [φ] ψ). -- intros θ Hin. inversion Hin. -- peapply Hyp. -- intro HF. apply Hψ in HF. tauto. @@ -918,11 +935,10 @@ intros Hp φ Hvarsφ; repeat split. destruct Hx as [Hneq [Hin | [θ [Hθ Hocc]]]]. * apply Hvarsφ in Hin. destruct Hin; subst; tauto. * inversion Hθ. - + peapply (entail_correct p ∅). + + peapply (entail_correct p []). + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp. - apply (TopL_rev _ ⊥). peapply (pq_correct p {[ψ]} ∅ φ). + apply (TopL_rev _ ⊥). peapply (pq_correct p {[ψ]} [] φ). * intros φ0 Hφ0. apply gmultiset_elem_of_singleton in Hφ0. subst. auto with *. * peapply Hyp. * now rewrite E_of_empty. Qed. -*) 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 4/6] 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. From cfa61cc6869544f2bf59c7b8a8afbdc7358021b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 28 Aug 2024 14:34:00 +0200 Subject: [PATCH 5/6] Remove yet another recursive call (A1) --- theories/iSL/PropQuantifiers.v | 33 +++++---------------------------- 1 file changed, 5 insertions(+), 28 deletions(-) diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v index 841a098..5e0eee0 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -89,7 +89,7 @@ match θ with then if decide (Var p = ϕ) then ⊤ (* A10 *) else ⊥ - else A (Δ', ϕ) _ (* A1 *) (* TODO: can be removed? *) + else ⊥ (* A1 modified : A (Δ', ϕ) can be removed *) (* A2 *) | δ₁ ∧ δ₂ => A ((Δ'•δ₁)•δ₂, ϕ) _ (* A3 *) @@ -361,29 +361,6 @@ Hint Extern 5 (?a ≺ ?b) => order_tac : proof. Opaque make_disj. Opaque make_conj. -(* TODO move *) -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. - 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) @@ -617,9 +594,9 @@ end; simpl. - Atac'. case decide; intro; subst; [exfalso; now apply (Hnin _ Hin0)|]; auto with proof. - split. (* case decide; intro; subst; try tauto; auto with proof. *) + intro Hneq. Etac. rewrite decide_False. auto with proof. trivial. - + Atac. case decide. - * intro Heqp0. rewrite decide_True by (f_equal; trivial). auto with proof. - * intro Hneq. foldEA. Atac'. Etac. do 2 rewrite decide_False by trivial. apply Atom. + + case (decide (p = p0)). + * intro Heqp0. Atac. do 2 rewrite decide_True by (f_equal; trivial). auto with proof. + * intro Hneq. Etac. Atac'. do 2 rewrite decide_False by trivial. apply Atom. (* ExFalso *) - auto 2 with proof. - auto 2 with proof. @@ -819,7 +796,7 @@ end; simpl. simpl. rewrite union_difference_L by trivial. ms. -- intro HF. apply (Hnin _ Hin0). simpl. tauto. * erewrite E_irr with (ϕ' := ψ). - exch 0. apply IHHp2. occ. rewrite Heq'. (* TODO: equiv_tac should do that *) equiv_tac. + exch 0. apply IHHp2. occ. clear Hequiv. equiv_tac. - split; Etac. + foldEA. apply make_impl_sound_L, ImpBox. -- do 2 apply weakening. apply make_impl_sound_R, ImpR. From 2701687f23e1a601e836f7feaf0d7b23b5fc03e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 28 Aug 2024 14:34:48 +0200 Subject: [PATCH 6/6] Add a benchmark (now feasible) --- bin/benchmark.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/bin/benchmark.ml b/bin/benchmark.ml index 2b311c8..be1479b 100644 --- a/bin/benchmark.ml +++ b/bin/benchmark.ml @@ -100,6 +100,7 @@ let test_cases = "□((p ∨ q) ∧ (p → r))"; "□(p ∨ □ q ∧ t) ∧(t → p)"; "□(□(t -> t))"; + "(q → (¬p ∨ ¬¬p)) ∧ ((¬p ∨ ¬¬ p) → q)"; ] let _ = bench test_cases