* Decorrelate the definition of Propositional quantifiers from the de…

…finition of the simplifications using modules

* move a few lemmas to better locations
* remove a ocaml compiler warning (unused module type in a functor) to allow compilation of extraction.

dune

@@ -1,4 +1,4 @@
 
 (env
   (dev
-    (flags (:standard -w -33))))
+    (flags (:standard -w -33-67))))

theories/extraction/UIML_extraction.v

@@ -5,9 +5,12 @@ Require Import ExtrOcamlBasic ExtrOcamlString.
 
 Require Import K.Interpolation.UIK_braga.
 Require Import KS_export.
-Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp_env.
-
+Require Import ISL.PropQuantifiers ISL.DecisionProcedure.
+Require ISL.Simp_env.
 
+(* Simplified propositional quantifiers *)
+Module Import S := Simp_env.S.
+Module Import SPQr := PropQuant S.
 
 Fixpoint MPropF_of_form (f : Formulas.form) : MPropF  :=
 match f with

theories/iSL/Optimizations.v

@@ -59,6 +59,7 @@ match obviously_smaller φ ψ with
 Lemma occurs_in_choose_conj v φ ψ : occurs_in v (choose_conj φ ψ) -> occurs_in v φ \/ occurs_in v ψ.
 Proof. unfold choose_conj; destruct obviously_smaller; simpl; intros; tauto. Qed.
 
+
 Definition make_conj φ ψ := 
 match ψ with
   | ψ1 ∧ ψ2 =>
@@ -288,6 +289,12 @@ apply AndR.
 - exch 0. now apply weakening.
 Qed.
 
+Lemma choose_conj_topL φ : (choose_conj φ ⊤ = φ).
+Proof.
+unfold choose_conj.
+rewrite (obviously_smaller_compatible_LT _ _).2. trivial.
+apply ImpR, ExFalso.
+Qed.
 
 Lemma choose_conj_sound_L Δ φ ψ:
   (Δ ⊢ φ) -> (Δ ⊢ ψ) -> Δ ⊢ choose_conj φ ψ.
