Use list instead of multiset when building propositional quantifiers.…

… Definitions only, soundness proof to go.

theories/iSL/Cut.v

@@ -1,29 +1,30 @@
 Require Import ISL.Formulas ISL.Sequents ISL.Order.
 Require Import ISL.SequentProps .
 
+Local Hint Rewrite elements_env_add : order.
+
+
 (* From "A New Calculus for Intuitionistic Strong Löb Logic" *)
 Theorem additive_cut Γ φ ψ :
   Γ ⊢ φ  -> Γ • φ ⊢ ψ ->
   Γ ⊢ ψ.
-Proof. (*
-Ltac order_tac := try (apply le_S_n; etransitivity; [|exact HW]); apply Nat.le_succ_l;
-match goal with |- env_weight .order_tac. *)
+Proof.
 remember (weight φ) as w. assert(Hw : weight φ ≤ w) by lia. clear Heqw.
 revert φ Hw ψ Γ.
 induction w; intros φ Hw; [pose (weight_pos φ); lia|].
 intros ψ Γ.
 remember (Γ, ψ) as pe.
 replace Γ with pe.1 by now subst.
 replace ψ with pe.2 by now subst. clear Heqpe Γ ψ. revert pe.
-refine  (@well_founded_induction _ _ wf_pointed_order _ _).
+refine  (@well_founded_induction _ _ wf_pointed_env_ms_order _ _).
 intros (Γ &ψ). simpl. intro IHW'. assert (IHW := fun Γ0 => fun ψ0 => IHW' (Γ0, ψ0)).
 simpl in IHW. clear IHW'. intros HPφ HPψ.
 Ltac otac Heq := subst; repeat rewrite env_replace in Heq by trivial; repeat rewrite env_add_remove by trivial; order_tac; rewrite Heq; order_tac.
 destruct HPφ; simpl in Hw.
 - now apply contraction.
 - apply ExFalso.
 - apply AndL_rev in HPψ. do 2 apply IHw in HPψ; trivial; try lia; apply weakening; assumption.
-- apply AndL. apply IHW; auto with proof. order_tac.
+- apply AndL. apply IHW; auto with proof. order_tac. 
 - apply OrL_rev in HPψ; apply (IHw φ); [lia| |]; tauto.
 - apply OrL_rev in HPψ; apply (IHw ψ0); [lia| |]; tauto.
 - apply OrL; apply IHW; auto with proof.
@@ -41,15 +42,15 @@ destruct HPφ; simpl in Hw.
   + forward. auto with proof.
   + apply AndR.
      * rw (symmetry Heq) 0. apply IHW.
-     -- order_tac.
+     -- unfold pointed_env_ms_order. order_tac.
      -- now apply ImpR.
      -- peapply HPψ1.
      * rw (symmetry Heq) 0. apply IHW.
        -- order_tac.
        -- apply ImpR. box_tac. peapply HPφ.
        -- peapply HPψ2.
   + forward. apply AndL. apply IHW.
-     * otac Heq.
+     * unfold pointed_env_ms_order. otac Heq.
      * apply AndL_rev. backward. rw (symmetry Heq) 0. apply ImpR, HPφ.
      * backward. peapply HPψ.
   + apply OrR1, IHW.
@@ -157,7 +158,7 @@ destruct HPφ; simpl in Hw.
     *  (* (V-f ) *)
        intro Hneq. forward. apply ImpBox.
        -- apply IHW.
-        ++ otac Heq.
+        ++ otac Heq. rewrite elements_open_boxes. otac Heq.
         ++ apply ImpR_rev, open_boxes_R, ImpR.
                 apply ImpLBox_prev with φ1. exch 0. apply weakening.
                 backward. rw (symmetry Heq) 0. apply ImpR, HPφ.
@@ -170,7 +171,7 @@ destruct HPφ; simpl in Hw.
         ++ exch 0.  rw (symmetry (difference_singleton _ _ Hin0)) 1. exact HPψ2.
   + subst. rw (symmetry Heq) 0. rewrite open_boxes_add in HPψ. simpl in HPψ.
       apply BoxR. apply IHW.
-    * otac Heq. (* todo: count rhs twice *)
+    * otac Heq. rewrite elements_open_boxes. otac Heq.
     * apply open_boxes_R, weakening, ImpR, HPφ.
     * exch 0. exact HPψ.
 - apply ImpLVar. eapply IHW; eauto.
@@ -269,7 +270,7 @@ destruct HPφ; simpl in Hw.
       forward. apply ImpBox.
      * (* π0 *)
         apply IHW.
