From f9148e4c7fe28efd7bad90b23493bc506b2a49f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 9 Oct 2024 10:58:06 +0200 Subject: [PATCH] Change weight definition from Dyckhoff and Negri's to Pitts' --- theories/iSL/Formulas.v | 2 +- theories/iSL/Order.v | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/theories/iSL/Formulas.v b/theories/iSL/Formulas.v index ca5da0e..4c026a6 100644 --- a/theories/iSL/Formulas.v +++ b/theories/iSL/Formulas.v @@ -105,7 +105,7 @@ Fixpoint weight (φ : form) : nat := match φ with | ⊥ => 1 | Var _ => 1 | φ ∧ ψ => 2 + weight φ + weight ψ -| φ ∨ ψ => 3 + weight φ + weight ψ +| φ ∨ ψ => 1 + weight φ + weight ψ | φ → ψ => 1 + weight φ + weight ψ | □φ => 1 + weight φ end. diff --git a/theories/iSL/Order.v b/theories/iSL/Order.v index 7370121..f2b01c5 100644 --- a/theories/iSL/Order.v +++ b/theories/iSL/Order.v @@ -413,3 +413,8 @@ apply Nat.pow_le_mono_r with (a := 5) in Hle; lia. Qed. Hint Resolve pointed_env_order_bot_L : order. + +Lemma weight_or_bot a b: weight(⊥) < weight (a ∨b). +Proof. destruct a; simpl; lia. Qed. + +Hint Resolve weight_or_bot : order.