KM.Sequent.Simplifications
Require Import Sequents SequentProps Order Optimizations Cut.
(* Definitions and properties about equivalent formulas and environments. *)
Section Equivalence.
Definition equiv_form (φ ψ : form) : Type := (φ ≼ ψ) * (ψ ≼ φ).
Lemma symmetric_equiv_form {φ ψ} : equiv_form φ ψ -> equiv_form ψ φ.
Proof. intros [H H']. now split. Qed.
(* Definitions and properties about equivalent formulas and environments. *)
Section Equivalence.
Definition equiv_form (φ ψ : form) : Type := (φ ≼ ψ) * (ψ ≼ φ).
Lemma symmetric_equiv_form {φ ψ} : equiv_form φ ψ -> equiv_form ψ φ.
Proof. intros [H H']. now split. Qed.
Definition equiv_envL Γ Γ': Set :=
(∀ Δ, list_to_set_disj Γ ⊢ Δ -> list_to_set_disj Γ' ⊢ Δ) *
(∀ Δ, list_to_set_disj Γ' ⊢ Δ -> list_to_set_disj Γ ⊢ Δ).
Lemma symmetric_equiv_envL Δ Γ: equiv_envL Δ Γ -> equiv_envL Γ Δ .
Proof. intros [H1 H2]. split; trivial. Qed.
Lemma equiv_envL_refl Δ : equiv_envL Δ Δ.
Proof. split; trivial. Qed.
Lemma equiv_envL_trans Δ Δ' Δ'' : equiv_envL Δ Δ' -> equiv_envL Δ' Δ'' -> equiv_envL Δ Δ''.
Proof.
intros [H11 H12] [H21 H22]. split; intros; auto.
Qed.
(∀ Δ, list_to_set_disj Γ ⊢ Δ -> list_to_set_disj Γ' ⊢ Δ) *
(∀ Δ, list_to_set_disj Γ' ⊢ Δ -> list_to_set_disj Γ ⊢ Δ).
Lemma symmetric_equiv_envL Δ Γ: equiv_envL Δ Γ -> equiv_envL Γ Δ .
Proof. intros [H1 H2]. split; trivial. Qed.
Lemma equiv_envL_refl Δ : equiv_envL Δ Δ.
Proof. split; trivial. Qed.
Lemma equiv_envL_trans Δ Δ' Δ'' : equiv_envL Δ Δ' -> equiv_envL Δ' Δ'' -> equiv_envL Δ Δ''.
Proof.
intros [H11 H12] [H21 H22]. split; intros; auto.
Qed.
Definition equiv_envR Δ Δ': Set :=
(∀ Γ, Γ ⊢ list_to_set_disj Δ -> Γ ⊢ list_to_set_disj Δ') *
(∀ Γ, Γ ⊢ list_to_set_disj Δ' -> Γ ⊢ list_to_set_disj Δ).
Lemma symmetric_equiv_envR Δ Γ: equiv_envR Δ Γ -> equiv_envR Γ Δ .
Proof. intros [H1 H2]. split; trivial. Qed.
Lemma equiv_envR_refl Δ : equiv_envR Δ Δ.
Proof. split; trivial. Qed.
Lemma equiv_envR_trans Δ Δ' Δ'' : equiv_envR Δ Δ' -> equiv_envR Δ' Δ'' -> equiv_envR Δ Δ''.
Proof.
intros [H11 H12] [H21 H22]. split; intros; auto.
Qed.
(* Left-equivalent contexts can be exchanged on the left-hand side of a sequent. *)
Lemma equiv_envL_spec Γ Δ Δ' Δ'': (equiv_envL Δ Δ') ->
Γ ⊎ list_to_set_disj Δ ⊢ Δ'' -> Γ ⊎ list_to_set_disj Δ' ⊢ Δ''.
Proof.
intros He Hp. apply additive_cut with (conjunction Δ).
- apply generalised_weakeninglL, He, conjunction_R.
- replace (Γ ⊎ list_to_set_disj Δ' • ⋀ Δ)
with ((Γ • ⋀ Δ) ⊎ list_to_set_disj Δ') by ms.
apply generalised_weakeninglR, conjunction_L'', Hp.
Qed.
(* Right-equivalent contexts can be exchanged on the right-hand side of a sequent. *)
Lemma equiv_envR_spec Γ Δ Δ' Δ'': (equiv_envR Δ Δ') ->
Γ ⊢ Δ'' ⊎ list_to_set_disj Δ -> Γ ⊢ Δ'' ⊎ list_to_set_disj Δ'.
Proof.
intros He Hp. apply symmetric_cut with (disjunction Δ).
- replace (Δ'' ⊎ list_to_set_disj Δ' • ⋁ Δ)
with ((Δ'' • ⋁ Δ) ⊎ list_to_set_disj Δ') by ms.
apply generalised_weakeningrR, disjunction_R'', Hp.
- apply generalised_weakeningrL, He. apply disjunction_L''.
Qed.
(* For singletons, the three notions of equivalence coincide. *)
Lemma equiv_envL_equiv_form φ φ': equiv_envL [φ] [φ'] -> equiv_form φ φ'.
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
- peapply (He2 (∅ • φ')). simpl. peapply (generalised_axiom ∅).
- peapply (He1 (∅ • φ)). simpl. peapply (generalised_axiom ∅).
Qed.
Lemma equiv_envR_equiv_form φ φ': equiv_envR [φ] [φ'] -> equiv_form φ φ'.
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
- peapply (He1 (∅ • φ)). simpl. peapply (generalised_axiom ∅ ∅).
- peapply (He2 (∅ • φ')). simpl. peapply (generalised_axiom ∅ ∅).
Qed.
Lemma equiv_form_equiv_env φ φ': equiv_form φ φ' -> equiv_envL [φ] [φ'].
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
- intros f Hp. simpl. apply additive_cut with φ.
+ apply He2.
+ apply generalised_weakeninglL. peapply Hp.
- intros f Hp. simpl. apply additive_cut with φ'.
+ apply He1.
+ apply generalised_weakeninglL. peapply Hp.
Qed.
Lemma equiv_form_equiv_envF φ φ': equiv_form φ φ' -> equiv_envR [φ] [φ'].
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder; intros Δ Hp.
- apply additive_cut with φ.
+ peapply Hp.
+ apply generalised_weakeninglL. peapply He1.
- apply additive_cut with φ'.
+ peapply Hp.
+ apply generalised_weakeninglL. peapply He2.
Qed.
End Equivalence.
Global Infix "≡f" := equiv_form (at level 120).
Global Infix "≡el" := equiv_envL (at level 120).
Global Infix "≡er" := equiv_envR (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_envL : list form -> list form.
Parameter simp_envR : list form -> list form.
Parameter simp_form : form -> form.
(* Orders are preserved *)
Parameter simp_envL_order : forall Δ, env_order_refl (simp_envL Δ) Δ.
Parameter simp_envR_order : forall Δ, env_order_refl (simp_envR Δ) Δ.
Parameter simp_form_weight: forall φ, weight(simp_form φ) <= weight φ.
Global Hint Resolve simp_envL_order simp_envR_order simp_form_weight : order.
End SimpT.
Module Type SimpProps (Import S : SimpT).
Parameter simp_envL_pointed_env_order:
forall pe Γ Δ, (pe ≺· (simp_envL Γ, Δ)) -> pe ≺· (Γ, Δ).
Parameter simp_envR_pointed_env_order :
forall pe Γ Δ, (pe ≺· (Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Parameter simp_env_pointed_env_order :
forall pe Γ Δ, (pe ≺· (simp_envL Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Parameter simp_envL_env_order: forall Δ Δ0, (Δ0 ≺ simp_envL Δ) -> Δ0 ≺ Δ.
Parameter simp_envR_env_order: forall Δ Δ0, (Δ0 ≺ simp_envR Δ) -> Δ0 ≺ Δ.
Parameter simp_envL_nil: simp_envL [] = [].
Parameter simp_envR_nil: simp_envR [] = [].
Global Hint Resolve simp_envL_pointed_env_order simp_envR_pointed_env_order
simp_env_pointed_env_order : order.
End SimpProps.
Module MakeSimpProps (Import S : SimpT) : SimpProps S.
Definition simp_envL_pointed_env_order pe Δ φ:
(pe ≺· (simp_envL Δ, φ)) -> pe ≺· (Δ, φ).
Proof. intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. Qed.
Definition simp_envL_env_order Δ Δ0: (Δ0 ≺ simp_envL Δ) -> Δ0 ≺ Δ.
Proof.
intro Hl. eapply env_order_lt_le_trans; eauto. auto with order.
Qed.
Definition simp_envR_env_order Δ Δ0: (Δ0 ≺ simp_envR Δ) -> Δ0 ≺ Δ.
Proof.
intro Hl. eapply env_order_lt_le_trans; eauto. auto with order.
Qed.
Definition simp_envR_pointed_env_order pe Γ Δ:
(pe ≺· (Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Proof. intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. Qed.
Definition simp_env_pointed_env_order pe Γ Δ:
(pe ≺· (simp_envL Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Proof. intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. Qed.
Definition simp_envL_nil : simp_envL [] = [].
Proof.
assert (Ho := (simp_envL_order [])). unfold env_order_refl in Ho.
destruct (simp_envL []) as [|a l]. trivial.
contradict Ho.
unfold env_weight, list_sum. simpl.
enough (0 < 9 ^ weight a) by lia.
pose(weight_pos a).
pose (Nat.pow_gt_1 9 (weight a)). lia.
Qed.
Definition simp_envR_nil : simp_envR [] = [].
Proof.
assert (Ho := (simp_envR_order [])). unfold env_order_refl in Ho.
destruct (simp_envR []) as [|a l]. trivial.
contradict Ho.
unfold env_weight, list_sum. simpl.
enough (0 < 9 ^ weight a) by lia.
pose(weight_pos a).
pose (Nat.pow_gt_1 9 (weight a)). lia.
Qed.
End MakeSimpProps.
(* A valid simplification module provides sound simplification of contexts on
both sides of a sequent that preserve the language and are idempotent. *)
Module Type SoundSimpT (Export S : SimpT).
(* Simplifications are sound *)
Parameter equiv_envL_simp_env: forall Δ, equiv_envL (simp_envL Δ) Δ.
Parameter equiv_envR_simp_env: forall Δ, equiv_envR (simp_envR Δ) Δ.
(* Parameter equiv_envF_simp_env: forall Δ, equiv_envF (simp_env Δ) Δ. *)
Parameter equiv_form_simp_form: forall φ, equiv_form (simp_form φ) φ.
(* The variable are preserved *)
Parameter equiv_envL_vars: forall Δ x,
(∃ θ : form, ((θ ∈ simp_envL Δ) /\ occurs_in x θ)) ->
∃ θ : form, ((θ ∈ Δ) /\ occurs_in x θ).
Parameter equiv_envR_vars: forall Δ x,
(∃ θ : form, ((θ ∈ simp_envR Δ) /\ 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_envL_idempotent: forall Δ, simp_envL (simp_envL Δ) = simp_envL Δ.
Parameter simp_envR_idempotent: forall Δ, simp_envR (simp_envR Δ) = simp_envR Δ.
End SoundSimpT.
(∀ Γ, Γ ⊢ list_to_set_disj Δ -> Γ ⊢ list_to_set_disj Δ') *
(∀ Γ, Γ ⊢ list_to_set_disj Δ' -> Γ ⊢ list_to_set_disj Δ).
Lemma symmetric_equiv_envR Δ Γ: equiv_envR Δ Γ -> equiv_envR Γ Δ .
Proof. intros [H1 H2]. split; trivial. Qed.
Lemma equiv_envR_refl Δ : equiv_envR Δ Δ.
Proof. split; trivial. Qed.
Lemma equiv_envR_trans Δ Δ' Δ'' : equiv_envR Δ Δ' -> equiv_envR Δ' Δ'' -> equiv_envR Δ Δ''.
Proof.
intros [H11 H12] [H21 H22]. split; intros; auto.
Qed.
(* Left-equivalent contexts can be exchanged on the left-hand side of a sequent. *)
Lemma equiv_envL_spec Γ Δ Δ' Δ'': (equiv_envL Δ Δ') ->
Γ ⊎ list_to_set_disj Δ ⊢ Δ'' -> Γ ⊎ list_to_set_disj Δ' ⊢ Δ''.
Proof.
intros He Hp. apply additive_cut with (conjunction Δ).
- apply generalised_weakeninglL, He, conjunction_R.
- replace (Γ ⊎ list_to_set_disj Δ' • ⋀ Δ)
with ((Γ • ⋀ Δ) ⊎ list_to_set_disj Δ') by ms.
apply generalised_weakeninglR, conjunction_L'', Hp.
Qed.
(* Right-equivalent contexts can be exchanged on the right-hand side of a sequent. *)
Lemma equiv_envR_spec Γ Δ Δ' Δ'': (equiv_envR Δ Δ') ->
Γ ⊢ Δ'' ⊎ list_to_set_disj Δ -> Γ ⊢ Δ'' ⊎ list_to_set_disj Δ'.
Proof.
intros He Hp. apply symmetric_cut with (disjunction Δ).
- replace (Δ'' ⊎ list_to_set_disj Δ' • ⋁ Δ)
with ((Δ'' • ⋁ Δ) ⊎ list_to_set_disj Δ') by ms.
apply generalised_weakeningrR, disjunction_R'', Hp.
- apply generalised_weakeningrL, He. apply disjunction_L''.
Qed.
(* For singletons, the three notions of equivalence coincide. *)
Lemma equiv_envL_equiv_form φ φ': equiv_envL [φ] [φ'] -> equiv_form φ φ'.
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
- peapply (He2 (∅ • φ')). simpl. peapply (generalised_axiom ∅).
- peapply (He1 (∅ • φ)). simpl. peapply (generalised_axiom ∅).
Qed.
Lemma equiv_envR_equiv_form φ φ': equiv_envR [φ] [φ'] -> equiv_form φ φ'.
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
- peapply (He1 (∅ • φ)). simpl. peapply (generalised_axiom ∅ ∅).
- peapply (He2 (∅ • φ')). simpl. peapply (generalised_axiom ∅ ∅).
Qed.
Lemma equiv_form_equiv_env φ φ': equiv_form φ φ' -> equiv_envL [φ] [φ'].
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
- intros f Hp. simpl. apply additive_cut with φ.
+ apply He2.
+ apply generalised_weakeninglL. peapply Hp.
- intros f Hp. simpl. apply additive_cut with φ'.
+ apply He1.
+ apply generalised_weakeninglL. peapply Hp.
Qed.
Lemma equiv_form_equiv_envF φ φ': equiv_form φ φ' -> equiv_envR [φ] [φ'].
Proof.
intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder; intros Δ Hp.
- apply additive_cut with φ.
+ peapply Hp.
+ apply generalised_weakeninglL. peapply He1.
- apply additive_cut with φ'.
+ peapply Hp.
+ apply generalised_weakeninglL. peapply He2.
Qed.
End Equivalence.
Global Infix "≡f" := equiv_form (at level 120).
Global Infix "≡el" := equiv_envL (at level 120).
Global Infix "≡er" := equiv_envR (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_envL : list form -> list form.
Parameter simp_envR : list form -> list form.
Parameter simp_form : form -> form.
(* Orders are preserved *)
Parameter simp_envL_order : forall Δ, env_order_refl (simp_envL Δ) Δ.
Parameter simp_envR_order : forall Δ, env_order_refl (simp_envR Δ) Δ.
Parameter simp_form_weight: forall φ, weight(simp_form φ) <= weight φ.
Global Hint Resolve simp_envL_order simp_envR_order simp_form_weight : order.
End SimpT.
Module Type SimpProps (Import S : SimpT).
Parameter simp_envL_pointed_env_order:
forall pe Γ Δ, (pe ≺· (simp_envL Γ, Δ)) -> pe ≺· (Γ, Δ).
Parameter simp_envR_pointed_env_order :
forall pe Γ Δ, (pe ≺· (Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Parameter simp_env_pointed_env_order :
forall pe Γ Δ, (pe ≺· (simp_envL Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Parameter simp_envL_env_order: forall Δ Δ0, (Δ0 ≺ simp_envL Δ) -> Δ0 ≺ Δ.
Parameter simp_envR_env_order: forall Δ Δ0, (Δ0 ≺ simp_envR Δ) -> Δ0 ≺ Δ.
Parameter simp_envL_nil: simp_envL [] = [].
Parameter simp_envR_nil: simp_envR [] = [].
Global Hint Resolve simp_envL_pointed_env_order simp_envR_pointed_env_order
simp_env_pointed_env_order : order.
End SimpProps.
Module MakeSimpProps (Import S : SimpT) : SimpProps S.
Definition simp_envL_pointed_env_order pe Δ φ:
(pe ≺· (simp_envL Δ, φ)) -> pe ≺· (Δ, φ).
Proof. intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. Qed.
Definition simp_envL_env_order Δ Δ0: (Δ0 ≺ simp_envL Δ) -> Δ0 ≺ Δ.
Proof.
intro Hl. eapply env_order_lt_le_trans; eauto. auto with order.
Qed.
Definition simp_envR_env_order Δ Δ0: (Δ0 ≺ simp_envR Δ) -> Δ0 ≺ Δ.
Proof.
intro Hl. eapply env_order_lt_le_trans; eauto. auto with order.
Qed.
Definition simp_envR_pointed_env_order pe Γ Δ:
(pe ≺· (Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Proof. intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. Qed.
Definition simp_env_pointed_env_order pe Γ Δ:
(pe ≺· (simp_envL Γ, simp_envR Δ)) -> pe ≺· (Γ, Δ).
Proof. intro Hl. eapply env_order_lt_le_trans; eauto. simpl. auto with order. Qed.
Definition simp_envL_nil : simp_envL [] = [].
Proof.
assert (Ho := (simp_envL_order [])). unfold env_order_refl in Ho.
destruct (simp_envL []) as [|a l]. trivial.
contradict Ho.
unfold env_weight, list_sum. simpl.
enough (0 < 9 ^ weight a) by lia.
pose(weight_pos a).
pose (Nat.pow_gt_1 9 (weight a)). lia.
Qed.
Definition simp_envR_nil : simp_envR [] = [].
Proof.
assert (Ho := (simp_envR_order [])). unfold env_order_refl in Ho.
destruct (simp_envR []) as [|a l]. trivial.
contradict Ho.
unfold env_weight, list_sum. simpl.
enough (0 < 9 ^ weight a) by lia.
pose(weight_pos a).
pose (Nat.pow_gt_1 9 (weight a)). lia.
Qed.
End MakeSimpProps.
(* A valid simplification module provides sound simplification of contexts on
both sides of a sequent that preserve the language and are idempotent. *)
Module Type SoundSimpT (Export S : SimpT).
(* Simplifications are sound *)
Parameter equiv_envL_simp_env: forall Δ, equiv_envL (simp_envL Δ) Δ.
Parameter equiv_envR_simp_env: forall Δ, equiv_envR (simp_envR Δ) Δ.
(* Parameter equiv_envF_simp_env: forall Δ, equiv_envF (simp_env Δ) Δ. *)
Parameter equiv_form_simp_form: forall φ, equiv_form (simp_form φ) φ.
(* The variable are preserved *)
Parameter equiv_envL_vars: forall Δ x,
(∃ θ : form, ((θ ∈ simp_envL Δ) /\ occurs_in x θ)) ->
∃ θ : form, ((θ ∈ Δ) /\ occurs_in x θ).
Parameter equiv_envR_vars: forall Δ x,
(∃ θ : form, ((θ ∈ simp_envR Δ) /\ 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_envL_idempotent: forall Δ, simp_envL (simp_envL Δ) = simp_envL Δ.
Parameter simp_envR_idempotent: forall Δ, simp_envR (simp_envR Δ) = simp_envR Δ.
End SoundSimpT.