Compare commits
9 Commits
332b7616cf
...
56c72e1388
Author | SHA1 | Date | |
---|---|---|---|
56c72e1388 | |||
0c30f8be48 | |||
75f981cb75 | |||
ca99e18184 | |||
702cf2c298 | |||
0c088ca2ae | |||
bc138d87f0 | |||
311ed75186 | |||
1ccc6f08e5 |
50
Analysis/Sign.agda
Normal file
50
Analysis/Sign.agda
Normal file
|
@ -0,0 +1,50 @@
|
|||
module Analysis.Sign where
|
||||
|
||||
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
|
||||
open import Language
|
||||
open import Lattice
|
||||
|
||||
data Sign : Set where
|
||||
+ : Sign
|
||||
- : Sign
|
||||
0ˢ : Sign
|
||||
|
||||
-- g for siGn; s is used for strings and i is not very descriptive.
|
||||
_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
|
||||
_≟ᵍ_ + + = yes refl
|
||||
_≟ᵍ_ + - = no (λ ())
|
||||
_≟ᵍ_ + 0ˢ = no (λ ())
|
||||
_≟ᵍ_ - + = no (λ ())
|
||||
_≟ᵍ_ - - = yes refl
|
||||
_≟ᵍ_ - 0ˢ = no (λ ())
|
||||
_≟ᵍ_ 0ˢ + = no (λ ())
|
||||
_≟ᵍ_ 0ˢ - = no (λ ())
|
||||
_≟ᵍ_ 0ˢ 0ˢ = yes refl
|
||||
|
||||
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 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 import Lattice.Bundles.FiniteValueMap String SignLattice _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵛ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵛ; _≈_ to _≈ᵛ_; ≈-dec to ≈ᵛ-dec-if-≈ᵍ-dec)
|
||||
|
||||
|
||||
VariableSigns = FiniteHeightTypeᵛ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
|
||||
finiteHeightLatticeᵛ = finiteHeightLatticeᵛ-if-B-finite finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
|
||||
≈ᵛ-dec = ≈ᵛ-dec-if-≈ᵍ-dec finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
|
||||
|
||||
-- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
|
||||
open import Lattice.Bundles.FiniteValueMap State VariableSigns _≟_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵐ)
|
||||
|
||||
StateVariables = FiniteHeightTypeᵐ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
|
||||
finiteHeightLatticeᵐ = finiteHeightLatticeᵐ-if-B-finite finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
|
|
@ -1,149 +0,0 @@
|
|||
open import Equivalence
|
||||
|
||||
module Homomorphism {a b} (A : Set a) (B : Set b)
|
||||
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
|
||||
(≈₂-equiv : IsEquivalence B _≈₂_)
|
||||
(f : A → B) where
|
||||
|
||||
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
|
||||
open import Function.Definitions using (Surjective)
|
||||
open import Relation.Binary.Core using (_Preserves_⟶_ )
|
||||
open import Data.Product using (_,_)
|
||||
open import Lattice
|
||||
|
||||
open IsEquivalence ≈₂-equiv using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; ≈-refl to ≈₂-refl)
|
||||
open import Relation.Binary.Reasoning.Base.Single _≈₂_ ≈₂-refl ≈₂-trans
|
||||
|
||||
infixl 20 _∙₂_
|
||||
_∙₂_ = ≈₂-trans
|
||||
|
||||
record SemilatticeHomomorphism (_⊔₁_ : A → A → A)
|
||||
(_⊔₂_ : B → B → B) : Set (a ⊔ℓ b) where
|
||||
field
|
||||
f-preserves-≈ : f Preserves _≈₁_ ⟶ _≈₂_
|
||||
f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂))
|
||||
|
||||
module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
|
||||
(sh : SemilatticeHomomorphism _⊔₁_ _⊔₂_)
|
||||
(≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
|
||||
(surF : Surjective _≈₁_ _≈₂_ f) where
|
||||
|
||||
open SemilatticeHomomorphism sh
|
||||
|
||||
transportSemilattice : IsSemilattice A _≈₁_ _⊔₁_ → IsSemilattice B _≈₂_ _⊔₂_
|
||||
transportSemilattice sA = record
|
||||
{ ≈-equiv = ≈₂-equiv
|
||||
; ≈-⊔-cong = ≈₂-⊔₂-cong
|
||||
; ⊔-assoc = λ b₁ b₂ b₃ →
|
||||
let (a₁ , fa₁≈b₁) = surF b₁
|
||||
(a₂ , fa₂≈b₂) = surF b₂
|
||||
(a₃ , fa₃≈b₃) = surF b₃
|
||||
in
|
||||
begin
|
||||
(b₁ ⊔₂ b₂) ⊔₂ b₃
|
||||
∼⟨ ≈₂-⊔₂-cong (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) (≈₂-sym fa₃≈b₃) ⟩
|
||||
(f a₁ ⊔₂ f a₂) ⊔₂ f a₃
|
||||
∼⟨ ≈₂-⊔₂-cong (≈₂-sym (f-⊔-distr a₁ a₂)) ≈₂-refl ⟩
|
||||
f (a₁ ⊔₁ a₂) ⊔₂ f a₃
|
||||
∼⟨ ≈₂-sym (f-⊔-distr (a₁ ⊔₁ a₂) a₃) ⟩
|
||||
f ((a₁ ⊔₁ a₂) ⊔₁ a₃)
|
||||
∼⟨ f-preserves-≈ (IsSemilattice.⊔-assoc sA a₁ a₂ a₃) ⟩
|
||||
f (a₁ ⊔₁ (a₂ ⊔₁ a₃))
|
||||
∼⟨ f-⊔-distr a₁ (a₂ ⊔₁ a₃) ⟩
|
||||
f a₁ ⊔₂ f (a₂ ⊔₁ a₃)
|
||||
∼⟨ ≈₂-⊔₂-cong ≈₂-refl (f-⊔-distr a₂ a₃) ⟩
|
||||
f a₁ ⊔₂ (f a₂ ⊔₂ f a₃)
|
||||
∼⟨ ≈₂-⊔₂-cong fa₁≈b₁ (≈₂-⊔₂-cong fa₂≈b₂ fa₃≈b₃) ⟩
|
||||
b₁ ⊔₂ (b₂ ⊔₂ b₃)
|
||||
∎
|
||||
; ⊔-comm = λ b₁ b₂ →
|
||||
let (a₁ , fa₁≈b₁) = surF b₁
|
||||
(a₂ , fa₂≈b₂) = surF b₂
|
||||
in
|
||||
begin
|
||||
b₁ ⊔₂ b₂
|
||||
∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂) ⟩
|
||||
f a₁ ⊔₂ f a₂
|
||||
∼⟨ ≈₂-sym (f-⊔-distr a₁ a₂) ⟩
|
||||
f (a₁ ⊔₁ a₂)
|
||||
∼⟨ f-preserves-≈ (IsSemilattice.⊔-comm sA a₁ a₂) ⟩
|
||||
f (a₂ ⊔₁ a₁)
|
||||
∼⟨ f-⊔-distr a₂ a₁ ⟩
|
||||
f a₂ ⊔₂ f a₁
|
||||
∼⟨ ≈₂-⊔₂-cong fa₂≈b₂ fa₁≈b₁ ⟩
|
||||
b₂ ⊔₂ b₁
|
||||
∎
|
||||
; ⊔-idemp = λ b →
|
||||
let (a , fa≈b) = surF b
|
||||
in
|
||||
begin
|
||||
b ⊔₂ b
|
||||
∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa≈b) (≈₂-sym fa≈b) ⟩
|
||||
f a ⊔₂ f a
|
||||
∼⟨ ≈₂-sym (f-⊔-distr a a) ⟩
|
||||
f (a ⊔₁ a)
|
||||
∼⟨ f-preserves-≈ (IsSemilattice.⊔-idemp sA a) ⟩
|
||||
f a
|
||||
∼⟨ fa≈b ⟩
|
||||
b
|
||||
∎
|
||||
}
|
||||
|
||||
|
||||
record LatticeHomomorphism (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
|
||||
(_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) : Set (a ⊔ℓ b) where
|
||||
field
|
||||
⊔-homomorphism : SemilatticeHomomorphism _⊔₁_ _⊔₂_
|
||||
⊓-homomorphism : SemilatticeHomomorphism _⊓₁_ _⊓₂_
|
||||
|
||||
open SemilatticeHomomorphism ⊔-homomorphism using (f-⊔-distr; f-preserves-≈) public
|
||||
open SemilatticeHomomorphism ⊓-homomorphism using () renaming (f-⊔-distr to f-⊓-distr) public
|
||||
|
||||
module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
|
||||
(_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
|
||||
(lh : LatticeHomomorphism _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_)
|
||||
(≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
|
||||
(≈₂-⊓₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊓₂ a₃) ≈₂ (a₂ ⊓₂ a₄))
|
||||
(surF : Surjective _≈₁_ _≈₂_ f) where
|
||||
|
||||
open LatticeHomomorphism lh
|
||||
|
||||
transportLattice : IsLattice A _≈₁_ _⊔₁_ _⊓₁_ → IsLattice B _≈₂_ _⊔₂_ _⊓₂_
|
||||
transportLattice lA = record
|
||||
{ joinSemilattice = transportSemilattice _⊔₁_ _⊔₂_ (LatticeHomomorphism.⊔-homomorphism lh) ≈₂-⊔₂-cong surF (IsLattice.joinSemilattice lA)
|
||||
; meetSemilattice = transportSemilattice _⊓₁_ _⊓₂_ (LatticeHomomorphism.⊓-homomorphism lh) ≈₂-⊓₂-cong surF (IsLattice.meetSemilattice lA)
|
||||
; absorb-⊔-⊓ = λ b₁ b₂ →
|
||||
let (a₁ , fa₁≈b₁) = surF b₁
|
||||
(a₂ , fa₂≈b₂) = surF b₂
|
||||
in
|
||||
begin
|
||||
b₁ ⊔₂ (b₁ ⊓₂ b₂)
|
||||
∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
|
||||
f a₁ ⊔₂ (f a₁ ⊓₂ f a₂)
|
||||
∼⟨ ≈₂-⊔₂-cong ≈₂-refl (≈₂-sym (f-⊓-distr a₁ a₂)) ⟩
|
||||
f a₁ ⊔₂ f (a₁ ⊓₁ a₂)
|
||||
∼⟨ ≈₂-sym (f-⊔-distr a₁ (a₁ ⊓₁ a₂)) ⟩
|
||||
f (a₁ ⊔₁ (a₁ ⊓₁ a₂))
|
||||
∼⟨ f-preserves-≈ (IsLattice.absorb-⊔-⊓ lA a₁ a₂) ⟩
|
||||
f a₁
|
||||
∼⟨ fa₁≈b₁ ⟩
|
||||
b₁
|
||||
∎
|
||||
; absorb-⊓-⊔ = λ b₁ b₂ →
|
||||
let (a₁ , fa₁≈b₁) = surF b₁
|
||||
(a₂ , fa₂≈b₂) = surF b₂
|
||||
in
|
||||
begin
|
||||
b₁ ⊓₂ (b₁ ⊔₂ b₂)
|
||||
∼⟨ ≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
|
||||
f a₁ ⊓₂ (f a₁ ⊔₂ f a₂)
|
||||
∼⟨ ≈₂-⊓₂-cong ≈₂-refl (≈₂-sym (f-⊔-distr a₁ a₂)) ⟩
|
||||
f a₁ ⊓₂ f (a₁ ⊔₁ a₂)
|
||||
∼⟨ ≈₂-sym (f-⊓-distr a₁ (a₁ ⊔₁ a₂)) ⟩
|
||||
f (a₁ ⊓₁ (a₁ ⊔₁ a₂))
|
||||
∼⟨ f-preserves-≈ (IsLattice.absorb-⊓-⊔ lA a₁ a₂) ⟩
|
||||
f a₁
|
||||
∼⟨ fa₁≈b₁ ⟩
|
||||
b₁
|
||||
∎
|
||||
}
|
|
@ -1,10 +1,93 @@
|
|||
module Language where
|
||||
|
||||
open import Data.String using (String)
|
||||
open import Data.Nat using (ℕ)
|
||||
open import Data.Nat using (ℕ; suc; pred)
|
||||
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
|
||||
open import Data.Product using (Σ; _,_; proj₁; proj₂)
|
||||
open import Data.Vec using (Vec; foldr)
|
||||
open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
|
||||
open import Data.List.Relation.Unary.All using (All; []; _∷_)
|
||||
open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
|
||||
open import Data.Fin.Properties using (suc-injective)
|
||||
open import Relation.Binary.PropositionalEquality using (cong; _≡_)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Function using (_∘_)
|
||||
|
||||
open import Lattice
|
||||
open import Utils using (Unique; Unique-map; empty; push)
|
||||
|
||||
data Expr : Set where
|
||||
_+_ : Expr → Expr → Expr
|
||||
_-_ : Expr → Expr → Expr
|
||||
`_ : String → Expr
|
||||
#_ : ℕ → Expr
|
||||
|
||||
data Stmt : Set where
|
||||
_←_ : String → Expr → Stmt
|
||||
|
||||
open import Lattice.MapSet String _≟ˢ_
|
||||
renaming
|
||||
( MapSet to StringSet
|
||||
; insert to insertˢ
|
||||
; to-List to to-Listˢ
|
||||
; empty to emptyˢ
|
||||
; _⊔_ to _⊔ˢ_
|
||||
)
|
||||
|
||||
private
|
||||
Expr-vars : Expr → StringSet
|
||||
Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
|
||||
Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
|
||||
Expr-vars (` s) = insertˢ s emptyˢ
|
||||
Expr-vars (# _) = emptyˢ
|
||||
|
||||
Stmt-vars : Stmt → StringSet
|
||||
Stmt-vars (x ← e) = insertˢ x (Expr-vars e)
|
||||
|
||||
-- Creating a new number from a natural number can never create one
|
||||
-- equal to one you get from weakening the bounds on another number.
|
||||
z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
|
||||
z≢sf f ()
|
||||
|
||||
z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
|
||||
z≢mapsfs [] = []
|
||||
z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
|
||||
|
||||
indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
|
||||
indices 0 = ([] , empty)
|
||||
indices (suc n') =
|
||||
let
|
||||
(inds' , unids') = indices n'
|
||||
in
|
||||
( zero ∷ mapˡ suc inds'
|
||||
, push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
|
||||
)
|
||||
|
||||
|
||||
-- For now, just represent the program and CFG as one type, without branching.
|
||||
record Program : Set where
|
||||
field
|
||||
length : ℕ
|
||||
stmts : Vec Stmt length
|
||||
|
||||
private
|
||||
vars-Set : StringSet
|
||||
vars-Set = foldr (λ n → StringSet)
|
||||
(λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts
|
||||
|
||||
vars : List String
|
||||
vars = to-Listˢ vars-Set
|
||||
|
||||
vars-Unique : Unique vars
|
||||
vars-Unique = proj₂ vars-Set
|
||||
|
||||
State : Set
|
||||
State = Fin length
|
||||
|
||||
states : List State
|
||||
states = proj₁ (indices length)
|
||||
|
||||
states-Unique : Unique states
|
||||
states-Unique = proj₂ (indices length)
|
||||
|
||||
_≟_ : IsDecidable (_≡_ {_} {State})
|
||||
_≟_ = _≟ᶠ_
|
||||
|
|
|
@ -19,8 +19,10 @@ module _ (fhB : FiniteHeightLattice B) where
|
|||
module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
|
||||
import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
|
||||
|
||||
FiniteHeightType = FVM.FiniteMap
|
||||
FiniteHeightType = FVM.FiniteMap ks
|
||||
|
||||
finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
|
||||
open FiniteHeightLattice finiteHeightLattice public
|
||||
|
||||
≈-dec = FVM.≈-dec ks ≈₂-dec
|
||||
|
||||
finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
|
||||
|
|
|
@ -2,7 +2,7 @@ open import Lattice
|
|||
open import Relation.Binary.PropositionalEquality as Eq
|
||||
using (_≡_;refl; sym; trans; cong; subst)
|
||||
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
|
||||
open import Data.List using (List)
|
||||
open import Data.List using (List; _∷_; [])
|
||||
|
||||
module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
|
||||
(_≈₂_ : B → B → Set b)
|
||||
|
@ -10,8 +10,9 @@ module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
|
|||
(≡-dec-A : IsDecidable (_≡_ {a} {A}))
|
||||
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
|
||||
|
||||
open IsLattice lB using () renaming (_≼_ to _≼₂_)
|
||||
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
|
||||
using (Map; ⊔-equal-keys; ⊓-equal-keys)
|
||||
using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
|
||||
renaming
|
||||
( _≈_ to _≈ᵐ_
|
||||
; _⊔_ to _⊔ᵐ_
|
||||
|
@ -28,9 +29,21 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
|
|||
; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
|
||||
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
|
||||
; ≈-dec to ≈ᵐ-dec
|
||||
; _[_] to _[_]ᵐ
|
||||
; locate to locateᵐ
|
||||
; keys to keysᵐ
|
||||
; _updating_via_ to _updatingᵐ_via_
|
||||
; updating-via-keys-≡ to updatingᵐ-via-keys-≡
|
||||
; f'-Monotonic to f'-Monotonicᵐ
|
||||
; _≼_ to _≼ᵐ_
|
||||
)
|
||||
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
|
||||
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
|
||||
open import Equivalence
|
||||
open import Function using (_∘_)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Utils using (Pairwise; _∷_; [])
|
||||
open import Data.Empty using (⊥-elim)
|
||||
|
||||
module _ (ks : List A) where
|
||||
FiniteMap : Set (a ⊔ℓ b)
|
||||
|
@ -56,6 +69,18 @@ module _ (ks : List A) where
|
|||
km₁≡ks
|
||||
)
|
||||
|
||||
_∈k_ : A → FiniteMap → Set a
|
||||
_∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
|
||||
|
||||
_updating_via_ : FiniteMap → List A → (A → B) → FiniteMap
|
||||
_updating_via_ (m₁ , ksm₁≡ks) ks f =
|
||||
( m₁ updatingᵐ ks via f
|
||||
, trans (sym (updatingᵐ-via-keys-≡ m₁ ks f)) ksm₁≡ks
|
||||
)
|
||||
|
||||
_[_] : FiniteMap → List A → List B
|
||||
_[_] (m₁ , _) ks = m₁ [ ks ]ᵐ
|
||||
|
||||
≈-equiv : IsEquivalence FiniteMap _≈_
|
||||
≈-equiv = record
|
||||
{ ≈-refl =
|
||||
|
@ -97,6 +122,8 @@ module _ (ks : List A) where
|
|||
; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
|
||||
}
|
||||
|
||||
open IsLattice isLattice using (_≼_) public
|
||||
|
||||
lattice : Lattice FiniteMap
|
||||
lattice = record
|
||||
{ _≈_ = _≈_
|
||||
|
@ -104,3 +131,46 @@ module _ (ks : List A) where
|
|||
; _⊓_ = _⊓_
|
||||
; isLattice = isLattice
|
||||
}
|
||||
|
||||
module _ {l} {L : Set l}
|
||||
{_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
|
||||
(lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
|
||||
open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
|
||||
|
||||
module _ (f : L → FiniteMap) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
|
||||
(g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic _≼ˡ_ _≼₂_ (g k))
|
||||
(ks : List A) where
|
||||
|
||||
updater : L → A → B
|
||||
updater l k = g k l
|
||||
|
||||
f' : L → FiniteMap
|
||||
f' l = (f l) updating ks via (updater l)
|
||||
|
||||
f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
|
||||
f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
|
||||
|
||||
all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂))
|
||||
all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)
|
||||
|
||||
∈k-exclusive : ∀ (fm₁ fm₂ : FiniteMap) {k : A} → ¬ ((k ∈k fm₁) × (¬ k ∈k fm₂))
|
||||
∈k-exclusive fm₁ fm₂ {k} (k∈kfm₁ , k∉kfm₂) =
|
||||
let
|
||||
k∈kfm₂ = subst (λ l → k ∈ˡ l) (all-equal-keys fm₁ fm₂) k∈kfm₁
|
||||
in
|
||||
k∉kfm₂ k∈kfm₂
|
||||
|
||||
m₁≼m₂⇒m₁[ks]≼m₂[ks] : ∀ (fm₁ fm₂ : FiniteMap) (ks' : List A) →
|
||||
fm₁ ≼ fm₂ → Pairwise _≼₂_ (fm₁ [ ks' ]) (fm₂ [ ks' ])
|
||||
m₁≼m₂⇒m₁[ks]≼m₂[ks] _ _ [] _ = []
|
||||
m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁@(m₁ , km₁≡ks) fm₂@(m₂ , km₂≡ks) (k ∷ ks'') m₁≼m₂
|
||||
with ∈k-dec k (proj₁ m₁) | ∈k-dec k (proj₁ m₂)
|
||||
... | yes k∈km₁ | yes k∈km₂ =
|
||||
let
|
||||
(v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁
|
||||
(v₂ , k,v₂∈m₂) = locateᵐ {m = m₂} k∈km₂
|
||||
in
|
||||
(m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂) ∷ m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
|
||||
... | no k∉km₁ | no k∉km₂ = m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
|
||||
... | yes k∈km₁ | no k∉km₂ = ⊥-elim (∈k-exclusive fm₁ fm₂ (k∈km₁ , k∉km₂))
|
||||
... | no k∉km₁ | yes k∈km₂ = ⊥-elim (∈k-exclusive fm₂ fm₁ (k∈km₂ , k∉km₁))
|
||||
|
|
|
@ -19,7 +19,7 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex
|
|||
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Equivalence
|
||||
open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
|
||||
open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
|
||||
|
||||
open IsLattice lB using () renaming
|
||||
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
|
||||
|
@ -34,6 +34,21 @@ private module ImplKeys where
|
|||
keys : List (A × B) → List A
|
||||
keys = map proj₁
|
||||
|
||||
-- See note on `forget` for why this is defined in global scope even though
|
||||
-- it operates on lists.
|
||||
∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l))
|
||||
∈k-dec k [] = no (λ ())
|
||||
∈k-dec k ((k' , v) ∷ xs)
|
||||
with (≡-dec-A k k')
|
||||
... | yes k≡k' = yes (here k≡k')
|
||||
... | no k≢k' with (∈k-dec k xs)
|
||||
... | yes k∈kxs = yes (there k∈kxs)
|
||||
... | no k∉kxs = no witness
|
||||
where
|
||||
witness : ¬ k ∈ˡ (ImplKeys.keys ((k' , v) ∷ xs))
|
||||
witness (here k≡k') = k≢k' k≡k'
|
||||
witness (there k∈kxs) = k∉kxs k∈kxs
|
||||
|
||||
private module _ where
|
||||
open MemProp using (_∈_)
|
||||
open ImplKeys
|
||||
|
@ -65,19 +80,6 @@ private module _ where
|
|||
... | yes k∈xs = yes (there k∈xs)
|
||||
... | no k∉xs = no (λ { (here k≡x) → k≢x k≡x; (there k∈xs) → k∉xs k∈xs })
|
||||
|
||||
∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ keys l)
|
||||
∈k-dec k [] = no (λ ())
|
||||
∈k-dec k ((k' , v) ∷ xs)
|
||||
with (≡-dec-A k k')
|
||||
... | yes k≡k' = yes (here k≡k')
|
||||
... | no k≢k' with (∈k-dec k xs)
|
||||
... | yes k∈kxs = yes (there k∈kxs)
|
||||
... | no k∉kxs = no witness
|
||||
where
|
||||
witness : ¬ k ∈ keys ((k' , v) ∷ xs)
|
||||
witness (here k≡k') = k≢k' k≡k'
|
||||
witness (there k∈kxs) = k∉kxs k∈kxs
|
||||
|
||||
∈-cong : ∀ {c d} {C : Set c} {D : Set d} {c : C} {l : List C} →
|
||||
(f : C → D) → c ∈ l → f c ∈ map f l
|
||||
∈-cong f (here c≡c') = here (cong f c≡c')
|
||||
|
@ -340,7 +342,7 @@ private module ImplInsert (f : B → B → B) where
|
|||
|
||||
restrict-preserves-Unique : ∀ {l₁ l₂ : List (A × B)} →
|
||||
Unique (keys l₂) → Unique (keys (restrict l₁ l₂))
|
||||
restrict-preserves-Unique {l₁} {[]} _ = empty
|
||||
restrict-preserves-Unique {l₁} {[]} _ = Utils.empty
|
||||
restrict-preserves-Unique {l₁} {(k , v) ∷ xs} (push k≢xs uxs)
|
||||
with ∈k-dec k l₁
|
||||
... | yes _ = push (restrict-preserves-k≢ k≢xs) (restrict-preserves-Unique uxs)
|
||||
|
@ -476,6 +478,9 @@ private module ImplInsert (f : B → B → B) where
|
|||
Map : Set (a ⊔ℓ b)
|
||||
Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
|
||||
|
||||
empty : Map
|
||||
empty = ([] , Utils.empty)
|
||||
|
||||
keys : Map → List A
|
||||
keys (kvs , _) = ImplKeys.keys kvs
|
||||
|
||||
|
@ -488,8 +493,9 @@ _∈k_ k m = MemProp._∈_ k (keys m)
|
|||
locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m)
|
||||
locate k∈km = locate-impl k∈km
|
||||
|
||||
-- defined this way because ∈ for maps uses projection, so the full map can't be guessed.
|
||||
-- On the other hand, list can be guessed.
|
||||
-- `forget` and `∈k-dec` are defined this way because ∈ for maps uses
|
||||
-- projection, so the full map can't be guessed. On the other hand, list can
|
||||
-- be guessed.
|
||||
forget : ∀ {k : A} {v : B} {l : List (A × B)} → (k , v) ∈ˡ l → k ∈ˡ (ImplKeys.keys l)
|
||||
forget = ∈-cong proj₁
|
||||
|
||||
|
@ -529,9 +535,12 @@ data Expr : Set (a ⊔ℓ b) where
|
|||
_∪_ : Expr → Expr → Expr
|
||||
_∩_ : Expr → Expr → Expr
|
||||
|
||||
open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
|
||||
open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys; insert-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
|
||||
open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
|
||||
|
||||
insert : A → B → Map → Map
|
||||
insert k v (l , uks) = (insert-impl k v l , insert-preserves-Unique uks)
|
||||
|
||||
_⊔_ : Map → Map → Map
|
||||
_⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
|
||||
|
||||
|
@ -878,6 +887,8 @@ isLattice = record
|
|||
; absorb-⊓-⊔ = absorb-⊓-⊔
|
||||
}
|
||||
|
||||
open IsLattice isLattice using (_≼_) public
|
||||
|
||||
lattice : Lattice Map
|
||||
lattice = record
|
||||
{ _≈_ = _≈_
|
||||
|
@ -958,6 +969,10 @@ _updating_via_ (kvs , uks) ks f =
|
|||
, subst Unique (transform-keys-≡ kvs ks f) uks
|
||||
)
|
||||
|
||||
updating-via-keys-≡ : ∀ (m : Map) (ks : List A) (f : A → B) →
|
||||
keys m ≡ keys (m updating ks via f)
|
||||
updating-via-keys-≡ (l , _) = transform-keys-≡ l
|
||||
|
||||
updating-via-∉k-forward : ∀ (m : Map) (ks : List A) (f : A → B) {k : A} →
|
||||
¬ k ∈k m → ¬ k ∈k (m updating ks via f)
|
||||
updating-via-∉k-forward m = transform-∉k-forward
|
||||
|
@ -995,7 +1010,6 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward
|
|||
module _ {l} {L : Set l}
|
||||
{_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
|
||||
(lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
|
||||
open IsLattice isLattice using (_≼_)
|
||||
open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
|
||||
|
||||
module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
|
||||
|
@ -1072,3 +1086,29 @@ module _ {l} {L : Set l}
|
|||
with refl ← Map-functional {m = f' l₂} k,v∈f'l₂ k,v₂∈f'l₂
|
||||
with refl ← Map-functional {m = f l₂} k,v'∈fl₂ k,v₂∈fl₂ =
|
||||
(v₁ ⊔₂ v , (v'≈v'' , k,v₁v₂∈f'l₁f'l₂))
|
||||
|
||||
|
||||
_[_] : Map → List A → List B
|
||||
_[_] m [] = []
|
||||
_[_] m (k ∷ ks)
|
||||
with ∈k-dec k (proj₁ m)
|
||||
... | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ])
|
||||
... | no _ = m [ ks ]
|
||||
|
||||
m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (m₁ m₂ : Map) {k : A} {v₁ v₂ : B} →
|
||||
m₁ ≼ m₂ → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → v₁ ≼₂ v₂
|
||||
m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
|
||||
with k,v₁v₂∈m₁m₂ ← ⊔-combines {m₁ = m₁} {m₂ = m₂} k,v₁∈m₁ k,v₂∈m₂
|
||||
with (v' , (v₁v₂≈v' , k,v'∈m₂)) ← (proj₁ m₁≼m₂) _ _ k,v₁v₂∈m₁m₂
|
||||
with refl ← Map-functional {m = m₂} k,v₂∈m₂ k,v'∈m₂
|
||||
= v₁v₂≈v'
|
||||
|
||||
m₁≼m₂⇒k∈km₁⇒k∈km₂ : ∀ (m₁ m₂ : Map) {k : A} →
|
||||
m₁ ≼ m₂ → k ∈k m₁ → k ∈k m₂
|
||||
m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
|
||||
let
|
||||
k∈km₁m₂ = union-preserves-∈k₁ {l₁ = proj₁ m₁} {l₂ = proj₁ m₂} k∈km₁
|
||||
(v , k,v∈m₁m₂) = locate {m = m₁ ⊔ m₂} k∈km₁m₂
|
||||
(v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
|
||||
in
|
||||
forget k,v'∈m₂
|
||||
|
|
|
@ -5,15 +5,25 @@ open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
|
|||
|
||||
module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
|
||||
|
||||
open import Lattice.Unit using (⊤) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
|
||||
open import Data.List using (List; map)
|
||||
open import Data.Product using (proj₁)
|
||||
open import Function using (_∘_)
|
||||
|
||||
open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
|
||||
import Lattice.Map
|
||||
|
||||
private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
|
||||
open UnitMap using (Map)
|
||||
open UnitMap using
|
||||
( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
|
||||
( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
|
||||
; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
|
||||
) public
|
||||
|
||||
MapSet : Set a
|
||||
MapSet = Map
|
||||
|
||||
to-List : MapSet → List A
|
||||
to-List = map proj₁ ∘ proj₁
|
||||
|
||||
insert : A → MapSet → MapSet
|
||||
insert k = UnitMap.insert k tt
|
||||
|
|
10
Main.agda
10
Main.agda
|
@ -22,7 +22,7 @@ xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (
|
|||
open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
|
||||
open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_ as AB using () renaming (≈-dec to ≈ᵘ-dec)
|
||||
open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
|
||||
open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
|
||||
open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ using () renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
|
||||
|
||||
fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
|
||||
|
||||
|
@ -33,7 +33,7 @@ showAboveBelow AB.⊤ = "⊤"
|
|||
showAboveBelow AB.⊥ = "⊥"
|
||||
showAboveBelow (AB.[_] tt) = "()"
|
||||
|
||||
showMap : ∀ {ks : List String} → FiniteHeightMap ks → String
|
||||
showMap : FiniteHeightMap → String
|
||||
showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
|
||||
|
||||
fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
|
||||
|
@ -44,16 +44,16 @@ open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}
|
|||
smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
|
||||
largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
|
||||
|
||||
dumb : FiniteHeightMap xyzw
|
||||
dumb : FiniteHeightMap
|
||||
dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
|
||||
|
||||
dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw
|
||||
dumbFunction : FiniteHeightMap → FiniteHeightMap
|
||||
dumbFunction = _⊔_ dumb
|
||||
|
||||
dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
|
||||
dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂
|
||||
|
||||
|
||||
open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
|
||||
open import Fixedpoint {0ℓ} {FiniteHeightMap} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
|
||||
|
||||
main = run {0ℓ} (putStrLn (showMap aᶠ))
|
||||
|
|
15
Utils.agda
15
Utils.agda
|
@ -2,10 +2,11 @@ module Utils where
|
|||
|
||||
open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
|
||||
open import Data.Nat using (ℕ; suc)
|
||||
open import Data.List using (List; []; _∷_; _++_)
|
||||
open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ)
|
||||
open import Data.List.Membership.Propositional using (_∈_)
|
||||
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
|
||||
open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
|
||||
open import Function.Definitions using (Injective)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
|
||||
open import Relation.Nullary using (¬_)
|
||||
|
||||
|
@ -29,6 +30,18 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
|
|||
help {[]} _ = x'≢x ∷ []
|
||||
help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
|
||||
|
||||
All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
|
||||
Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
|
||||
All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
|
||||
All-≢-map x f f-Injecitve [] = []
|
||||
All-≢-map x {x' ∷ xs'} f f-Injecitve (x≢x' ∷ x≢xs') = (λ fx≡fx' → x≢x' (f-Injecitve fx≡fx')) ∷ All-≢-map x f f-Injecitve x≢xs'
|
||||
|
||||
Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
|
||||
Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
|
||||
Unique l → Unique (mapˡ f l)
|
||||
Unique-map {l = []} _ _ _ = empty
|
||||
Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
|
||||
|
||||
All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
|
||||
All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
|
||||
All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
|
||||
|
|
Loading…
Reference in New Issue
Block a user