From afe5bac2dc2fed94c0974fbee5e4d8a5ed068ad1 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 10 Mar 2024 13:54:19 -0700
Subject: [PATCH] Commit result of (unsuccessfully) trying to prove
 monotonicity of plus.

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

diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index f8cfd96..20ba11b 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -1,10 +1,11 @@
 module Analysis.Sign where
 
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
-open import Data.Product using (proj₁)
-open import Data.List using (foldr)
+open import Data.Product using (_×_; proj₁; _,_)
+open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
 open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Unit using (⊤)
 
 open import Language
 open import Lattice
@@ -30,19 +31,56 @@ _≟ᵍ_ 0ˢ + = no (λ ())
 _≟ᵍ_ 0ˢ - = no (λ ())
 _≟ᵍ_ 0ˢ 0ˢ = yes refl
 
+-- embelish 'sign' with a top and bottom element.
+open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB
+    using ()
+    renaming
+        ( AboveBelow to SignLattice
+        ; ≈-dec to ≈ᵍ-dec
+        ; ⊥ to ⊥ᵍ
+        ; ⊤ to ⊤ᵍ
+        ; [_] to [_]ᵍ
+        ; ≈-⊥-⊥ to ≈ᵍ-⊥ᵍ-⊥ᵍ
+        ; ≈-⊤-⊤ to ≈ᵍ-⊤ᵍ-⊤ᵍ
+        ; ≈-lift to ≈ᵍ-lift
+        )
+-- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
+open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
+
+finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ
+
+open FiniteHeightLattice finiteHeightLatticeᵍ
+    using ()
+    renaming
+        ( _≼_ to _≼ᵍ_
+        ; _≈_ to _≈ᵍ_
+        ; _⊔_ to _⊔ᵍ_
+        ; ≈-refl to ≈ᵍ-refl
+        )
+
+plus : SignLattice → SignLattice → SignLattice
+plus ⊥ᵍ _ = ⊥ᵍ
+plus _ ⊥ᵍ = ⊥ᵍ
+plus ⊤ᵍ _ = ⊤ᵍ
+plus _ ⊤ᵍ = ⊤ᵍ
+plus [ + ]ᵍ [ + ]ᵍ = [ + ]ᵍ
+plus [ + ]ᵍ [ - ]ᵍ = ⊤ᵍ
+plus [ + ]ᵍ [ 0ˢ ]ᵍ = [ + ]ᵍ
+plus [ - ]ᵍ [ + ]ᵍ = ⊤ᵍ
+plus [ - ]ᵍ [ - ]ᵍ = [ - ]ᵍ
+plus [ - ]ᵍ [ 0ˢ ]ᵍ = [ - ]ᵍ
+plus [ 0ˢ ]ᵍ [ + ]ᵍ = [ + ]ᵍ
+plus [ 0ˢ ]ᵍ [ - ]ᵍ = [ - ]ᵍ
+plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
+
+-- this is incredibly tedious: 125 cases per monotonicity proof, and tactics
+-- are hard. postulate for now.
+postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
+postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
+
 module _ (prog : Program) where
     open Program prog
 
-    -- embelish 'sign' with a top and bottom element.
-    open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB
-        using ()
-        renaming (AboveBelow to SignLattice; ≈-dec to ≈ᵍ-dec)
-    -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
-    open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
-
-
-    finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ
-
     -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
     open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
         using ()