Define a linear remove function on lists (to mimic multiset differnce

with a singleton).
Prove a_rule_env_spec as a poc.

theories/iSL/Environments.v

@@ -478,10 +478,21 @@ rewrite gmultiset_disj_union_difference with (X := {[θ']}).
 - now apply gmultiset_singleton_subseteq_l.
 Qed.
 
+Fixpoint rm x l := match l with
+| h :: t => if form_eq_dec x h then t else h :: rm x t
+| [] => []
+end.
+
+Lemma in_rm l x y: In x (rm y l) -> In x l.
+Proof.
+induction l; simpl. tauto.
+destruct form_eq_dec. tauto. firstorder.
+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.
+  θ ∈ rm θ' Δ -> θ ∈ Δ.
+Proof. intros Hin' Hin. eapply elem_of_list_In, in_rm, elem_of_list_In, Hin. Qed.
 
 
 (* technical lemma : one can constructively find whether an environment contains

theories/iSL/Order.v

@@ -282,7 +282,7 @@ Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order.
 Ltac get_diff_form g := match g with
 | ?Γ ∖{[?φ]} => φ
 | _ (?Γ ∖{[?φ]}) => φ
-| _ (remove _ ?φ _) => φ
+| _ (rm ?φ _) => φ
 | ?Γ • _ => get_diff_form Γ
 end.
 
@@ -293,28 +293,24 @@ end.
 
 Global Hint Rewrite open_boxes_remove : order.
 
-Lemma remove_env_order Δ φ:  remove form_eq_dec φ Δ ≼ Δ.
+Lemma remove_env_order Δ φ:  rm φ Δ ≼ Δ.
 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.
+- simpl.  destruct form_eq_dec; auto with order.
 Qed.
 
 Global Hint Resolve remove_env_order : order.
 
-Lemma remove_In_env_order_refl Δ φ:  In φ Δ -> remove form_eq_dec φ Δ • φ ≼ Δ.
+Lemma remove_In_env_order_refl Δ φ:  In φ Δ -> rm φ Δ • φ ≼ Δ.
 Proof.
 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.
+      * rewrite (Permutation_swap ψ φ (rm φ Δ)). auto with order.
 Qed.
 
 Global Hint Resolve remove_In_env_order_refl : order.
@@ -325,7 +321,7 @@ Proof. intros Hlt [Hlt' | Heq]. transitivity Γ'; auto with order. now rewrite <
 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 φ Δ ≺ Δ.
+Lemma remove_In_env_order Δ φ:  In φ Δ -> rm φ Δ ≺ Δ.
 Proof.
 intro Hin. apply remove_In_env_order_refl in Hin.
 eapply env_order_lt_le_trans; [|apply Hin]. auto with order.

theories/iSL/PropQuantifiers.v

@@ -45,7 +45,7 @@ Program Definition e_rule {Δ : list form } {ϕ : form}
   (θ: form) (Hin : θ ∈ Δ) : form :=
 let E Δ H := fst (EA0 (Δ, ϕ) H) in
 let A pe0 H := snd (EA0 pe0 H) in
-let Δ'  := remove form_eq_dec θ Δ in
+let Δ'  := rm θ Δ in
 match θ with
 | Bot => ⊥  (* E0 *)
 | Var q =>
@@ -78,11 +78,11 @@ end.
     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 : ∀ pe (Hpe : pe ≺· (Δ, ϕ)), 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 Δ'  := remove form_eq_dec θ Δ in
+let Δ'  := rm θ Δ in
 match θ with
 | Var q =>
     if decide (p = q)
@@ -119,6 +119,7 @@ match θ with
 (* 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 {Δ : list form} {ϕ : form}
@@ -283,7 +284,7 @@ Lemma e_rule_vars Δ (θ : form) (Hin : θ ∈ Δ) (ϕ : form)
       (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.
+Proof. 
 destruct θ; unfold e_rule; simpl; try tauto; try solve [repeat case decide; repeat vars_tac].
 destruct θ1; repeat case decide; repeat vars_tac.
 Qed.
@@ -297,7 +298,7 @@ Lemma a_rule_env_vars Δ θ Hin ϕ
       (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 (a_rule_env EA0 θ Hin) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ).
-Proof.
+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.
 Qed.
@@ -309,14 +310,14 @@ Lemma a_rule_form_vars Δ ϕ
       (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 (a_rule_form EA0) -> x ≠ p ∧ (occurs_in x ϕ \/ ∃ θ, θ ∈ Δ /\ occurs_in x θ).
-Proof.
+Proof. 
 destruct ϕ; unfold a_rule_form; simpl; try tauto; try solve [repeat case decide; repeat vars_tac].
 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 θ))).
-Proof.
+Proof. 
 remember (Δ, ϕ) as pe.
 replace Δ with pe.1 by now subst.
 replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. revert pe.
@@ -359,52 +360,74 @@ Section EntailmentCorrect.
 Hint Extern 5 (?a ≺ ?b) => order_tac : proof.
 Opaque make_disj.
 Opaque make_conj.
+
+(* TODO move *)
+Lemma list_to_set_disj_rm Δ v: (list_to_set_disj Δ : env) ∖ {[v]} = list_to_set_disj (rm v Δ).
+Proof.
+Admitted.
+
+Lemma list_to_set_disj_env_add Δ v: ((list_to_set_disj Δ : env) • v : env)≡ list_to_set_disj (v :: Δ).
+Proof.
+Admitted.
+
+Lemma list_to_set_disj_open_boxes Δ:  ((⊗ (list_to_set_disj Δ)) ≡ list_to_set_disj (map open_box Δ)).
+Proof.
+Admitted.
+
+Local Ltac l_tac :=
+    rewrite (proper_Provable _ _ (list_to_set_disj_env_add _ _) _ _ eq_refl)
+|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)) _ _ eq_refl)
+|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _))) _ _ eq_refl)
+|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_env_add _ _)))) _ _ eq_refl)
+|| rewrite (proper_Provable _ _ (equiv_disj_union_compat_r(equiv_disj_union_compat_r (equiv_disj_union_compat_r (list_to_set_disj_open_boxes _)))) _ _ eq_refl).
+
 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 ⊢ ϕ).
