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] 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.