From e83da2d12b164d97ad951172ae27ce559d34659e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Fri, 18 Oct 2024 23:32:35 +0200 Subject: [PATCH] * Decorrelate the definition of Propositional quantifiers from the definition of the simplifications using modules * move a few lemmas to better locations * remove a ocaml compiler warning (unused module type in a functor) to allow compilation of extraction. --- dune | 2 +- theories/extraction/UIML_extraction.v | 7 +- theories/iSL/Optimizations.v | 88 +++++- theories/iSL/Order.v | 15 +- theories/iSL/PropQuantifiers.v | 99 +++--- theories/iSL/SequentProps.v | 94 +++++- theories/iSL/Sequents.v | 9 + theories/iSL/Simp_env.v | 413 ++++++++------------------ theories/iSL/Simplifications.v | 110 +++++++ 9 files changed, 498 insertions(+), 339 deletions(-) create mode 100644 theories/iSL/Simplifications.v diff --git a/dune b/dune index c3d6dfd..772db9f 100644 --- a/dune +++ b/dune @@ -1,4 +1,4 @@ (env (dev - (flags (:standard -w -33)))) + (flags (:standard -w -33-67)))) diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v index 4a62ee3..4e7fe90 100644 --- a/theories/extraction/UIML_extraction.v +++ b/theories/extraction/UIML_extraction.v @@ -5,9 +5,12 @@ Require Import ExtrOcamlBasic ExtrOcamlString. Require Import K.Interpolation.UIK_braga. Require Import KS_export. -Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp_env. - +Require Import ISL.PropQuantifiers ISL.DecisionProcedure. +Require ISL.Simp_env. +(* Simplified propositional quantifiers *) +Module Import S := Simp_env.S. +Module Import SPQr := PropQuant S. Fixpoint MPropF_of_form (f : Formulas.form) : MPropF := match f with diff --git a/theories/iSL/Optimizations.v b/theories/iSL/Optimizations.v index 25a599c..97d7005 100644 --- a/theories/iSL/Optimizations.v +++ b/theories/iSL/Optimizations.v @@ -59,6 +59,7 @@ match obviously_smaller φ ψ with Lemma occurs_in_choose_conj v φ ψ : occurs_in v (choose_conj φ ψ) -> occurs_in v φ \/ occurs_in v ψ. Proof. unfold choose_conj; destruct obviously_smaller; simpl; intros; tauto. Qed. + Definition make_conj φ ψ := match ψ with | ψ1 ∧ ψ2 => @@ -288,6 +289,12 @@ apply AndR. - exch 0. now apply weakening. Qed. +Lemma choose_conj_topL φ : (choose_conj φ ⊤ = φ). +Proof. +unfold choose_conj. +rewrite (obviously_smaller_compatible_LT _ _).2. trivial. +apply ImpR, ExFalso. +Qed. Lemma choose_conj_sound_L Δ φ ψ: (Δ ⊢ φ) -> (Δ ⊢ ψ) -> Δ ⊢ choose_conj φ ψ. @@ -847,12 +854,85 @@ assert(Hcut : forall ψ, ((φ ∈ Δ) + (Γ•ψ ⊢ θ)) -> (Γ•foldl make_co intro Hin. apply Hcut. now left. Qed. +Lemma conjunction_L' Γ Δ ϕ: (Γ ⊎ {[⋀ Δ]} ⊢ ϕ) -> Γ ⊎ list_to_set_disj Δ ⊢ ϕ. +Proof. +revert ϕ. unfold conjunction. +assert( Hstrong: ∀ θ ϕ : form, Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ + → (Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ). +{ + induction Δ as [|δ Δ]; intros θ ϕ; simpl. + - intro Hp. peapply Hp. + - case in_dec; intros Hin Hp. + + peapply (weakening δ). apply IHΔ, Hp. ms. + + simpl in Hp. apply IHΔ in Hp. + peapply (AndL_rev (Γ ⊎ list_to_set_disj Δ) θ δ). apply make_conj_complete_L, Hp. +} + intros; apply additive_cut with (φ := ⊤); eauto with proof. +Qed. + +Lemma conjunction_R Δ: list_to_set_disj Δ ⊢ ⋀ Δ. +Proof. +apply conjunction_R1. intros φ Hφ. apply elem_of_list_to_set_disj in Hφ. +exhibit Hφ 0. apply generalised_axiom. +Qed. + +Lemma conjunction_L'' Γ Δ ϕ: Γ ⊎ list_to_set_disj Δ ⊢ ϕ -> (Γ ⊎ {[⋀ Δ]} ⊢ ϕ). +Proof. +revert ϕ. unfold conjunction. +assert( Hstrong: ∀ θ ϕ : form,(Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ -> Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ). +{ + induction Δ as [|δ Δ]; intros θ ϕ; simpl. + - intro Hp. peapply Hp. + - case in_dec; intros Hin Hp. + + apply IHΔ. + assert(Hin' : δ ∈ (Γ ⊎ list_to_set_disj Δ)). + { apply gmultiset_elem_of_disj_union; right; apply elem_of_list_to_set_disj, elem_of_list_In, Hin. } + exhibit Hin' 1. exch 0. apply contraction. exch 1. exch 0. + rw (symmetry (difference_singleton _ _ Hin')) 2. peapply Hp. + + simpl. apply IHΔ. apply make_conj_sound_L, AndL. peapply Hp. +} +intros. apply Hstrong, weakening. assumption. +Qed. + +(* begin details *) +(** + - [choose_impl_weight]: The weight of the chosen implication is less than or equal to the weight of the implication. + - [choose_impl_top_weight]: The weight of the chosen implication with ⊤ is less than or equal to the weight of the formula. + - [obviously_smaller_top_not_Eq]: ⊤ is not obviously smaller than any formula. + - [contextual_simp_form_weight]: The simplified form of a formula in a given context is either ⊤, or has a weight less than or equal to the original formula. +*) +(* end details *) -Lemma OrR_idemp Γ ψ : Γ ⊢ ψ ∨ ψ -> Γ ⊢ ψ. -Proof. intro Hp. dependent induction Hp; auto with proof. Qed. +Lemma choose_impl_weight φ ψ: weight (choose_impl φ ψ) ≤ weight (φ → ψ). +Proof. +pose (weight_pos φ). pose (weight_pos ψ). +unfold choose_impl; repeat case decide; intros; simpl; lia. +Qed. + +Lemma choose_impl_top_weight ψ: weight (choose_impl ⊤ ψ) ≤ weight ψ. +Proof. +pose (weight_pos ψ). +unfold choose_impl; repeat case decide; intros; try lia. +- destruct (weight_tautology ψ). + + apply obviously_smaller_compatible_LT in e. + apply additive_cut with ⊤; auto with proof. + + subst; simpl in *; tauto || lia. + + subst; simpl in *; tauto || lia. +- destruct (weight_tautology ψ). + + apply obviously_smaller_compatible_LT in e. + apply additive_cut with ⊤; auto with proof. + + subst; simpl in *; tauto || lia. + + subst; simpl in *; tauto || lia. +- contradict n. apply obviously_smaller_compatible_LT. auto with proof. +- contradict n0. apply obviously_smaller_compatible_LT. auto with proof. +- contradict n2. apply obviously_smaller_compatible_LT. auto with proof. +Qed. -Lemma strongness φ : ∅ • φ ⊢ □ φ. +Lemma obviously_smaller_top_not_Eq φ: obviously_smaller ⊤ φ ≠ Eq. Proof. -apply BoxR. box_tac. apply weakening, open_box_L, generalised_axiom. +unfold obviously_smaller. +case Provable_dec. discriminate. intro. case Provable_dec. discriminate. +intro Hf. contradict Hf. auto with proof. Qed. + diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v index 14e4d82..ba2bac8 100644 --- a/theories/iSL/Order.v +++ b/theories/iSL/Order.v @@ -136,6 +136,8 @@ 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. +Global Hint Resolve env_order_compat' : order. + Lemma env_order_add_compat Δ Δ' φ : (Δ ≺ Δ') -> (Δ • φ) ≺ (Δ' • φ). Proof. unfold env_order, ltof. do 2 rewrite env_weight_add. lia. @@ -263,9 +265,12 @@ Qed. Lemma env_order_cancel_right Δ Δ' φ: (Δ ≺ Δ') -> Δ ≺ (Δ' • φ). Proof. etransitivity; [|apply env_order_0]. assumption. Qed. -Lemma env_order_eq_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ). +Lemma env_order_refl_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ). Proof. unfold env_order_refl. do 2 rewrite env_weight_add. lia. Qed. +Lemma env_order_refl_add' Δ Δ' φ φ': weight φ ≤ weight φ' -> (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ'). +Proof. unfold env_order_refl. do 2 rewrite env_weight_add. +intros. apply Nat.add_le_mono. lia. apply Nat.pow_le_mono_r; lia. Qed. Global Hint Resolve env_order_0 : order. Global Hint Resolve env_order_1 : order. @@ -274,7 +279,8 @@ Global Hint Resolve env_order_3 : order. Global Hint Resolve env_order_4 : order. Global Hint Resolve env_order_add_compat : order. Global Hint Resolve env_order_cancel_right : order. -Global Hint Resolve env_order_eq_add : order. +Global Hint Resolve env_order_refl_add : order. +Global Hint Resolve env_order_refl_add' : order. Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order. Ltac get_diff_form g := match g with @@ -351,7 +357,7 @@ unfold pointed_env_order; subst; simpl; repeat rewrite open_boxes_add; try match | 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) ] ] ) +eapply env_order_lt_le_trans; [| (apply env_order_refl_add; apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial) ] ] ) |H : ?a = _ |- context[?a] => rewrite H; try prepare_order end. @@ -419,3 +425,6 @@ Lemma weight_or_bot a b: weight(⊥) < weight (a ∨b). Proof. destruct a; simpl; lia. Qed. Hint Resolve weight_or_bot : order. + +Definition pointed_env_order_refl pe1 pe2 := + env_order_refl (pe1.2 :: pe1.2 :: pe1.1) (pe2.2 :: pe2.2 :: pe2.1). diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v index cc8b466..e674139 100644 --- a/theories/iSL/PropQuantifiers.v +++ b/theories/iSL/PropQuantifiers.v @@ -14,19 +14,23 @@ It consists of two parts: Require Import ISL.Sequents ISL.Formulas. Require Import ISL.SequentProps ISL.Order ISL.Optimizations. Require Import Coq.Program.Equality. (* for dependent induction *) -Require Import ISL.Simp_env. +Require Import ISL.Simplifications. -Section UniformInterpolation. -(** Throughout the construction and proof, we fix a variable p, with respect to - which the propositional quantifier will be computed. *) -Variable p : variable. +(* We define propositional quantifiers given a simplification method + for formulas and contexts *) +Module Type PropQuantT (S : SimpT). + Include S. +End PropQuantT. +Module PropQuant (Import S : SimpT). (** ** Definition of propositional quantifiers. *) Section PropQuantDefinition. - +(** Throughout the construction and proof, we fix a variable p, with respect to + which the propositional quantifier will be computed. *) +Variable p : variable. (** We define the formulas Eφ and Aφ associated to any formula φ. This is an implementation of Pitts' Table 5, together with a (mostly automatic) proof that the definition terminates*) @@ -72,6 +76,7 @@ match θ with | (□δ1 → δ2) => (□(E((□⁻¹ Δ') • δ2 • □δ1) _ ⇢ A((□⁻¹ Δ') • δ2 • □δ1, δ1) _)) ⇢ E(Δ' • δ2) _ end. +Hint Extern 2 (_ <= _) => lia : order. (** 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, @@ -153,10 +158,10 @@ Next Obligation. intros. subst Δ ϕ. eapply env_order_lt_le_trans; [exact H|]. Definition E Δ:= EA true (Δ, ⊥). Definition A := EA false. +(* TODO: simplify the output too now rather than in extraction *) Definition Ef (ψ : form) := E ([ψ]). Definition Af (ψ : form) := A ([], ψ). - (** Congruence lemmas: if we apply any of e_rule, a_rule_env, or a_rule_form to two equal environments, then they give the same results. *) Lemma e_rule_cong Δ ϕ θ (Hin: θ ∈ Δ) E1 A1 E2 A2: @@ -238,9 +243,15 @@ Definition E_eq Δ := proj1 (EA_eq Δ ⊥). Definition A_eq Δ ϕ := proj2 (EA_eq Δ ϕ). End PropQuantDefinition. +End PropQuant. + +Module PropQuantProp (Import S : SimpT) (Import SoundS : SoundSimpT S). +Module Import SP := MakeSimpProps S. +Module Import PropQuandDef := PropQuant S. (** ** Correctness *) Section Correctness. +Context {p : variable}. (** This section contains the proof of Proposition 5, the main correctness result, stating that the E- and A-formulas defined above are indeed existential and universal propositional quantified versions of the original formula, respectively. *) @@ -288,7 +299,7 @@ Lemma e_rule_vars Δ (θ : form) (Hin : θ ∈ Δ) (ϕ : form) (HE0 : ∀ pe Hpe, (occurs_in x (E0 pe Hpe) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ (occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))) : -occurs_in x (e_rule E0 A0 θ Hin) -> x ≠ p ∧ ∃ θ, θ ∈ Δ /\ occurs_in x θ. +occurs_in x (e_rule p E0 A0 θ Hin) -> x ≠ p ∧ ∃ θ, θ ∈ Δ /\ occurs_in x θ. Proof. destruct θ; unfold e_rule; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. destruct θ1; repeat case decide; repeat vars_tac. @@ -304,7 +315,7 @@ Lemma a_rule_env_vars Δ θ Hin ϕ (HEA0 : ∀ pe Hpe, (occurs_in x (E0 pe Hpe) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ (occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): -occurs_in x (a_rule_env E0 A0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). +occurs_in x (a_rule_env p E0 A0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). 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. @@ -318,14 +329,19 @@ Lemma a_rule_form_vars Δ ϕ (HEA0 : ∀ pe Hpe, (occurs_in x (E0 pe Hpe) -> x ≠ p ∧ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ) /\ (occurs_in x (A0 pe Hpe) -> x ≠ p ∧ (occurs_in x pe.2 \/ ∃ θ, θ ∈ pe.1 /\ occurs_in x θ))): - occurs_in x (a_rule_form E0 A0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). + occurs_in x (a_rule_form p E0 A0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ). Proof. destruct ϕ; unfold a_rule_form; simpl; try tauto; try solve [repeat case decide; repeat vars_tac]. Qed. +Lemma simp_form_pointed_env_order_R {pe Δ φ}: (pe ≺· (Δ, simp_form φ)) -> pe ≺· (Δ, φ). +Proof. +intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. +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 θ))). + (occurs_in x (E p Δ) -> x <> p /\ ∃ θ, θ ∈ Δ /\ occurs_in x θ) /\ + (occurs_in x (A p (Δ, ϕ)) -> x <> p /\ (occurs_in x ϕ \/ (∃ θ, θ ∈ Δ /\ occurs_in x θ))). Proof. remember (Δ, ϕ) as pe. replace Δ with pe.1 by now subst. @@ -382,7 +398,7 @@ Lemma a_rule_env_spec (Δ : list form) θ ϕ Hin (E0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) (A0 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), form) (HEA : forall Δ ϕ Hpe, (list_to_set_disj Δ ⊢ E0 (Δ, ϕ) Hpe) * (list_to_set_disj Δ• A0 (Δ, ϕ) Hpe ⊢ ϕ)) : - (list_to_set_disj Δ • a_rule_env E0 A0 θ Hin ⊢ ϕ). + (list_to_set_disj Δ • a_rule_env p E0 A0 θ 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)). @@ -426,7 +442,7 @@ rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat - auto with proof. Qed. -Proposition entail_correct Δ ϕ : (list_to_set_disj Δ ⊢ E Δ) * (list_to_set_disj Δ•A (Δ, ϕ) ⊢ ϕ). +Proposition entail_correct Δ ϕ : (list_to_set_disj Δ ⊢ E p Δ) * (list_to_set_disj Δ•A p (Δ, ϕ) ⊢ ϕ). Proof with (auto with proof). remember (Δ, ϕ) as pe. replace Δ with pe.1 by now subst. @@ -447,7 +463,7 @@ split. { (* E *) apply conjunction_R1. intros φ Hin. apply in_in_map in Hin. destruct Hin as (ψ&Hin&Heq). subst φ. -apply simp_env_equiv_env. +apply equiv_env_simp_env. rewrite <- HeqΔ' in *. clear HeqΔ' Δ. rename Δ' into Δ. assert(Hi : ψ ∈ list_to_set_disj Δ) by now apply elem_of_list_to_set_disj. destruct ψ; unfold e_rule; exhibit Hi 0; rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (list_to_set_disj_rm _ _)) _ _ eq_refl). @@ -480,7 +496,7 @@ destruct ψ; unfold e_rule; exhibit Hi 0; rewrite (proper_Provable _ _ (equiv_di - apply BoxR. apply weakening. box_tac. l_tac. apply HE. order_tac. } (* A *) -apply ImpR_rev, simp_env_equiv_env, ImpR. +apply ImpR_rev, equiv_env_simp_env, ImpR. rewrite <- HeqΔ' in *. clear HeqΔ' Δ. rename Δ' into Δ. apply make_disj_sound_L, OrL. - apply disjunction_L. intros φ Hin. @@ -508,48 +524,49 @@ Section PropQuantCorrect. *) (* This holds by idempotence of simp_env *) -Lemma A_simp_env Δ φ: A(simp_env Δ, φ) = A (Δ, φ). +Lemma A_simp_env Δ φ: A p (simp_env Δ, φ) = A p (Δ, φ). Proof. do 2 rewrite A_eq. now rewrite simp_env_idempotent. Qed. -Lemma E_simp_env Δ: E(simp_env Δ) = E (Δ). +Lemma E_simp_env Δ: E p (simp_env Δ) = E p Δ. Proof. do 2 rewrite E_eq. now rewrite simp_env_idempotent. Qed. Lemma E_left {Γ} {θ} {Δ' Δ : list form} {φ : form}: (Δ' = simp_env Δ) -> ∀ (Hin : φ ∈ Δ'), -(Γ • e_rule (λ pe (_ : pe ≺· (Δ', ⊥)), E pe.1) (λ pe (_ : pe ≺· (Δ', ⊥)), A pe) φ Hin) ⊢ θ -> -Γ • E Δ' ⊢ θ. +(Γ • e_rule p (λ pe (_ : pe ≺· (Δ', ⊥)), E p pe.1) (λ pe (_ : pe ≺· (Δ', ⊥)), A p pe) φ Hin) ⊢ θ -> +Γ • E p Δ' ⊢ θ. Proof. intros Heq Hin Hp. subst Δ'. rewrite E_simp_env, E_eq. -destruct (@in_map_in _ _ _ (e_rule (λ pe (_ : pe ≺· (simp_env Δ, ⊥)), E pe.1) (λ pe (_ : pe ≺· (simp_env Δ, ⊥)), A pe) ) _ Hin) as [Hin' Hrule]. +destruct (@in_map_in _ _ _ (e_rule p (λ pe (_ : pe ≺· (simp_env Δ, ⊥)), E p pe.1) (λ pe (_ : pe ≺· (simp_env Δ, ⊥)), A p pe) ) _ Hin) as [Hin' Hrule]. eapply conjunction_L. - apply Hrule. - exact Hp. Qed. -Lemma A_right {Γ} {Δ Δ'} {φ φ'} : (Δ' = simp_env Δ) -> ∀ (Hin : φ ∈ Δ'), -Γ ⊢ a_rule_env (λ pe (_ : pe ≺· (Δ', φ')), E pe.1) (λ pe (_ : pe ≺· (Δ', φ')), A pe) φ Hin -> -Γ ⊢ A (Δ', φ'). +Local Lemma A_right {Γ} {Δ Δ'} {φ φ'} : (Δ' = simp_env Δ) -> ∀ (Hin : φ ∈ Δ'), +Γ ⊢ a_rule_env p (λ pe (_ : pe ≺· (Δ', φ')), E p pe.1) (λ pe (_ : pe ≺· (Δ', φ')), A p pe) φ Hin -> +Γ ⊢ A p (Δ', φ'). Proof. intros Heq Hin Hp. subst Δ'. rewrite A_simp_env, A_eq. -destruct (@in_map_in _ _ _ (a_rule_env (λ pe (_ : pe ≺· (simp_env Δ, φ')), E pe.1) (λ pe (_ : pe ≺· (simp_env Δ, φ')), A pe)) _ Hin) as [Hin' Hrule]. +destruct (@in_map_in _ _ _ (a_rule_env p (λ pe (_ : pe ≺· (simp_env Δ, φ')), E p pe.1) (λ pe (_ : pe ≺· (simp_env Δ, φ')), A p pe)) _ Hin) as [Hin' Hrule]. eapply make_disj_sound_R, OrR1, disjunction_R. - exact Hrule. - exact Hp. Qed. + Proposition pq_correct Γ Δ ϕ: (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> (Γ ⊎ list_to_set_disj Δ ⊢ ϕ) -> - (¬ occurs_in p ϕ -> Γ•E Δ ⊢ ϕ) * (Γ•E Δ ⊢ A (Δ, ϕ)). + (¬ occurs_in p ϕ -> Γ • E p Δ ⊢ ϕ) * (Γ • E p Δ ⊢ A p (Δ, ϕ)). Proof. (* This proof goes by induction on the ordering w.r.t (Γ ⊎Δ, ϕ) instead of on the structure of Γ ⊎Δ ⊢ ϕ, to allow better rules *) (* we want to use an E rule *) Local Ltac Etac := foldEA; intros; match goal with -| HeqΔ': ?Δ' = simp_env ?Δ, Hin : ?a ∈ list_to_set_disj ?Δ' |- _•E ?Δ' ⊢ _=> +| HeqΔ': ?Δ' = simp_env ?Δ, Hin : ?a ∈ list_to_set_disj ?Δ' |- _ • E _ ?Δ' ⊢ _=> apply (E_left HeqΔ'(proj1 (elem_of_list_to_set_disj _ _) Hin)); unfold e_rule end. (* we want to use an A rule defined in a_rule_env *) Local Ltac Atac := foldEA; match goal with -| HeqΔ': ?Δ' = simp_env ?Δ, Hin : ?a ∈ list_to_set_disj ?Δ' |- _ ⊢ A (?Δ', _) => +| HeqΔ': ?Δ' = simp_env ?Δ, Hin : ?a ∈ list_to_set_disj ?Δ' |- _ ⊢ A _ (?Δ', _) => apply (A_right HeqΔ' (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 *) @@ -596,7 +613,7 @@ assert(Ho' : pointed_env_order_refl (elements Γ ++ simp_env Δ, ϕ) (elements assert(Hind' := λ Γ0 Δ0 ψ Ho, Hind (elements Γ0 ++ Δ0, ψ) (env_order_lt_le_trans _ _ _ Ho Ho') _ _ _ eq_refl). simpl in Hind'. clear Ho'. clear Hind. rename Hind' into Hind. rewrite <- E_simp_env, <- A_simp_env. -assert(Hp' := equiv_env_L1 Γ _ _ _ (symmetric_equiv_env _ _ (simp_env_equiv_env Δ)) Hp). +assert(Hp' := equiv_env_L1 Γ _ _ _ (symmetric_equiv_env _ _ (equiv_env_simp_env Δ)) Hp). remember (simp_env Δ) as Δ'. clear Hp. rename Hp' into Hp. dependent destruction Hp; @@ -919,7 +936,7 @@ end; simpl. repeat rewrite Permutation_middle. apply env_order_disj_union_compat_strong_left. order_tac. apply env_order_2. simpl; lia. simpl; lia. - apply env_order_eq_add. apply env_order_env_order_refl. order_tac. + apply env_order_refl_add. apply env_order_env_order_refl. order_tac. -- intros φ0 Hφ0 HF. apply gmultiset_elem_of_disj_union in Hφ0. destruct Hφ0 as [Hφ0|]; [|ms]. destruct (occurs_in_open_boxes _ _ _ HF Hφ0) as (θ0 & Hθ0 & Hinθ). apply (Hnin θ0); ms. @@ -962,14 +979,12 @@ End PropQuantCorrect. End Correctness. -End UniformInterpolation. - (** ** Main uniform interpolation Theorem *) Open Scope type_scope. - +Context {p : variable}. Lemma E_of_empty p : E p [] = (Implies Bot Bot). -Proof. +Proof. rewrite E_eq, simp_env_nil. simpl. rewrite in_map_empty. now unfold conjunction, nodup, foldl. Qed. @@ -987,23 +1002,25 @@ 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. + + intros x Hx. apply (@EA_vars p _ ⊥ x) in Hx. destruct Hx as [Hneq [θ [Hθ Hocc]]]. apply elem_of_list_singleton in Hθ. subst. apply Hvarsφ in Hocc. destruct Hocc; subst; tauto. - + replace {[φ]} with (list_to_set_disj [φ] : env). apply (entail_correct _ _ ⊥). ms. + + replace {[φ]} with (list_to_set_disj [φ] : env). apply (@entail_correct _ _ ⊥). ms. + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp. unfold Ef. - * peapply (pq_correct p ∅ [φ] ψ). + * peapply (@pq_correct p ∅ [φ] ψ). -- intros θ Hin. inversion Hin. -- peapply Hyp. -- intro HF. apply Hψ in HF. tauto. - + intros x Hx. apply (EA_vars p ∅ φ x) in Hx. + + intros x Hx. apply (@EA_vars p ∅ φ x) in Hx. 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. \ No newline at end of file +Qed. + +End PropQuantProp. diff --git a/theories/iSL/SequentProps.v b/theories/iSL/SequentProps.v index d65ef40..f9a36b1 100644 --- a/theories/iSL/SequentProps.v +++ b/theories/iSL/SequentProps.v @@ -870,4 +870,96 @@ induction Δ as [|ψ Δ IH] using gmultiset_rec. ++ apply list_to_set_disj_perm, Permutation_map. apply Permutation_refl', gmultiset_elements_singleton. ++ simpl. ms. -Qed. \ No newline at end of file +Qed. + +Lemma OrR_idemp Γ ψ : Γ ⊢ ψ ∨ ψ -> Γ ⊢ ψ. +Proof. intro Hp. dependent induction Hp; auto with proof. Qed. + + +Lemma strongness φ : ∅ • φ ⊢ □ φ. +Proof. +apply BoxR. box_tac. apply weakening, open_box_L, generalised_axiom. +Qed. + +(** + - [var_not_tautology]: A variable cannot be a tautology. + - [bot_not_tautology]: ⊥ is not a tautology. + - [box_var_not_tautology]: A boxed variable cannot be a tautology. + - [box_bot_not_tautology]: A boxed ⊥ cannot be a tautology. +*) + +Lemma bot_not_tautology : (∅ ⊢ ⊥) -> False. +Proof. +intro Hf. dependent destruction Hf; simpl in *; +match goal with x : _ ⊎ {[+?φ+]} = _ |- _ => +exfalso; eapply (gmultiset_elem_of_empty φ); setoid_rewrite <- x; ms end. +Qed. + +Lemma var_not_tautology v: (∅ ⊢ Var v) -> False. +Proof. +intro Hp. +remember ∅ as Γ. +dependent induction Hp; +match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; + pose(Heq' := env_equiv_eq _ _ Heq); + apply (gmultiset_not_elem_of_empty f); rewrite Heq'; ms + end. +Qed. + +Lemma box_var_not_tautology v: (∅ ⊢ □ (Var v)) -> False. +Proof. +intro Hp. +remember ∅ as Γ. +dependent induction Hp; +try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; + pose(Heq' := env_equiv_eq _ _ Heq); + apply (gmultiset_not_elem_of_empty f); rewrite Heq'; ms + end. +rewrite open_boxes_empty in Hp. +clear IHHp. +dependent induction Hp; +try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; + pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; + apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; + [discriminate|ms] + end. +Qed. + +Lemma box_bot_not_tautology: (∅ ⊢ □⊥) -> False. +Proof. + intro Hp. + +dependent induction Hp; +try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; + pose(Heq' := env_equiv_eq _ _ Heq); + apply (gmultiset_not_elem_of_empty f); rewrite Heq'; ms + end. +rewrite open_boxes_empty in Hp. +clear IHHp. +dependent induction Hp; +try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; + pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; + apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; + [discriminate|ms] + end. +Qed. + +(* A tautology is either equal to ⊤ or has a weight of at least 3. *) +Lemma weight_tautology φ: (∅ ⊢ φ) -> {φ = ⊤} + {3 ≤ weight φ}. +Proof. +intro Hp. +destruct φ. +- contradict Hp. apply var_not_tautology. +- contradict Hp. apply bot_not_tautology. +- right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. +- right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. +- right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. +- destruct φ. + + contradict Hp. apply box_var_not_tautology. + + contradict Hp. apply box_bot_not_tautology. + + right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. + + right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. + + right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. + + right. simpl. pose(weight_pos φ). lia. +Qed. + diff --git a/theories/iSL/Sequents.v b/theories/iSL/Sequents.v index c34b0f0..6fcb47f 100644 --- a/theories/iSL/Sequents.v +++ b/theories/iSL/Sequents.v @@ -66,6 +66,15 @@ Global Hint Constructors Provable : proof. Global Instance proper_Provable : Proper ((≡@{env}) ==> (=) ==> (=)) Provable. Proof. intros Γ Γ' Heq φ φ' Heq'. ms. Qed. +Global Ltac equiv_tac := + repeat rewrite <- list_to_set_disj_rm; + repeat rewrite <- list_to_set_disj_env_add; + repeat (rewrite <- difference_singleton; trivial); + try rewrite <- list_to_set_disj_rm; + try (rewrite union_difference_L by trivial); + try (rewrite union_difference_R by trivial); + try ms. + (** We introduce a tactic "peapply" which allows for application of a G4ip rule even in case the environment needs to be reordered *) Ltac peapply th := diff --git a/theories/iSL/Simp_env.v b/theories/iSL/Simp_env.v index bdf6725..b506b99 100644 --- a/theories/iSL/Simp_env.v +++ b/theories/iSL/Simp_env.v @@ -1,7 +1,7 @@ (** * Simplifications for formulas and contexts -This file defines the main simplifications for formulas and contexts, maintaining intuitionistic -equivalence. +This file defines the main simplifications for formulas and contexts, +maintaining intuitionistic equivalence. *) @@ -11,12 +11,17 @@ Require Import ISL.Sequents ISL.SequentProps. Require Import ISL.Order ISL.DecisionProcedure. Require Import ISL.Cut. Require Import ISL.Optimizations. (* NB This import must come last. *) +Require Import ISL.Simplifications. + + +Module S <: SimpT. (** ** Applicability of rules - This section provides definitions for checking the applicability of various logical rules - within a given context (list of formulas). The definitions use decidable existence checks - to determine if specific patterns of formulas are present in the context. + This section provides definitions for checking the applicability of various + logical rules within a given context (list of formulas). + The definitions use decidable existence checks to determine if specific + patterns of formulas are present in the context. *) Definition applicable_AndL (Γ : list form): {ψ1 & {ψ2 | (And ψ1 ψ2) ∈ Γ}} + (∀ ψ1 ψ2, (And ψ1 ψ2) ∈ Γ -> False). Proof. @@ -31,8 +36,10 @@ Definition applicable_ImpLVar (Γ : list form): {q & {ψ | Var q ∈ Γ /\ (Implies (Var q) ψ) ∈ Γ}} + (∀ q ψ, Var q ∈ Γ -> (Implies (Var q) ψ) ∈ Γ -> False). Proof. - pose (fIp :=λ p θ, match θ with | Implies (Var q) _ => if decide (p = q) then true else false | _ => false end). - pose (fp:= (fun θ => match θ with |Var p => if (exists_dec (fIp p) Γ) then true else false | _ => false end)). + pose (fIp :=λ p θ, match θ with | Implies (Var q) _ => + if decide (p = q) then true else false | _ => false end). + pose (fp:= (fun θ => match θ with |Var p => + if (exists_dec (fIp p) Γ) then true else false | _ => false end)). destruct (exists_dec fp Γ) as [(θ & Hin & Hθ) | Hf]. - left. subst fp. destruct θ. 2-6: auto with *. case exists_dec as [(ψ &Hinψ & Hψ)|] in Hθ; [|auto with *]. @@ -40,7 +47,8 @@ Proof. destruct ψ1. 2-6: auto with *. case decide in Hψ; [|auto with *]. subst. apply elem_of_list_In in Hinψ, Hin. do 2 eexists. split; eauto. - - right. intros q ψ Hp Hψ. rewrite elem_of_list_In in Hp, Hψ. apply Hf in Hp. subst fp fIp. + - right. intros q ψ Hp Hψ. rewrite elem_of_list_In in Hp, Hψ. + apply Hf in Hp. subst fp fIp. simpl in Hp. case exists_dec as [|Hf'] in Hp. auto with *. apply (Hf' _ Hψ). rewrite decide_True; trivial. auto with *. Defined. @@ -49,11 +57,14 @@ Definition applicable_ImpLAnd (Γ : list form): {φ1 & {φ2 & {φ3 | (Implies (And φ1 φ2) φ3) ∈ Γ}}} + (∀ φ1 φ2 φ3, (Implies (And φ1 φ2) φ3) ∈ Γ -> False). Proof. - pose (fII := (fun θ => match θ with |Implies (And _ _) _ => true | _ => false end)). + pose (fII := (fun θ => match θ with |Implies (And _ _) _ => true + | _ => false end)). destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf]. - left. subst fII. destruct θ. 1-4, 6: auto with *. - destruct θ1. 1-2,4-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto. - - right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fII. simpl in Hψ. tauto. + destruct θ1. 1-2,4-6: auto with *. + do 3 eexists; apply elem_of_list_In; eauto. + - right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. + apply Hf in Hψ. subst fII. simpl in Hψ. tauto. Defined. Definition applicable_ImpLOr (Γ : list form): @@ -64,7 +75,8 @@ Proof. destruct (exists_dec fII Γ) as [(θ & Hin & Hθ) | Hf]. - left. subst fII. destruct θ. 1-4, 6: auto with *. destruct θ1. 1-3, 5-6: auto with *. do 3 eexists; apply elem_of_list_In; eauto. - - right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fII. simpl in Hψ. tauto. + - right. intros ψ1 ψ2 ψ3 Hψ. rewrite elem_of_list_In in Hψ. + apply Hf in Hψ. subst fII. simpl in Hψ. tauto. Defined. @@ -82,28 +94,33 @@ destruct (exists_dec (λ φ, if Provable_dec (rm φ Γ) φ then true else false) Defined. (** ** Ternary if notation - This section defines a set of functions and notations for handling ternary conditional logic. The functions [sumor_bind0], [sumor_bind1], [sumor_bind2], and - [sumor_bind3] provide a way to handle different levels of nested dependent sums and + This section defines a set of functions and notations for handling ternary + conditional logic. The functions [sumor_bind0], [sumor_bind1], [sumor_bind2], and + [sumor_bind3] provide a way to handle different levels of nested dependent sums and propositions. Each function takes a sum type and applies a function to the left component - if it exists, or returns a default value otherwise. - The notations `cond '?' A '⋮₀' B`, `cond '?' A '⋮₁' B`, `cond '?' A '⋮₂' B`, and `cond '?' A '⋮₃' B` are provided to simplify the usage of these functions. + if it exists, or returns a default value otherwise. The notations + `cond '?' A '⋮₀' B`, `cond '?' A '⋮₁' B`, `cond '?' A '⋮₂' B`, and `cond '?' A '⋮₃' B` + are provided to simplify the usage of these functions. This notation is used in the definition of [simp_env]. *) -Definition sumor_bind0 {A} {B : Prop} {C}: A + B -> (A -> C) -> C -> C := +Definition sumor_bind0 {A} {B : Prop} {C}: + A + B -> (A -> C) -> C -> C := λ qH f c, match qH with | inl a => f a | inr _ => c end. -Definition sumor_bind1 {A A'} {B : Prop} {C}: {q : A | A' q} + B -> (forall x (_ : A' x), C) -> C -> C := +Definition sumor_bind1 {A A'} {B : Prop} {C}: + {q : A | A' q} + B -> (forall x (_ : A' x), C) -> C -> C := λ qH f c, match qH with | inl (exist _ q Hq) => f q Hq | inr _ => c end. -Definition sumor_bind2 {A A' A''} {B : Prop} {C}: {q : A & {r : A' | A'' q r}} + B -> (forall x y (_ : A'' x y), C) -> C -> C := +Definition sumor_bind2 {A A' A''} {B : Prop} {C}: + {q : A & {r : A' | A'' q r}} + B -> (forall x y (_ : A'' x y), C) -> C -> C := λ qH f c, match qH with | inl (existT q (exist _ r Hq)) => f q r Hq @@ -111,7 +128,8 @@ match qH with end. Definition sumor_bind3 {A A' A'' A'''} {B : Prop} {C}: - {q : A & {r : A' & { s : A'' | A''' q r s}}} + B -> (forall x y z (_ : A''' x y z), C) -> C -> C := + {q : A & {r : A' & { s : A'' | A''' q r s}}} + B -> + (forall x y z (_ : A''' x y z), C) -> C -> C := λ qH f c, match qH with | inl (existT q (existT r (exist _ s Hq))) => f q r s Hq @@ -127,8 +145,10 @@ Local Notation "Δ '•' φ" := (cons φ Δ) : list_scope. (** ** Definition of contextual simplification *) -(** The [contextual_simp_form] function performs contextual simplification on a given formula [φ] within a context [Δ]. - It recursively simplifies conjunctions, disjunctions, and implications by considering the context in which each subformula appears. +(** The [contextual_simp_form] function performs contextual simplification on a + given formula [φ] within a context [Δ]. + It recursively simplifies conjunctions, disjunctions, and implications by + considering the context in which each subformula appears. *) Fixpoint contextual_simp_form Δ φ := match φ with @@ -146,181 +166,59 @@ end. their simplified forms. *) -(* begin details *) -(** - - [choose_conj_topL]: The conjunction of a formula with ⊤ is the formula itself. - - [empty_entails_not_bot]: The empty context does not entail ⊥. - - [var_not_tautology]: A variable cannot be a tautology. - - [bot_not_tautology]: ⊥ is not a tautology. - - [box_var_not_tautology]: A boxed variable cannot be a tautology. - - [box_bot_not_tautology]: A boxed ⊥ cannot be a tautology. - - [weight_tautology]: A tautology is either equal to ⊤ or has a weight of at least 3. - - [choose_impl_weight]: The weight of the chosen implication is less than or equal to the weight of the implication. - - [choose_impl_top_weight]: The weight of the chosen implication with ⊤ is less than or equal to the weight of the formula. - - [obviously_smaller_top_not_Eq]: ⊤ is not obviously smaller than any formula. - - [contextual_simp_form_weight]: The simplified form of a formula in a given context is either ⊤, or has a weight less than or equal to the original formula. -*) -(* end details *) - -Lemma choose_conj_topL φ : (choose_conj φ ⊤ = φ). -Proof. -unfold make_conj, choose_conj. -rewrite (obviously_smaller_compatible_LT _ _).2. trivial. auto with proof. -Qed. - - -Lemma empty_entails_not_bot : (∅ ⊢ ⊥) -> False. -Proof. -intro Hf. dependent destruction Hf; simpl in *; -match goal with x : _ ⊎ {[+?φ+]} = _ |- _ => -exfalso; eapply (gmultiset_elem_of_empty φ); setoid_rewrite <- x; ms end. -Qed. - -Lemma var_not_tautology v: (⊤ ≼ Var v) -> False. -Proof. -unfold Lindenbaum_Tarski_preorder. intro Hp. -remember ∅ as Γ. -dependent induction Hp; -try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; - pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; - apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; [discriminate|ms] - end. -Qed. - -Lemma bot_not_tautology: (⊤ ≼ ⊥) -> False. -Proof. -unfold Lindenbaum_Tarski_preorder. intro Hp. -remember ∅ as Γ. -dependent induction Hp; -try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; - pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; - apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; [discriminate|ms] - end. -Qed. - -Lemma box_var_not_tautology v: (⊤ ≼ □ (Var v)) -> False. -Proof. -unfold Lindenbaum_Tarski_preorder. intro Hp. -remember ∅ as Γ. -dependent induction Hp; -try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; - pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; - apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; [discriminate|ms] - end. -assert(Hp' : ∅ • □ v ⊢ v). -{ apply additive_cut with ⊤. apply top_provable. exch 0. peapply Hp. } -clear IHHp Hp. -dependent induction Hp'; -try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; - pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; - apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; [discriminate|ms] - end. -Qed. - -Lemma box_bot_not_tautology: (⊤ ≼ □⊥) -> False. -Proof. -unfold Lindenbaum_Tarski_preorder. intro Hp. -remember ∅ as Γ. -dependent induction Hp; -try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; - pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; - apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; [discriminate|ms] - end. -assert(Hp' : ∅ • □ ⊥ ⊢ ⊥). -{ apply additive_cut with ⊤. apply top_provable. exch 0. peapply Hp. } -clear IHHp Hp. -dependent induction Hp'; -try match goal with | Heq : (_ • ?f%stdpp) = _ |- _ => symmetry in Heq; - pose(Heq' := env_equiv_eq _ _ Heq); apply env_add_inv' in Heq'; - apply (gmultiset_not_elem_of_empty f); rewrite Heq'; apply in_difference; [discriminate|ms] - end. -Qed. - -Lemma weight_tautology φ: (⊤ ≼ φ) -> {φ = ⊤} + {3 ≤ weight φ}. -Proof. -intro Hp. -destruct φ. -- contradict Hp. apply var_not_tautology. -- contradict Hp. apply bot_not_tautology. -- right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. -- right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. -- right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. -- destruct φ. - + contradict Hp. apply box_var_not_tautology. - + contradict Hp. apply box_bot_not_tautology. - + right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. - + right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. - + right. simpl. pose(weight_pos φ1). pose(weight_pos φ2). lia. - + right. simpl. pose(weight_pos φ). lia. -Qed. - -Lemma choose_impl_weight φ ψ: weight (choose_impl φ ψ) ≤ weight (φ → ψ). -Proof. -pose (weight_pos φ). pose (weight_pos ψ). -unfold choose_impl; repeat case decide; intros; simpl; lia. -Qed. - -Lemma choose_impl_top_weight ψ: weight (choose_impl ⊤ ψ) ≤ weight ψ. -Proof. -pose (weight_pos ψ). -unfold choose_impl; repeat case decide; intros; try lia. -- apply obviously_smaller_compatible_LT, weight_tautology in e. destruct e; subst; simpl in *; tauto || lia. -- apply obviously_smaller_compatible_LT, weight_tautology in e. destruct e; subst; simpl in *. -discriminate. lia. -- apply obviously_smaller_compatible_LT, weight_tautology in e. destruct e; subst; simpl in *; lia. -- contradict n. apply obviously_smaller_compatible_LT. auto with proof. -- contradict n0. apply obviously_smaller_compatible_LT. auto with proof. -- contradict n2. apply obviously_smaller_compatible_LT. auto with proof. -Qed. - -Lemma obviously_smaller_top_not_Eq φ: obviously_smaller ⊤ φ ≠ Eq. -Proof. -unfold obviously_smaller. -case Provable_dec. discriminate. intro. case Provable_dec. discriminate. -intro Hf. contradict Hf. auto with proof. -Qed. - Lemma contextual_simp_form_weight Δ φ: - {contextual_simp_form Δ φ = ⊤} + {weight (contextual_simp_form Δ φ) ≤ weight φ}. + (contextual_simp_form Δ φ = ⊤ /\ (φ = Bot \/ φ = (□ Bot) \/ exists (v : variable), φ = v \/ φ = □ v)) \/ + (weight (contextual_simp_form Δ φ) ≤ weight φ). Proof. revert Δ. induction φ; intro Δ; simpl. -1,2: (case Provable_dec; simpl; [tauto| right; lia]). +1, 2: (case Provable_dec; simpl; [left; intuition; eauto| right; lia]). +1-3:right; try pose (weight_pos φ1); try pose (weight_pos φ2). - pose (contextual_simp_form (Δ • φ1) φ2) as φ2'. - destruct (IHφ1 (φ2' :: Δ)) as [Heq1 | Hle1]; destruct (IHφ2 (φ1 :: Δ)) as [Heq2 | Hle2]; + destruct (IHφ1 (φ2' :: Δ)) as [[Heq1 _]| Hle1]; + destruct (IHφ2 (φ1 :: Δ)) as [[Heq2 _]| Hle2]; repeat rewrite ?Heq1, ?Heq2; subst φ2'. - + rewrite choose_conj_topL. rewrite Heq2 in Heq1. tauto. - + unfold choose_conj. rewrite Heq1. case_eq (obviously_smaller ⊤ (contextual_simp_form (φ1 :: Δ) φ2)). + + rewrite choose_conj_topL. rewrite Heq2 in Heq1. rewrite Heq1. simpl. lia. + + unfold choose_conj. rewrite Heq1. + case_eq (obviously_smaller ⊤ (contextual_simp_form (φ1 :: Δ) φ2)). * intro Hf. contradict Hf. apply obviously_smaller_top_not_Eq. - * intro. tauto. - * intro. right. destruct (IHφ2 (φ1 :: Δ)); lia. + * intro. simpl; lia. + * intro. destruct (IHφ2 (φ1 :: Δ)); lia. + rewrite choose_conj_topL. pose (weight_pos φ1); pose (weight_pos φ2). - right. simpl. destruct (IHφ1 (⊤ :: Δ)) as [e|]. rewrite e. simpl. lia. lia. - + right. unfold choose_conj. destruct obviously_smaller; simpl; lia. -- destruct (IHφ1 Δ) as [Heq1 | Hle1]; destruct (IHφ2 Δ) as [Heq2 | Hle2]; + simpl. destruct (IHφ1 (⊤ :: Δ)) as [[e _]|]. rewrite e. simpl. lia. lia. + + unfold choose_conj. destruct obviously_smaller; simpl; lia. +- destruct (IHφ1 Δ) as [[Heq1 _] | Hle1]; destruct (IHφ2 Δ) as [[Heq2 _] | Hle2]; repeat rewrite ?Heq1, ?Heq2; unfold choose_disj. - + left. rewrite (obviously_smaller_compatible_LT _ _).2. trivial. auto with proof. + + rewrite (obviously_smaller_compatible_LT _ _).2. simpl; lia. apply generalised_axiom. + case_eq (obviously_smaller ⊤ (contextual_simp_form Δ φ2)). * intro Hf. contradict Hf. apply obviously_smaller_top_not_Eq. * intro. right. lia. - * tauto. - + rewrite (obviously_smaller_compatible_LT _ _).2. tauto. auto with proof. - + right. destruct obviously_smaller; simpl; lia. + * intro. simpl; lia. + + rewrite (obviously_smaller_compatible_LT _ _).2. simpl; lia. + auto with proof. + + destruct obviously_smaller; simpl; lia. - pose (weight_pos φ1). pose (weight_pos φ2). - destruct (IHφ1 Δ) as [Heq1 | Hle1]; destruct (IHφ2 (φ1 :: Δ)) as [Heq2 | Hle2]; + destruct (IHφ1 Δ) as [[Heq1 _] | Hle1]; + destruct (IHφ2 (φ1 :: Δ)) as [[Heq2 _] | Hle2]; repeat rewrite ?Heq1, ?Heq2. - + right. etransitivity. apply choose_impl_top_weight. simpl. lia. - + right. etransitivity. apply choose_impl_top_weight. simpl. lia. - + left. unfold choose_impl. rewrite (obviously_smaller_compatible_LT _ ⊤).2; simpl. trivial. + + etransitivity. apply choose_impl_top_weight. simpl. lia. + + etransitivity. apply choose_impl_top_weight. simpl. lia. + + unfold choose_impl. + rewrite (obviously_smaller_compatible_LT _ ⊤).2; simpl. lia. auto with proof. - + right. etransitivity. apply choose_impl_weight. simpl. lia. -- case Provable_dec. tauto. right; simpl; lia. + + etransitivity. apply choose_impl_weight. simpl. lia. +- destruct φ. + 1, 2: (case Provable_dec; simpl; [left; intuition; eauto| right; lia]). + 1-4:right; try pose (weight_pos φ1); try pose (weight_pos φ2); + case Provable_dec; simpl; try lia. + pose (weight_pos φ). lia. Qed. (** ** Simplifying environments This section contains the function [simp_env], which simplifies an environment (context) Δ. -If none of the left rules are applicable anymore to Δ, then the function calls [applicable_contextual_simp_form] to find a simplification for one of the formulas in Δ, given +If none of the left rules are applicable anymore to Δ, then the function calls +[applicable_contextual_simp_form] to find a simplification for one of the formulas in Δ, given the fact that it appears in context Δ. We also define [simp_form], which tries to simplify a formula in the empty context. *) @@ -330,7 +228,8 @@ Definition applicable_contextual_simp_form Δ: (forall φ, φ ∈ Δ -> weight(contextual_simp_form (rm φ Δ) φ) ≥ weight φ). Proof. (* try not to do the simplification twice. *) -assert(Hs: forall φ, {φ' | φ' = contextual_simp_form (rm φ Δ) φ /\ weight φ' < weight φ} + (weight(contextual_simp_form (rm φ Δ) φ) ≥ weight φ)). +assert(Hs: forall φ, {φ' | φ' = contextual_simp_form (rm φ Δ) φ /\ weight φ' < weight φ} + + (weight(contextual_simp_form (rm φ Δ) φ) ≥ weight φ)). { intros φ. remember (contextual_simp_form (rm φ Δ) φ) as φ'. case (decide (weight φ' < weight φ)). - intro Hlt. left. exists φ'. tauto. @@ -362,7 +261,7 @@ Program Fixpoint simp_env (Δ : list form) {wf env_order Δ} : list form := Next Obligation. apply Wf.measure_wf, wf_env_order. Qed. -Lemma simp_env_eq (Δ : list form): simp_env Δ = +Global Lemma simp_env_eq (Δ : list form): simp_env Δ = (* invertible left rules *) if Δ ⊢? ⊥ then [⊥] else applicable_AndL Δ ? λ δ₁ δ₂ _, simp_env ((rm (δ₁ ∧ δ₂) Δ•δ₁)•δ₂) ⋮₂ @@ -380,12 +279,31 @@ Qed. Definition simp_form φ:= contextual_simp_form [] φ. +(* Simplification of formulas always decreases the weight. + This is due to the fact that the only formulas with lower weight than ⊤ + are ⊥, v, □⊥, □v, which are not tautologies *) +Lemma simp_form_weight φ: weight(simp_form φ) <= weight φ. +Proof. +unfold simp_form. +destruct (contextual_simp_form_weight [] φ) as [(_ & [Hbot|[Hbox|[v [Ht | Hb]]]] )|Hw]; +subst; simpl. +- case Provable_dec; [|simpl; lia]. intros (Hf&_). + exfalso; apply bot_not_tautology. auto with proof. +- case Provable_dec; [|simpl; lia]. intros (Hf&_). + exfalso; apply box_bot_not_tautology. auto with proof. +- unfold contextual_simp_form. fold contextual_simp_form. simpl. case Provable_dec; [|simpl; lia]. intros (Hf&_). + exfalso; apply (var_not_tautology v). auto with proof. +- unfold contextual_simp_form. fold contextual_simp_form. simpl. case Provable_dec; [|simpl; lia]. intros (Hf&_). + exfalso; apply (box_var_not_tautology v). auto with proof. +- exact Hw. +Qed. -Definition pointed_env_order_refl pe1 pe2 := env_order_refl (pe1.2 :: pe1.2 :: pe1.1) (pe2.2 :: pe2.2 :: pe2.1). (** ** Simplification and the weight ordering -In [simp_env_order], we show that the simplification [simp_env] always decreases the weight of a context. We introduce a tactic [simp_env_tac] for this, which is also used later. +In [simp_env_order], we show that the simplification [simp_env] always +decreases the weight of a context. We introduce a tactic [simp_env_tac] +for this, which is also used later. *) Ltac simp_env_tac := @@ -408,7 +326,7 @@ revert Δ. apply (well_founded_induction_type wf_env_order). intros Δ Hind. rewrite simp_env_eq. case (Δ ⊢? ⊥). { intros [Hf _]. destruct Δ as [|φ Δ]. - + now apply empty_entails_not_bot in Hf. + + now apply bot_not_tautology in Hf. + unfold env_order_refl. do 2 rewrite env_weight_add. simpl. pose (weight_pos φ). replace 5 with (0 + 5^1) at 1 by trivial. apply Nat.add_le_mono. lia. apply Nat.pow_le_mono_r; lia. @@ -419,8 +337,6 @@ all: try (apply env_order_env_order_refl; eapply env_order_le_lt_trans; [apply H apply env_order_self. Qed. -Global Hint Resolve simp_env_order : order. - Lemma simp_env_nil: simp_env [] = []. Proof. assert(Ho := simp_env_order []). destruct (simp_env []) as [|φ Δ]. @@ -429,91 +345,22 @@ contradict Ho. unfold env_order_refl. rewrite env_weight_add. apply Nat.lt_nge. unfold env_weight. simpl. pose(Order.pow5_gt_0 (weight φ)). lia. Qed. +End S. +Import S. -Lemma simp_env_pointed_env_order_L pe Δ φ: (pe ≺· (simp_env Δ, φ)) -> pe ≺· (Δ, φ). -Proof. -intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. -Qed. - -Lemma simp_env_env_order_L Δ Δ0: (Δ0 ≺ simp_env Δ) -> Δ0 ≺ Δ. -Proof. -intro Hl. eapply env_order_lt_le_trans; eauto. auto with order. -Qed. - -Global Hint Resolve simp_env_pointed_env_order_L : order. -Global Hint Resolve simp_env_env_order_L : order. (** ** Simplification is provably equivalent -The goal in this section is to prove that the simplification of a formula (in context) is equivalent -to the original. -We prove in [contextual_simp_form_spec] that the function [contextual_simp_form] creates equivalent -formulas (in context). -This lets us then prove in [simp_env_equiv_env] that [simp_env] also creates equivalent contexts. +The goal in this section is to prove that the simplification of a formula +(in context) is equivalent to the original. +We prove in [contextual_simp_form_spec] that the function [contextual_simp_form] +creates equivalent formulas (in context). +This lets us then prove in [equiv_env_simp_env] that [simp_env] also creates +equivalent contexts. *) Section Equivalence. -Definition equiv_form φ ψ : Type := (φ ≼ ψ) * (ψ ≼ φ). - -Definition equiv_env Δ Δ': Set := - (∀ φ, list_to_set_disj Δ ⊢ φ -> list_to_set_disj Δ' ⊢ φ) * - (∀ φ, list_to_set_disj Δ' ⊢ φ -> list_to_set_disj Δ ⊢ φ). - - -Lemma symmetric_equiv_env Δ Γ: equiv_env Δ Γ -> equiv_env Γ Δ . -Proof. intros [H1 H2]. split; trivial. Qed. - -(* TODO: move *) -Lemma conjunction_L' Γ Δ ϕ: (Γ ⊎ {[⋀ Δ]} ⊢ ϕ) -> Γ ⊎ list_to_set_disj Δ ⊢ ϕ. -Proof. -revert ϕ. unfold conjunction. -assert( Hstrong: ∀ θ ϕ : form, Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ - → (Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ). -{ - induction Δ as [|δ Δ]; intros θ ϕ; simpl. - - intro Hp. peapply Hp. - - case in_dec; intros Hin Hp. - + peapply (weakening δ). apply IHΔ, Hp. ms. - + simpl in Hp. apply IHΔ in Hp. - peapply (AndL_rev (Γ ⊎ list_to_set_disj Δ) θ δ). apply make_conj_complete_L, Hp. -} - intros; apply additive_cut with (φ := ⊤); eauto with proof. -Qed. - -Lemma conjunction_R Δ: list_to_set_disj Δ ⊢ ⋀ Δ. -Proof. -apply conjunction_R1. intros φ Hφ. apply elem_of_list_to_set_disj in Hφ. -exhibit Hφ 0. apply generalised_axiom. -Qed. - -Lemma conjunction_L'' Γ Δ ϕ: Γ ⊎ list_to_set_disj Δ ⊢ ϕ -> (Γ ⊎ {[⋀ Δ]} ⊢ ϕ). -Proof. -revert ϕ. unfold conjunction. -assert( Hstrong: ∀ θ ϕ : form,(Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ -> Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ). -{ - induction Δ as [|δ Δ]; intros θ ϕ; simpl. - - intro Hp. peapply Hp. - - case in_dec; intros Hin Hp. - + apply IHΔ. - assert(Hin' : δ ∈ (Γ ⊎ list_to_set_disj Δ)). - { apply gmultiset_elem_of_disj_union; right; apply elem_of_list_to_set_disj, elem_of_list_In, Hin. } - exhibit Hin' 1. exch 0. apply contraction. exch 1. exch 0. - rw (symmetry (difference_singleton _ _ Hin')) 2. peapply Hp. - + simpl. apply IHΔ. apply make_conj_sound_L, AndL. peapply Hp. -} -intros. apply Hstrong, weakening. assumption. -Qed. - - -Local Ltac equiv_tac := - repeat rewrite <- list_to_set_disj_rm; - repeat rewrite <- list_to_set_disj_env_add; - repeat (rewrite <- difference_singleton; trivial); - try rewrite <- list_to_set_disj_rm; - try (rewrite union_difference_L by trivial); - try (rewrite union_difference_R by trivial); - try ms. Local Ltac peapply' th := (erewrite proper_Provable; [| |reflexivity]); [eapply th|equiv_tac]. @@ -632,22 +479,11 @@ revert Δ. induction φ; intros Δ Hin; simpl; apply elem_of_list_to_set_disj in peapply' Hφ. + split; intros φ0 Hp; peapply' Hp; equiv_tac. Qed. - -Lemma equiv_env_refl Δ : equiv_env Δ Δ. -Proof. split; trivial. Qed. - -Lemma equiv_env_trans Δ Δ' Δ'' : equiv_env Δ Δ' -> equiv_env Δ' Δ'' -> equiv_env Δ Δ''. -Proof. -intros [H11 H12] [H21 H22]. split; intros; auto. -Qed. (* TODO: move *) Hint Resolve elem_of_list_to_set_disj : proof. - - - -Lemma simp_env_equiv_env Δ: equiv_env (simp_env Δ) Δ. +Lemma equiv_env_simp_env Δ: equiv_env (simp_env Δ) Δ. Proof. revert Δ. apply (well_founded_induction_type wf_env_order). intros Δ Hind. rewrite simp_env_eq. @@ -701,25 +537,15 @@ repeat simp_env_tac; (try (eapply equiv_env_trans; [apply Hind; intuition; order - apply equiv_env_refl. Qed. -Lemma equiv_env_L1 Γ Δ Δ' φ: (equiv_env Δ Δ') -> - Γ ⊎ list_to_set_disj Δ ⊢ φ -> Γ ⊎ list_to_set_disj Δ' ⊢ φ. +Lemma equiv_form_simp_form φ: equiv_form (simp_form φ) φ. Proof. -intros [H1 _] Hp. -revert φ Hp. -induction Γ as [|x Γ] using gmultiset_rec; intros φ Hp. -- peapply H1. peapply Hp. -- peapply (ImpR_rev (Γ ⊎ list_to_set_disj Δ') x). - apply IHΓ, ImpR. peapply Hp. +assert (Hφ := contextual_simp_form_spec [φ] φ). +simpl in Hφ. destruct form_eq_dec in Hφ; [|tauto]. +apply equiv_env_equiv_form. apply Hφ. auto with *. Qed. End Equivalence. -(* Global Hint Resolve simp_env_L1 : proof. *) - -Infix "≡f" := equiv_form (at level 120). - -Global Infix "≡e" := equiv_env (at level 120). - Section Variables. (** ** Simplification does not introduce new variables @@ -778,6 +604,9 @@ all:(decompose record Hc; try decompose record Hc0; match goal with | Hin : ?a ∈ _ |- _ => exists a; split; trivial; simpl in *; tauto end)). Qed. +Lemma occurs_in_simp_form x φ: occurs_in x (simp_form φ) → occurs_in x φ. +Proof. apply occurs_in_contextual_simp_form. Qed. + End Variables. @@ -798,3 +627,13 @@ repeat simp_env_tac; try (try (apply Provable_dec_of_Prop in Hc); contradict Hc; - eapply Nat.le_ngt. eapply Hf1. eauto. subst; trivial. - eapply Hf4. eauto. now apply Provable_dec_of_Prop. Qed. + + +Module SoundS : SoundSimpT S. + Definition equiv_env_simp_env := equiv_env_simp_env. + Definition equiv_form_simp_form:= equiv_form_simp_form. + Definition equiv_env_vars := equiv_env_vars. + Definition occurs_in_simp_form := occurs_in_simp_form. + Definition simp_env_idempotent := simp_env_idempotent. + Definition simp_env_nil := simp_env_nil. +End SoundS. diff --git a/theories/iSL/Simplifications.v b/theories/iSL/Simplifications.v new file mode 100644 index 0000000..a89e158 --- /dev/null +++ b/theories/iSL/Simplifications.v @@ -0,0 +1,110 @@ +Require Import ISL.Sequents ISL.SequentProps ISL.Order ISL.Optimizations. + +(* Definitions and properties about equivalent formulas and environments *) +Section Equivalence. + +Definition equiv_form (φ ψ : form) : Type := (φ ≼ ψ) * (ψ ≼ φ). + +Definition equiv_env Δ Δ': Set := + (∀ φ, list_to_set_disj Δ ⊢ φ -> list_to_set_disj Δ' ⊢ φ) * + (∀ φ, list_to_set_disj Δ' ⊢ φ -> list_to_set_disj Δ ⊢ φ). + + +Lemma symmetric_equiv_env Δ Γ: equiv_env Δ Γ -> equiv_env Γ Δ . +Proof. intros [H1 H2]. split; trivial. Qed. + +Lemma equiv_env_refl Δ : equiv_env Δ Δ. +Proof. split; trivial. Qed. + +Lemma equiv_env_trans Δ Δ' Δ'' : equiv_env Δ Δ' -> equiv_env Δ' Δ'' -> equiv_env Δ Δ''. +Proof. +intros [H11 H12] [H21 H22]. split; intros; auto. +Qed. + +Lemma equiv_env_L1 Γ Δ Δ' φ: (equiv_env Δ Δ') -> + Γ ⊎ list_to_set_disj Δ ⊢ φ -> Γ ⊎ list_to_set_disj Δ' ⊢ φ. +Proof. +intros [H1 _] Hp. +revert φ Hp. +induction Γ as [|x Γ] using gmultiset_rec; intros φ Hp. +- peapply H1. peapply Hp. +- peapply (ImpR_rev (Γ ⊎ list_to_set_disj Δ') x). + apply IHΓ, ImpR. peapply Hp. +Qed. + +Lemma equiv_env_equiv_form φ φ': equiv_env [φ] [φ'] -> equiv_form φ φ'. +Proof. +intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder. +- peapply (He2 φ'). simpl. peapply (generalised_axiom ∅). +- peapply (He1 φ). simpl. peapply (generalised_axiom ∅). +Qed. + +End Equivalence. + +Global Infix "≡f" := equiv_form (at level 120). + +Global Infix "≡e" := equiv_env (at level 120). + + +(* The module type of weight-decreasing simplification functions over + environments and formulas is the minimum to define uniform interpolants *) + +Module Type SimpT. + (* The simplification functions *) + Parameter simp_env : list form -> list form. + Parameter simp_form : form -> form. + (* Orders are preserved *) + Parameter simp_env_order: forall Δ, env_order_refl (simp_env Δ) Δ. + Parameter simp_form_weight: forall φ, weight(simp_form φ) <= weight φ. + Global Hint Resolve simp_env_order : order. + Global Hint Resolve simp_env_order : order. + Global Hint Resolve simp_form_weight : order. +End SimpT. + +Module Type SimpProps (Import S : SimpT). + Parameter simp_env_pointed_env_order_L: + forall pe Δ φ, (pe ≺· (simp_env Δ, φ)) -> pe ≺· (Δ, φ). + Parameter simp_env_env_order_L: forall Δ Δ0, (Δ0 ≺ simp_env Δ) -> Δ0 ≺ Δ. + Parameter simp_env_nil: simp_env [] = []. + Global Hint Resolve simp_env_pointed_env_order_L : order. + Global Hint Resolve simp_env_env_order_L : order. +End SimpProps. + +Module MakeSimpProps (Import S : SimpT) : SimpProps S. + Definition simp_env_pointed_env_order_L pe Δ φ: (pe ≺· (simp_env Δ, φ)) -> pe ≺· (Δ, φ). + Proof. intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. Qed. + + Definition simp_env_env_order_L Δ Δ0: (Δ0 ≺ simp_env Δ) -> Δ0 ≺ Δ. + Proof. + intro Hl. eapply env_order_lt_le_trans; eauto. auto with order. + Qed. + + Definition simp_env_nil: simp_env [] = []. + Proof. + assert (Ho := (simp_env_order [])). unfold env_order_refl in Ho. + destruct (simp_env []) as [|a l]. trivial. + contradict Ho. + unfold env_weight, list_sum. simpl. + enough (0 < 5 ^ weight a) by lia. + pose(weight_pos a). + pose (Nat.pow_gt_1 5 (weight a)). lia. + Qed. +End MakeSimpProps. + +(* Soundness properties *) +Module Type SoundSimpT (Export S : SimpT). + (* Simplifications are sound *) + Parameter equiv_env_simp_env: forall Δ, equiv_env (simp_env Δ) Δ. + Parameter equiv_form_simp_form: forall φ, equiv_form (simp_form φ) φ. + + (* The variable are preserved *) + Parameter equiv_env_vars: forall Δ x, + (∃ θ : form, ((θ ∈ simp_env Δ) /\ occurs_in x θ)) -> + ∃ θ : form, ((θ ∈ Δ) /\ occurs_in x θ). + + Parameter occurs_in_simp_form: + forall x φ, occurs_in x (simp_form φ) → occurs_in x φ. + + (* To be removed in the future *) + Parameter simp_env_idempotent: forall Δ, simp_env (simp_env Δ) = simp_env Δ. +End SoundSimpT.