fix definition for env_order_

refl
hferee · Sep 10, 2024 · b218377 · b218377
1 parent c3ceeca
commit b218377
Showing 1 changed file with 14 additions and 30 deletions.
diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v
@@ -32,7 +32,7 @@ intro Hw. unfold env_order, ltof. do 2 rewrite env_weight_singleton.
 apply Nat.pow_lt_mono_r. lia. trivial.
 Qed.
 
-Definition env_order_refl Δ Δ' := (Δ ≺ Δ') \/ Δ ≡ₚ Δ'.
+Definition env_order_refl Δ Δ' :=  (env_weight Δ) ≤(env_weight Δ').
 
 Global Notation "Δ ≼ Δ'" := (env_order_refl Δ Δ') (at level 150).
 
@@ -44,12 +44,7 @@ Qed.
 
 Global Instance Proper_env_order_refl_env_weight:
   Proper ((env_order_refl) ==> le) env_weight.
-Proof.
-intros Γ Δ.
-unfold env_order. intros [Hle | Heq].
-- auto with *.
-- now rewrite Heq.
-Qed.
+Proof. intros Γ Δ Hle. auto with *. Qed.
 
 Global Hint Resolve Proper_env_order_refl_env_weight : order.
 
@@ -164,8 +159,7 @@ Lemma env_order_refl_disj_union_compat Δ Δ' Δ'' Δ''':
   (env_order_refl Δ Δ'') -> (env_order_refl Δ' Δ''') -> env_order_refl (Δ ++ Δ') (Δ'' ++ Δ''').
 Proof.
 unfold env_order_refl, env_order, ltof. repeat rewrite env_weight_disj_union.
-intros [Hlt1 | Heq1] [Hlt2 | Heq2]; try rewrite Heq1; try rewrite Heq2; try lia.
-right. trivial.
+intros Hle1 Hle2; try rewrite Heq1; try rewrite Heq2; try lia.
 Qed.
 
 Global Hint Resolve env_order_refl_disj_union_compat : order.
@@ -174,20 +168,13 @@ Hint Unfold env_order_refl : order.
 Lemma env_order_disj_union_compat_strong_right Δ Δ' Δ'' Δ''':
   (Δ ≺ Δ'') -> (Δ' ≼ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
 Proof.
-intros H1 H2. 
-destruct H2 as [Hlt|Heq].
-- unfold env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia.
-- rewrite Heq. now apply env_order_disj_union_compat_left.
+intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia.
 Qed.
 
 Lemma env_order_disj_union_compat_strong_left Δ Δ' Δ'' Δ''':
   (Δ ≼ Δ'') -> (Δ' ≺ Δ''') -> Δ ++ Δ' ≺ Δ'' ++ Δ'''.
 Proof.
-intros H1 H2.
-destruct H1 as [Hlt|Heq].
-- unfold env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia.
-- rewrite Heq. now apply env_order_disj_union_compat_right.
-Qed.
+intros Hlt Hle. unfold env_order_refl, env_order, ltof in *. do 2 rewrite env_weight_disj_union. lia. Qed.
 
 Global Hint Resolve env_order_disj_union_compat_strong_left : order.
 Global Hint Rewrite elements_open_boxes : order.
@@ -197,12 +184,9 @@ Proof. destruct φ; simpl; lia. Qed.
 
 Lemma open_boxes_env_order Δ : (map open_box Δ) ≼ Δ.
 Proof.
-induction Δ as [|φ Δ].
-- right. trivial.
-- destruct IHΔ as [Hlt | Heq]; simpl.
-  + left. apply env_order_compat'; trivial. apply weight_open_box. 
-  + rewrite Heq. auto with order. destruct φ; simpl; try auto with order.
-       left. auto with order.
+unfold env_order_refl.
+induction Δ as [|φ Δ]; trivial.
+simpl. do 2 rewrite env_weight_add. destruct φ; simpl; lia.
 Qed.
 
 Global Hint Resolve open_boxes_env_order : order.
@@ -281,7 +265,7 @@ Proof. etransitivity; [|apply env_order_0].	 assumption. Qed.
 
 
 Lemma env_order_eq_add Δ Δ' φ: (Δ ≼ Δ') -> (Δ • φ) ≼ (Δ' • φ).
-Proof. intros[Heq|Hlt]. left. now apply env_order_add_compat. right. ms. Qed.
+Proof. unfold env_order_refl. do 2 rewrite env_weight_add. lia. Qed.
 
 
 Global Hint Resolve env_order_0 : order.
@@ -312,9 +296,9 @@ Global Hint Rewrite open_boxes_remove : order.
 
 Lemma remove_env_order Δ φ:  rm φ Δ ≼ Δ.
 Proof.
-induction Δ as [|ψ Δ].
-- simpl. right. auto.
-- simpl.  destruct form_eq_dec; auto with order.
+unfold env_order_refl.
+induction Δ as [|ψ Δ]. trivial. 
+simpl. destruct form_eq_dec; repeat rewrite env_weight_add; lia.
 Qed.
 
 Global Hint Resolve remove_env_order : order.
@@ -333,10 +317,10 @@ Qed.
 Global Hint Resolve remove_In_env_order_refl : order.
 
 Lemma env_order_lt_le_trans Γ Γ' Γ'' : (Γ ≺ Γ') -> (Γ' ≼ Γ'') -> Γ ≺ Γ''.
-Proof. intros Hlt [Hlt' | Heq]. transitivity Γ'; auto with order. now rewrite <- Heq. Qed.
+Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
 
 Lemma env_order_le_lt_trans Γ Γ' Γ'' : (Γ ≼ Γ') -> (Γ' ≺ Γ'') -> Γ ≺ Γ''.
-Proof. intros [Hlt' | Heq] Hlt. transitivity Γ'; auto with order. now rewrite Heq. Qed.
+Proof. unfold env_order, env_order_refl, ltof. lia. Qed.
 
 Lemma remove_In_env_order Δ φ:  In φ Δ -> rm φ Δ ≺ Δ.
 Proof.