+  (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)).
 clear HEA.
-destruct θ; exhibit Hin 1.
+assert(Hi : θ ∈ list_to_set_disj  Δ) by now apply elem_of_list_to_set_disj.
+destruct θ; exhibit Hi 1; rewrite list_to_set_disj_rm in *.
 - simpl; case decide; intro Hp.
   + subst. case_decide; subst; auto with proof.
   + exch 0...
 - constructor 2.
-- simpl; exch 0. apply AndL. exch 1; exch 0...
+- simpl; exch 0. apply AndL. exch 1; exch 0. do 2 l_tac...
 - apply make_conj_sound_L.
   exch 0. apply OrL; exch 0.
-  + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L... (* uses imp_cut *)
-  + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L. auto with proof.
+  + apply AndL. apply make_impl_sound_L. exch 0. apply make_impl_sound_L.
+      l_tac. apply ImpL...
+  + apply AndL. l_tac. apply make_impl_sound_L. exch 0. apply make_impl_sound_L...
 - destruct θ1.
   + simpl; case decide; intro Hp.
     * subst. case decide.
       -- intros Hp.
-         assert(Hin' : (p → θ2) ∈ Δ ∖ {[Var p]})
-         by (rewrite (gmultiset_disj_union_difference' _ _ Hp) in Hin; ms).
-         assert (Hin'' : Var p ∈ Δ ∖ {[p → θ2]}) by now apply in_difference.
-         exhibit Hin'' 2. exch 0; exch 1. apply ImpLVar.
-         exch 1. exch 0. peapply HA. rewrite <- difference_singleton by trivial. reflexivity.
+         assert (Hin'' : Var p ∈ (list_to_set_disj (rm (p → θ2) Δ) : env)).
+          (rewrite <- list_to_set_disj_rm; apply in_difference; try easy; now apply elem_of_list_to_set_disj).
+         exhibit Hin'' 2. exch 0; exch 1. apply ImpLVar. exch 0. backward.
+         rewrite env_add_remove. exch 0. l_tac...
       -- intro; constructor 2.
     * apply make_conj_sound_L. constructor 4. exch 0. exch 1. exch 0. apply ImpLVar.
-      exch 0. apply weakening. exch 0...
+      exch 0. exch 1. l_tac. apply weakening...
   + constructor 2.
-  + simpl; exch 0. apply ImpLAnd. apply make_impl_complete_L2. exch 0...
-  + simpl; exch 0. apply ImpLOr. exch 1. exch 0...
+  + simpl; exch 0. apply ImpLAnd. exch 0. l_tac...
+  + simpl; exch 0. apply ImpLOr. exch 1. l_tac. exch 0. l_tac...
   + apply make_conj_sound_L. exch 0. apply ImpLImp; exch 0.
-      * apply AndL. exch 0. apply make_impl_sound_L. exch 0...
-      * apply AndL. exch 0. apply weakening, HA.
+      * apply AndL. exch 0. apply make_impl_sound_L. l_tac. exch 0...
+      * apply AndL. exch 0. l_tac. apply weakening, HA.
   + exch 0. exch 0. simpl. apply  AndL. exch 1; exch 0. apply ImpBox.
       * box_tac. box_tac. exch 0; exch 1; exch 0. apply weakening. exch 1; exch 0.
-         apply make_impl_sound_L. apply ImpL.
+         apply make_impl_sound_L. do 3 l_tac. apply ImpL.
          -- auto with proof.
          -- apply HA.
-      * exch 1; exch 0. apply weakening. exch 0. auto with proof.
+      * exch 1; exch 0. apply weakening. exch 0. l_tac. auto with proof.
 - auto with proof.
 Qed.
 
 Proposition entail_correct Δ ϕ : (Δ ⊢ E (Δ, ϕ)) * (Δ•A (Δ, ϕ) ⊢ ϕ).
-Proof.
+Proof. Admitted.
 remember (Δ, ϕ) as pe.
 replace Δ with pe.1 by now subst.
 replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ. revert pe.
@@ -475,7 +498,7 @@ Section PropQuantCorrect.
 
 (** E's second argument is mostly irrelevant and is only there for uniform treatment with A *)
 Lemma E_irr ϕ' Δ ϕ : E (Δ, ϕ) = E (Δ, ϕ').
-Proof.
+Proof. 
 remember ((Δ, ϕ) : pointed_env) as pe.
 replace Δ with pe.1 by now subst.
 replace ϕ with pe.2 by now subst. clear Heqpe Δ ϕ.
@@ -492,7 +515,7 @@ Qed.
 Lemma E_left {Γ} {θ} {Δ} {φ φ'} (Hin : φ ∈ Δ) :
 (Γ•e_rule (λ pe (_ : pe ≺· (Δ, φ')),  EA pe)  φ Hin) ⊢ θ ->
 Γ•E (Δ, φ') ⊢ θ.
-Proof.
+Proof. 
 intro Hp. rewrite E_eq.
 destruct (@in_map_in _ _ _  (e_rule (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule].
 eapply conjunction_L.
@@ -503,7 +526,7 @@ Qed.
 Lemma A_right {Γ} {Δ} {φ φ'} (Hin : φ ∈ Δ) :
 Γ ⊢ a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe) φ Hin ->
 Γ ⊢ A (Δ, φ').
-Proof. intro Hp. rewrite A_eq.
+Proof.  intro Hp. rewrite A_eq.
 destruct (@in_map_in _ _ _  (a_rule_env (λ pe (_ : pe ≺· (Δ, φ')), EA pe)) _ Hin) as [Hin' Hrule].
 eapply make_disj_sound_R, OrR1, disjunction_R.
 - exact Hrule.
@@ -514,7 +537,7 @@ Qed.
 Proposition pq_correct Γ Δ ϕ: (∀ φ0, φ0 ∈ Γ -> ¬ occurs_in p φ0) -> (Γ ⊎ Δ ⊢ ϕ) ->
   (¬ occurs_in p ϕ -> Γ•E (Δ, ϕ) ⊢ ϕ) *
   (Γ•E (Δ, ϕ) ⊢ A (Δ, ϕ)).
-Proof.
+Proof. 
 (* we want to use an E rule *)
 Ltac Etac := foldEA; intros; match goal with | Hin : ?a ∈ ?Δ |- _•E (?Δ, _) ⊢ _=> apply (E_left Hin); unfold e_rule end.
 
@@ -863,7 +886,7 @@ Open Scope type_scope.
 
 
 Lemma E_of_empty p φ : E p (∅, φ) = (Implies Bot Bot).
-Proof.
+Proof. 
   rewrite E_eq. rewrite in_map_empty. now unfold conjunction, nodup, foldl.
 Qed.
 
@@ -879,7 +902,7 @@ Theorem iSL_uniform_interpolation p V: p ∉ V ->
   * (vars_incl (Af p φ) V)
   * ({[Af p φ]} ⊢ φ)
   * (∀ θ, vars_incl θ V -> {[θ]} ⊢ φ -> {[θ]} ⊢ Af p φ).
-Proof.
+Proof. 
 intros Hp φ Hvarsφ; repeat split.
 
   + intros x Hx. apply (EA_vars p _ ⊥ x) in Hx.