@@ -847,12 +854,85 @@ assert(Hcut : forall ψ, ((φ ∈ Δ) + (Γ•ψ ⊢ θ)) -> (Γ•foldl make_co
 intro Hin. apply Hcut. now left.
 Qed.
 
+Lemma conjunction_L' Γ Δ ϕ: (Γ ⊎ {[⋀ Δ]} ⊢ ϕ) -> Γ ⊎ list_to_set_disj Δ ⊢ ϕ.
+Proof.
+revert ϕ. unfold conjunction.
+assert( Hstrong: ∀ θ ϕ : form, Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ
+  → (Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ).
+{
+  induction Δ as [|δ Δ]; intros θ ϕ; simpl.
+  - intro Hp. peapply Hp.
+  - case in_dec; intros Hin Hp.
+    + peapply (weakening δ). apply IHΔ, Hp. ms.
+    + simpl in Hp. apply IHΔ in Hp.
+        peapply (AndL_rev (Γ ⊎ list_to_set_disj Δ) θ δ). apply make_conj_complete_L, Hp.
+}
+  intros; apply additive_cut with (φ := ⊤); eauto with proof.
+Qed.
+
+Lemma conjunction_R Δ: list_to_set_disj Δ ⊢ ⋀ Δ.
+Proof.
+apply conjunction_R1. intros φ Hφ. apply elem_of_list_to_set_disj in Hφ.
+exhibit Hφ 0. apply generalised_axiom. 
+Qed.
+
+Lemma conjunction_L'' Γ Δ ϕ: Γ ⊎ list_to_set_disj Δ ⊢ ϕ -> (Γ ⊎ {[⋀ Δ]} ⊢ ϕ).
+Proof.
+revert ϕ. unfold conjunction.
+assert( Hstrong: ∀ θ ϕ : form,(Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ ϕ -> Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ ϕ).
+{
+  induction Δ as [|δ Δ]; intros θ ϕ; simpl.
+  - intro Hp. peapply Hp.
+  - case in_dec; intros Hin Hp.
+    + apply IHΔ.
+         assert(Hin' : δ ∈ (Γ ⊎ list_to_set_disj Δ)).
+         { apply gmultiset_elem_of_disj_union; right; apply elem_of_list_to_set_disj, elem_of_list_In, Hin. }
+         exhibit Hin' 1. exch 0. apply contraction. exch 1. exch 0.
+         rw (symmetry (difference_singleton _ _ Hin')) 2. peapply Hp.
+    + simpl. apply IHΔ. apply make_conj_sound_L, AndL. peapply Hp.
+}
+intros. apply Hstrong, weakening. assumption.
+Qed.
+
+(* begin details *)
+(**
+  - [choose_impl_weight]: The weight of the chosen implication is less than or equal to the weight of the implication.
+  - [choose_impl_top_weight]: The weight of the chosen implication with ⊤ is less than or equal to the weight of the formula.
+  - [obviously_smaller_top_not_Eq]: ⊤ is not obviously smaller than any formula.
+  - [contextual_simp_form_weight]: The simplified form of a formula in a given context is either ⊤, or has a weight less than or equal to the original formula.
+*)
+(* end details *)
 
-Lemma OrR_idemp Γ ψ : Γ ⊢ ψ ∨ ψ -> Γ ⊢ ψ.
-Proof. intro Hp. dependent induction Hp; auto with proof. Qed.
 
+Lemma choose_impl_weight φ ψ: weight (choose_impl φ ψ) ≤ weight (φ → ψ).
+Proof.
+pose (weight_pos φ). pose (weight_pos ψ).
+unfold choose_impl; repeat case decide; intros; simpl; lia.
+Qed.
+
+Lemma choose_impl_top_weight ψ: weight (choose_impl ⊤ ψ) ≤ weight ψ.
+Proof.
+pose (weight_pos ψ).
+unfold choose_impl; repeat case decide; intros; try lia.
+- destruct (weight_tautology ψ).
+  + apply obviously_smaller_compatible_LT in e.
+    apply additive_cut with ⊤; auto with proof.
+  + subst; simpl in *; tauto || lia.
+  + subst; simpl in *; tauto || lia.
+- destruct (weight_tautology ψ).
+  + apply obviously_smaller_compatible_LT in e.
+    apply additive_cut with ⊤; auto with proof.
+  + subst; simpl in *; tauto || lia.
+  + subst; simpl in *; tauto || lia.
+- contradict n. apply obviously_smaller_compatible_LT. auto with proof.
+- contradict n0. apply obviously_smaller_compatible_LT. auto with proof.
+- contradict n2. apply obviously_smaller_compatible_LT. auto with proof.
+Qed.
 
-Lemma strongness φ : ∅ •  φ ⊢ □ φ.
+Lemma obviously_smaller_top_not_Eq φ: obviously_smaller ⊤ φ ≠ Eq.
 Proof.
-apply BoxR. box_tac. apply weakening, open_box_L, generalised_axiom.
+unfold obviously_smaller.
+case Provable_dec. discriminate. intro. case Provable_dec. discriminate.
+intro Hf. contradict Hf. auto with proof.
 Qed.
+

theories/iSL/Order.v

@@ -136,6 +136,8 @@ intros.  unfold env_order, ltof. repeat rewrite env_weight_add.
 apply Nat.add_lt_le_mono; auto with *. now apply Nat.pow_le_mono_r.
 Qed.
 
+Global Hint Resolve env_order_compat' : order.
+
 Lemma env_order_add_compat Δ Δ' φ : (Δ ≺ Δ') -> (Δ • φ) ≺ (Δ' • φ).
 Proof.
 unfold env_order, ltof. do 2 rewrite env_weight_add. lia.
@@ -263,9 +265,12 @@ Qed.
 Lemma env_order_cancel_right Δ Δ' φ:  (Δ ≺ Δ') -> Δ ≺ (Δ' • φ).
 Proof. etransitivity; [|apply env_order_0].	 assumption. Qed.
 
-Lemma env_order_eq_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ).
+Lemma env_order_refl_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ).
 Proof. unfold env_order_refl. do 2 rewrite env_weight_add. lia. Qed.
 
+Lemma env_order_refl_add' Δ Δ' φ φ': weight φ ≤ weight φ' -> (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ').
+Proof. unfold env_order_refl. do 2 rewrite env_weight_add.
+intros. apply Nat.add_le_mono. lia. apply Nat.pow_le_mono_r; lia. Qed.
 
 Global Hint Resolve env_order_0 : order.
 Global Hint Resolve env_order_1 : order.
@@ -274,7 +279,8 @@ Global Hint Resolve env_order_3 : order.
 Global Hint Resolve env_order_4 : order.
 Global Hint Resolve env_order_add_compat : order.
 Global Hint Resolve env_order_cancel_right : order.
-Global Hint Resolve env_order_eq_add : order.
+Global Hint Resolve env_order_refl_add : order.
+Global Hint Resolve env_order_refl_add' : order.
 Global Hint Extern 1 (?a < ?b) => subst; simpl; lia : order.
 
 Ltac get_diff_form g := match g with
@@ -351,7 +357,7 @@ unfold pointed_env_order; subst; simpl; repeat rewrite open_boxes_add; try match
 | H : ?ψ ∈ ?Γ |- ?Γ' ≺ (_ :: _ :: ?Γ) => let ψ' := (get_diff_form Γ') in
 apply (env_order_equiv_right_compat (equiv_disj_union_compat_r(equiv_disj_union_compat_r(difference_singleton Γ ψ' H)))) ||
 (eapply env_order_le_lt_trans; [| apply env_order_add_compat; 
-eapply env_order_lt_le_trans; [| (apply env_order_eq_add; apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial) ] ] )
+eapply env_order_lt_le_trans; [| (apply env_order_refl_add; apply (remove_In_env_order_refl _ ψ'); try apply elem_of_list_In; trivial) ] ] )
 |H : ?a = _ |- context[?a] => rewrite H; try prepare_order
 end.
 
@@ -419,3 +425,6 @@ Lemma weight_or_bot a b: weight(⊥) < weight (a ∨b).
 Proof. destruct a; simpl; lia. Qed.
 
 Hint Resolve weight_or_bot : order.
+
+Definition pointed_env_order_refl pe1 pe2 :=
+  env_order_refl (pe1.2 :: pe1.2 :: pe1.1) (pe2.2 :: pe2.2 :: pe2.1).