make progress in defining a correct simplification for environments, …

…interleaved during the computation of Pitts Interpolants

theories/extraction/UIML_extraction.v

@@ -5,9 +5,8 @@ Require Import ExtrOcamlBasic ExtrOcamlString.
 
 Require Import K.Interpolation.UIK_braga.
 Require Import KS_export.
-Require Import ISL.PropQuantifiers ISL.DecisionProcedure.
+Require Import ISL.InvPropQuantifiers ISL.DecisionProcedure ISL.Simp.
 
-Require Import ISL.Simp.
 
 Fixpoint MPropF_of_form (f : Formulas.form) : MPropF  :=
 match f with

theories/iSL/DecisionProcedure.v

@@ -21,6 +21,7 @@ induction l as [|x l].
     * right. simpl. intros z [Hz|Hz]; subst; try rewrite Heq; auto with *.
 Defined.
 
+
 (* This function computes a proof tree of a sequent, if there is one, or produces a proof that there is none *)
 Proposition Proof_tree_dec Γ φ :
   {_ : list_to_set_disj Γ ⊢ φ & True} + {forall H : list_to_set_disj  Γ ⊢ φ, False}.

theories/iSL/InvPropQuantifiers.v

@@ -1,41 +1,12 @@
-Require Import ISL.Sequents ISL.SequentProps ISL.Order ISL.Optimizations ISL.DecisionProcedure.
 Require Import Coq.Program.Equality. (* for dependent induction *)
-
-(** * Overview: Propositional Quantifiers
-
-The main theorem proved in this file was first proved as Theorem 1 in:
-
-(Pitts 1992). A. M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log., 57(1):33–52.
-It has been further extended to handle iSL
-
-It consists of two parts: 
-
-1) the inductive construction of the propositional quantifiers; 
-
-2) a proof of its correctness. *)
+Require Import ISL.PropQuantifiers ISL.Sequents ISL.SequentProps.
+Require Import ISL.Order ISL.DecisionProcedure.
 
 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.
-
-
-(** * Definition of propositional quantifiers. *)
-
-Section PropQuantDefinition.
-
-(** 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*)
-
-Local Notation "Δ '•' φ" := (cons φ Δ).
-
-Notation "□⁻¹ Γ" := (map open_box Γ) (at level 75).
-
 Definition applicable_AndR φ: {φ1 & {φ2 | φ = (And φ1 φ2)}} + (∀ φ1 φ2, φ ≠ (And φ1 φ2)).
 Proof. (destruct φ; eauto). Defined.
-
+(*
 Definition applicable_other_var (Γ : list form): {q | p ≠ q /\ Var q ∈ Γ} + (∀ q, p ≠ q -> Var q ∈ Γ -> False).
 Proof.
   pose (fA := (fun θ => match θ with |Var q => if decide (p = q)  then false else true | _ => false end)).
@@ -46,6 +17,7 @@ Proof.
   - right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fA. simpl in Hψ.
      case decide in Hψ; auto with *.
 Defined.
+*)
 
 Definition applicable_AndL (Γ : list form): {ψ1 & {ψ2 | (And ψ1 ψ2) ∈ Γ}} + (∀ ψ1 ψ2, (And ψ1 ψ2) ∈ Γ -> False).
 Proof.
@@ -69,6 +41,7 @@ Proof.
   - right. intros ψ1 ψ2 Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fA. simpl in Hψ. tauto.
 Defined.
 
+(*
 Definition applicable_ImpL_other_Var (Γ : list form):
   {q & {ψ | q ≠ p /\ (Implies (Var q) ψ) ∈ Γ}} +
   (∀ q ψ, q ≠ p -> (Implies (Var q) ψ) ∈ Γ -> False).
@@ -83,6 +56,7 @@ Proof.
   - right. intros q ψ Hp Hψ. rewrite elem_of_list_In in Hψ. apply Hf in Hψ. subst fIp.
     simpl in Hψ. rewrite decide_False in Hψ; trivial; auto with *.
 Defined.
+*)
 
 Definition applicable_ImpLVar (Γ : list form):
   {q & {ψ | Var q ∈ Γ /\ (Implies (Var q) ψ) ∈ Γ}} +
@@ -151,6 +125,7 @@ Proof. destruct φ; eauto with *. Defined.
 Definition applicable_BoxR φ: {φ' | φ = (□ φ')} + (∀ φ', φ = (□ φ') -> False).
 Proof. destruct φ; eauto with *. Defined.
 
+(*
 Definition applicable_ImpLImp (Γ : list form):
   {φ1 & {φ2 & {φ3 | ((φ1 → φ2) → φ3) ∈ Γ}}} +(forall φ1 φ2 φ3, ((φ1 → φ2) → φ3) ∈ Γ -> False).
 Proof.
@@ -160,6 +135,7 @@ Proof.
       destruct θ1. 1-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.
+*)
 
 (* can this be replaced with generalised axiom?*)
 Definition applicable_Atom q (Δ : list form) ϕ :
