From a0826841ea809f95bffdbce9337bf135a3cfecb4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= <feree@irif.fr>
Date: Sat, 19 Oct 2024 01:06:34 +0200
Subject: [PATCH] (Provably) Simplify before and after uniform interpolation

---
 theories/extraction/UIML_extraction.v |  4 +-
 theories/iSL/PropQuantifiers.v        | 59 +++++++++++++++++----------
 theories/iSL/Simplifications.v        | 32 ++++++++++++++-
 3 files changed, 71 insertions(+), 24 deletions(-)

diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v
index 4e7fe90..79b13b0 100644
--- a/theories/extraction/UIML_extraction.v
+++ b/theories/extraction/UIML_extraction.v
@@ -41,8 +41,8 @@ Definition isl_A v f := Af v f.
   Notable exception: (a ∨b) → c *)
 Definition isl_simp f := simp_form f.
 
-Definition isl_simplified_E p ψ := isl_simp (E p [ψ]).
-Definition isl_simplified_A p ψ := isl_simp (Af p (ψ)).
+Definition isl_simplified_E p ψ := E p [ψ].
+Definition isl_simplified_A p ψ := Af p (ψ).
 
 Set Extraction Output Directory "extraction".
 
diff --git a/theories/iSL/PropQuantifiers.v b/theories/iSL/PropQuantifiers.v
index e674139..4e41cc4 100644
--- a/theories/iSL/PropQuantifiers.v
+++ b/theories/iSL/PropQuantifiers.v
@@ -159,8 +159,8 @@ 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 ([], ψ).
+Definition Ef (ψ : form) := simp_form (E ([simp_form ψ])).
+Definition Af (ψ : form) := simp_form (A ([], simp_form ψ)).
 
 (** 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. *)
@@ -1000,27 +1000,44 @@ Theorem iSL_uniform_interpolation p V: p ∉ V ->
   * (vars_incl (Af p φ) V)
   * ({[Af p φ]} ⊢ φ)
   * (∀ θ, vars_incl θ V -> {[θ]} ⊢ φ -> {[θ]} ⊢ Af p φ).
-Proof. 
+Proof.
+unfold Ef, Af.
 intros Hp φ Hvarsφ; repeat split.
-  + 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.
-  + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp. unfold Ef.
-      * 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.
-      destruct Hx as [Hneq [Hin | [θ [Hθ Hocc]]]].
-      * apply Hvarsφ in Hin. destruct Hin; subst; tauto.
-      * inversion Hθ.
-  + peapply (@entail_correct p []).
+  + intros x Hx.
+    apply occurs_in_simp_form, (@EA_vars p _ ⊥ x) in Hx.
+    destruct Hx as [Hneq [θ [Hθ Hocc]]]. apply elem_of_list_singleton in Hθ. subst.
+    apply occurs_in_simp_form, Hvarsφ in Hocc. destruct Hocc; subst; tauto.
+  + replace {[φ]} with (list_to_set_disj [φ] : env) by ms.
+    apply (equiv_form_R (symmetric_equiv_form (equiv_form_simp_form _))).
+    peapply (equiv_form_L (equiv_form_simp_form φ) ∅).
+    peapply (@entail_correct p [simp_form φ] ⊥).
+  + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp.
+    peapply (equiv_form_L (symmetric_equiv_form(equiv_form_simp_form (E p [simp_form φ]))) ∅).
+    peapply (@pq_correct p ∅ [simp_form φ] ψ).
+    * intros θ Hin. inversion Hin.
+    * peapply (equiv_form_L (symmetric_equiv_form(equiv_form_simp_form φ)) ∅).
+      peapply Hyp.
+    * intro HF. apply Hψ in HF. tauto.
+  + intros x Hx.
+    apply occurs_in_simp_form, EA_vars in Hx.
+    destruct Hx as [Hneq [Hx | [θ [Hθ Hocc]]]].
+    * apply occurs_in_simp_form, Hvarsφ in Hx. simpl in Hx.
+      firstorder. subst. tauto.
+    * inversion Hθ.
+  + peapply (equiv_form_L (symmetric_equiv_form(equiv_form_simp_form (A p ([], simp_form φ)))) ∅).
+    apply (equiv_form_R (equiv_form_simp_form _)).
+    peapply (@entail_correct p []).
   + intros ψ Hψ Hyp. rewrite elem_of_list_In in Hp.
-      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.
+    apply (equiv_form_R (symmetric_equiv_form (equiv_form_simp_form _))).
+    peapply (equiv_form_L ((equiv_form_simp_form ψ)) ∅).
+      apply (TopL_rev _ ⊥). peapply (@pq_correct p {[simp_form ψ]} []).
+      * intros φ0 Hφ0. apply gmultiset_elem_of_singleton in Hφ0. subst.
+        intro Ho; apply occurs_in_simp_form in Ho. auto with *.
+      * simpl.
+        apply (equiv_form_R (symmetric_equiv_form (equiv_form_simp_form _))).
+        peapply (equiv_form_L (symmetric_equiv_form(equiv_form_simp_form ψ)) ∅).
+        peapply Hyp.
+      * rewrite E_of_empty. ms.
 Qed.
 
 End PropQuantProp.
diff --git a/theories/iSL/Simplifications.v b/theories/iSL/Simplifications.v
index a89e158..3457c45 100644
--- a/theories/iSL/Simplifications.v
+++ b/theories/iSL/Simplifications.v
@@ -1,10 +1,29 @@
-Require Import ISL.Sequents ISL.SequentProps ISL.Order ISL.Optimizations.
+Require Import ISL.Sequents ISL.SequentProps ISL.Order ISL.Optimizations ISL.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.
+
+Lemma equiv_form_R {φ ψ} : (equiv_form φ ψ) ->
+  forall Γ, Provable Γ φ -> Provable Γ ψ.
+Proof.
+intros Heq g Hp. apply additive_cut with φ. (* cut is only required here in this file*)
+- auto with proof.
+- apply generalised_weakeningL. peapply Heq.
+Qed.
+
+Lemma equiv_form_L {φ ψ} : (equiv_form φ ψ) ->
+  forall Γ θ, Γ • φ ⊢ θ -> Γ • ψ ⊢ θ.
+Proof.
+intros Heq Γ θ Hp. apply additive_cut with φ. (* cut is only required here in this file*)
+- apply generalised_weakeningL. peapply Heq.
+- auto with proof.
+Qed.
+
 Definition equiv_env Δ Δ': Set :=
  (∀ φ, list_to_set_disj Δ ⊢ φ ->  list_to_set_disj Δ' ⊢ φ) *
  (∀ φ, list_to_set_disj Δ' ⊢ φ ->  list_to_set_disj Δ ⊢ φ).
@@ -39,6 +58,17 @@ intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
 - peapply (He1 φ). simpl. peapply (generalised_axiom ∅).
 Qed.
 
+Lemma equiv_form_equiv_env φ φ': equiv_form φ φ' -> equiv_env [φ] [φ'].
+Proof.
+intros [He1 He2]; split; unfold Lindenbaum_Tarski_preorder.
+- intros f Hp. simpl. apply additive_cut with φ.
+  + apply He2.
+  + apply generalised_weakeningL. peapply Hp.
+- intros f Hp. simpl. apply additive_cut with φ'.
+  + apply He1.
+  + apply generalised_weakeningL. peapply Hp.
+Qed.
+
 End Equivalence.
 
 Global Infix "≡f" := equiv_form (at level 120).