From 51accb64384ccac83154906a4720dfca7712f551 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 10 Mar 2024 16:40:49 -0700
Subject: [PATCH] Define 'minus', too -- with no monotonicity proof.

I'm still thinking about how this should be achieved most easily.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Analysis/Sign.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index 20ba11b..d572668 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -78,6 +78,24 @@ plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
 postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
 
+minus : SignLattice → SignLattice → SignLattice
+minus ⊥ᵍ _ = ⊥ᵍ
+minus _ ⊥ᵍ = ⊥ᵍ
+minus ⊤ᵍ _ = ⊤ᵍ
+minus _ ⊤ᵍ = ⊤ᵍ
+minus [ + ]ᵍ [ + ]ᵍ = ⊤ᵍ
+minus [ + ]ᵍ [ - ]ᵍ = [ + ]ᵍ
+minus [ + ]ᵍ [ 0ˢ ]ᵍ = [ + ]ᵍ
+minus [ - ]ᵍ [ + ]ᵍ = [ - ]ᵍ
+minus [ - ]ᵍ [ - ]ᵍ = ⊤ᵍ
+minus [ - ]ᵍ [ 0ˢ ]ᵍ = [ - ]ᵍ
+minus [ 0ˢ ]ᵍ [ + ]ᵍ = [ - ]ᵍ
+minus [ 0ˢ ]ᵍ [ - ]ᵍ = [ + ]ᵍ
+minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
+
+postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
+postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
+
 module _ (prog : Program) where
     open Program prog