Done simplifying Δ in E(Δ) and A(Δ, φ)

hferee · Sep 11, 2024 · 9cd5481 · 9cd5481
1 parent b218377
commit 9cd5481
Show file tree

Hide file tree

Showing 6 changed files with 237 additions and 380 deletions.
diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v
@@ -5,7 +5,7 @@ Require Import ExtrOcamlBasic ExtrOcamlString.
 
 Require Import K.Interpolation.UIK_braga.
 Require Import KS_export.
-Require Import ISL.InvPropQuantifiers ISL.DecisionProcedure ISL.Simp.
+Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp.
 
 
 Fixpoint MPropF_of_form (f : Formulas.form) : MPropF  :=

diff --git a/theories/iSL/InvPropQuantifiers.v b/theories/iSL/InvPropQuantifiers.v
diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v
@@ -36,6 +36,14 @@ Definition env_order_refl Δ Δ' :=  (env_weight Δ) ≤(env_weight Δ').
 
 Global Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150).
 
+Lemma env_order_env_order_refl Δ Δ' : env_order Δ Δ' -> env_order_refl Δ Δ'.
+Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
+
+Global Hint Resolve env_order_env_order_refl: order.
+
+Lemma env_order_self Δ : Δ ≼ Δ.
+Proof. unfold env_order_refl. trivial. Qed.
+
 Global Instance Proper_env_weight: Proper ((≡ₚ) ==> (=)) env_weight.
 Proof.
 intros Γ Δ Heq. unfold env_weight. now rewrite Heq.
@@ -396,12 +404,22 @@ Hint Extern 5 (?a ≺· ?b) => order_tac : proof.
 
 Lemma pointed_env_order_bot_R pe Δ φ: (pe ≺· (Δ, ⊥)) -> pe ≺· (Δ, φ).
 Proof.
-Admitted.
+intro Hlt. destruct pe as (Γ, ψ). unfold pointed_env_order. simpl.
+eapply env_order_lt_le_trans. exact Hlt. simpl.
+unfold env_order_refl. repeat rewrite env_weight_add.
+assert(Hle: weight ⊥ ≤ weight φ) by (destruct φ; simpl; lia).
+apply Nat.pow_le_mono_r with (a := 5) in Hle; lia.
+Qed.
 
 Hint Resolve pointed_env_order_bot_R : order.
 
 Lemma pointed_env_order_bot_L pe Δ φ: ((Δ, φ) ≺· pe) -> (Δ, ⊥) ≺· pe.
 Proof.
-Admitted.
+intro Hlt. destruct pe as (Γ, ψ). unfold pointed_env_order. simpl.
+eapply env_order_le_lt_trans; [|exact Hlt]. simpl.
+unfold env_order_refl. repeat rewrite env_weight_add.
+assert(Hle: weight ⊥ ≤ weight φ) by (destruct φ; simpl; lia).
+apply Nat.pow_le_mono_r with (a := 5) in Hle; lia.
+Qed.
 
 Hint Resolve pointed_env_order_bot_L : order.