-      -- otac Heq.
+      -- otac Heq. rewrite elements_open_boxes. otac Heq.
       -- apply ImpLBox_prev with (φ1 := φ1).
           exch 0. apply weakening.
           apply open_boxes_R. backward. rw (symmetry Heq) 0. apply BoxR, HPφ.
@@ -294,7 +295,7 @@ destruct HPφ; simpl in Hw.
   + (* (VIII-c) *)
       subst. rw (symmetry Heq) 0. rewrite open_boxes_add in HPψ. simpl in HPψ.
       apply BoxR. apply IHW.
-    * otac Heq. (* todo: count rhs twice *)
+    * otac Heq. rewrite elements_open_boxes. otac Heq.
     * apply open_boxes_R, weakening, BoxR, HPφ.
     * apply (IHw φ).
       -- lia.

theories/iSL/Environments.v

@@ -45,9 +45,16 @@ Global Instance proper_disj_union : Proper ((≡@{env}) ==> (≡@{env}) ==> (≡
 Proof. intros Γ Γ' Heq Δ Δ' Heq'. ms. Qed.
 
 
-
 Global Notation "Γ • φ" := (disj_union Γ (base.singletonMS φ)) (at level 105, φ at level 85, left associativity).
 
+Lemma elements_env_add (Γ : env) φ : elements(Γ • φ) ≡ₚ φ :: elements Γ.
+Proof.
+rewrite (gmultiset_elements_disj_union Γ).
+setoid_rewrite (gmultiset_elements_singleton φ).
+symmetry. apply Permutation_cons_append.
+Qed.
+
+
 (** * Multiset utilities *)
 
 Lemma multeq_meq (M N: env) : (forall x, multiplicity x M = multiplicity x N) -> M ≡  N.
@@ -325,21 +332,21 @@ Qed.
 (* a dependent map on lists, with knowledge that we are on that list *)
 (* should work with any set-like type *)
 
-Program Fixpoint in_map_aux {A : Type} (Γ : env) (f : forall φ, (φ ∈ Γ) -> A)
- Γ' (HΓ' : Γ' ⊆ elements Γ) : list A:=
+Program Fixpoint in_map_aux {A : Type} (Γ : list form) (f : forall φ, (φ ∈ Γ) -> A)
+ Γ' (HΓ' : Γ' ⊆ Γ) : list A:=
 match Γ' with
 | [] => []
 | a::Γ' => f a _ :: in_map_aux Γ f Γ' _
 end.
 Next Obligation.
-intros. apply gmultiset_elem_of_elements. auto with *.
+intros. auto with *.
 Qed.
 Next Obligation. auto with *. Qed.
 
 
-Definition in_map {A : Type} (Γ : env)
+Definition in_map {A : Type} (Γ : list form)
   (f : forall φ, (φ ∈ Γ) -> A) : list A :=
-  in_map_aux Γ f (elements Γ) (reflexivity _).
+  in_map_aux Γ f Γ (reflexivity _).
 
 
 (* This generalises to any type. decidability of equality over this type is necessary for a result in "Type" *)
@@ -348,7 +355,7 @@ Lemma in_in_map {A : Type} {HD : forall a b : A, Decision (a = b)}
   ψ ∈ (in_map Γ f) -> {ψ0 & {Hin | ψ = f ψ0 Hin}}.
 Proof.
 unfold in_map.
-assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ), ψ ∈ in_map_aux Γ f Γ' HΓ'
+assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ Γ), ψ ∈ in_map_aux Γ f Γ' HΓ'
   → {ψ0 & {Hin : ψ0 ∈ Γ | ψ = f ψ0 Hin}}); [|apply Hcut].
 induction Γ'; simpl; intros HΓ' Hin.
 - contradict Hin. auto. now rewrite elem_of_nil.
@@ -369,7 +376,7 @@ Lemma in_map_in {A : Type} {HD : forall a b : A, Decision (a = b)}
   {Hin' | f ψ0 Hin' ∈ (in_map Γ f)}.
 Proof.
 unfold in_map.
-assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ) ψ0 (Hin : In ψ0 Γ'),
+assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ Γ) ψ0 (Hin : In ψ0 Γ'),
   {Hin' | f ψ0 Hin' ∈ in_map_aux Γ f Γ' HΓ'}).
 - induction Γ'; simpl; intros HΓ' ψ' Hin'; [auto with *|].
   case (decide (ψ' = a)).
@@ -378,12 +385,12 @@ assert(Hcut : forall Γ' (HΓ' : Γ' ⊆ elements Γ) ψ0 (Hin : In ψ0 Γ'),
       pose (Hincl := (in_map_aux_obligation_2 Γ (a :: Γ') HΓ' a Γ' eq_refl)).
       destruct (IHΓ' Hincl ψ' Hin'') as [Hin0 Hprop].
       eexists. right. apply Hprop.
-- destruct (Hcut (elements Γ) (reflexivity (elements Γ)) ψ0) as [Hin' Hprop].
-  + now apply elem_of_list_In,  gmultiset_elem_of_elements.
+- destruct (Hcut Γ (reflexivity Γ) ψ0) as [Hin' Hprop].
+  + auto. now apply elem_of_list_In.
   + exists Hin'. exact Hprop.
 Qed.
 
-Lemma in_map_empty A f : @in_map A ∅ f = [].
+Lemma in_map_empty A f : @in_map A [] f = [].
 Proof. auto with *. Qed.
 
 Lemma in_map_ext {A} Δ f g:
@@ -461,7 +468,6 @@ Proof.
   apply Hinsert, IH; multiset_solver.
 Qed.
 
-
 Lemma difference_include (θ θ' : form) (Δ : env) :
   (θ' ∈ Δ) ->
   θ ∈ Δ ∖ {[θ']} -> θ ∈ Δ.
@@ -472,6 +478,11 @@ rewrite gmultiset_disj_union_difference with (X := {[θ']}).
 - now apply gmultiset_singleton_subseteq_l.
 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.
+
 
 (* technical lemma : one can constructively find whether an environment contains
    an element satisfying a decidable property *)
@@ -577,6 +588,13 @@ Proof.
 intros Hx Hφ. apply elem_of_open_boxes in Hφ. destruct Hφ as [Hφ|Hφ]; eauto.
 Qed.
 
+Lemma occurs_in_map_open_box x φ Δ : occurs_in x φ -> φ ∈ (map open_box Δ) -> exists θ, θ ∈ Δ /\ occurs_in x θ.
+Proof.
+intros Hx Hφ. apply elem_of_list_In, in_map_iff in Hφ.
+destruct Hφ as [ψ [Hφ Hin]]; subst.
+exists ψ. split. now apply elem_of_list_In. destruct ψ; trivial.
+Qed.
+
 
 Global Hint Rewrite open_boxes_disj_union : proof.
 
@@ -634,27 +652,18 @@ Global Hint Rewrite open_boxes_singleton : proof.
 Global Hint Resolve open_boxes_spec' : proof.
 Global Hint Resolve open_boxes_spec : proof.
 
+Global Instance Proper_elements : Proper ((≡) ==> (≡ₚ)) ((λ Γ : env, elements Γ)).
+Proof.
+intros Γ Δ Heq; apply AntiSymm_instance_0; apply gmultiset_elements_submseteq; ms.
+Qed.
 
-Ltac vars_tac :=
-intros; subst;
-repeat match goal with
-| HE : context [occurs_in ?x (?E _ _)], H : occurs_in ?x (?E _ _) |- _ =>
-    apply HE in H
-end;
-intuition;
-repeat match goal with | H : exists x, _ |- _ => destruct H end;
-intuition;
-simpl in *; in_tac; try (split; [tauto || auto with *|]); simpl in *;
-try match goal with
-| H : occurs_in _ (?a ⇢ (?b ⇢ ?c)) |- _ => apply occurs_in_make_impl2 in H
-| H : occurs_in _ (?a ⇢ ?b) |- _ => apply occurs_in_make_impl in H
-|H1 : ?x0 ∈ (⊗ ?Δ), H2 : occurs_in ?x ?x0 |- _ =>
-      apply (occurs_in_open_boxes _ _ _ H2) in H1
-end;
-repeat match goal with | H : exists x, _ |- _ => destruct H end; intuition;
-try multimatch goal with
-| H : ?θ0 ∈ ?Δ0 |- context [exists θ, θ ∈ ?Δ /\ occurs_in ?x θ] =>
-  solve[try right; exists θ0; split; [eauto using difference_include|simpl; tauto]; eauto] end.
-
+Lemma elements_open_boxes Γ: elements (⊗ Γ) ≡ₚ map open_box (elements Γ).
+Proof.
+unfold open_boxes. remember (elements Γ) as l. clear Γ Heql.
+induction l as [| a l].
+- ms.
+- simpl. setoid_rewrite gmultiset_elements_disj_union.
+  rewrite IHl. setoid_rewrite gmultiset_elements_singleton. trivial.
+Qed.
 
 (* TODO: move in optimisations *)