@@ -204,100 +180,76 @@ Notation "cond '?' A ':1' B" := (sumor_bind1 cond A B) (at level 150, right asso
 Notation "cond '?' A ':2' B" := (sumor_bind2 cond A B) (at level 150, right associativity).
 Notation "cond '?' A ':3' B" := (sumor_bind3 cond A B) (at level 150, right associativity).
 
-(* solves the obligations of the following programs *)
-Obligation Tactic := simpl; intros; order_tac.
-Program Definition e_rule {Δ : list form } {ϕ : form}
-  (EA0 : ∀ bool pe (Hpe : pe ≺· (Δ, ϕ)), form)
-  (θ: form) (Hin : θ ∈ Δ) : form :=
-let E Δ H := EA0 true (Δ, ϕ) H in
-let A pe0 H := EA0 false pe0 H in
-let Δ'  := rm θ Δ in
-match θ with
-| Var q → δ => if decide (p = q) then ⊤ else q → E (Δ'•δ) _ (* E5 modified *)
-(* E8 modified *)
-| ((δ₁→ δ₂)→ δ₃) =>
-  (E (Δ'•(δ₂ → δ₃) • δ₁) _⇢ A (Δ'•(δ₂ → δ₃) • δ₁, δ₂) _) ⇢ E (Δ'•δ₃) _
-| □ φ => □(E ((□⁻¹ Δ') • φ ) _) (* very redundant ; identical for each box *)
-| (□δ1 → δ2) =>  (□(E((□⁻¹ Δ') • δ2 • □δ1) _ ⇢ A((□⁻¹ Δ') • δ2 • □δ1, δ1) _)) ⇢ E(Δ' • δ2) _
-| _ => ⊤
-end.
+(* TODO: plan:
+  - reuse propquantifiers (esp, don't redefine erule); 
+  - define propquant' as the same fixpoint as propquant, but with a simplification step
+  - the simplification shold look like the monadic simplifications done here, but more general
+  - to ensure that' it's still correct, prove that simplified sequents are "equivalent" to the original ones
+  -  show (by induction on the definition of EA and EA') that EA equiv EA'
+  *)
+
+Local Notation "Δ '•' φ" := (cons φ Δ).
 
-(** 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 {Δ : list form} {ϕ : form}
-  (EA0 : ∀ bool pe (Hpe : pe ≺· (Δ, ϕ)), form)
-  (θ: form) (Hin : θ ∈ Δ) : form :=
-let E Δ H := EA0 true (Δ, ϕ) H in
-let A pe0 H := EA0 false pe0 H in
-let Δ'  := rm θ Δ in
-match θ with
-| Var q → δ => if decide (p = q) then ⊥ else q ⊼ A (Δ'•δ, ϕ) _ (* A4 *)
-(* A6 *)
-(* A8 modified*)
-| ((δ₁→ δ₂)→ δ₃) =>
-  (E (Δ'•(δ₂ → δ₃) • δ₁) _ ⇢ A (Δ'•(δ₂ → δ₃) • δ₁, δ₂) _)
-  ⊼ A (Δ'•δ₃, ϕ) _
-| ((□δ1) → δ2) => (□(E((□⁻¹ Δ')• δ2 • □δ1) _  ⇢ A((□⁻¹ Δ')• δ2 • □δ1, δ1) _)) ∧ A(Δ' • δ2, ϕ) _
-(* using ⊼ here breaks congruence *)
-| _ => ⊥
-end.
+Infix "⊢?" := Provable_dec (at level 80).
 
-Program Definition a_rule_form {Δ : list form} {ϕ : form}
-  (EA0 : ∀ bool pe (Hpe : pe ≺· (Δ, ϕ)), form) :=
-let E pe0:= EA0 true pe0 in
-let A pe0 H := EA0 false pe0 H in
-match ϕ with
-| Var q =>
-    if decide (p = q)
-    then ⊥
-    else Var q (* A9 *)
-(* A12 *)
-| ϕ₁ ∨ ϕ₂ => A (Δ, ϕ₁) _ ⊻ A (Δ, ϕ₂) _
-| □δ => □((E ((□⁻¹ Δ) • □δ, δ) _) ⇢ A((□⁻¹ Δ) • □δ, δ) _)
-| _ => ⊥
-end.
+(* Probably very costly *)
+Definition applicable_strong_weakening (Γ : list form):
+  {φ : form | φ ∈ Γ /\ exists (_ : list_to_set_disj (rm φ Γ) ⊢ φ), True}
+  + (∀ φ, φ ∈ Γ -> forall (_ : list_to_set_disj (rm φ Γ) ⊢ φ), False).
+Proof.
+destruct (exists_dec (λ φ, if Provable_dec (rm φ Γ) φ then true else false) Γ) as [[φ [Hin Hφ]]| Hf].
+- left. exists φ; split.
+  + now apply elem_of_list_In.
+  + destruct ((rm φ Γ) ⊢? φ). trivial. contradict Hφ.
+- right. intros φ Hin Hφ. apply (Hf φ). now apply elem_of_list_In.
+   destruct ((rm φ Γ) ⊢? φ). auto with *. tauto.
+Defined.
+
+Obligation Tactic := (simpl; intuition order_tac).
+Program Fixpoint simp_env (Δ : list form) {wf env_order Δ} : list form :=
+    (* invertible left rules *)
+    applicable_AndL Δ ? λ δ₁ δ₂  _, simp_env ((rm (δ₁ ∧ δ₂) Δ•δ₁)•δ₂) :2
+    applicable_ImpLVar Δ ? λ q ψ  _, simp_env ((rm (Var q → ψ) Δ • ψ)) :2
+    applicable_ImpLAnd Δ ? λ δ₁ δ₂ δ₃  _, simp_env ((rm ((δ₁ ∧ δ₂)→ δ₃) Δ • (δ₁ → (δ₂ → δ₃)))) :3
+    applicable_ImpLOr Δ ? λ δ₁ δ₂ δ₃  _, simp_env (rm ((δ₁ ∨ δ₂)→ δ₃) Δ • (δ₁ → δ₃) • (δ₂ → δ₃)) :3
+    (* remove redundant assumptions *)
+    applicable_strong_weakening Δ ? λ φ _, simp_env (rm φ Δ) :1
+    Δ
+.
+Next Obligation. apply Wf.measure_wf, wf_env_order. Qed.
+
+Definition simp_form φ:= ⋀ (simp_env [φ]).
+
+Definition pointed_env_order_refl pe1 pe2 := env_order_refl (pe1.2 :: pe1.2 :: pe1.1) (pe2.2 :: pe2.2 :: pe2.1).
+
+Lemma simp_env_order pe : env_order_refl (simp_env pe) pe.
+Proof.
+Admitted.
+
+Variable p : variable.
 
 Obligation Tactic := solve[simpl; intros; simpl in *; intuition;  order_tac] || (try (apply Wf.measure_wf, wf_pointed_order)).
-Program Fixpoint EA (b : bool) (pe : list form * form) {wf pointed_env_order pe} :=
-  let Δ := fst pe in
-  let ϕ := snd pe in
-  let E := EA true in
-  let A := EA false in
+Program Fixpoint EA (b : bool) (pe : pointed_env) {wf pointed_env_order pe} : form :=
+  let Δ := simp_env pe.1 in (* because pattern matchin in lets is not broken *)
+  let ϕ := pe.2 in
+  let E pe H := EA true pe in
+  let A pe H := EA false pe in
   (* E *)
   if b then
-    if decide (⊥ ∈ Δ) then ⊥ else
-    applicable_other_var Δ ? λ q _, q ⊼ E (rm (Var q) Δ, ϕ) _ :1
-    applicable_AndL Δ ? λ δ₁ δ₂  _, E ((rm (δ₁ ∧ δ₂) Δ•δ₁)•δ₂, ϕ) _ :2
-    applicable_OrL Δ ? λ δ₁ δ₂  _, E ((rm (δ₁ ∨ δ₂) Δ•δ₁, ϕ)) _ ⊻E ((rm (δ₁ ∨ δ₂) Δ•δ₂, ϕ)) _ :2
-    applicable_ImpLVar Δ ? λ q ψ  _, E ((rm (Var q → ψ) Δ • ψ, ϕ)) _ :2
-    applicable_ImpLAnd Δ ? λ δ₁ δ₂ δ₃  _, E ((rm ((δ₁ ∧ δ₂)→ δ₃) Δ • (δ₁ → (δ₂ → δ₃)), ϕ)) _ :3
-    applicable_ImpLOr Δ ? λ δ₁ δ₂ δ₃  _, E (rm ((δ₁ ∨ δ₂)→ δ₃) Δ • (δ₁ → δ₃) • (δ₂ → δ₃), ϕ) _ :3
-    ⋀ (in_map Δ (e_rule EA)) (* the non-invertible rules *)
-
+    ⋀ (in_map Δ (@e_rule p Δ ϕ E A))
   (* A *)
   else
-    applicable_other_var Δ ? λ q _, A (rm (Var q) Δ, ϕ) _ :1
-    applicable_AndL Δ ? λ δ₁ δ₂  _, A ((rm (δ₁ ∧ δ₂) Δ•δ₁)•δ₂, ϕ) _ :2
-    applicable_OrL Δ ? λ δ₁ δ₂  _, (E ((rm (δ₁ ∨ δ₂) Δ•δ₁, ϕ)) _ ⇢ A ((rm (δ₁ ∨ δ₂) Δ•δ₁, ϕ)) _) ⊼
-                                                          (E ((rm (δ₁ ∨ δ₂) Δ•δ₂, ϕ)) _ ⇢ A ((rm (δ₁ ∨ δ₂) Δ•δ₂, ϕ)) _) :2
-    applicable_ImpLVar Δ ? λ q ψ _, A (rm (Var q → ψ) Δ • ψ, ϕ) _ :2
-    applicable_ImpLAnd Δ ? λ δ₁ δ₂ δ₃  _, A ((rm ((δ₁ ∧ δ₂)→ δ₃) Δ • (δ₁ → (δ₂ → δ₃)), ϕ)) _ :3
-    applicable_ImpLOr Δ ? λ δ₁ δ₂ δ₃  _, A (rm ((δ₁ ∨ δ₂)→ δ₃) Δ • (δ₁ → δ₃) • (δ₂ → δ₃), ϕ) _ :3
-    applicable_Atom p Δ ϕ ? λ _, ⊤ :0
-    applicable_AndR ϕ ? λ ϕ₁ ϕ₂ _, A (Δ, ϕ₁) _ ⊼ A (Δ, ϕ₂) _ :2
-    applicable_ImpR ϕ ? λ ϕ₁ ϕ₂ _, E (Δ • ϕ₁, ϕ₂) _ ⇢ A (Δ • ϕ₁, ϕ₂) _ :2
-    (⋁ (in_map Δ (a_rule_env EA)) ⊻ a_rule_form EA) (* the non-invertible rules *)
-.
+    ⋁ (in_map Δ (@a_rule_env p  Δ ϕ E A)) ⊻ @a_rule_form p  Δ ϕ E A.
+Next Obligation. intros. subst Δ ϕ. eapply env_order_lt_le_trans; [exact H|].
+order_tac. do 2 apply env_order_eq_add. apply simp_env_order. Qed.
+Next Obligation. intros. subst Δ ϕ. eapply env_order_lt_le_trans; [exact H|].
+order_tac. do 2 apply env_order_eq_add. apply simp_env_order. Qed.
 
 
-Definition E pe := EA true pe.
-Definition A pe := EA false pe.
+Definition E := EA true.
+Definition A := EA false.
 
 Definition Ef (ψ : form) := E ([ψ], ⊥).
 Definition Af (ψ : form) := A ([], ψ).
 
-End PropQuantDefinition.
-
 End UniformInterpolation.
-

theories/iSL/Order.v

@@ -34,7 +34,7 @@ Qed.
 
 Definition env_order_refl Δ Δ' := (Δ ≺ Δ') \/ Δ ≡ₚ Δ'.
 
-Local Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150).
+Global Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150).
 
 Global Instance Proper_env_weight: Proper ((≡ₚ) ==> (=)) env_weight.
 Proof.
@@ -392,6 +392,15 @@ Qed.
 
 Global Hint Resolve openboxes_env_order : order.
 
+Lemma weight_Arrow_1 φ ψ : 1 < weight (φ → ψ).
+Proof. simpl. pose (weight_pos  φ). lia. Qed.
+
+Lemma weight_Box_1 φ: 1 < weight (□ φ).
+Proof. simpl. pose (weight_pos  φ). lia. Qed.
+
+Global Hint Resolve weight_Arrow_1 : order.
+Global Hint Resolve weight_Box_1 : order.
+
 Ltac order_tac :=
 try unfold pointed_env_ms_order; prepare_order;
 repeat rewrite elements_env_add; 

theories/iSL/PropQuantifiers.v

@@ -1,7 +1,8 @@
-Require Import ISL.Sequents.
+Require Import ISL.Sequents ISL.Formulas.
 Require Import ISL.SequentProps ISL.Order ISL.Optimizations.
 Require Import Coq.Program.Equality. (* for dependent induction *)
 
+
 (** * Overview: Propositional Quantifiers
 
 The main theorem proved in this file was first proved as Theorem 1 in:

theories/iSL/Simp.v

@@ -527,10 +527,10 @@ match goal with
 end.
 Qed.
 
-Require Import ISL.PropQuantifiers.
+Require Import ISL.InvPropQuantifiers.
 
-Definition E_simplified (p: variable) (ψ: form) := simp (E p ([ψ],  ⊥)).
-Definition A_simplified (p: variable) (ψ: form) := simp (Af p (ψ)).
+Definition E_simplified (p: variable) (ψ: form) := simp_form (E p ([ψ],  ⊥)).
+Definition A_simplified (p: variable) (ψ: form) := simp_form (Af p (ψ)).
 
 (*
 Lemma bot_vars_incl V: vars_incl ⊥ V.