DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Define 'minus', too -- with no monotonicity proof.

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

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-10 16:40:49 -07:00
parent afe5bac2dc
commit 51accb6438
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Analysis/Sign.agda
View File

@ -78,6 +78,24 @@ plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂) postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus 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 module _ (prog : Program) where
open Program prog open Program prog