From 9f2790c500c542eba04877e55830323b6bacbbdb Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 5 Jan 2025 19:35:56 -0800
Subject: [PATCH] Actually force proof of 'analyze-correct'

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Analysis/Forward.agda |  3 ++-
 Analysis/Sign.agda    | 41 ++++++++++++++++++-----------------------
 2 files changed, 20 insertions(+), 24 deletions(-)

diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index c3a94da..fba6e22 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -8,6 +8,7 @@ module Analysis.Forward
     {{≈ˡ-dec : IsDecidable _≈ˡ_}} where
 
 open import Data.Empty using (⊥-elim)
+open import Data.Unit using (⊤)
 open import Data.String using (String)
 open import Data.Product using (_,_)
 open import Data.List using (_∷_; []; foldr; foldl)
@@ -77,7 +78,7 @@ module WithProg (prog : Program) where
             updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
 
         module WithValidInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
-                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} where
+                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} (dummy : ⊤) where
             open ValidStmtEvaluator validEvaluator
 
             eval-fold-valid : ∀ {s bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip (eval s)) vs bss ⟧ᵛ ρ₂
diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index 47609f2..f4364e6 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -16,6 +16,7 @@ open import Lattice
 open import Equivalence
 open import Showable using (Showable; show)
 open import Utils using (_⇒_; _∧_; _∨_)
+open import Analysis.Utils using (eval-combine₂)
 import Analysis.Forward
 
 data Sign : Set where
@@ -101,6 +102,9 @@ plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
 postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
 
+plus-Mono₂ : Monotonic₂ _≼ᵍ_ _≼ᵍ_ _≼ᵍ_ plus
+plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ)
+
 minus : SignLattice → SignLattice → SignLattice
 minus ⊥ᵍ _ = ⊥ᵍ
 minus _ ⊥ᵍ = ⊥ᵍ
@@ -119,6 +123,9 @@ minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
 postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
 
+minus-Mono₂ : Monotonic₂ _≼ᵍ_ _≼ᵍ_ _≼ᵍ_ minus
+minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ)
+
 ⟦_⟧ᵍ : SignLattice → Value → Set
 ⟦_⟧ᵍ ⊥ᵍ _ = ⊥
 ⟦_⟧ᵍ ⊤ᵍ _ = ⊤
@@ -195,29 +202,13 @@ module WithProg (prog : Program) where
 
     eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
     eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-        let
-            -- TODO: can this be done with less boilerplate?
-            g₁vs₁ = eval e₁ vs₁
-            g₂vs₁ = eval e₂ vs₁
-            g₁vs₂ = eval e₁ vs₂
-            g₂vs₂ = eval e₂ vs₂
-        in
-            ≼ᵍ-trans
-                {plus g₁vs₁ g₂vs₁} {plus g₁vs₂ g₂vs₁} {plus g₁vs₂ g₂vs₂}
-                (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Monoʳ e₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Monoʳ e₂ {vs₁} {vs₂} vs₁≼vs₂))
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᵍ-trans {x} {y} {z})
+                      plus plus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
     eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-        let
-            -- TODO: here too -- can this be done with less boilerplate?
-            g₁vs₁ = eval e₁ vs₁
-            g₂vs₁ = eval e₂ vs₁
-            g₁vs₂ = eval e₁ vs₂
-            g₂vs₂ = eval e₂ vs₂
-        in
-            ≼ᵍ-trans
-                {minus g₁vs₁ g₂vs₁} {minus g₁vs₂ g₂vs₁} {minus g₁vs₂ g₂vs₂}
-                (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Monoʳ e₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Monoʳ e₂ {vs₁} {vs₂} vs₁≼vs₂))
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᵍ-trans {x} {y} {z})
+                      minus minus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
     eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
         with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
     ...   | yes k∈kvs₁ | yes k∈kvs₂ =
@@ -301,4 +292,8 @@ module WithProg (prog : Program) where
     eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl
     eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
 
-    analyze-correct = Analysis.Forward.WithProg.analyze-correct
+    instance
+        SignEvalValid : ValidExprEvaluator SignEval latticeInterpretationᵍ
+        SignEvalValid = record { valid = eval-valid }
+
+    analyze-correct = Analysis.Forward.WithProg.analyze-correct SignLattice prog tt