From 94a1c16d72b0888ee450998d1ba25e63f552d398 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 23 Sep 2025 00:27:33 +0000 Subject: [PATCH 1/9] Use the `agda-sets` library --- docs/agda-spec/src/Axiom/Set.agda | 374 --------------- docs/agda-spec/src/Axiom/Set/Factor.agda | 74 --- docs/agda-spec/src/Axiom/Set/List.agda | 65 --- docs/agda-spec/src/Axiom/Set/Map.agda | 386 ---------------- docs/agda-spec/src/Axiom/Set/Map/Dec.agda | 86 ---- docs/agda-spec/src/Axiom/Set/Properties.agda | 428 ------------------ docs/agda-spec/src/Axiom/Set/Rel.agda | 284 ------------ docs/agda-spec/src/Axiom/Set/Sum.agda | 157 ------- docs/agda-spec/src/Axiom/Set/TotalMap.agda | 109 ----- docs/agda-spec/src/Axiom/Set/TotalMapOn.agda | 59 --- docs/agda-spec/src/Data/Integer/Ext.agda | 29 -- docs/agda-spec/src/Data/List/Ext.agda | 51 --- .../src/Data/List/Ext/Properties.agda | 334 -------------- .../List/Relation/Binary/Sublist/Ext.agda | 10 - .../src/Data/List/Relation/Unary/MOf.agda | 57 --- .../Propositional/Properties/WithK.agda | 48 -- .../src/Data/Maybe/Properties/Ext.agda | 13 - .../src/Data/Nat/Properties/Ext.agda | 30 -- docs/agda-spec/src/Data/Product/Ext.agda | 8 - .../src/Data/Product/Properties/Ext.agda | 53 --- .../Data/Relation/Nullary/Decidable/Ext.agda | 15 - docs/agda-spec/src/Interface/HasEmptySet.agda | 11 - .../agda-spec/src/Interface/HasSingleton.agda | 24 - docs/agda-spec/src/Interface/IsSet.agda | 54 --- docs/agda-spec/src/Ledger/Prelude.agda | 10 +- docs/agda-spec/src/Ledger/Prelude/Base.agda | 2 + .../src/Ledger/Prelude/Instances.agda | 8 + docs/agda-spec/src/Ledger/Set.agda | 6 - docs/agda-spec/src/Ledger/Set/HashMap.agda | 14 - docs/agda-spec/src/Ledger/Set/Theory.agda | 143 ------ docs/agda-spec/src/Ledger/Types/Epoch.agda | 2 +- docs/agda-spec/src/formal-consensus.agda-lib | 1 + nix/agda.nix | 18 +- 33 files changed, 33 insertions(+), 2930 deletions(-) delete mode 100644 docs/agda-spec/src/Axiom/Set.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/Factor.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/List.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/Map.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/Map/Dec.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/Properties.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/Rel.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/Sum.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/TotalMap.agda delete mode 100644 docs/agda-spec/src/Axiom/Set/TotalMapOn.agda delete mode 100644 docs/agda-spec/src/Data/Integer/Ext.agda delete mode 100644 docs/agda-spec/src/Data/List/Ext.agda delete mode 100644 docs/agda-spec/src/Data/List/Ext/Properties.agda delete mode 100644 docs/agda-spec/src/Data/List/Relation/Binary/Sublist/Ext.agda delete mode 100644 docs/agda-spec/src/Data/List/Relation/Unary/MOf.agda delete mode 100644 docs/agda-spec/src/Data/List/Relation/Unary/Unique/Propositional/Properties/WithK.agda delete mode 100644 docs/agda-spec/src/Data/Maybe/Properties/Ext.agda delete mode 100644 docs/agda-spec/src/Data/Nat/Properties/Ext.agda delete mode 100644 docs/agda-spec/src/Data/Product/Ext.agda delete mode 100644 docs/agda-spec/src/Data/Product/Properties/Ext.agda delete mode 100644 docs/agda-spec/src/Data/Relation/Nullary/Decidable/Ext.agda delete mode 100644 docs/agda-spec/src/Interface/HasEmptySet.agda delete mode 100644 docs/agda-spec/src/Interface/HasSingleton.agda delete mode 100644 docs/agda-spec/src/Interface/IsSet.agda create mode 100644 docs/agda-spec/src/Ledger/Prelude/Instances.agda delete mode 100644 docs/agda-spec/src/Ledger/Set.agda delete mode 100644 docs/agda-spec/src/Ledger/Set/HashMap.agda delete mode 100644 docs/agda-spec/src/Ledger/Set/Theory.agda diff --git a/docs/agda-spec/src/Axiom/Set.agda b/docs/agda-spec/src/Axiom/Set.agda deleted file mode 100644 index 83486f9b82..0000000000 --- a/docs/agda-spec/src/Axiom/Set.agda +++ /dev/null @@ -1,374 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} - -module Axiom.Set where - -open import Prelude hiding (map) - -import Function.Related.Propositional as R -open import Data.List.Ext.Properties using (∈-dedup; _×-cong_) -open import Data.List.Relation.Unary.Any using (here; there) -open import Data.List.Relation.Unary.Unique.DecPropositional.Properties using (deduplicate-!) -open import Data.List.Relation.Unary.Unique.Propositional using (Unique; []) -open import Data.Product.Algebra using (×-comm) -open import Data.Product.Properties using (∃∃↔∃∃) -open import Data.Product.Properties.Ext using (∃-cong′; ∃-≡) -open import Class.DecEq using (DecEq; _≟_) -open import Relation.Binary using () renaming (Decidable to Dec₂) - -private variable - ℓ : Level - A B C : Type ℓ - P : A → Type - l : List A - -_Preserves₁_⟶_ : {A : Type ℓ} → (A → B) → Pred A 0ℓ → Pred B 0ℓ → Type ℓ -f Preserves₁ P ⟶ Q = ∀ {a} → P a → Q (f a) - -_Preserves₁₂_⟶_⟶_ : {A B : Type ℓ} → (A → B → C) → Pred A ℓ → Pred B ℓ → Pred C ℓ → Type ℓ -f Preserves₁₂ P ⟶ P' ⟶ Q = ∀ {a b} → P a → P' b → Q (f a b) - -record SpecProperty {ℓ} : Type (sucˡ ℓ) where - field specProperty : {A : Type ℓ} → (A → Type) → Type - sp-∘ : specProperty P → (f : B → A) → specProperty (P ∘ f) - sp-¬ : specProperty P → specProperty (¬_ ∘ P) - -Dec-SpecProperty : SpecProperty -Dec-SpecProperty = record - { specProperty = Decidable¹ - ; sp-∘ = λ P? → P? ∘_ - ; sp-¬ = λ P? → ¬? ∘ P? - } - -record Theory {ℓ} : Type (sucˡ ℓ) where - infix 4 _⊆_ _≡ᵉ_ _∈_ _∉_ - infixr 6 _∪_ - - field Set : Type ℓ → Type ℓ - _∈_ : A → Set A → Type - sp : SpecProperty - open SpecProperty sp public - - _⊆_ : Set A → Set A → Type ℓ - X ⊆ Y = ∀ {a} → a ∈ X → a ∈ Y - - -- we might want to either have all properties or - -- decidable properties allowed for specification - field specification : (X : Set A) - → specProperty P → ∃[ Y ] ∀ {a} → (P a × a ∈ X) ⇔ a ∈ Y - unions : (X : Set (Set A)) - → ∃[ Y ] ∀ {a} → (∃[ T ] (T ∈ X × a ∈ T)) ⇔ a ∈ Y - replacement : (f : A → B) (X : Set A) - → ∃[ Y ] ∀ {b} → (∃[ a ] b ≡ f a × a ∈ X) ⇔ b ∈ Y - listing : (l : List A) - → ∃[ X ] ∀ {a} → a ∈ˡ l ⇔ a ∈ X - -- ^ equivalent to pairing + empty set - -- power-set : (X : Set A) → ∃[ Y ] ∀ {T} → T ⊆ X → T ∈ Y - - private variable X X' Y : Set A - - _≡ᵉ_ : Set A → Set A → Type ℓ - X ≡ᵉ Y = X ⊆ Y × Y ⊆ X - - _≡ᵉ'_ : Set A → Set A → Type ℓ - X ≡ᵉ' Y = ∀ a → a ∈ X ⇔ a ∈ Y - - _∉_ : A → Set A → Type - _∉_ = ¬_ ∘₂ _∈_ - - ≡→∈ : {X : Set A}{a a' : A} → a ∈ X → a ≡ a' → a' ∈ X - ≡→∈ a∈X refl = a∈X - - -- The following is useful in case we have `(a , p)` and `(a , q)`, where `p` - -- and `q` are proofs of `a ∈ X`, and we want to prove `(a , p) ≡ (a , q)`. - ∈-irrelevant : Set A → Type ℓ - ∈-irrelevant X = ∀ {a} (p q : a ∈ X) → p ≡ q - - open Equivalence - - _Preservesˢ_ : (Set A → Set B) → (∀ {A} → Set A → Type) → Type ℓ - f Preservesˢ P = f Preserves₁ P ⟶ P - - _Preservesˢ₂_ : (Set A → Set B → Set C) → (∀ {A : Type ℓ} → Set A → Type ℓ) → Type ℓ - f Preservesˢ₂ P = f Preserves₁₂ P ⟶ P ⟶ P - - disjoint : Set A → Set A → Type ℓ - disjoint X Y = ∀ {a} → a ∈ X → a ∈ Y → ⊥ - - finite : Set A → Type ℓ - finite X = ∃[ l ] ∀ {a} → a ∈ X ⇔ a ∈ˡ l - - Show-finite : ⦃ Show A ⦄ → Show (Σ (Set A) finite) - Show.show Show-finite (X , (l , _)) = Show-List .show l - - weakly-finite : Set A → Type ℓ - weakly-finite X = ∃[ l ] ∀ {a} → a ∈ X → a ∈ˡ l - - -- there exists a list without duplicates that has exactly the members of the set - strongly-finite : Set A → Type ℓ - strongly-finite X = ∃[ l ] Unique l × ∀ {a} → a ∈ X ⇔ a ∈ˡ l - - DecEq∧finite⇒strongly-finite : ⦃ _ : DecEq A ⦄ (X : Set A) - → finite X → strongly-finite X - DecEq∧finite⇒strongly-finite ⦃ eq? ⦄ X (l , h) = let _≟_ = eq? ._≟_ in - deduplicate _≟_ l , deduplicate-! _≟_ l , λ {a} → - a ∈ X ∼⟨ h ⟩ - a ∈ˡ l ∼⟨ ∈-dedup ⟩ - a ∈ˡ deduplicate _≟_ l ∎ - where open R.EquationalReasoning - - card : Σ (Set A) strongly-finite → ℕ - card (_ , l , _) = length l - - ⊆-weakly-finite : X ⊆ Y → weakly-finite Y → weakly-finite X - ⊆-weakly-finite X⊆Y (l , hl) = l , hl ∘ X⊆Y - - isMaximal : Set A → Type ℓ - isMaximal {A} X = {a : A} → a ∈ X - - maximal-⊆ : isMaximal Y → X ⊆ Y - maximal-⊆ maxY _ = maxY - - maximal-unique : isMaximal X → isMaximal Y → X ≡ᵉ Y - maximal-unique maxX maxY = maximal-⊆ maxY , maximal-⊆ maxX - - FinSet : Type ℓ → Type ℓ - FinSet A = Σ (Set A) finite - - -- if you can construct a set that contains all elements satisfying - -- P, you can construct a set containing exactly the elements satisfying P - strictify : specProperty P → (∃[ Y ] ∀ {a} → P a → a ∈ Y) → ∃[ Y ] ∀ {a} → P a ⇔ a ∈ Y - strictify sp p with specification (proj₁ p) sp - ... | (Y , p') = Y , (mk⇔ (λ a∈l → to p' (a∈l , proj₂ p a∈l)) (proj₁ ∘ from p')) - - map : (A → B) → Set A → Set B - map = proj₁ ∘₂ replacement - - ∈-map : ∀ {f : A → B} {b} → (∃[ a ] b ≡ f a × a ∈ X) ⇔ b ∈ map f X - ∈-map = proj₂ $ replacement _ _ - - ∈-map′ : ∀ {f : A → B} {a} → a ∈ X → f a ∈ map f X - ∈-map′ {a = a} a∈X = to ∈-map (a , refl , a∈X) - - -- don't know that there's a set containing all members of a type, which this is equivalent to - -- _⁻¹_ : (A → B) → Set B → Set A - -- f ⁻¹ X = {!!} - - filter : {P : A → Type} → specProperty P → Set A → Set A - filter = proj₁ ∘₂ flip specification - - ∈-filter : ∀ {sp-P : specProperty P} {a} → (P a × a ∈ X) ⇔ a ∈ filter sp-P X - ∈-filter = proj₂ $ specification _ _ - - fromList : List A → Set A - fromList = proj₁ ∘ listing - - ∈-fromList : ∀ {a} → a ∈ˡ l ⇔ a ∈ fromList l - ∈-fromList = proj₂ $ listing _ - - ∈-unions : {a : A} {U : Set (Set A)} → (∃[ T ] T ∈ U × a ∈ T) ⇔ a ∈ proj₁ (unions U) - ∈-unions = proj₂ $ unions _ - - ∅ : Set A - ∅ = fromList [] - - ∅-strongly-finite : strongly-finite {A} ∅ - ∅-strongly-finite = [] , [] , R.SK-sym ∈-fromList - - card-∅ : card (∅ {A} , ∅-strongly-finite) ≡ 0 - card-∅ = refl - - singleton : A → Set A - singleton a = fromList [ a ] - - ❴_❵ = singleton - - ∈-singleton : {a b : A} → a ≡ b ⇔ a ∈ singleton b - ∈-singleton {_} {a} {b} = - a ≡ b ∼⟨ mk⇔ (λ where refl → here refl) (λ where (here refl) → refl) ⟩ - a ∈ˡ [ b ] ∼⟨ ∈-fromList ⟩ - a ∈ singleton b ∎ - where open R.EquationalReasoning - - partialToSet : (A → Maybe B) → A → Set B - partialToSet f a = maybe (fromList ∘ [_]) ∅ (f a) - - ∈-partialToSet : ∀ {a : A} {b : B} {f} → f a ≡ just b ⇔ b ∈ partialToSet f a - ∈-partialToSet {a = a} {b} {f} = mk⇔ - (λ h → subst (λ x → b ∈ maybe (fromList ∘ [_]) ∅ x) (sym h) (to ∈-singleton refl)) - (case f a returning (λ y → b ∈ maybe (λ x → fromList [ x ]) ∅ y → y ≡ just b) of - λ where (just x) → λ h → cong just (sym $ from ∈-singleton h) - nothing → λ h → case from ∈-fromList h of λ ()) - - concatMapˢ : (A → Set B) → Set A → Set B - concatMapˢ f a = proj₁ $ unions (map f a) - - ∈-concatMapˢ : {y : B} {f : A → Set B} - → (∃[ x ] x ∈ X × y ∈ f x) ⇔ y ∈ concatMapˢ f X - ∈-concatMapˢ {X = X} {y} {f} = - (∃[ x ] x ∈ X × y ∈ f x) - ∼⟨ ∃-cong′ (λ {x} → ∃-≡ (λ T → x ∈ X × y ∈ T)) ⟩ - (∃[ x ] ∃[ T ] T ≡ f x × x ∈ X × y ∈ T) - ↔⟨ ∃∃↔∃∃ (λ x T → T ≡ f x × x ∈ X × y ∈ T) ⟩ - (∃[ T ] ∃[ x ] T ≡ f x × x ∈ X × y ∈ T) - ∼⟨ ∃-cong′ $ mk⇔ - (λ where (x , p₁ , p₂ , p₃) → (x , p₁ , p₂) , p₃) - (λ where ((x , p₁ , p₂) , p₃) → x , p₁ , p₂ , p₃) ⟩ - (∃[ T ] (∃[ x ] T ≡ f x × x ∈ X) × y ∈ T) - ∼⟨ ∃-cong′ (∈-map ×-cong R.K-refl) ⟩ - (∃[ T ] T ∈ map f X × y ∈ T) - ∼⟨ ∈-unions ⟩ - y ∈ concatMapˢ f X ∎ - where open R.EquationalReasoning - - mapPartial : (A → Maybe B) → Set A → Set B - mapPartial f = concatMapˢ (partialToSet f) - - ∈-mapPartial : {y : B} {f : A → Maybe B} - → (∃[ x ] x ∈ X × f x ≡ just y) ⇔ y ∈ mapPartial f X - ∈-mapPartial {X = X} {y} {f} = - (∃[ x ] x ∈ X × f x ≡ just y) - ∼⟨ ∃-cong′ (R.K-refl ×-cong (∈-partialToSet {f = f})) ⟩ - (∃[ x ] x ∈ X × y ∈ partialToSet f x) - ∼⟨ ∈-concatMapˢ ⟩ - y ∈ mapPartial f X ∎ - where open R.EquationalReasoning - - ⊆-mapPartial : ∀ {f : A → Maybe B} → map just (mapPartial f X) ⊆ map f X - ⊆-mapPartial {f = f} a∈m with from ∈-map a∈m - ... | x , refl , a∈mp with from (∈-mapPartial {f = f}) a∈mp - ... | x' , x'∈X , jx≡fx = to ∈-map (x' , sym jx≡fx , x'∈X) - - binary-unions : ∃[ Y ] ∀ {a} → (a ∈ X ⊎ a ∈ X') ⇔ a ∈ Y - binary-unions {X = X} {X'} with unions (fromList (X ∷ [ X' ])) - ... | (Y , h) = Y , mk⇔ (λ where - (inj₁ a∈X) → to h (X , to ∈-fromList (here refl) , a∈X) - (inj₂ a∈X') → to h (X' , to ∈-fromList (there (here refl)) , a∈X')) - (λ a∈Y → case from h a∈Y of λ (T , H , a∈T) → case from ∈-fromList H of λ where - (here refl) → inj₁ a∈T - (there (here refl)) → inj₂ a∈T) - - _∪_ : Set A → Set A → Set A - X ∪ Y = proj₁ binary-unions - - ∈-∪ : ∀ {a} → (a ∈ X ⊎ a ∈ Y) ⇔ a ∈ X ∪ Y - ∈-∪ = proj₂ binary-unions - - spec-∈ : Type ℓ → Type ℓ - spec-∈ A = {X : Set A} → specProperty (_∈ X) - - -- membership needs to be a specProperty to have intersections - module Intersection (sp-∈ : spec-∈ A) where - - infixr 7 _∩_ - _∩_ : Set A → Set A → Set A - X ∩ Y = filter sp-∈ X - - ∈-∩ : ∀ {a} → (a ∈ X × a ∈ Y) ⇔ a ∈ X ∩ Y - ∈-∩ {X} {Y} {a} = (a ∈ X × a ∈ Y) ↔⟨ ×-comm _ _ ⟩ - (a ∈ Y × a ∈ X) ∼⟨ ∈-filter ⟩ - a ∈ X ∩ Y ∎ - where open R.EquationalReasoning - - disjoint' : Set A → Set A → Type ℓ - disjoint' X Y = X ∩ Y ≡ᵉ ∅ - - _＼_ : Set A → Set A → Set A - X ＼ Y = filter (sp-¬ (sp-∈ {Y})) X - - All : (A → Type) → Set A → Type ℓ - All P X = ∀ {a} → a ∈ X → P a - - Any : (A → Type) → Set A → Type ℓ - Any P X = ∃[ a ] a ∈ X × P a - --- finite set theories -record Theoryᶠ : Type₁ where - field theory : Theory - open Theory theory public - - field finiteness : (X : Set A) → finite X - - DecEq⇒strongly-finite : ⦃ DecEq A ⦄ → (X : Set A) → strongly-finite X - DecEq⇒strongly-finite X = DecEq∧finite⇒strongly-finite X (finiteness X) - - lengthˢ : ⦃ DecEq A ⦄ → Set A → ℕ - lengthˢ X = card (X , DecEq⇒strongly-finite X) - - module _ {A : Type} ⦃ _ : Show A ⦄ where - instance - Show-Set : Show (Set A) - Show-Set .show = λ x → Show-finite .show (x , (finiteness x)) - --- set theories with an infinite set (containing all natural numbers) -record Theoryⁱ : Type₁ where - field theory : Theory - open Theory theory public - - field infinity : ∃[ Y ] ((n : ℕ) → n ∈ Y) - --- theories with decidable properties -record Theoryᵈ : Type₁ where - field th : Theory - open Theory th public - open Equivalence - - field - ∈-sp : ⦃ DecEq A ⦄ → spec-∈ A - _∈?_ : ⦃ DecEq A ⦄ → Decidable² (_∈_ {A = A}) - all? : {P : A → Type} (P? : Decidable¹ P) {X : Set A} → Dec (All P X) - any? : {P : A → Type} (P? : Decidable¹ P) (X : Set A) → Dec (Any P X) - - - module _ {A : Type} {P : A → Type} where - module _ ⦃ _ : P ⁇¹ ⦄ where instance - Dec-Allˢ : All P ⁇¹ - Dec-Allˢ = ⁇¹ λ x → all? dec¹ {x} - - Dec-Anyˢ : Any P ⁇¹ - Dec-Anyˢ = ⁇¹ any? dec¹ - - module _ (P? : Decidable¹ P) where - allᵇ anyᵇ : (X : Set A) → Bool - allᵇ X = ⌊ all? P? {X} ⌋ - anyᵇ X = ⌊ any? P? X ⌋ - - module _ {A : Type} ⦃ _ : DecEq A ⦄ where - - _∈ᵇ_ : A → Set A → Bool - a ∈ᵇ X = ⌊ a ∈? X ⌋ - - instance - Dec-∈ : _∈_ {A = A} ⁇² - Dec-∈ = ⁇² _∈?_ - - _ = _∈_ {A = A} ⁇² ∋ it - _ = _⊆_ {A = A} ⁇² ∋ it - _ = _≡ᵉ_ {A = A} ⁇² ∋ it - - incl-set' : (X : Set A) → A → Maybe (∃[ a ] a ∈ X) - incl-set' X x with x ∈? X - ... | yes p = just (x , p) - ... | no p = nothing - - incl-set : (X : Set A) → Set (∃[ a ] a ∈ X) - incl-set X = mapPartial (incl-set' X) X - - module _ {X : Set A} where - incl-set-proj₁⊆ : map proj₁ (incl-set X) ⊆ X - incl-set-proj₁⊆ x with from ∈-map x - ... | (_ , pf) , refl , _ = pf - - incl-set-proj₁⊇ : X ⊆ map proj₁ (incl-set X) - incl-set-proj₁⊇ {x} x∈X with x ∈? X in eq - ... | no ¬p = contradiction x∈X ¬p - ... | yes p = to ∈-map - ( (x , p) - , refl - , to (∈-mapPartial {f = incl-set' X}) (x , x∈X , helper eq) - ) - where helper : x ∈? X ≡ yes p → incl-set' X x ≡ just (x , p) - helper h with x ∈? X | h - ... | _ | refl = refl - - incl-set-proj₁ : map proj₁ (incl-set X) ≡ᵉ X - incl-set-proj₁ = incl-set-proj₁⊆ , incl-set-proj₁⊇ diff --git a/docs/agda-spec/src/Axiom/Set/Factor.agda b/docs/agda-spec/src/Axiom/Set/Factor.agda deleted file mode 100644 index 77607b271a..0000000000 --- a/docs/agda-spec/src/Axiom/Set/Factor.agda +++ /dev/null @@ -1,74 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} - -open import Prelude -open import Axiom.Set - -module Axiom.Set.Factor (th : Theory {lzero}) where - -open Theory th -open import Axiom.Set.Properties th - -import Function.Related.Propositional as R -open import Data.List.Ext.Properties -open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_) -open import Data.List.Relation.Binary.BagAndSetEquality -open import Data.List.Relation.Binary.Disjoint.Propositional -open import Data.List.Relation.Binary.Permutation.Propositional -open import Data.List.Relation.Unary.Unique.DecPropositional.Properties -open import Data.List.Relation.Unary.Unique.Propositional -open import Data.List.Relation.Unary.Unique.Propositional.Properties.WithK -open import Class.DecEq -open import Relation.Binary - -open Equivalence - -private variable A B : Type - -_ᶠ : (X : Set A) → ⦃ finite X ⦄ → FinSet A -_ᶠ X ⦃ Xᶠ ⦄ = X , Xᶠ - -instance - ∪-preserves-finite' : {X Y : Set A} → ⦃ finite X ⦄ → ⦃ finite Y ⦄ → finite (X ∪ Y) - ∪-preserves-finite' ⦃ Xᶠ ⦄ ⦃ Yᶠ ⦄ = ∪-preserves-finite Xᶠ Yᶠ - -module Factor (_≈_ : B → B → Type) (f : List A → B) (f-cong : ∀ {l l'} → l ∼[ set ] l' → f l ≈ f l') where - - factor : FinSet A → B - factor (_ , l , _) = f l - - factor-cong : factor Preserves (_≡ᵉ_ on proj₁) ⟶ _≈_ - factor-cong {X , Xˡ , hX} {Y , Yˡ , hY} X≡ᵉY = f-cong λ {a} → - a ∈ˡ Xˡ ∼⟨ R.SK-sym hX ⟩ a ∈ X ∼⟨ to ≡ᵉ⇔≡ᵉ' X≡ᵉY _ ⟩ - a ∈ Y ∼⟨ hY ⟩ a ∈ˡ Yˡ ∎ - where open R.EquationalReasoning - - factor-∪ : ∀ {R : B → B → B → Type} {X Y : Set A} ⦃ Xᶠ : finite X ⦄ ⦃ Yᶠ : finite Y ⦄ - → (∀ {l l'} → R (f l) (f l') (f (l ++ l'))) - → R (factor (X ᶠ)) (factor (Y ᶠ)) (factor ((X ∪ Y) ᶠ)) - factor-∪ hR = hR - -module FactorUnique ⦃ _ : DecEq A ⦄ (_≈_ : B → B → Type) (f : (Σ (List A) Unique) → B) - (f-cong : ∀ {l l'} → proj₁ l ↭ proj₁ l' → f l ≈ f l') where - - f-cong' : ∀ {l l'} → (∀ {a} → a ∈ˡ proj₁ l ⇔ a ∈ˡ proj₁ l') → f l ≈ f l' - f-cong' {l} {l'} h = f-cong (∼bag⇒↭ (unique∧set⇒bag (proj₂ l) (proj₂ l') h)) - - deduplicate-Σ : List A → Σ (List A) Unique - deduplicate-Σ l = (deduplicate _≟_ l , deduplicate-! _≟_ _) - - ext : List A → B - ext = f ∘ deduplicate-Σ - - ext-cong : ∀ {l l'} → l ∼[ set ] l' → ext l ≈ ext l' - ext-cong {l} {l'} h = f-cong' λ {a} → - a ∈ˡ deduplicate _≟_ l ∼⟨ R.SK-sym ∈-dedup ⟩ a ∈ˡ l ∼⟨ h ⟩ - a ∈ˡ l' ∼⟨ ∈-dedup ⟩ a ∈ˡ deduplicate _≟_ l' ∎ - where open R.EquationalReasoning - - open Factor _≈_ ext ext-cong public - - factor-∪' : ∀ {R : B → B → B → Type} {X Y : Set A} ⦃ Xᶠ : finite X ⦄ ⦃ Yᶠ : finite Y ⦄ - → disjoint X Y - → (∀ {l l'} → Disjoint l l' → R (ext l) (ext l') (ext (l ++ l'))) - → R (factor (X ᶠ)) (factor (Y ᶠ)) (factor ((X ∪ Y) ᶠ)) - factor-∪' ⦃ _ , Xᶠ ⦄ ⦃ _ , Yᶠ ⦄ disj hR = hR λ where (a∈X , a∈Y) → ⊥-elim $ disj (from Xᶠ a∈X) (from Yᶠ a∈Y) diff --git a/docs/agda-spec/src/Axiom/Set/List.agda b/docs/agda-spec/src/Axiom/Set/List.agda deleted file mode 100644 index b74e788460..0000000000 --- a/docs/agda-spec/src/Axiom/Set/List.agda +++ /dev/null @@ -1,65 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} - -module Axiom.Set.List where - -open import Prelude hiding (find) - -open import Axiom.Set - -open import Data.List using (filter) -import Data.List.Relation.Unary.All as All -import Data.List.Relation.Unary.Any as Any -import Function -import Function.Properties.Inverse as I -import Function.Related.Propositional as R -import Relation.Nullary.Decidable as Dec -open import Data.List.Membership.Propositional using (find; lose) renaming (_∈_ to _∈ˡ_) -open import Data.List.Membership.Propositional.Properties -open import Data.Product -open import Data.Product.Algebra -open import Data.Product.Properties.Ext -open import Class.DecEq -open import Relation.Binary using () renaming (Decidable to Dec₂) -open import Relation.Nullary.Decidable - -List-Model : Theory -List-Model = λ where - .Set → List - ._∈_ → _∈ˡ_ - .sp → Dec-SpecProperty - .specification → λ X P? → filter P? X , mk⇔ - (λ where (Pa , a∈X) → ∈-filter⁺ P? a∈X Pa) - (λ a∈f → Data.Product.swap (∈-filter⁻ P? a∈f)) - .unions → λ X → concat X , mk⇔ - (λ where (T , T∈X , a∈T) → ∈-concat⁺′ a∈T T∈X) - (λ a∈cX → case ∈-concat⁻′ _ a∈cX of λ where (T , a∈T , T∈X) → (T , T∈X , a∈T)) - .replacement → λ f X → Data.List.map f X , λ {b} → - (∃[ a ] b ≡ f a × a ∈ˡ X) ∼⟨ ∃-cong′ (I.↔⇒⇔ (×-comm _ _)) ⟩ - (∃[ a ] a ∈ˡ X × b ≡ f a) ⤖⟨ I.↔⇒⤖ (map-∈↔ f) ⟩ - b ∈ˡ Data.List.map f X ∎ - .listing → λ l → l , mk⇔ id id - where open Theory hiding (filter) - open R.EquationalReasoning - -List-Modelᶠ : Theoryᶠ -List-Modelᶠ = λ where - .theory → List-Model - .finiteness → λ X → X , mk⇔ id id - where open Theoryᶠ - -module Decˡ {A : Type} ⦃ _ : DecEq A ⦄ where - open Theory List-Model - - _∈?_ : Dec₂ (_∈ˡ_ {A = A}) - _∈?_ a = Any.any? (a ≟_) - - DecEq-Set : DecEq (Set A) - DecEq-Set = DecEq-List - -List-Modelᵈ : Theoryᵈ -List-Modelᵈ = record - { th = List-Model - ; ∈-sp = Decˡ._∈? _ - ; _∈?_ = Decˡ._∈?_ - ; all? = λ P? {X} → Dec.map (mk⇔ All.lookup All.tabulate) (All.all? P? X) - ; any? = λ P? X → Dec.map (mk⇔ find (uncurry lose ∘ proj₂)) (Any.any? P? X) } diff --git a/docs/agda-spec/src/Axiom/Set/Map.agda b/docs/agda-spec/src/Axiom/Set/Map.agda deleted file mode 100644 index 3d12497c22..0000000000 --- a/docs/agda-spec/src/Axiom/Set/Map.agda +++ /dev/null @@ -1,386 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} -{-# OPTIONS -v allTactics:100 #-} - -open import Prelude -open import Axiom.Set using (Theory) - -module Axiom.Set.Map (th : Theory {lzero}) where - -open Theory th renaming (map to mapˢ) - -open import Axiom.Set.Rel th hiding (_∣'_; _∣^'_) -open import Axiom.Set.Properties th - -import Data.Sum as ⊎ -open import Data.List.Ext.Properties using (AllPairs⇒≡∨R∨Rᵒᵖ) -open import Data.Product.Ext using (×-dup) -open import Data.Product.Properties using (×-≡,≡→≡; ×-≡,≡←≡) -open import Data.Maybe.Properties using (just-injective) -open import Relation.Unary using (Decidable) -import Relation.Binary.PropositionalEquality as I -import Relation.Binary.Reasoning.Setoid as SetoidReasoning - -open Equivalence - -open import Class.DecEq using (DecEq; _≟_) - -open import Reflection.Tactic using (initTac) -open import Tactic.AnyOf -open import Tactic.Assumption -open import Tactic.Defaults -open import Tactic.ByEq - --- Because of missing macro hygiene, we have to copy&paste this. --- c.f. https://github.com/agda/agda/issues/3819 -private macro - ∈⇒P = anyOfⁿᵗ - (quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ ∷ []) - P⇒∈ = anyOfⁿᵗ - (quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - ∈⇔P = anyOfⁿᵗ - ( quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ - ∷ quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - -private variable - A A' B B' C D : Type - R R' : Rel A B - X Y : Set A - a : A - a' : A' - b : B - b' : B' - -left-unique : Rel A B → Type -left-unique R = ∀ {a b b'} → (a , b) ∈ R → (a , b') ∈ R → b ≡ b' - -record IsLeftUnique (R : Rel A B) : Type where - field isLeftUnique : left-unique R - -instance - ∅-left-unique : IsLeftUnique {A = A} {B = B} ∅ - ∅-left-unique .IsLeftUnique.isLeftUnique h h' = ⊥-elim $ ∉-∅ h - -⊆-left-unique : R ⊆ R' → left-unique R' → left-unique R -⊆-left-unique R⊆R' h = R⊆R' -⟨ h ⟩- R⊆R' -- on isn't dependent enough - -left-unique-mapˢ : {f : A → B} (X : Set A) → left-unique (mapˢ (λ y → (y , f y)) X) -left-unique-mapˢ _ p q with from ∈-map p | from ∈-map q -... | _ , refl , _ | _ , refl , _ = refl - -Map : Type → Type → Type -Map A B = Σ (Rel A B) left-unique - -_≡ᵐ_ : Map A B → Map A B → Type -(x , _) ≡ᵐ (y , _) = x ≡ᵉ y - -private variable m m' : Map A B - -_ˢ : Map A B → Rel A B -_ˢ = proj₁ - -_ᵐ : (R : Rel A B) → ⦃ IsLeftUnique R ⦄ → Map A B -_ᵐ R ⦃ record { isLeftUnique = h } ⦄ = R , h - -infix 4 _≡ᵉᵐ_ - -_≡ᵉᵐ_ : Map A B → Map A B → Type -_≡ᵉᵐ_ = _≡ᵉ_ on _ˢ - -⊆-map : (f : Rel A B → Rel A B) → (∀ {R} → f R ⊆ R) → Map A B → Map A B -⊆-map f H m = f (m ˢ) , ⊆-left-unique H (proj₂ m) - -ˢ-left-unique : IsLeftUnique (m ˢ) -ˢ-left-unique {m = m} = record { isLeftUnique = proj₂ m } - -instance - _ = ˢ-left-unique - -∅ᵐ : Map A B -∅ᵐ = _ᵐ ∅ ⦃ ∅-left-unique ⦄ - -fromListᵐ : ⦃ _ : DecEq A ⦄ → List (A × B) → Map A B -fromListᵐ l = fromList (deduplicate (λ x y → proj₁ x ≟ proj₁ y) l) , - (λ where (inj₁ refl) → refl - (inj₂ (inj₁ x)) → ⊥-elim (x refl) - (inj₂ (inj₂ x)) → ⊥-elim (x refl)) - ∘₂ (∈⇒P -⟨ AllPairs⇒≡∨R∨Rᵒᵖ - $ deduplicate-! (On.decSetoid (Prelude.decSetoid _≟_) proj₁) l ⟩- ∈⇒P) - where open import Data.List.Relation.Unary.Unique.DecSetoid.Properties - open import Relation.Binary.Construct.On as On - -FinMap : Type → Type → Type -FinMap A B = Σ (Rel A B) (λ R → left-unique R × finite R) - -toFinMap : (m : Map A B) → finite (m ˢ) → FinMap A B -toFinMap (m , h) fin = m , h , fin - -toMap : FinMap A B → Map A B -toMap (m , l , _) = m , l - -toRel : FinMap A B → Rel A B -toRel (m , l , _) = m - -module Intersectionᵐ (sp-∈ : spec-∈ (A × B)) where - open Intersection sp-∈ - open Intersectionᵖ sp-∈ - - _∩ᵐ_ : Map A B → Map A B → Map A B - m ∩ᵐ m' = (m ˢ ∩ m' ˢ , ⊆-left-unique ∩-⊆ˡ (proj₂ m)) - -disj-∪ : (m m' : Map A B) → disjoint (dom (m ˢ)) (dom (m' ˢ)) → Map A B -disj-∪ m m' disj = m ˢ ∪ m' ˢ , λ h h' → case ∈⇔P h , ∈⇔P h' of λ where - (inj₁ hm , inj₁ h'm) → proj₂ m hm h'm - (inj₂ hm' , inj₁ h'm) → ⊥-elim $ disj (∈-map⁺'' h'm) (∈-map⁺'' hm') - (inj₁ hm , inj₂ h'm') → ⊥-elim $ disj (∈-map⁺'' hm) (∈-map⁺'' h'm') - (inj₂ hm' , inj₂ h'm') → proj₂ m' hm' h'm' - -filterᵐ : {P : Pred (A × B) 0ℓ} → specProperty P → Map A B → Map A B -filterᵐ sp-P m = filter sp-P (m ˢ) , ⊆-left-unique filter-⊆ (proj₂ m) - -filterᵐ-finite : {P : A × B → Type} → (sp : specProperty P) → Decidable P - → finite (m ˢ) → finite (filterᵐ sp m ˢ) -filterᵐ-finite = filter-finite - -filterKeys : {P : A → Type} → specProperty P → Map A B → Map A B -filterKeys sp-P = filterᵐ (sp-∘ sp-P proj₁) - -singletonᵐ : A → B → Map A B -singletonᵐ a b = ❴ (a , b) ❵ - , (from ∈-singleton -⟨ (λ where refl refl → refl) ⟩- from ∈-singleton) - -❴_❵ᵐ : A × B → Map A B -❴ k , v ❵ᵐ = singletonᵐ k v - -disj-dom : ∀ {m m₁ m₂ : Map A B} - → (m ˢ) ≡ (m₁ ˢ) ⨿ (m₂ ˢ) - → disjoint (dom (m₁ ˢ)) (dom (m₂ ˢ)) -disj-dom {m = m@(_ , uniq)} {m₁} {m₂} (m≡m₁∪m₂ , disj) a∈domm₁ a∈domm₂ - with (a , b₁) , (refl , h₁) ← ∈⇔P a∈domm₁ - with (_ , b₂) , (refl , h₂) ← ∈⇔P a∈domm₂ - = disj (subst _ (uniq (∈mᵢ⇒∈m (inj₁ h₁)) (∈mᵢ⇒∈m (inj₂ h₂))) h₁) h₂ - where - ∈mᵢ⇒∈m : ∀ {a} → a ∈ (m₁ ˢ) ⊎ a ∈ (m₂ ˢ) → a ∈ (m ˢ) - ∈mᵢ⇒∈m = proj₂ m≡m₁∪m₂ ∘ to ∈-∪ - -InjectiveOn : Set A → (A → B) → Type -InjectiveOn X f = ∀ {x y} → x ∈ X → y ∈ X → f x ≡ f y → x ≡ y - -weaken-Injective : ∀ {X : Set A} {f : A → B} → Injective _≡_ _≡_ f → InjectiveOn X f -weaken-Injective p _ _ = p - -mapˡ-uniq : {f : A → A'} - → {@(tactic by-eq) inj : InjectiveOn (dom R) f} - → left-unique R - → left-unique (mapˡ f R) -mapˡ-uniq {inj = inj} uniq = λ h h' → case ∈⇔P h ,′ ∈⇔P h' of λ where - (((_ , b) , refl , Ha) , ((_ , b') , eqb , Hb)) → uniq Ha - $ subst _ ( sym - $ ×-≡,≡→≡ - $ map₁ (inj (to dom∈ (b , Ha)) (to dom∈ (b' , Hb))) - (×-≡,≡←≡ eqb)) - Hb - -mapʳ-uniq : {f : B → B'} → left-unique R → left-unique (mapʳ f R) -mapʳ-uniq uniq = λ h h' → case ∈⇔P h ,′ ∈⇔P h' of λ where - ((_ , refl , Ha) , (_ , refl , Hb)) → cong _ $ uniq Ha Hb - -mapKeys : (f : A → A') → (m : Map A B) - → {@(tactic by-eq) _ : InjectiveOn (dom (m ˢ)) f} - → Map A' B -mapKeys f (R , uniq) {inj} = mapˡ f R , mapˡ-uniq {inj = inj} uniq - -mapValues : (B → B') → Map A B → Map A B' -mapValues f (R , uniq) = mapʳ f R , mapʳ-uniq uniq - -module Unionᵐ (sp-∈ : spec-∈ A) where - infixr 6 _∪ˡ_ - - _∪ˡ'_ : Rel A B → Rel A B → Rel A B - m ∪ˡ' m' = m ∪ filter (sp-∘ (sp-¬ (sp-∈ {dom m})) proj₁) m' - - _∪ˡ_ : Map A B → Map A B → Map A B - m ∪ˡ m' = disj-∪ m (filterᵐ (sp-∘ (sp-¬ sp-∈) proj₁) m') - (∈⇔P -⟨ (λ where x (_ , refl , hy) → proj₁ (∈⇔P hy) (∈⇔P x)) ⟩- ∈⇔P) - - disjoint-∪ˡ-∪ : (H : disjoint (dom R) (dom R')) → R ∪ˡ' R' ≡ᵉ R ∪ R' - disjoint-∪ˡ-∪ disj = from ≡ᵉ⇔≡ᵉ' λ _ → mk⇔ - (∈-∪⁺ ∘′ ⊎.map₂ (proj₂ ∘′ ∈⇔P) ∘′ ∈⇔P) - (∈⇔P ∘′ ⊎.map₂ (to ∈-filter ∘′ (λ h → (flip disj (∈-map⁺'' h)) , h)) ∘ ∈⇔P) - - insert : Map A B → A → B → Map A B - insert m a b = ❴ a , b ❵ᵐ ∪ˡ m - - insertIfJust : ⦃ DecEq A ⦄ → A → Maybe B → Map A B → Map A B - insertIfJust x nothing m = m - insertIfJust x (just y) m = insert m x y - - disjoint-∪ˡ-mapValues : {M M' : Map A B} - (f : B → C) - → (H : disjoint (dom (M ˢ)) (dom (M' ˢ))) - → (mapValues f (M ∪ˡ M')) ˢ ≡ᵉ (mapValues f M ∪ˡ mapValues f M') ˢ - disjoint-∪ˡ-mapValues {M = M} {M'} f disj = begin - proj₁ (mapValues f (M ∪ˡ M')) - ≈⟨ map-≡ᵉ (disjoint-∪ˡ-∪ disj) ⟩ - (mapʳ f ((proj₁ M) ∪ (proj₁ M'))) - ≈⟨ map-∪ _ ⟩ - (mapʳ f (proj₁ M) ∪ mapʳ f (proj₁ M')) - ≈˘⟨ disjoint-∪ˡ-∪ (λ x₁ x₂ → disj (dom-mapʳ⊆ x₁) (dom-mapʳ⊆ x₂)) ⟩ - proj₁ (mapValues f M ∪ˡ mapValues f M') - ∎ - where open SetoidReasoning ≡ᵉ-Setoid - -map⦅×-dup⦆-uniq : ∀ {x : Set A} → left-unique (mapˢ ×-dup x) -map⦅×-dup⦆-uniq x y with ∈-map⁻' x | ∈-map⁻' y -... | fst , refl , _ | .fst , refl , _ = refl - -mapˡ∘map⦅×-dup⦆-uniq : ∀ {S : Set A} {f : A → B} - → {@(tactic by-eq) inj : Injective _≡_ _≡_ f} - → left-unique $ mapˡ f (mapˢ ×-dup S) -mapˡ∘map⦅×-dup⦆-uniq {inj = inj} = mapˡ-uniq {inj = λ _ _ → inj} map⦅×-dup⦆-uniq - -idMap : Set A → Map A A -idMap s = -, map⦅×-dup⦆-uniq {x = s} - -mapFromFun : (A → B) → Set A → Map A B -mapFromFun f s = mapValues f (idMap s) - -mapWithKey-uniq : {f : A → B → B'} - → left-unique R - → left-unique (mapˢ (λ { (x , y) → x , f x y }) R) -mapWithKey-uniq {f = f} uniq p q with from ∈-map p | from ∈-map q -... | (x , y) , refl , xy∈r | (x' , y') , refl , xy'∈r = cong (f x) (uniq xy∈r xy'∈r) - -mapWithKey : (A → B → B') → Map A B → Map A B' -mapWithKey f m@(r , p) = mapˢ (λ { (x , y) → x , f x y}) r , mapWithKey-uniq p - -mapValues-dom : {f : B → C} → dom (m ˢ) ≡ᵉ dom (mapValues f m ˢ) -mapValues-dom {m = _ , _} = mapʳ-dom - -_∣'_ : {P : A → Type} → Map A B → specProperty P → Map A B -m ∣' P? = filterᵐ (sp-∘ P? proj₁) m - -_∣^'_ : {P : B → Type} → Map A B → specProperty P → Map A B -m ∣^' P? = filterᵐ (sp-∘ P? proj₂) m - -constMap : Set A → B → Map A B -constMap X b = mapˢ (_, b) X , λ x x₁ → - trans (proj₂ $ ×-≡,≡←≡ $ proj₁ $ proj₂ (∈⇔P x)) - (sym $ proj₂ $ ×-≡,≡←≡ $ proj₁ $ proj₂ (∈⇔P x₁)) - -mapPartialLiftKey-just-uniq : ∀ {f : A → B → Maybe B'} - → left-unique R - → just (a , b) ∈ mapˢ (mapPartialLiftKey f) R - → just (a , b') ∈ mapˢ (mapPartialLiftKey f) R - → b ≡ b' -mapPartialLiftKey-just-uniq {f = f} prop a∈ a'∈ = - let _ , eq , ax∈r = mapPartialLiftKey-map {f = f} a∈ - _ , eq' , ax'∈r = mapPartialLiftKey-map {f = f} a'∈ - in - just-injective $ trans eq (trans (cong (f _) (prop ax∈r ax'∈r)) (sym eq')) - -mapPartial-uniq : ∀ {r : Rel A B} {f : A → B → Maybe B' } - → left-unique r - → left-unique (mapPartial (mapPartialLiftKey f) r) -mapPartial-uniq {f = f} prop {a} {b} {b'} p q = - let p = ∈-map′ p - q = ∈-map′ q - in mapPartialLiftKey-just-uniq {f = f} prop (⊆-mapPartial p) (⊆-mapPartial q) - -mapMaybeWithKeyᵐ : (A → B → Maybe B') → Map A B → Map A B' -mapMaybeWithKeyᵐ f (rel , prop) = mapMaybeWithKey f rel , mapPartial-uniq {f = f} prop - -mapFromPartialFun : (A → Maybe B) → Set A → Map A B -mapFromPartialFun f s = mapMaybeWithKeyᵐ (λ _ → f) (idMap s) - -module Restrictionᵐ (sp-∈ : spec-∈ A) where - private module R = Restriction sp-∈ - open Unionᵐ sp-∈ - - _∣_ : Map A B → Set A → Map A B - m ∣ X = ⊆-map (R._∣ X) R.res-⊆ m - - _∣_ᶜ : Map A B → Set A → Map A B - m ∣ X ᶜ = ⊆-map (R._∣ X ᶜ) R.ex-⊆ m - - resᵐ-∅ᶜ : {M : Map A B} → (M ∣ ∅ ᶜ) ˢ ≡ᵉ M ˢ - resᵐ-∅ᶜ = R.res-∅ᶜ - - -- map only values in X - mapValueRestricted : (B → B) → Map A B → Set A → Map A B - mapValueRestricted f m X = mapValues f (m ∣ X) ∪ˡ m - - -- map only value at a - mapSingleValue : (B → B) → Map A B → A → Map A B - mapSingleValue f m a = mapValueRestricted f m ❴ a ❵ - - curryᵐ : Map (A × B) C → A → Map B C - curryᵐ m a = R.curryʳ (m ˢ) a , λ h h' → proj₂ m (R.∈-curryʳ h) (R.∈-curryʳ h') - - res-singleton : ∀ {k} → k ∈ dom (m ˢ) → ∃[ v ] m ∣ ❴ k ❵ ≡ᵉᵐ ❴ k , v ❵ᵐ - res-singleton {m = m@(_ , uniq)} k∈domm - with (k , v) , (refl , h) ← ∈⇔P k∈domm - = v - , (λ a∈m∣k → to ∈-singleton $ case ∈⇔P a∈m∣k of λ (mem₁ , mem₂) → - let eq = from ∈-singleton mem₁ - in ×-≡,≡→≡ (eq , (uniq mem₂ (subst _ (sym eq) h)))) - , λ a∈❴k,v❵ → subst (_∈ ((m ∣ ❴ k ❵) ˢ)) - (sym $ from ∈-singleton a∈❴k,v❵) - (∈⇔P (to ∈-singleton refl , h)) - - res-singleton' : ∀ {k v} → (k , v) ∈ m ˢ → m ∣ ❴ k ❵ ≡ᵉᵐ ❴ k , v ❵ᵐ - res-singleton' {m = m} kv∈m - with _ , h ← res-singleton {m = m} (∈⇔P (-, (refl , kv∈m))) - = subst _ (sym $ proj₂ m kv∈m (R.res-⊆ $ proj₂ h $ to ∈-singleton refl)) h - - res-singleton⁺ : {k : A}{v : B} → (k , v) ∈ m ˢ → (k , v) ∈ (m ∣ ❴ k ❵)ˢ - res-singleton⁺ kv∈m = to ∈-filter ((to ∈-singleton refl) , kv∈m) - - res-singleton-inhabited : ∀ {k a} → a ∈ (m ∣ ❴ k ❵) ˢ → k ∈ dom (m ˢ) - res-singleton-inhabited {m = m} {k} {a} a∈ = - to dom∈ ( proj₂ a , subst (λ x → (x , proj₂ a) ∈ (m ˢ)) - (from ∈-singleton (R.res-dom (∈-dom a∈))) - (R.res-⊆ a∈) ) - - res-singleton'' : ∀ {k a} → a ∈ (m ∣ ❴ k ❵)ˢ → ∃[ v ] a ≡ (k , v) - res-singleton'' {m = m}{k}{a} a∈m = - let (v , m|≡) = res-singleton {m = m} (res-singleton-inhabited{m = m} a∈m) in - v , from ∈-singleton (proj₁ m|≡ a∈m) - - -- f(x,-) - infix 30 _⦅_,-⦆ - _⦅_,-⦆ = curryᵐ - - update : A → Maybe B → Map A B → Map A B - update x (just y) m = insert m x y - update x nothing m = m ∣ ❴ x ❵ ᶜ - -module Lookupᵐ (sp-∈ : spec-∈ A) where - open import Relation.Nullary.Decidable - private module R = Restriction sp-∈ - open Unionᵐ sp-∈ - open Restriction sp-∈ - - module _ (m : Map A B) (x : A) where - lookupᵐ : {@(tactic initTac assumption') _ : x ∈ dom (m ˢ)} → B - lookupᵐ {h} = proj₁ (from dom∈ h) - - lookupᵐ? : ⦃ (x ∈ dom (m ˢ)) ⁇ ⦄ → Maybe B - lookupᵐ? ⦃ ⁇ no _ ⦄ = nothing - lookupᵐ? ⦃ ⁇ yes _ ⦄ = just lookupᵐ - - pullbackMap : (m : Map A B) → ⦃ ∀ {x} → (x ∈ dom (m ˢ)) ⁇ ⦄ → (A' → A) → Set A' → Map A' B - pullbackMap m f s = mapMaybeWithKeyᵐ (λ a _ → lookupᵐ? m (f a)) (idMap s) - -module Corestrictionᵐ (sp-∈ : spec-∈ B) where - private module R = Corestriction sp-∈ - - _∣^_ : Map A B → Set B → Map A B - m ∣^ X = ⊆-map (R._∣^ X) R.cores-⊆ m - - _∣^_ᶜ : Map A B → Set B → Map A B - m ∣^ X ᶜ = ⊆-map (R._∣^ X ᶜ) R.coex-⊆ m - - -- f⁻¹(x) - infix 25 _⁻¹_ - _⁻¹_ : Map A B → B → Set A - m ⁻¹ a = dom ((m ∣^ ❴ a ❵) ˢ) diff --git a/docs/agda-spec/src/Axiom/Set/Map/Dec.agda b/docs/agda-spec/src/Axiom/Set/Map/Dec.agda deleted file mode 100644 index 473f3382cb..0000000000 --- a/docs/agda-spec/src/Axiom/Set/Map/Dec.agda +++ /dev/null @@ -1,86 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} -open import Axiom.Set using (Theoryᵈ; Theory) - -module Axiom.Set.Map.Dec (thᵈ : Theoryᵈ) where - -open import Prelude hiding (map; Monoid) - -open import Algebra using (Monoid) -import Data.Sum as Sum -open import Data.These hiding (map) -open import Class.DecEq using (DecEq) - -open Theoryᵈ thᵈ using (_∈?_; th; incl-set'; incl-set; incl-set-proj₁⊇) -open Theory th -open import Axiom.Set.Rel th using (dom; dom∈) -open import Axiom.Set.Map th -open import Data.Product.Properties using (×-≡,≡→≡; ×-≡,≡←≡) - -open import Interface.IsCommutativeMonoid - -open Equivalence - -private variable A B C D : Type - -module Lookupᵐᵈ (sp-∈ : spec-∈ A) where - open Lookupᵐ sp-∈ - - unionThese : ⦃ DecEq A ⦄ → (m : Map A B) (m' : Map A C) (x : A) - → x ∈ dom (m ˢ) ∪ dom (m' ˢ) → These B C - unionThese m m' x dp with x ∈? dom (m ˢ) | x ∈? dom (m' ˢ) - ... | yes mr | yes mr' = these (lookupᵐ m x) (lookupᵐ m' x) - ... | yes mr | no mr' = this (lookupᵐ m x) - ... | no mr | yes mr' = that (lookupᵐ m' x) - ... | no mr | no mr' = Sum.[ flip contradiction mr , flip contradiction mr' ] - (from ∈-∪ dp) - - unionWith : ⦃ DecEq A ⦄ → (These B C → D) → Map A B → Map A C → Map A D - unionWith f m@(r , p) m'@(r' , p') = m'' , helper - where - d = dom r ∪ dom r' - m'' = map (λ (x , p) → x , f (unionThese m m' x p)) (incl-set d) - - helper : left-unique m'' - helper q q' - with _ , refl , t ← from ∈-map q - with _ , refl , t' ← from ∈-map q' - with from (∈-mapPartial {f = incl-set' _}) t - | from (∈-mapPartial {f = incl-set' _}) t' - ... | z , _ | z' , _ - with z ∈? d in eq | z' ∈? d in eq' - helper _ _ | _ , _ , refl | _ , _ , refl | yes _ | yes _ - with refl ← trans (sym eq) eq' = refl - - module _ {V : Type} ⦃ mon : IsCommutativeMonoid' 0ℓ 0ℓ V ⦄ ⦃ _ : DecEq A ⦄ where - infixr 6 _∪⁺_ - open IsCommutativeMonoid' mon - - _∪⁺_ : Map A V → Map A V → Map A V - _∪⁺_ = unionWith (fold id id _◇_) - - aggregate₊ : FinSet (A × V) → Map A V - aggregate₊ (_ , l , _) = foldl (λ m x → m ∪⁺ ❴ x ❵ᵐ) ∅ᵐ l - - module _ {m m' : Map A V} where - ∪dom-lookup : ∃[ a ] a ∈ dom (m ˢ) ∪ dom (m' ˢ) → A × V - ∪dom-lookup (a , a∈) = a , (fold id id _◇_)(unionThese m m' a a∈) - - dom∪⁺⊆∪dom : dom ((m ∪⁺ m') ˢ) ⊆ dom (m ˢ) ∪ dom (m' ˢ) - dom∪⁺⊆∪dom {a} a∈ = subst (_∈ dom (m ˢ) ∪ dom (m' ˢ)) - (Prelude.sym $ proj₁ (×-≡,≡←≡ $ proj₁ (proj₂ ∈-dom∪⁺))) - (proj₂ $ proj₁ ∈-dom∪⁺) - where - ∈-dom∪⁺ : ∃[ c ] (a , proj₁ (from dom∈ a∈)) ≡ ∪dom-lookup c - × c ∈ incl-set (dom (m ˢ) ∪ dom (m' ˢ)) - ∈-dom∪⁺ = from ∈-map $ proj₂ $ from dom∈ a∈ - - ∪dom⊆dom∪⁺ : dom (m ˢ) ∪ dom (m' ˢ) ⊆ dom ((m ∪⁺ m') ˢ) - ∪dom⊆dom∪⁺ {a} a∈ with from ∈-map (incl-set-proj₁⊇ a∈) - ... | c' , a≡c₁' , c'∈ = - to dom∈ (proj₂ (∪dom-lookup c') , to ∈-map (c' , ×-≡,≡→≡ (a≡c₁' , Prelude.refl) , c'∈)) - - dom∪⁺⇔∪dom : ∀ {a} → a ∈ dom ((m ∪⁺ m')ˢ) ⇔ a ∈ dom (m ˢ) ∪ dom (m' ˢ) - dom∪⁺⇔∪dom {a} = mk⇔ dom∪⁺⊆∪dom ∪dom⊆dom∪⁺ - - dom∪⁺≡∪dom : dom ((m ∪⁺ m')ˢ) ≡ᵉ dom (m ˢ) ∪ dom (m' ˢ) - dom∪⁺≡∪dom = to dom∪⁺⇔∪dom , from dom∪⁺⇔∪dom diff --git a/docs/agda-spec/src/Axiom/Set/Properties.agda b/docs/agda-spec/src/Axiom/Set/Properties.agda deleted file mode 100644 index ea68e4b4b3..0000000000 --- a/docs/agda-spec/src/Axiom/Set/Properties.agda +++ /dev/null @@ -1,428 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} - -open import Axiom.Set using (Theory) - -module Axiom.Set.Properties {ℓ} (th : Theory {ℓ}) where - -open import Prelude hiding (isEquivalence; trans; map; map₂) -open Theory th - -import Data.List -import Data.Sum -import Function.Related.Propositional as R -import Relation.Nullary.Decidable -open import Data.List.Ext.Properties using (_×-cong_; _⊎-cong_) -open import Data.List.Membership.DecPropositional using () renaming (_∈?_ to _∈ˡ?_) -open import Data.List.Membership.Propositional.Properties using (∈-filter⁺; ∈-filter⁻; ∈-++⁺ˡ; ∈-++⁺ʳ; ∈-++⁻) -open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭) -open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (↭-length) -open import Data.List.Relation.Binary.Subset.Propositional using () renaming (_⊆_ to _⊆ˡ_) -open import Data.List.Relation.Unary.Any using (here; there) -open import Data.List.Relation.Unary.Unique.Propositional.Properties.WithK using (unique∧set⇒bag) -open import Data.Product using (map₂; swap) -open import Data.Product.Properties.Ext -open import Data.Relation.Nullary.Decidable.Ext using (map′⇔) -open import Relation.Binary hiding (_⇔_) -open import Relation.Binary.Lattice -import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as Bounded∨Semilattice -import Relation.Binary.Lattice.Properties.JoinSemilattice as ∨Semilattice -open import Relation.Binary.Morphism using (IsOrderHomomorphism) - -open Equivalence - -private variable - A B C : Type ℓ - X Y Z : Set A - -module _ {f : A → B} {X} {b} where - ∈-map⁻' : b ∈ map f X → (∃[ a ] b ≡ f a × a ∈ X) - ∈-map⁻' = from ∈-map - - ∈-map⁺' : (∃[ a ] b ≡ f a × a ∈ X) → b ∈ map f X - ∈-map⁺' = to ∈-map - -∈-map⁺'' : ∀ {f : A → B} {X} {a} → a ∈ X → f a ∈ map f X -∈-map⁺'' h = to ∈-map (-, refl , h) - -module _ {X : Set A} {P : A → Type} {sp-P : specProperty P} {a} where - ∈-filter⁻' : a ∈ filter sp-P X → (P a × a ∈ X) - ∈-filter⁻' = from ∈-filter - - ∈-filter⁺' : (P a × a ∈ X) → a ∈ filter sp-P X - ∈-filter⁺' = to ∈-filter - -module _ {X Y : Set A} {a} where - ∈-∪⁻ : a ∈ X ∪ Y → a ∈ X ⊎ a ∈ Y - ∈-∪⁻ = from ∈-∪ - - ∈-∪⁺ : a ∈ X ⊎ a ∈ Y → a ∈ X ∪ Y - ∈-∪⁺ = to ∈-∪ - -module _ {l : List A} {a} where - ∈-fromList⁻ : a ∈ fromList l → a ∈ˡ l - ∈-fromList⁻ = from ∈-fromList - - ∈-fromList⁺ : a ∈ˡ l → a ∈ fromList l - ∈-fromList⁺ = to ∈-fromList - -open import Tactic.AnyOf -open import Tactic.Defaults - --- Because of missing macro hygiene, we have to copy&paste this. --- c.f. https://github.com/agda/agda/issues/3819 -private macro - ∈⇒P = anyOfⁿᵗ - (quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ ∷ []) - P⇒∈ = anyOfⁿᵗ - (quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - ∈⇔P = anyOfⁿᵗ - ( quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ - ∷ quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - -_≡_⨿_ : Set A → Set A → Set A → Type ℓ -X ≡ Y ⨿ Z = X ≡ᵉ Y ∪ Z × disjoint Y Z - --- FIXME: proving this has some weird issues when making a implicit in --- in the definiton of _≡ᵉ'_ -≡ᵉ⇔≡ᵉ' : X ≡ᵉ Y ⇔ X ≡ᵉ' Y -≡ᵉ⇔≡ᵉ' = mk⇔ - (λ where (X⊆Y , Y⊆X) _ → mk⇔ X⊆Y Y⊆X) - (λ a∈X⇔a∈Y → (λ {_} → to (a∈X⇔a∈Y _)) , λ {_} → from (a∈X⇔a∈Y _)) - -cong-⊆⇒cong : {f : Set A → Set B} → f Preserves _⊆_ ⟶ _⊆_ → f Preserves _≡ᵉ_ ⟶ _≡ᵉ_ -cong-⊆⇒cong h X≡ᵉX' = h (proj₁ X≡ᵉX') , h (proj₂ X≡ᵉX') - -cong-⊆⇒cong₂ : {f : Set A → Set B → Set C} - → f Preserves₂ _⊆_ ⟶ _⊆_ ⟶ _⊆_ → f Preserves₂ _≡ᵉ_ ⟶ _≡ᵉ_ ⟶ _≡ᵉ_ -cong-⊆⇒cong₂ h X≡ᵉX' Y≡ᵉY' = h (proj₁ X≡ᵉX') (proj₁ Y≡ᵉY') - , h (proj₂ X≡ᵉX') (proj₂ Y≡ᵉY') - -⊆-Transitive : Transitive (_⊆_ {A}) -⊆-Transitive X⊆Y Y⊆Z = Y⊆Z ∘ X⊆Y - -≡ᵉ-isEquivalence : IsEquivalence (_≡ᵉ_ {A}) -≡ᵉ-isEquivalence = record - { refl = id , id - ; sym = λ where (h , h') → (h' , h) - ; trans = λ eq₁ eq₂ → ⊆-Transitive (proj₁ eq₁) (proj₁ eq₂) - , ⊆-Transitive (proj₂ eq₂) (proj₂ eq₁) - } - -≡ᵉ-Setoid : ∀ {A} → Setoid ℓ ℓ -≡ᵉ-Setoid {A} = record - { Carrier = Set A - ; _≈_ = _≡ᵉ_ - ; isEquivalence = ≡ᵉ-isEquivalence - } - -⊆-isPreorder : IsPreorder (_≡ᵉ_ {A}) _⊆_ -⊆-isPreorder = λ where - .isEquivalence → ≡ᵉ-isEquivalence - .reflexive → proj₁ - .trans → ⊆-Transitive - where open IsPreorder - -⊆-Preorder : {A} → Preorder _ _ _ -⊆-Preorder {A} = record - { Carrier = Set A ; _≈_ = _≡ᵉ_ ; _≲_ = _⊆_ ; isPreorder = ⊆-isPreorder } - -⊆-PartialOrder : IsPartialOrder (_≡ᵉ_ {A}) _⊆_ -⊆-PartialOrder = record - { isPreorder = ⊆-isPreorder - ; antisym = _,_ } - -∈-× : {a : A} {b : B} → (a , b) ∈ X → (a ∈ map proj₁ X × b ∈ map proj₂ X) -∈-× {a = a} {b} x = to ∈-map ((a , b) , refl , x) , to ∈-map ((a , b) , refl , x) - -module _ {f : A → B} {g : B → C} where - map-⊆∘ : map g (map f X) ⊆ map (g ∘ f) X - map-⊆∘ a∘∈ - with b , a≡gb , b∈prfX ← from ∈-map a∘∈ - with a , refl , a∈X ← from ∈-map b∈prfX - = to ∈-map (a , a≡gb , a∈X) - - map-∘⊆ : map (g ∘ f) X ⊆ map g (map f X) - map-∘⊆ a∈∘ with from ∈-map a∈∘ - ... | a₁ , a₁≡gfa , a₁∈X = to ∈-map (f a₁ , a₁≡gfa , to ∈-map (a₁ , refl , a₁∈X)) - - map-∘ : map g (map f X) ≡ᵉ map (g ∘ f) X - map-∘ = map-⊆∘ , map-∘⊆ - - ∈-map⁺-∘ : ∀ {b} → b ∈ map f X → g b ∈ map (g ∘ f) X - ∈-map⁺-∘ = map-⊆∘ ∘ ∈-map⁺'' - -map-⊆ : {X Y : Set A} {f : A → B} → X ⊆ Y → map f X ⊆ map f Y -map-⊆ x⊆y a∈map with from ∈-map a∈map -... | a₁ , a≡fa₁ , a₁∈x = to ∈-map (a₁ , a≡fa₁ , x⊆y a₁∈x) - -map-≡ᵉ : {X Y : Set A} {f : A → B} → X ≡ᵉ Y → map f X ≡ᵉ map f Y -map-≡ᵉ (x⊆y , y⊆x) = map-⊆ x⊆y , map-⊆ y⊆x - -∉-∅ : {a : A} → a ∉ ∅ -∉-∅ h = case ∈⇔P h of λ () - -∅-minimum : Minimum (_⊆_ {A}) ∅ -∅-minimum = λ _ → ⊥-elim ∘ ∉-∅ - -∅-least : X ⊆ ∅ → X ≡ᵉ ∅ -∅-least X⊆∅ = (X⊆∅ , ∅-minimum _) - -∅-weakly-finite : weakly-finite {A = A} ∅ -∅-weakly-finite = [] , ⊥-elim ∘ ∉-∅ - -∅-finite : finite {A = A} ∅ -∅-finite = [] , mk⇔ (⊥-elim ∘ ∉-∅) λ () - -map-∅ : {X : Set A} {f : A → B} → map f ∅ ≡ᵉ ∅ -map-∅ = ∅-least λ x∈map → case ∈-map⁻' x∈map of λ where (_ , _ , h) → ⊥-elim (∉-∅ h) - -map-∪ : {X Y : Set A} → (f : A → B) → map f (X ∪ Y) ≡ᵉ map f X ∪ map f Y -map-∪ {X = X} {Y} f = from ≡ᵉ⇔≡ᵉ' λ b → - b ∈ map f (X ∪ Y) - ∼⟨ R.SK-sym ∈-map ⟩ - (∃[ a ] b ≡ f a × a ∈ X ∪ Y) - ∼⟨ ∃-cong′ (R.K-refl ×-cong R.SK-sym ∈-∪) ⟩ - (∃[ a ] b ≡ f a × (a ∈ X ⊎ a ∈ Y)) - ↔⟨ ∃-cong′ ×-distribˡ-⊎' ⟩ - (∃[ a ] (b ≡ f a × a ∈ X ⊎ b ≡ f a × a ∈ Y)) - ↔⟨ ∃-distrib-⊎' ⟩ - (∃[ a ] b ≡ f a × a ∈ X ⊎ ∃[ a ] b ≡ f a × a ∈ Y) - ∼⟨ ∈-map ⊎-cong ∈-map ⟩ - (b ∈ map f X ⊎ b ∈ map f Y) - ∼⟨ ∈-∪ ⟩ - b ∈ map f X ∪ map f Y ∎ - where open R.EquationalReasoning - -mapPartial-∅ : {f : A → Maybe B} → mapPartial f ∅ ≡ᵉ ∅ -mapPartial-∅ {f = f} = ∅-least λ x∈map → case from (∈-mapPartial {f = f}) x∈map of λ where - (_ , h , _) → ⊥-elim (∉-∅ h) - -card-≡ᵉ : (X Y : Σ (Set A) strongly-finite) → proj₁ X ≡ᵉ proj₁ Y → card X ≡ card Y -card-≡ᵉ (X , lX , lXᵘ , eqX) (Y , lY , lYᵘ , eqY) X≡Y = - ↭-length $ ∼bag⇒↭ $ unique∧set⇒bag lXᵘ lYᵘ λ {a} → - a ∈ˡ lX ∼⟨ R.SK-sym eqX ⟩ - a ∈ X ∼⟨ to ≡ᵉ⇔≡ᵉ' X≡Y a ⟩ - a ∈ Y ∼⟨ eqY ⟩ - a ∈ˡ lY ∎ - where open R.EquationalReasoning - -module _ {P : A → Type} {sp-P : specProperty P} where - - filter-∅ : (∀ a → a ∈ X → ¬ P a) → filter sp-P X ≡ᵉ ∅ - proj₁ (filter-∅ h) {a} h' with from ∈-filter h' - ... | (Pa , a∈) = ⊥-elim (h a a∈ Pa) - proj₂ (filter-∅ h) {a} h' = ⊥-elim (∉-∅ h') - - filter-⊆ : filter sp-P X ⊆ X - filter-⊆ = proj₂ ∘′ ∈⇔P - - filter-pres-⊆ : X ⊆ Y → filter sp-P X ⊆ filter sp-P Y - filter-pres-⊆ xy a∈ = let Pa∈ = from ∈-filter a∈ in - to ∈-filter (map₂ xy Pa∈) - - filter-pres-≡ᵉ : X ≡ᵉ Y → filter sp-P X ≡ᵉ filter sp-P Y - filter-pres-≡ᵉ (X⊆Y , Y⊆X) = filter-pres-⊆ X⊆Y , filter-pres-⊆ Y⊆X - - filter-split-∪ : ∀ {a} → a ∈ filter sp-P (X ∪ Y) → (P a × a ∈ X) ⊎ (P a × a ∈ Y) - filter-split-∪ a∈ = case (proj₁ (from ∈-filter a∈) , from ∈-∪ (proj₂ (from ∈-filter a∈))) of - λ where - (Pa , inj₁ a∈X) → inj₁ (Pa , a∈X) - (Pa , inj₂ a∈Y) → inj₂ (Pa , a∈Y) - - filter-hom-⊆ : filter sp-P (X ∪ Y) ⊆ filter sp-P X ∪ filter sp-P Y - filter-hom-⊆ {a = a} a∈ = to ∈-∪ (case filter-split-∪ a∈ of λ where - (inj₁ v) → inj₁ (to ∈-filter v) - (inj₂ v) → inj₂ (to ∈-filter v)) - - filter-hom-⊇ : filter sp-P X ∪ filter sp-P Y ⊆ filter sp-P (X ∪ Y) - filter-hom-⊇ a∈ = to ∈-filter (case (from ∈-∪ a∈) of λ where - (inj₁ v) → proj₁ (from ∈-filter v) , to ∈-∪ (inj₁ (proj₂ (from ∈-filter v))) - (inj₂ v) → proj₁ (from ∈-filter v) , to ∈-∪ (inj₂ (proj₂ (from ∈-filter v))) ) - - filter-hom-∪ : filter sp-P (X ∪ Y) ≡ᵉ (filter sp-P X) ∪ (filter sp-P Y) - filter-hom-∪ = filter-hom-⊆ , filter-hom-⊇ - -Dec-∈-fromList : ∀ {a : A} → ⦃ DecEq A ⦄ → (l : List A) → Decidable¹ (_∈ fromList l) -Dec-∈-fromList _ _ = Relation.Nullary.Decidable.map ∈-fromList (_∈ˡ?_ _≟_ _ _) - -Dec-∈-singleton : ∀ {a : A} → ⦃ DecEq A ⦄ → Decidable¹ (_∈ ❴ a ❵) -Dec-∈-singleton _ = Relation.Nullary.Decidable.map ∈-singleton (_ ≟ _) - -singleton-finite : ∀ {a : A} → finite ❴ a ❵ -singleton-finite {a = a} = [ a ] , λ {x} → - x ∈ ❴ a ❵ ∼⟨ R.SK-sym ∈-fromList ⟩ - x ∈ˡ [ a ] ∎ - where open R.EquationalReasoning - -filter-finite : ∀ {P : A → Type} - → (sp : specProperty P) → Decidable¹ P → finite X → finite (filter sp X) -filter-finite {X = X} {P} sp P? (l , hl) = Data.List.filter P? l , λ {a} → - a ∈ filter sp X ∼⟨ R.SK-sym ∈-filter ⟩ - (P a × a ∈ X) ∼⟨ R.K-refl ×-cong hl ⟩ - (P a × a ∈ˡ l) ∼⟨ mk⇔ (uncurry $ flip $ ∈-filter⁺ P?) - (swap ∘ ∈-filter⁻ P?) ⟩ - a ∈ˡ Data.List.filter P? l ∎ - where open R.EquationalReasoning - -∪-⊆ˡ : X ⊆ X ∪ Y -∪-⊆ˡ = ∈⇔P ∘′ inj₁ - -∪-⊆ʳ : Y ⊆ X ∪ Y -∪-⊆ʳ = ∈⇔P ∘′ inj₂ - -∪-⊆ : X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z -∪-⊆ X⊆Z Y⊆Z = λ a∈X∪Y → [ X⊆Z , Y⊆Z ]′ (∈⇔P a∈X∪Y) - -⊆→∪ : X ⊆ Y → X ∪ Y ≡ᵉ Y -⊆→∪ X⊆Y = (λ {a} x → case from ∈-∪ x of λ where - (inj₁ v) → X⊆Y v - (inj₂ v) → v) , ∪-⊆ʳ - -∪-Supremum : Supremum (_⊆_ {A}) _∪_ -∪-Supremum _ _ = ∪-⊆ˡ , ∪-⊆ʳ , λ _ → ∪-⊆ - -∪-cong-⊆ : _∪_ {A} Preserves₂ _⊆_ ⟶ _⊆_ ⟶ _⊆_ -∪-cong-⊆ X⊆X' Y⊆Y' = ∈⇔P ∘′ (Data.Sum.map X⊆X' Y⊆Y') ∘′ ∈⇔P - -∪-cong : _∪_ {A} Preserves₂ _≡ᵉ_ ⟶ _≡ᵉ_ ⟶ _≡ᵉ_ -∪-cong = cong-⊆⇒cong₂ ∪-cong-⊆ - -∪-preserves-finite : _∪_ {A} Preservesˢ₂ finite -∪-preserves-finite {a = X} {Y} (l , hX) (l' , hY) = (l ++ l') , λ {a} → - a ∈ X ∪ Y ∼⟨ R.SK-sym ∈-∪ ⟩ - (a ∈ X ⊎ a ∈ Y) ∼⟨ hX ⊎-cong hY ⟩ - (a ∈ˡ l ⊎ a ∈ˡ l') ∼⟨ mk⇔ Data.Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ] (∈-++⁻ _) ⟩ - a ∈ˡ l ++ l' ∎ - where open R.EquationalReasoning - -∪-sym : X ∪ Y ≡ᵉ Y ∪ X -∪-sym = ∪-⊆ ∪-⊆ʳ ∪-⊆ˡ , ∪-⊆ ∪-⊆ʳ ∪-⊆ˡ - -Set-JoinSemilattice : IsJoinSemilattice (_≡ᵉ_ {A}) _⊆_ _∪_ -Set-JoinSemilattice = record - { isPartialOrder = ⊆-PartialOrder ; supremum = ∪-Supremum } - -Set-BoundedJoinSemilattice : IsBoundedJoinSemilattice (_≡ᵉ_ {A}) _⊆_ _∪_ ∅ -Set-BoundedJoinSemilattice = record - { isJoinSemilattice = Set-JoinSemilattice ; minimum = ∅-minimum } - -Set-BddSemilattice : {A : Type ℓ} → BoundedJoinSemilattice _ _ _ -Set-BddSemilattice {A} = record - { Carrier = Set A - ; _≈_ = _≡ᵉ_ {A} - ; _≤_ = _⊆_ - ; _∨_ = _∪_ - ; ⊥ = ∅ - ; isBoundedJoinSemilattice = Set-BoundedJoinSemilattice - } - -module _ {A : Type ℓ} where - open Bounded∨Semilattice (Set-BddSemilattice {A}) - open ∨Semilattice (BoundedJoinSemilattice.joinSemilattice (Set-BddSemilattice {A})) - using (∨-comm; ∨-assoc) - - ∪-identityˡ : (X : Set A) → ∅ ∪ X ≡ᵉ X - ∪-identityˡ = identityˡ - - ∪-identityʳ : (X : Set A) → X ∪ ∅ ≡ᵉ X - ∪-identityʳ = identityʳ - - ∪-comm : (X Y : Set A) → X ∪ Y ≡ᵉ Y ∪ X - ∪-comm = ∨-comm - - ∪-assoc : (X Y Z : Set A) → (X ∪ Y) ∪ Z ≡ᵉ X ∪ (Y ∪ Z) - ∪-assoc = ∨-assoc - -fromList-∪-singleton : {A : Type ℓ} {x : A} {l : List A} → fromList (x ∷ l) ≡ᵉ ❴ x ❵ ∪ fromList l -fromList-∪-singleton .proj₁ h with from ∈-fromList h -... | here refl = ∈-∪⁺ (inj₁ (to ∈-fromList (here refl))) -... | there q = ∈-∪⁺ (inj₂ (to ∈-fromList q)) -fromList-∪-singleton .proj₂ h with ∈-∪⁻ h -... | (inj₁ a∈) = to ∈-fromList (here (from ∈-singleton a∈)) -... | (inj₂ a∈) = to ∈-fromList (there (from ∈-fromList a∈)) - -∪-fromList-++ : (ll lr : List A) → fromList ll ∪ fromList lr ≡ᵉ fromList (ll ++ lr) -∪-fromList-++ [] lr = ∪-identityˡ (fromList lr) -∪-fromList-++ (x ∷ l) lr = - begin - fromList (x ∷ l) ∪ fromList lr ≈⟨ ∪-cong fromList-∪-singleton ≡ᵉ.refl ⟩ - (❴ x ❵ ∪ fromList l) ∪ fromList lr ≈⟨ ∪-assoc ❴ x ❵ (fromList l) (fromList lr) ⟩ - ❴ x ❵ ∪ (fromList l ∪ fromList lr) ≈⟨ ∪-cong ≡ᵉ.refl (∪-fromList-++ l lr) ⟩ - ❴ x ❵ ∪ fromList (l ++ lr) ≈˘⟨ fromList-∪-singleton ⟩ - fromList (x ∷ (l ++ lr)) ∎ - where - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence) - open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid - -disjoint-sym : disjoint X Y → disjoint Y X -disjoint-sym disj = flip disj - -module Intersectionᵖ (sp-∈ : spec-∈ A) where - open Intersection sp-∈ - - disjoint⇒disjoint' : disjoint X Y → disjoint' X Y - disjoint⇒disjoint' h = ∅-least (⊥-elim ∘ uncurry h ∘ from ∈-∩) - - disjoint'⇒disjoint : disjoint' X Y → disjoint X Y - disjoint'⇒disjoint h a∈X a∈Y = ∉-∅ (to (to ≡ᵉ⇔≡ᵉ' h _) (to ∈-∩ (a∈X , a∈Y))) - - ∩-⊆ˡ : X ∩ Y ⊆ X - ∩-⊆ˡ = proj₁ ∘ from ∈-∩ - - ∩-⊆ʳ : X ∩ Y ⊆ Y - ∩-⊆ʳ = proj₂ ∘ from ∈-∩ - - ∩-⊆ : Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y - ∩-⊆ Z⊆X Z⊆Y = λ x∈Z → to ∈-∩ (< Z⊆X , Z⊆Y > x∈Z) - - ∩-Infimum : Infimum _⊆_ _∩_ - ∩-Infimum X Y = ∩-⊆ˡ , ∩-⊆ʳ , λ _ → ∩-⊆ - - ∩-preserves-finite : _∩_ Preservesˢ₂ weakly-finite - ∩-preserves-finite _ = ⊆-weakly-finite ∩-⊆ʳ - - ∩-cong-⊆ : _∩_ Preserves₂ _⊆_ ⟶ _⊆_ ⟶ _⊆_ - ∩-cong-⊆ X⊆X' Y⊆Y' a∈X∩Y = to ∈-∩ (Data.Product.map X⊆X' Y⊆Y' (from ∈-∩ a∈X∩Y)) - - ∩-cong : _∩_ Preserves₂ _≡ᵉ_ ⟶ _≡ᵉ_ ⟶ _≡ᵉ_ - ∩-cong = cong-⊆⇒cong₂ ∩-cong-⊆ - - ∩-OrderHomomorphismʳ : ∀ {X} → IsOrderHomomorphism _≡ᵉ_ _≡ᵉ_ _⊆_ _⊆_ (X ∩_) - ∩-OrderHomomorphismʳ = record { cong = ∩-cong (id , id) ; mono = ∩-cong-⊆ id } - - ∩-OrderHomomorphismˡ : ∀ {X} → IsOrderHomomorphism _≡ᵉ_ _≡ᵉ_ _⊆_ _⊆_ (_∩ X) - ∩-OrderHomomorphismˡ = record - { cong = flip ∩-cong (id , id) ; mono = flip ∩-cong-⊆ id } - - Set-Lattice : IsLattice _≡ᵉ_ _⊆_ _∪_ _∩_ - Set-Lattice = record - { isPartialOrder = ⊆-PartialOrder ; supremum = ∪-Supremum ; infimum = ∩-Infimum } - - ∩-sym⊆ : X ∩ Y ⊆ Y ∩ X - ∩-sym⊆ a∈X∩Y with from ∈-∩ a∈X∩Y - ... | a∈X , a∈Y = to ∈-∩ (a∈Y , a∈X) - - ∩-sym : X ∩ Y ≡ᵉ Y ∩ X - ∩-sym = ∩-sym⊆ , ∩-sym⊆ - --- Additional properties of lists and sets. -module _ {L : List A} where - open Equivalence - - sublist-⇔ : {l : List A} → fromList l ⊆ fromList L ⇔ l ⊆ˡ L - sublist-⇔ {[]} = mk⇔ (λ x ()) (λ _ {_} → ⊥-elim ∘ ∉-∅) - sublist-⇔ {x ∷ xs} = mk⇔ onlyif (λ u → to ∈-fromList ∘ u ∘ from ∈-fromList) - where - onlyif : ({a : A} → a ∈ fromList (x ∷ xs) → a ∈ fromList L) → x ∷ xs ⊆ˡ L - onlyif h (here refl) = from ∈-fromList (h (to ∈-fromList (here refl))) - onlyif h (there x'∈) = from ∈-fromList (h (to ∈-fromList (there x'∈))) - - module _ {ℓ : Level} {P : Pred (List A) ℓ} where - ∃-sublist-⇔ : (∃[ l ] fromList l ⊆ fromList L × P l) ⇔ (∃[ l ] l ⊆ˡ L × P l) - ∃-sublist-⇔ = mk⇔ (λ (l , l⊆L , Pl) → l , to sublist-⇔ l⊆L , Pl) - (λ (l , l⊆L , Pl) → l , from sublist-⇔ l⊆L , Pl) - - ∃?-sublist-⇔ : Dec (∃[ l ] fromList l ⊆ fromList L × P l) ⇔ Dec (∃[ l ] l ⊆ˡ L × P l) - ∃?-sublist-⇔ = map′⇔ ∃-sublist-⇔ - - diff --git a/docs/agda-spec/src/Axiom/Set/Rel.agda b/docs/agda-spec/src/Axiom/Set/Rel.agda deleted file mode 100644 index 3971f9250a..0000000000 --- a/docs/agda-spec/src/Axiom/Set/Rel.agda +++ /dev/null @@ -1,284 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} -{-# OPTIONS -v allTactics:100 #-} - -open import Prelude hiding (map) -open import Axiom.Set using (Theory) - -module Axiom.Set.Rel (th : Theory {lzero}) where - -import Relation.Binary.Reasoning.Setoid as SetoidReasoning -import Function.Related.Propositional as R - -open Theory th -open import Axiom.Set.Properties th - -import Data.Product -open import Data.List.Ext.Properties using (_⊎-cong_) -open import Data.These hiding (map) -open import Data.Maybe.Base using () renaming (map to map?) -open import Data.Product.Properties using (,-injectiveˡ; ×-≡,≡→≡) -open import Data.Product.Properties.Ext using (∃-cong′; ∃-distrib-⊎') -open import Relation.Unary using (Decidable) -open import Relation.Nullary using (yes; no) -open import Relation.Binary using (_Preserves_⟶_) -import Relation.Binary.PropositionalEquality as I - -open Equivalence - -open import Tactic.AnyOf -open import Tactic.Defaults - --- Because of missing macro hygiene, we have to copy&paste this. --- c.f. https://github.com/agda/agda/issues/3819 -private macro - ∈⇒P = anyOfⁿᵗ - (quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ ∷ []) - P⇒∈ = anyOfⁿᵗ - (quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - ∈⇔P = anyOfⁿᵗ - ( quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ - ∷ quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - -Rel : Type → Type → Type -Rel A B = Set (A × B) - -private variable A A' B B' C : Type - R R' : Rel A B - X : Set A - -relatedˡ : Rel A B → Set A -relatedˡ = map proj₁ - -∅ʳ : Rel A B -∅ʳ = ∅ - -dom : Rel A B → Set A -dom = map proj₁ - -range : Rel A B → Set B -range = map proj₂ - -disjoint-dom⇒disjoint : disjoint (dom R) (dom R') → disjoint R R' -disjoint-dom⇒disjoint disj = ∈-map⁺'' -⟨ disj ⟩- ∈-map⁺'' - -_∣'_ : {P : A → Type} → Rel A B → specProperty P → Rel A B -m ∣' P? = filter (sp-∘ P? proj₁) m - -_∣^'_ : {P : B → Type} → Rel A B → specProperty P → Rel A B -m ∣^' P? = filter (sp-∘ P? proj₂) m - -impl⇒res⊆ : ∀ {X : Rel A B} {P P'} (sp-P : specProperty P) (sp-P' : specProperty P') - → (∀ {a} → P a → P' a) → X ∣' sp-P ⊆ X ∣' sp-P' -impl⇒res⊆ sp-P sp-P' P⇒P' a∈X∣'P = ∈⇔P (Data.Product.map₁ P⇒P' (∈⇔P a∈X∣'P)) - -impl⇒cores⊆ : ∀ {X : Rel A B} {P P'} (sp-P : specProperty P) (sp-P' : specProperty P') - → (∀ {b} → P b → P' b) → X ∣^' sp-P ⊆ X ∣^' sp-P' -impl⇒cores⊆ sp-P sp-P' P⇒P' a∈X∣^'P = ∈⇔P (Data.Product.map₁ P⇒P' (∈⇔P a∈X∣^'P)) - -mapˡ : (A → A') → Rel A B → Rel A' B -mapˡ f R = map (Data.Product.map₁ f) R - -mapʳ : (B → B') → Rel A B → Rel A B' -mapʳ f R = map (Data.Product.map₂ f) R - -dom∈ : ∀ {a} → (∃[ b ] (a , b) ∈ R) ⇔ a ∈ dom R -dom∈ {R = R} {a} = - (∃[ b ] (a , b) ∈ R) ∼⟨ R.SK-sym (mk⇔ (λ { ((_ , y) , refl , ay∈R) → y , ay∈R }) - (λ (x , ax∈R) → (a , x) , refl , ax∈R)) ⟩ - (∃[ a₁ ] a ≡ proj₁ a₁ × a₁ ∈ R) ∼⟨ ∈-map ⟩ - - a ∈ dom R ∎ - where open R.EquationalReasoning - -module _ {x : A} {y : B} where - module _ {a : A} where - ∈-dom-singleton-pair : a ≡ x ⇔ a ∈ dom ❴ x , y ❵ - ∈-dom-singleton-pair = mk⇔ (λ a≡x → to dom∈ (y , to ∈-singleton (×-≡,≡→≡ (a≡x , refl)))) - (,-injectiveˡ ∘ from ∈-singleton ∘ proj₂ ∘ from dom∈) - - dom-single→single : a ∈ dom ❴ x , y ❵ → a ∈ ❴ x ❵ - dom-single→single = to ∈-singleton ∘ from ∈-dom-singleton-pair - - single→dom-single : a ∈ ❴ x ❵ → a ∈ dom ❴ x , y ❵ - single→dom-single = to ∈-dom-singleton-pair ∘ from ∈-singleton - - dom-single≡single : dom ❴ x , y ❵ ≡ᵉ ❴ x ❵ - dom-single≡single = dom-single→single , single→dom-single - -∈-dom : {a : A × B} → a ∈ R → proj₁ a ∈ dom R -∈-dom {a = a} a∈ = to ∈-map (a , (refl , a∈)) - -∉-dom∅ : {a : A} → a ∉ dom{A}{B} ∅ -∉-dom∅ {a} a∈dom∅ = ⊥-elim $ ∉-∅ $ proj₂ $ (from dom∈) a∈dom∅ - -dom∅ : dom{A}{B} ∅ ≡ᵉ ∅ -dom∅ = ⊥-elim ∘ ∉-dom∅ , ∅-minimum (dom ∅) - -dom∪ : dom (R ∪ R') ≡ᵉ dom R ∪ dom R' -dom∪ {R = R} {R'} = from ≡ᵉ⇔≡ᵉ' λ a → - a ∈ dom (R ∪ R') ∼⟨ R.SK-sym dom∈ ⟩ - (∃[ b ] (a , b) ∈ R ∪ R') ∼⟨ ∃-cong′ (R.SK-sym ∈-∪) ⟩ - (∃[ b ] ((a , b) ∈ R ⊎ (a , b) ∈ R')) ↔⟨ ∃-distrib-⊎' ⟩ - (∃[ b ] (a , b) ∈ R ⊎ ∃[ b ] (a , b) ∈ R') ∼⟨ dom∈ ⊎-cong dom∈ ⟩ - (a ∈ dom R ⊎ a ∈ dom R') ∼⟨ ∈-∪ ⟩ - a ∈ dom R ∪ dom R' ∎ - where open R.EquationalReasoning - -dom⊆ : dom{A}{B} Preserves _⊆_ ⟶ _⊆_ -dom⊆ R⊆R' a∈ = to dom∈ $ proj₁ (from dom∈ a∈) , R⊆R' (proj₂ (from dom∈ a∈)) - -dom-cong : R ≡ᵉ R' → dom R ≡ᵉ dom R' -dom-cong RR' = (dom⊆ (proj₁ RR')) , (dom⊆ (proj₂ RR')) - -dom-⊆mapʳ : {f : B → B'} → dom R ⊆ dom (mapʳ f R) -dom-⊆mapʳ {f = f} {a} a∈domR with from dom∈ a∈domR -... | b , ab∈R = to dom∈ (f b , to ∈-map ((a , b) , refl , ab∈R)) - -dom-mapʳ⊆ : {f : B → B'} → dom (mapʳ f R) ⊆ dom R -dom-mapʳ⊆ a∈dmR with from dom∈ a∈dmR -... | _ , p∈map with from ∈-map p∈map -... | (_ , b) , refl , ab∈R = to dom∈ (b , ab∈R) - -mapʳ-dom : {f : B → B'} → dom R ≡ᵉ dom (mapʳ f R) -mapʳ-dom = dom-⊆mapʳ , dom-mapʳ⊆ - -dom-∅ : dom R ⊆ ∅ → R ≡ᵉ ∅ -dom-∅ dom⊆∅ = ∅-least (λ {x} x∈R → ⊥-elim $ ∉-∅ $ dom⊆∅ $ to dom∈ (-, x∈R)) - -mapPartialLiftKey : (A → B → Maybe B') → A × B → Maybe (A × B') -mapPartialLiftKey f (k , v) = map? (k ,_) (f k v) - -mapPartialLiftKey-map : ∀ {a : A} {b' : B'} {f : A → B → Maybe B'} {r : Rel A B} - → just (a , b') ∈ map (mapPartialLiftKey f) r - → ∃[ b ] just b' ≡ f a b × (a , b) ∈ r -mapPartialLiftKey-map {f = f} ab∈m - with from ∈-map ab∈m -... | (a' , b') , ≡ , a'b'∈r - with f a' b' in eq -mapPartialLiftKey-map {f = f} ab∈m | (a' , b') , refl , a'b'∈r | just x - = b' , sym eq , a'b'∈r - -mapMaybeWithKey : (A → B → Maybe B') → Rel A B → Rel A B' -mapMaybeWithKey f r = mapPartial (mapPartialLiftKey f) r - -∈-mapMaybeWithKey : ∀ {a : A} {b' : B'} {f : A → B → Maybe B'} {r : Rel A B} - → (a , b') ∈ mapMaybeWithKey f r - → ∃[ b ] (just b' ≡ f a b × (a , b) ∈ r) -∈-mapMaybeWithKey {a = a} {b'} {f} ab'∈ - = mapPartialLiftKey-map {f = f} - $ ⊆-mapPartial - $ to (∈-map {f = just}) ((a , b') , refl , ab'∈) - -module Restriction (sp-∈ : spec-∈ A) where - - _∣_ : Rel A B → Set A → Rel A B - m ∣ X = m ∣' sp-∈ {X} - - _∣_ᶜ : Rel A B → Set A → Rel A B - m ∣ X ᶜ = m ∣' sp-¬ (sp-∈ {X}) - - _⟪$⟫_ : Rel A B → Set A → Set B - m ⟪$⟫ X = range (m ∣ X) - - res-cong : (R ∣_) Preserves _≡ᵉ_ ⟶ _≡ᵉ_ - res-cong (X⊆Y , Y⊆X) = (λ ∈R∣X → ∈⇔P (Data.Product.map₁ X⊆Y (∈⇔P ∈R∣X))) - , (λ ∈R∣Y → ∈⇔P (Data.Product.map₁ Y⊆X (∈⇔P ∈R∣Y))) - - res-dom : dom (R ∣ X) ⊆ X - res-dom a∈dom with ∈⇔P a∈dom - ... | _ , refl , h = proj₁ $ ∈⇔P h - - res-domᵐ : dom (R ∣ X) ⊆ dom R - res-domᵐ a∈dom with ∈⇔P a∈dom - ... | _ , refl , h = ∈-map⁺'' $ proj₂ (∈⇔P h) - - res-comp-cong : (R ∣_ᶜ) Preserves _≡ᵉ_ ⟶ _≡ᵉ_ - res-comp-cong (X⊆Y , Y⊆X) = (λ ∈R∣X → ∈⇔P (Data.Product.map₁ (_∘ Y⊆X) (∈⇔P ∈R∣X))) - , (λ ∈R∣Y → ∈⇔P (Data.Product.map₁ (_∘ X⊆Y) (∈⇔P ∈R∣Y))) - - res-comp-dom : ∀ {a} → a ∈ dom (R ∣ X ᶜ) → a ∉ X - res-comp-dom a∈dom with ∈⇔P a∈dom - ... | _ , refl , h = proj₁ $ ∈⇔P h - - - res-comp-domᵐ : dom (R ∣ X ᶜ) ⊆ dom R - res-comp-domᵐ a∈dom with ∈⇔P a∈dom - ... | _ , refl , h = ∈-map⁺'' (proj₂ (∈⇔P h)) - - res-⊆ : (R ∣ X) ⊆ R - res-⊆ = proj₂ ∘′ ∈⇔P - - ex-⊆ : (R ∣ X ᶜ) ⊆ R - ex-⊆ = proj₂ ∘′ ∈⇔P - - res-∅ : R ∣ ∅ ≡ᵉ ∅ - res-∅ = dom-∅ res-dom - - res-∅ᶜ : R ∣ ∅ ᶜ ≡ᵉ R - res-∅ᶜ = ex-⊆ , λ a∈R → ∈⇔P (∉-∅ , a∈R) - - ∈-resᶜ-dom⁻ : ∀ {a} → a ∈ dom (R ∣ X ᶜ) → a ∉ X × ∃[ b ] (a , b) ∈ R - ∈-resᶜ-dom⁻ a∈ = res-comp-dom a∈ , from dom∈ (dom⊆ ex-⊆ a∈) - - ∈-resᶜ-dom⁺ : ∀ {a} → a ∉ X × ∃[ b ] (a , b) ∈ R → a ∈ dom (R ∣ X ᶜ) - ∈-resᶜ-dom⁺ (a∉X , (b , ab∈R)) = to dom∈ (b , (∈⇔P (a∉X , ab∈R))) - - ∈-resᶜ-dom : ∀ {a} → a ∈ dom (R ∣ X ᶜ) ⇔ (a ∉ X × ∃[ b ] (a , b) ∈ R) - ∈-resᶜ-dom = mk⇔ ∈-resᶜ-dom⁻ ∈-resᶜ-dom⁺ - - res-ex-∪ : Decidable (_∈ X) → (R ∣ X) ∪ (R ∣ X ᶜ) ≡ᵉ R - res-ex-∪ ∈X? = ∪-⊆ res-⊆ ex-⊆ , λ {a} h → case ∈X? (proj₁ a) of λ where - (yes p) → ∈⇔P (inj₁ (∈⇔P (p , h))) - (no ¬p) → ∈⇔P (inj₂ (∈⇔P (¬p , h))) - - res-ex-disjoint : disjoint (dom (R ∣ X)) (dom (R ∣ X ᶜ)) - res-ex-disjoint h h' = res-comp-dom h' (res-dom h) - - res-ex-disj-∪ : Decidable (_∈ X) → R ≡ (R ∣ X) ⨿ (R ∣ X ᶜ) - res-ex-disj-∪ ∈X? = IsEquivalence.sym ≡ᵉ-isEquivalence (res-ex-∪ ∈X?) - , disjoint-dom⇒disjoint res-ex-disjoint - where open import Relation.Binary using (IsEquivalence) - - curryʳ : Rel (A × B) C → A → Rel B C - curryʳ R a = mapˡ proj₂ (R ∣' (sp-∘ (sp-∈ {X = ❴ a ❵}) proj₁)) - - ∈-curryʳ : ∀ {a} {b : B} {c : C} → (b , c) ∈ curryʳ R a → ((a , b) , c) ∈ R - ∈-curryʳ h = case ∈⇔P h of λ where - (((a , b) , c) , refl , h'') → case ∈⇔P h'' of λ where - (p , p') → case from ∈-singleton p of λ where refl → p' - - open Intersection sp-∈ - open Intersectionᵖ sp-∈ - - res-dom-comm⊆∩ : {m : Rel A B} {m' : Rel A C} → dom (m ∣ dom m') ⊆ dom m ∩ dom m' - res-dom-comm⊆∩ x = to ∈-∩ (res-domᵐ x , res-dom x) - - res-dom-comm∩⊆ : {m : Rel A B} {m' : Rel A C} → dom m ∩ dom m' ⊆ dom (m ∣ dom m') - res-dom-comm∩⊆ {m = m} {m' = m'} x with from ∈-∩ x - ... | a∈dm , a∈dm' with from dom∈ a∈dm | from dom∈ a∈dm' - ... | b , ab∈m | c , ac∈m = to dom∈ (b , to ∈-filter (a∈dm' , ab∈m)) - - res-dom-comm' : {m : Rel A B} {m' : Rel A C} → dom (m ∣ dom m') ≡ᵉ dom m ∩ dom m' - res-dom-comm' = res-dom-comm⊆∩ , res-dom-comm∩⊆ - - res-dom-comm : {m : Rel A B} {m' : Rel A C} → dom (m ∣ dom m') ≡ᵉ dom (m' ∣ dom m) - res-dom-comm {m = m} {m'} = begin - dom (m ∣ dom m') ≈⟨ res-dom-comm' ⟩ - dom m ∩ dom m' ≈˘⟨ ∩-sym ⟩ - dom m' ∩ dom m ≈˘⟨ res-dom-comm' ⟩ - dom (m' ∣ dom m) ∎ - where open SetoidReasoning ≡ᵉ-Setoid - -module Corestriction (sp-∈ : spec-∈ B) where - - _∣^_ : Rel A B → Set B → Rel A B - m ∣^ X = m ∣^' sp-∈ {X} - - _∣^_ᶜ : Rel A B → Set B → Rel A B - m ∣^ X ᶜ = m ∣^' sp-¬ (sp-∈ {X}) - - cores-⊆ : (R ∣^ X) ⊆ R - cores-⊆ = proj₂ ∘′ ∈⇔P - - coex-⊆ : (R ∣^ X ᶜ) ⊆ R - coex-⊆ = proj₂ ∘′ ∈⇔P diff --git a/docs/agda-spec/src/Axiom/Set/Sum.agda b/docs/agda-spec/src/Axiom/Set/Sum.agda deleted file mode 100644 index 8e38eabd7e..0000000000 --- a/docs/agda-spec/src/Axiom/Set/Sum.agda +++ /dev/null @@ -1,157 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} - -open import Axiom.Set using (Theory) -open import Algebra using (CommutativeMonoid) - -open import Prelude hiding (ε) - --- FIXME: this presents a much nicer interface if we use IsCommutativeMonoid' instead -module Axiom.Set.Sum (th : Theory {lzero}) ⦃ M : CommutativeMonoid 0ℓ 0ℓ ⦄ where -open Theory th -open import Axiom.Set.Factor th -open import Axiom.Set.Properties th -open import Axiom.Set.Rel th -open import Axiom.Set.Map th - -open import Algebra.Properties.CommutativeSemigroup using (x∙yz≈y∙xz) -import Data.Sum.Properties as ⊎ -open import Data.List.Ext.Properties using (dedup-++-↭) -open import Data.List.Relation.Binary.Permutation.Propositional -open import Data.List.Relation.Unary.Unique.Propositional using (Unique) -open import Relation.Binary using (_Preserves_⟶_; IsEquivalence) -open import Relation.Unary using (Decidable) - -open import Tactic.AnyOf -open import Tactic.Defaults - --- Because of missing macro hygiene, we have to copy&paste this. --- c.f. https://github.com/agda/agda/issues/3819 -private macro - ∈⇒P = anyOfⁿᵗ - (quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ ∷ []) - P⇒∈ = anyOfⁿᵗ - (quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - ∈⇔P = anyOfⁿᵗ - ( quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ - ∷ quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ []) - -private variable - A B : Type - X Y : Set A - -open CommutativeMonoid M renaming (trans to ≈-trans) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning -open SetoidReasoning (CommutativeMonoid.setoid M) -open import Data.List.Properties using (foldr-++) - -private variable f : A → Carrier - -indexedSumL : (A → Carrier) → List A → Carrier -indexedSumL f = foldr (λ x → f x ∙_) ε - -syntax indexedSumL (λ a → x) m = ∑ˡ[ a ← m ] x - -indexedSumL' : (A → Carrier) → Σ (List A) Unique → Carrier -indexedSumL' f = indexedSumL f ∘ proj₁ - -fold-cong↭ : ∀ {l l' : List A} - → l ↭ l' - → foldr (λ x → f x ∙_) ε l ≈ foldr (λ x → f x ∙_) ε l' -fold-cong↭ refl = begin _ ∎ -fold-cong↭ (prep _ h) = ∙-congˡ (fold-cong↭ h) -fold-cong↭ {f = f} (swap {xs} {ys} x y h) = begin - f x ∙ (f y ∙ indexedSumL f xs) ≈⟨ x∙yz≈y∙xz commutativeSemigroup _ _ _ ⟩ - f y ∙ (f x ∙ indexedSumL f xs) ≈⟨ ∙-congˡ (∙-congˡ (fold-cong↭ h)) ⟩ - f y ∙ (f x ∙ indexedSumL f ys) ∎ -fold-cong↭ (trans h h₁) = ≈-trans (fold-cong↭ h) (fold-cong↭ h₁) - -indexedSum : ⦃ _ : DecEq A ⦄ → (A → Carrier) → FinSet A → Carrier -indexedSum f = let open FactorUnique _≈_ (indexedSumL' f) fold-cong↭ in factor - -indexedSumL-++ : {l l' : List A} - → indexedSumL f (l ++ l') ≈ indexedSumL f l ∙ indexedSumL f l' -indexedSumL-++ {f = f} {l = l} {l'} = begin - indexedSumL f (l ++ l') ≡⟨ foldr-++ (λ x → f x ∙_) ε l l' ⟩ - foldr (λ x → f x ∙_) (indexedSumL f l') l ≈⟨ helper (indexedSumL f l') l f ⟩ - indexedSumL f l ∙ indexedSumL f l' ∎ - where - helper : ∀ m (l : List A) f → foldr (λ x → f x ∙_) m l ≈ indexedSumL f l ∙ m - helper m [] f = begin m ≈˘⟨ identityˡ m ⟩ ε ∙ m ∎ - helper m (x ∷ l) f = begin - f x ∙ foldr (λ y → f y ∙_) m l ≈⟨ ∙-congˡ (helper m l f) ⟩ - f x ∙ (indexedSumL f l ∙ m) ≈˘⟨ assoc _ _ _ ⟩ - f x ∙ indexedSumL f l ∙ m ∎ - - -module _ ⦃ _ : DecEq A ⦄ {f : A → Carrier} where - open FactorUnique _≈_ (indexedSumL' f) fold-cong↭ - - indexedSum-cong : indexedSum f Preserves (_≡ᵉ_ on proj₁) ⟶ _≈_ - indexedSum-cong {x} {y} = factor-cong {x = x} {y} - - indexedSum-∅ : indexedSum f (∅ , ∅-finite) ≈ ε - indexedSum-∅ = begin _ ∎ - - indexedSum-∪ : ⦃ Xᶠ : finite X ⦄ ⦃ Yᶠ : finite Y ⦄ → disjoint X Y - → indexedSum f ((X ∪ Y) ᶠ) ≈ indexedSum f (X ᶠ) ∙ indexedSum f (Y ᶠ) - indexedSum-∪ disj = factor-∪' {λ x y z → z ≈ x ∙ y} disj - λ {l} disj' → ≈-trans (fold-cong↭ (dedup-++-↭ disj')) - (indexedSumL-++ {l = deduplicate _≟_ l}) - - indexedSum-singleton : ∀ {x} → indexedSum f (❴ x ❵ , singleton-finite) ≈ f x - indexedSum-singleton = identityʳ _ - - indexedSum-singleton' : ∀ {x} → (pf : finite ❴ x ❵) - → indexedSum f (❴ x ❵ , pf) ≈ f x - indexedSum-singleton' {x = x} pf = - ≈-trans (indexedSum-cong {x = -, pf} {y = -, singleton-finite} ≡ᵉ.refl) - indexedSum-singleton - where module ≡ᵉ = IsEquivalence ≡ᵉ-isEquivalence - -module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where - - indexedSumᵐ : (A × B → Carrier) → FinMap A B → Carrier - indexedSumᵐ f (m , _ , h) = indexedSum f (m , h) - - indexedSumᵛ : (B → Carrier) → FinMap A B → Carrier - indexedSumᵛ f = indexedSumᵐ (f ∘ proj₂) - - indexedSumᵐ-cong : {f : A × B → Carrier} - → indexedSumᵐ f Preserves (_≡ᵉ_ on proj₁) ⟶ _≈_ - indexedSumᵐ-cong {x = x , _ , h} {y , _ , h'} = indexedSum-cong {x = x , h} {y , h'} - - module IndexedSumUnionᵐ - (sp-∈ : spec-∈ A) (∈-A-dec : {X : Set A} → Decidable¹ (_∈ X)) where - - open Unionᵐ sp-∈ - - ∪ˡ-finite : {R R' : Rel A B} → finite R → finite R' → finite (R ∪ˡ' R') - ∪ˡ-finite Rᶠ R'ᶠ = ∪-preserves-finite Rᶠ - $ filter-finite (sp-∘ (sp-¬ sp-∈) _) (¬? ∘ ∈-A-dec ∘ _) R'ᶠ - - _∪ˡᶠ_ : FinMap A B → FinMap A B → FinMap A B - (_ , hX , Xᶠ) ∪ˡᶠ (_ , hY , Yᶠ) = - toFinMap ((_ , hX) ∪ˡ (_ , hY)) (∪ˡ-finite Xᶠ Yᶠ) - - indexedSumᵐ-∪ : ∀ {X Y : FinMap A B} {f} - → disjoint (dom (toRel X)) (dom (toRel Y)) - → indexedSumᵐ f (X ∪ˡᶠ Y) ≈ indexedSumᵐ f X ∙ indexedSumᵐ f Y - indexedSumᵐ-∪ {X = X'@(X , _ , Xᶠ)} {Y'@(Y , _ , Yᶠ)} {f} disj = begin - indexedSumᵐ f (X' ∪ˡᶠ Y') ≈⟨ indexedSum-cong {x = -, ∪ˡ-finite Xᶠ Yᶠ} {(X ∪ Y) ᶠ} - $ disjoint-∪ˡ-∪ disj ⟩ - indexedSum f ((X ∪ Y) ᶠ) ≈⟨ indexedSum-∪ (disjoint-dom⇒disjoint disj) ⟩ - indexedSumᵐ f X' ∙ indexedSumᵐ f Y' ∎ - where instance _ = Xᶠ - _ = Yᶠ - - indexedSumᵐ-partition : ∀ {m m₁ m₂ : FinMap A B} {f} → toRel m ≡ toRel m₁ ⨿ toRel m₂ - → indexedSumᵐ f m ≈ indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂ - indexedSumᵐ-partition {m} {m₁} {m₂} {f} m≡m₁∪m₂ = begin - indexedSumᵐ f m ≈⟨ indexedSumᵐ-cong {x = m} {m₁ ∪ˡᶠ m₂} helper ⟩ - indexedSumᵐ f (m₁ ∪ˡᶠ m₂) ≈⟨ indexedSumᵐ-∪ {X = m₁} {Y = m₂} disj-dom' ⟩ - indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂ ∎ - where module ≡ᵉ = IsEquivalence ≡ᵉ-isEquivalence - disj-dom' = disj-dom {m = toMap m} {toMap m₁} {toMap m₂} m≡m₁∪m₂ - - helper : toRel m ≡ᵉ toRel (m₁ ∪ˡᶠ m₂) - helper = ≡ᵉ.trans (proj₁ m≡m₁∪m₂) (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj-dom') diff --git a/docs/agda-spec/src/Axiom/Set/TotalMap.agda b/docs/agda-spec/src/Axiom/Set/TotalMap.agda deleted file mode 100644 index e03e65ec72..0000000000 --- a/docs/agda-spec/src/Axiom/Set/TotalMap.agda +++ /dev/null @@ -1,109 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} - -open import Axiom.Set using ( Theory ) - -module Axiom.Set.TotalMap (th : Theory) where - -open import Prelude hiding (lookup; map) - -open import Data.Product.Properties using (Σ-≡,≡→≡) -open import Axiom.Set.Map th using (left-unique; Map ; mapWithKey-uniq ; left-unique-mapˢ) -open import Axiom.Set.Rel th using (Rel ; dom ; dom∈) -open import Class.DecEq using (DecEq ; _≟_) - -open Theory th using (_∈_ ; map ; Set ; ∈-map ; ∈-map′ ; isMaximal) -open Equivalence using (to ; from) - -private variable A B : Type - - --- defines a total map for a given set -total : Rel A B → Type -total R = ∀ {a} → a ∈ dom R - - -record TotalMap (A B : Type) : Type where - field rel : Set (A × B) - left-unique-rel : left-unique rel - total-rel : total rel - - toMap : Map A B - toMap = rel , left-unique-rel - - lookup : A → B - lookup _ = proj₁ (from dom∈ total-rel) - - -- verify that lookup is what we expect - lookup∈rel : {a : A} → (a , lookup a) ∈ rel - lookup∈rel = proj₂ (from dom∈ total-rel) - - -- this is useful for proving equalities involving lookup - ∈-rel⇒lookup-≡ : {a : A}{b : B} → (a , b) ∈ rel → lookup a ≡ b - ∈-rel⇒lookup-≡ ab∈rel = sym (left-unique-rel ab∈rel (proj₂ (from dom∈ total-rel))) - - -module Update {B : Type} ⦃ _ : DecEq A ⦄ where - - private - updateFn : A × B → A → B → B - updateFn (a , b) x y with (x ≟ a) - ... | yes _ = b - ... | no _ = y - - updateFn-id : {a : A}{b b' : B} → b ≡ updateFn (a , b) a b' - updateFn-id {a = a} with (a ≟ a) - ... | yes _ = refl - ... | no ¬p = ⊥-elim (¬p refl) - - - open TotalMap - - mapWithKey : {B' : Type} → (A → B → B') → TotalMap A B → TotalMap A B' - mapWithKey f tm .rel = map (λ{(x , y) → x , f x y}) (rel tm) - mapWithKey _ tm .left-unique-rel = mapWithKey-uniq (left-unique-rel tm) - mapWithKey _ tm .total-rel = ∈-map′ (∈-map′ (proj₂ (from dom∈ (total-rel tm)))) - - update : A → B → TotalMap A B → TotalMap A B - update a b = mapWithKey (updateFn (a , b)) - - - -module LookupUpdate - {X : Set A} - {a : A} {a∈X : a ∈ X} - {b : B} - ⦃ decEqA : DecEq A ⦄ where - - open TotalMap - open Update - - ∈-rel-update : (tm : TotalMap A B) → (a , b) ∈ rel (update a b tm) - ∈-rel-update tm = to ∈-map ((a , lookup tm a) , Σ-≡,≡→≡ (refl , updateFn-id {A = A}) , lookup∈rel tm) - - lookup-update-id : (tm : TotalMap A B) → lookup (update a b tm) a ≡ b - lookup-update-id tm = ∈-rel⇒lookup-≡ (update _ _ tm) (∈-rel-update tm) - - - ------------------------------------------------------- --- Correspondences between total maps and functions -- - -module FunTot (X : Set A) (⋁A≡X : isMaximal X) where - open TotalMap - - Fun⇒Map : ∀ {A B} {f : A → B} (X : Set A) → Map A B - Fun⇒Map {f = f} X = map (λ x → (x , f x)) X , left-unique-mapˢ X - - - Fun⇒TotalMap : (f : A → B) → TotalMap A B - Fun⇒TotalMap f .rel = map (λ x → (x , f x)) X - Fun⇒TotalMap _ .left-unique-rel = left-unique-mapˢ X - Fun⇒TotalMap _ .total-rel = ∈-map′ (∈-map′ ⋁A≡X) - - Fun∈TotalMap : {f : A → B}{a : A} - → a ∈ X → (a , f a) ∈ rel (Fun⇒TotalMap f) - Fun∈TotalMap a∈X = ∈-map′ a∈X - - lookup∘Fun⇒TotalMap-id : {f : A → B}{a : A} - → lookup (Fun⇒TotalMap f) a ≡ f a - lookup∘Fun⇒TotalMap-id {f = f} = ∈-rel⇒lookup-≡ ((Fun⇒TotalMap f)) (Fun∈TotalMap ⋁A≡X) diff --git a/docs/agda-spec/src/Axiom/Set/TotalMapOn.agda b/docs/agda-spec/src/Axiom/Set/TotalMapOn.agda deleted file mode 100644 index e542b0ba82..0000000000 --- a/docs/agda-spec/src/Axiom/Set/TotalMapOn.agda +++ /dev/null @@ -1,59 +0,0 @@ -{-# OPTIONS --safe --no-import-sorts #-} - -open import Axiom.Set using (Theory) - -module Axiom.Set.TotalMapOn (th : Theory) where - -open import Prelude hiding (lookup; map) - -open import Axiom.Set.Map th using (left-unique ; Map ; mapWithKey-uniq) -open import Axiom.Set.Rel th using (Rel ; dom ; dom∈) -open import Class.DecEq using (DecEq ; _≟_) - -open Theory th using ( Set ; _⊆_ ; _∈_ ; map ; ∈-map′ ) -open Equivalence using (from) - -private variable A B : Type - -_TotalOn_ : Rel A B → Set A → Type -R TotalOn X = X ⊆ dom R - - -record TotalMapOn {A : Type}(X : Set A)(B : Type) : Type where - field rel : Set (A × B) - left-unique-rel : left-unique rel - total-rel : rel TotalOn X - - toMap : Map A B - toMap = rel , left-unique-rel - - lookup : Σ A (_∈ X) → B - lookup (_ , a∈X) = proj₁ (from dom∈ (total-rel a∈X)) - - -- verify that lookup is what we expect - lookup∈rel : {a : A} (a∈X : a ∈ X) → (a , lookup (a , a∈X)) ∈ rel - lookup∈rel a∈X = proj₂ (from dom∈ (total-rel a∈X)) - - -- this is useful for proving equalities involving lookup - rel⇒lookup : {a : A} {a∈dom : a ∈ X} {b : B} → (a , b) ∈ rel → lookup (a , a∈dom) ≡ b - rel⇒lookup {a} {a∈dom} ab∈rel = sym (left-unique-rel ab∈rel (proj₂ (from dom∈ (total-rel a∈dom)))) - - -module UpdateOn {B : Type} ⦃ _ : DecEq A ⦄ where - - private - updateFn : A × B → A → B → B - updateFn (a , b) x y with (x ≟ a) - ... | yes _ = b - ... | no _ = y - - open TotalMapOn - - mapWithKeyOn : {X : Set A}{B' : Type} → (A → B → B') → TotalMapOn X B → TotalMapOn X B' - mapWithKeyOn f tm .rel = map (λ{(x , y) → x , f x y}) (rel tm) - mapWithKeyOn _ tm .left-unique-rel = mapWithKey-uniq (left-unique-rel tm) - mapWithKeyOn _ tm .total-rel a∈X = ∈-map′ (∈-map′ (proj₂ (from dom∈ ((total-rel tm) a∈X)))) - - -- Return a new total map which is the same as the given total map except at a. - update : {X : Set A} → A → B → TotalMapOn X B → TotalMapOn X B - update a b = mapWithKeyOn (updateFn (a , b)) diff --git a/docs/agda-spec/src/Data/Integer/Ext.agda b/docs/agda-spec/src/Data/Integer/Ext.agda deleted file mode 100644 index 5604a540eb..0000000000 --- a/docs/agda-spec/src/Data/Integer/Ext.agda +++ /dev/null @@ -1,29 +0,0 @@ -{-# OPTIONS --safe #-} - -module Data.Integer.Ext where - -open import Data.Integer -open import Data.Integer.Properties using ([1+m]⊖[1+n]≡m⊖n) -open import Data.Nat -open import Data.Product -open import Data.Sign -open import Relation.Binary.PropositionalEquality using (_≡_; sym; cong; trans) - -ℤtoSignedℕ : ℤ → Sign × ℕ -ℤtoSignedℕ x = (sign x , ∣ x ∣) - -posPart : ℤ → ℕ -posPart x with ℤtoSignedℕ x -... | (Sign.+ , x) = x -... | _ = 0 - -negPart : ℤ → ℕ -negPart x with ℤtoSignedℕ x -... | (Sign.- , x) = x -... | _ = 0 - -∸≡posPart⊖ : {m n : ℕ} → (m ∸ n) ≡ posPart (m ⊖ n) -∸≡posPart⊖ {zero} {zero} = _≡_.refl -∸≡posPart⊖ {zero} {ℕ.suc n} = _≡_.refl -∸≡posPart⊖ {ℕ.suc m} {zero} = _≡_.refl -∸≡posPart⊖ {ℕ.suc m} {ℕ.suc n} = trans (∸≡posPart⊖{m}{n}) (sym (cong posPart (([1+m]⊖[1+n]≡m⊖n m n)))) diff --git a/docs/agda-spec/src/Data/List/Ext.agda b/docs/agda-spec/src/Data/List/Ext.agda deleted file mode 100644 index 4a48151e44..0000000000 --- a/docs/agda-spec/src/Data/List/Ext.agda +++ /dev/null @@ -1,51 +0,0 @@ -{-# OPTIONS --safe #-} -module Data.List.Ext where - -open import Agda.Primitive using () renaming (Set to Type) - -open import Data.List using (List; _++_; map; concatMap; filter) -open import Data.List.Membership.Propositional using (_∈_) -open import Data.List.Membership.Propositional.Properties using (∈-map⁻; ∈-map⁺; ∈-filter⁻; ∈-filter⁺) -open import Data.Maybe using (Maybe) -open import Data.Nat using (ℕ) -open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂) -open import Function.Bundles using (_⇔_; mk⇔; Equivalence) -open import Level using (Level) -open import Relation.Binary.PropositionalEquality using (_≡_) -open import Relation.Unary using (Decidable) -open Maybe; open List; open ℕ -private variable - ℓ : Level - A B : Type ℓ - --- Looking up an index into the list; fails when out-of-bounds. -_⁉_ : List A → ℕ → Maybe A -[] ⁉ _ = nothing -(x ∷ _) ⁉ zero = just x -(_ ∷ xs) ⁉ suc n = xs ⁉ n - --- sublists of the given list -sublists : List A → List (List A) -sublists [] = [] ∷ [] -sublists (x ∷ xs) = map (x ∷_) (sublists xs) ++ sublists xs - --- insert the given element in every position of the given list -insert : A → List A → List (List A) -insert x [] = (x ∷ []) ∷ [] -insert x (y ∷ ys) = (x ∷ y ∷ ys) ∷ map (y ∷_) (insert x ys) - --- permutations of all sublists of the given list -subpermutations : List A → List (List A) -subpermutations [] = [] ∷ [] -subpermutations (x ∷ xs) = concatMap (insert x) (subpermutations xs) ++ subpermutations xs - -module _ {f : A → B} {l : List A} {b} {P : A → Type} {P? : Decidable P} where - ∈ˡ-map-filter⁻ : b ∈ map f (filter P? l) → (∃[ a ] a ∈ l × b ≡ f a × P a) - ∈ˡ-map-filter⁻ h with ∈-map⁻ f h - ... | a , a∈X , _≡_.refl = a , proj₁ (∈-filter⁻ P? a∈X) , _≡_.refl , proj₂ (∈-filter⁻ P? {xs = l} a∈X) - - ∈ˡ-map-filter⁺ : (∃[ a ] a ∈ l × b ≡ f a × P a) → b ∈ map f (filter P? l) - ∈ˡ-map-filter⁺ (a , a∈l , _≡_.refl , Pa) = ∈-map⁺ f (∈-filter⁺ P? a∈l Pa) - - ∈ˡ-map-filter : (∃[ a ] a ∈ l × b ≡ f a × P a) ⇔ b ∈ map f (filter P? l) - ∈ˡ-map-filter = mk⇔ ∈ˡ-map-filter⁺ ∈ˡ-map-filter⁻ diff --git a/docs/agda-spec/src/Data/List/Ext/Properties.agda b/docs/agda-spec/src/Data/List/Ext/Properties.agda deleted file mode 100644 index 37766254f9..0000000000 --- a/docs/agda-spec/src/Data/List/Ext/Properties.agda +++ /dev/null @@ -1,334 +0,0 @@ -{-# OPTIONS --safe #-} - -module Data.List.Ext.Properties where - -open import Prelude hiding (lookup; map) - -import Data.Product -import Data.Sum -import Function.Related.Propositional as R -open import Data.List using (List; [_]; []; _++_; head; tail; length; map; filter) -open import Data.List.Ext using (insert; subpermutations; sublists) -open import Data.List.Properties using (concat-++; map-++; ++-identityʳ; ++-assoc) -open import Data.List.Membership.Propositional using (_∈_) -open import Data.List.Membership.Propositional.Properties - using (∈-++⁻; ∈-++⁺ˡ; ∈-++⁺ʳ; ∈-deduplicate⁻; ∈-deduplicate⁺; ∈-map⁺) -open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭) -open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint) -open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_) -open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_) -open import Data.List.Relation.Binary.Subset.Propositional.Properties as P - using (xs⊆ys++xs; xs⊆xs++ys; ⊆-reflexive; ⊆-trans) -open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) -open import Data.List.Relation.Unary.All using (all?; All; lookup) renaming (tail to Alltail) -open import Data.List.Relation.Unary.Any using (Any; here; there) -open import Data.List.Relation.Unary.Unique.Propositional using (Unique) -open import Data.List.Relation.Unary.Unique.Propositional.Properties using (drop⁺) -open import Data.List.Relation.Unary.Unique.Propositional.Properties.WithK using (unique∧set⇒bag) -open import Data.Nat.Properties using (_≤?_; ⊔-identityʳ; ≤-reflexive; ≤-trans; m≤n⊔m; m≤m⊔n) -open import Data.Nat using (_⊔_; _≤_) - -open Equivalence - --- TODO: stdlib? -_×-cong_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {k} → A R.∼[ k ] B → C R.∼[ k ] D → (A × C) R.∼[ k ] (B × D) -h ×-cong h' = (h M.×-cong h') - where open import Data.Product.Function.NonDependent.Propositional as M - -_⊎-cong_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {k} → A R.∼[ k ] B → C R.∼[ k ] D → (A ⊎ C) R.∼[ k ] (B ⊎ D) -h ⊎-cong h' = (h M.⊎-cong h') - where open import Data.Sum.Function.Propositional as M - --- TODO: stdlib? -AllPairs⇒≡∨R∨Rᵒᵖ : ∀ {ℓ ℓ'} {A : Set ℓ} {R : A → A → Set ℓ'} {a b l} - → AllPairs R l → a ∈ l → b ∈ l → a ≡ b ⊎ R a b ⊎ R b a -AllPairs⇒≡∨R∨Rᵒᵖ (_ ∷ _) (here refl) (here refl) = inj₁ refl -AllPairs⇒≡∨R∨Rᵒᵖ (x ∷ _) (here refl) (there b∈l) = inj₂ (inj₁ (lookup x b∈l)) -AllPairs⇒≡∨R∨Rᵒᵖ (x ∷ _) (there a∈l) (here refl) = inj₂ (inj₂ (lookup x a∈l)) -AllPairs⇒≡∨R∨Rᵒᵖ (x ∷ h) (there a∈l) (there b∈l) = AllPairs⇒≡∨R∨Rᵒᵖ h a∈l b∈l - --------------------------------------------------------------- -------- duplicate entries in lists and deduplication --------- --------------------------------------------------------------- -module _ {a} {A : Set a} ⦃ _ : DecEq A ⦄ where - open import Data.List.Relation.Unary.Unique.DecPropositional.Properties {A = A} _≟_ - - deduplicate≡ : List A → List A - deduplicate≡ = deduplicate _≟_ - - disj-on-dedup : ∀ {l l'} → Disjoint l l' → Disjoint (deduplicate≡ l) (deduplicate≡ l') - disj-on-dedup = _∘ Data.Product.map (∈-deduplicate⁻ _≟_ _) (∈-deduplicate⁻ _≟_ _) - - ∈-dedup : ∀ {l a} → a ∈ l ⇔ a ∈ deduplicate≡ l - ∈-dedup = mk⇔ (∈-deduplicate⁺ _≟_) (∈-deduplicate⁻ _≟_ _) - - -- TODO: stdlib? - dedup-++-↭ : {l l' : List A} → Disjoint l l' → deduplicate≡ (l ++ l') ↭ deduplicate≡ l ++ deduplicate≡ l' - dedup-++-↭ {l = l} {l'} disj = let dedup-unique = λ {l} → deduplicate-! l in ∼bag⇒↭ $ - unique∧set⇒bag dedup-unique (++⁺ dedup-unique dedup-unique (disj-on-dedup disj)) λ {a} → - a ∈ deduplicate≡ (l ++ l') ∼⟨ R.SK-sym ∈-dedup ⟩ - a ∈ l ++ l' ∼⟨ helper ⟩ - (a ∈ l ⊎ a ∈ l') ∼⟨ ∈-dedup ⊎-cong ∈-dedup ⟩ - (a ∈ deduplicate≡ l ⊎ a ∈ deduplicate≡ l') ∼⟨ R.SK-sym helper ⟩ - a ∈ deduplicate≡ l ++ deduplicate≡ l' ∎ - where open R.EquationalReasoning - helper : ∀ {l l' a} → a ∈ l ++ l' ⇔ (a ∈ l ⊎ a ∈ l') - helper = mk⇔ (∈-++⁻ _) Data.Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ] - ------------------------------------------------------------- --------- maximum length of lists in a list of lists -------- ------------------------------------------------------------- -module _ {a} {A : Set a} where - maxlen : List (List A) → ℕ - maxlen ls = foldr (λ l n → length l ⊔ n) 0 ls - - maxlen≤∷ : ∀ ls l → maxlen ls ≤ maxlen (l ∷ ls) - maxlen≤∷ [] _ = z≤n - maxlen≤∷ (l' ∷ ls) l = subst (maxlen (l' ∷ ls) ≤_) refl (m≤n⊔m (length l) (maxlen (l' ∷ ls))) - - ∈-maxlen-≤ : ∀ {ls} l → l ∈ ls → length l ≤ maxlen ls - ∈-maxlen-≤ {l ∷ ls} .l (here refl) = subst (length l ≤_) refl (m≤m⊔n (length l) (maxlen ls)) - ∈-maxlen-≤ {l' ∷ ls} l (there l∈) = ≤-trans (∈-maxlen-≤ l l∈) (maxlen≤∷ ls l') - -------------------------------- ------- properties of map ------ -------------------------------- -module _ {a} {A : Set a} where - - ¬[]∈map : {ls : List (List A)} {z : A} → ¬ [] ∈ map (z ∷_) ls - ¬[]∈map {_ ∷ _} (there p) = ¬[]∈map p - - map∷decomp∈ : {ls : List (List A)} {xs : List A} {y x : A} → x ∷ xs ∈ map (y ∷_) ls → x ≡ y × xs ∈ ls - map∷decomp∈ {_ ∷ _} (here refl) = refl , (here refl) - map∷decomp∈ {_ ∷ _} (there xxs∈) = (proj₁ (map∷decomp∈ xxs∈)) , there (proj₂ (map∷decomp∈ xxs∈)) - - map∷decomp : {ls : List (List A)} {xs : List A} {y : A} - → xs ∈ map (y ∷_) ls → ∃[ ys ] ys ∈ ls × y ∷ ys ≡ xs - map∷decomp {l ∷ _} {.(_ ∷ l)} (here refl) = l , ((here refl) , refl) - map∷decomp {_ ∷ _} {[]} (there xs∈) = ⊥-elim (¬[]∈map xs∈) - map∷decomp {_ ∷ _} {x ∷ xs} (there xs∈) = - xs , there (proj₂ (map∷decomp∈ xs∈)) , subst (λ u → u ∷ xs ≡ x ∷ xs) (proj₁ (map∷decomp∈ xs∈)) refl - - ∈-map : {ls : List (List A)} {y : A} → ∀ l → l ∈ map (y ∷_) ls → y ∈ l - ∈-map {l ∷ _} .(_ ∷ l) (here refl) = here refl - ∈-map {_ ∷ _} l (there l∈) = ∈-map l l∈ - ------------------------------------------------------- --------- Properties of list-subset inclusion --------- ------------------------------------------------------- -module _ {a} {A : Set a} where - ⊆y∷∧y∉→⊆ys : ∀ {ys xs} {y : A} → xs ⊆ y ∷ ys → ¬ y ∈ xs → xs ⊆ ys - ⊆y∷∧y∉→⊆ys xsyys y∉xs x∈xs with xsyys x∈xs - ... | here refl = ⊥-elim (y∉xs x∈xs) - ... | there p = p - - ¬∈[] : {x : A} → ¬ x ∈ [] - ¬∈[] = λ () - - ¬⊆[] : {xs : List A} {x : A} → ¬ x ∷ xs ⊆ [] - ¬⊆[] p = ¬∈[] (p (here refl)) - - ∈∷∧⊆→∈ : {ys xs : List A} {y x : A} → x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys - ∈∷∧⊆→∈ (here px) _ = here px - ∈∷∧⊆→∈ (there x∈) xs⊆ = there (xs⊆ x∈) - ------------------------------------------- --------- Properties of concatMap --------- ------------------------------------------- -module _ {a} {A : Set a} where - - concatMap⁺ : {ys xs : List A} {f : A → List A} → xs ⊆ ys → concatMap f xs ⊆ concatMap f ys - concatMap⁺ = P.concat⁺ ∘ P.map⁺ _ - - concatMap-++ : ∀ {b} {B : Set b} (f : A → List B) xs ys - → concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys - concatMap-++ f xs ys = begin - concatMap f (xs ++ ys) ≡⟨⟩ - concat (map f (xs ++ ys)) ≡⟨ cong concat $ map-++ f xs ys ⟩ - concat (map f xs ++ map f ys) ≡˘⟨ concat-++ (map f xs) (map f ys) ⟩ - concatMap f xs ++ concatMap f ys ∎ where open ≡-Reasoning - - concatMap-decomp : ∀ {b} {B : Set b} {l : List A} {x : B} {f : A → List B} - → x ∈ concatMap f l ⇔ (∃[ z ] z ∈ l × x ∈ f z) - concatMap-decomp {l = []} = mk⇔ (λ ()) (λ (_ , v , _) → ⊥-elim (¬∈[] v)) - concatMap-decomp {l = y ∷ ys} {x} {f} = mk⇔ i ii - where - i : x ∈ concatMap f (y ∷ ys) → ∃[ z ] z ∈ y ∷ ys × x ∈ f z - i x∈ with ∈-++⁻ _ x∈ - ...| inj₁ v = y , (here refl , v) - ...| inj₂ v with to concatMap-decomp v - ...| z , z∈ys , x∈fz = z , there z∈ys , x∈fz - - ii : ∃[ z ] z ∈ y ∷ ys × x ∈ f z → x ∈ concatMap f (y ∷ ys) - ii (z , here refl , x∈) = xs⊆xs++ys (f z) _ x∈ - ii (z , there z∈ , x∈) = xs⊆ys++xs _ (f y) (from concatMap-decomp (z , (z∈ , x∈))) - ------------------------------------- -------- properties of insert ------- ------------------------------------- -module _ {a} {A : Set a} where - ∷∈insert : {ys : List A} {x : A} → x ∷ ys ∈ insert x ys - ∷∈insert {[]} = here refl - ∷∈insert {_ ∷ _} = here refl - - ∈-insert : ∀ {ys} {x : A} l → l ∈ insert x ys → x ∈ l - ∈-insert {[]} _ (here refl) = here refl - ∈-insert {_ ∷ _} _ (here refl) = here refl - ∈-insert {_ ∷ _} {x} _ (there l∈) with map∷decomp l∈ - ... | (l' , l'∈ , yl'l) = subst (x ∈_) yl'l (there (∈-insert l' l'∈)) - - ∈→∈-insert : ∀ {ys : List A} {y x : A} l → x ∈ ys → l ∈ insert y ys → x ∈ l - ∈→∈-insert {_ ∷ _} _ x∈ (here refl) = there x∈ - ∈→∈-insert {_ ∷ _} l (here refl) (there l∈) = ∈-map l l∈ - ∈→∈-insert {_ ∷ _} {y} {x} l (there x∈) (there l∈) with map∷decomp l∈ - ... | (l' , l'∈ , y'l'l) = subst (x ∈_) y'l'l (there (∈→∈-insert l' x∈ l'∈)) - - insert⊆∷ : ∀ {xs : List A} {x : A} l → l ∈ insert x xs → l ⊆ x ∷ xs - insert⊆∷ {[]} (_ ∷ _) (here refl) y∈ = y∈ - insert⊆∷ {_ ∷ _} (_ ∷ _) (here refl) y∈ = y∈ - insert⊆∷ {_ ∷ _} (_ ∷ _) (there l∈) {y} y∈ with map∷decomp l∈ - ... | (l' , l'∈ , x'l'zzs) = case (subst (y ∈ˡ_) (sym x'l'zzs) y∈) of λ where - (here refl) → there (here refl) - (there q) → case (insert⊆∷ l' l'∈ q) of λ where - (here refl) → here refl - (there x) → there (there x) - - insert-decomp : {ls : List (List A)} {x : A} → ∀ ys → ys ∈ concatMap (insert x) ls - → ∃[ l ] l ∈ ls × ys ⊆ x ∷ l - insert-decomp _ h = case to concatMap-decomp h of λ where - (x , y , z) → x , y , λ {_} → insert⊆∷ _ z - - insert-decomp≡ : ∀ {ys : List A} {y : A} xs → xs ∈ insert y ys - → ∃[ ll ] ∃[ lr ] xs ≡ ll ++ [ y ] ++ lr × ys ≡ ll ++ lr - insert-decomp≡ {[]} _ (here refl) = [] , [] , refl , refl - insert-decomp≡ {y ∷ ys} _ (here refl) = [] , y ∷ ys , refl , refl - insert-decomp≡ {_ ∷ _} [] (there h) = ⊥-elim (¬[]∈map h) - insert-decomp≡ {y' ∷ _} (z ∷ zs) (there h) = - case insert-decomp≡ zs (proj₂ (map∷decomp∈ h)) , proj₁ (map∷decomp∈ h) of λ where - ((ll , lr , zs≡llylr , ys≡lllr) , refl) → - y' ∷ ll , lr , cong (y' ∷_) zs≡llylr , cong (y' ∷_) ys≡lllr - ----------------------------------------------- -------- properties of subpermutations -------- ----------------------------------------------- -module _ {a} {A : Set a} where - []∈subpermutations : (l : List A) → [] ∈ subpermutations l - []∈subpermutations [] = here refl - []∈subpermutations (x ∷ xs) = xs⊆ys++xs _ (concatMap (insert x) (subpermutations xs)) - ([]∈subpermutations xs) - - Unique→dropSubheadUnique : {xs : List A} {x y : A} → Unique (x ∷ y ∷ xs) → Unique (x ∷ xs) - Unique→dropSubheadUnique ((_ All.∷ xxsU) ∷ yxsU) = xxsU ∷ (drop⁺ 1 yxsU) - - Unique→head∉tail : {xs : List A} {x : A} → Unique (x ∷ xs) → ¬ x ∈ xs - Unique→head∉tail ((px All.∷ _) ∷ _) (here refl) = px refl - Unique→head∉tail xxsU (there p) = Unique→head∉tail (Unique→dropSubheadUnique xxsU) p - - ∈-insert-cancelˡ : (ls : List (List A)) {xs : List A} {y : A} - → ¬ y ∈ xs → xs ∈ concatMap (insert y) ls ++ ls → xs ∈ ls - ∈-insert-cancelˡ ls {xs} y∉xs xs∈yls = case (∈-++⁻ _ xs∈yls) of λ where - (inj₁ v) → case (to (concatMap-decomp {l = ls}) v) of λ where - (l' , l'∈ , l∈xl') → ⊥-elim (y∉xs (∈-insert xs l∈xl')) - (inj₂ v) → v - -module _ {a} {A : Set a} where - ∈insert→∷∈insert' : {ys xs : List A} {y x : A} → x ∈ ys → ¬ x ∈ xs - → ∃[ sp ] sp ∈ subpermutations ys × xs ∈ insert y sp - → ∃[ sp' ] sp' ∈ subpermutations ys × x ∷ xs ∈ insert y sp' - - ∈insert→∷∈insert' {x ∷ ys} {xs} {y} {x} (here refl) h₂ (sp , h₃ , h₄) - = case ∈-++⁻ (concatMap (insert x) (subpermutations ys)) h₃ of λ where - (inj₁ v) → case to (concatMap-decomp {l = subpermutations ys}) v of λ where - (x , y , z) → ⊥-elim (h₂ (∈→∈-insert xs (∈-insert sp z) h₄)) - (inj₂ v) → case insert-decomp≡ _ h₄ of λ where - (ll , lr , xs≡ , sp≡) → x ∷ sp , ∈-++⁺ˡ (from concatMap-decomp (sp , v , ∷∈insert)) - , there (∈-map⁺ (x ∷_) h₄) - - ∈insert→∷∈insert' {y' ∷ ys} {xs} {y} {x} (there h₁) h₂ (sp , h₃ , h₄) - = case ∈-++⁻ (concatMap (insert y') (subpermutations ys)) h₃ of λ where - (inj₁ v) → case to concatMap-decomp v of λ where - (l , l∈ , xs∈) → case ∈insert→∷∈insert' h₁ (λ p → h₂ (∈→∈-insert xs p h₄)) (l , l∈ , xs∈) of λ where - f → let v' = x ∷ sp ∈ concatMap (insert y') (subpermutations ys) ∋ from concatMap-decomp f - in to concatMap-decomp (subst (x ∷ xs ∈ˡ_) - (sym (concatMap-++ (insert y) (concatMap (insert y') (subpermutations ys)) _)) - (∈-++⁺ˡ (from concatMap-decomp (x ∷ sp , v' , (there $ ∈-map⁺ (x ∷_) h₄))))) - (inj₂ v) → case ∈insert→∷∈insert' h₁ h₂ (sp , v , h₄) of λ where - (sp' , h'₁ , h'₂) → sp' , ∈-++⁺ʳ _ h'₁ , h'₂ - - - ∈insert→∷∈insert : {ys xs : List A} {y x : A} → x ∈ ys → ¬ x ∈ xs - → xs ∈ concatMap (insert y) (subpermutations ys) - → x ∷ xs ∈ concatMap (insert y) (subpermutations ys) - - ∈insert→∷∈insert h₁ h₂ h₃ = from concatMap-decomp $ ∈insert→∷∈insert' h₁ h₂ $ to concatMap-decomp h₃ - - - ∈-subperm-addhead : {ys xs : List A} {x : A} → x ∈ ys → ¬ x ∈ xs - → xs ∈ subpermutations ys → x ∷ xs ∈ subpermutations ys - - ∈-subperm-addhead {_ ∷ ys} (here refl) y∉xs xs∈sp = - xs⊆xs++ys _ _ (from concatMap-decomp (_ , ∈-insert-cancelˡ (subpermutations ys) y∉xs xs∈sp , ∷∈insert)) - - ∈-subperm-addhead {_ ∷ _} (there x∈ys) x∉xs xs∈sp = case ∈-++⁻ _ xs∈sp of λ where - (inj₁ v) → xs⊆xs++ys _ _ (∈insert→∷∈insert x∈ys x∉xs v) - (inj₂ v) → xs⊆ys++xs _ _ (∈-subperm-addhead x∈ys x∉xs v) - - ----------------------------------------------------------------- ------------- maximal sublists satisfying a predicate ---------- ----------------------------------------------------------------- -module _ {a} {A : Set a} - {p} {P : Pred (List A) p} where - - -- sublists of a given list which satisfy P - sublists⊧P : Decidable¹ P → List A → List (List A) - sublists⊧P P? ys = filter P? (sublists ys) - - -- sublists of a given list which satisfy P and are of maximum length among those satisfying P - maxsublists⊧P : Decidable¹ P → List A → List (List A) - maxsublists⊧P P? ys = filter (λ l → length l ≟ maxlen (sublists⊧P P? ys)) (sublists⊧P P? ys) - --------------------------------------------------------------------------- ------------- l ⊆ ys ⋀ l Unique ⇔ l ∈ subpermutations ys ---------- --------------------------------------------------------------------------- -module _ {a} {A : Set a} where - -- If l ⊆ ys and l has no repeated elements, then l is a subpermutation of ys. - uniqueSubset→subperm : ∀ {ys : List A} l → Unique l → l ⊆ ys → l ∈ subpermutations ys - uniqueSubset→subperm {[]} [] _ _ = here refl - uniqueSubset→subperm {[]} (_ ∷ _) _ l⊆ = ⊥-elim (¬⊆[] l⊆) - uniqueSubset→subperm {_ ∷ ys} [] _ _ = xs⊆ys++xs _ _ ([]∈subpermutations ys) - uniqueSubset→subperm {_ ∷ _} (_ ∷ xs) lU l⊆ = case l⊆ (here refl) of λ where - (here refl) → let - xs⊆ys = ⊆y∷∧y∉→⊆ys (l⊆ ∘ there) (Unique→head∉tail lU) in - xs⊆xs++ys _ _ (from concatMap-decomp (xs , uniqueSubset→subperm xs (drop⁺ 1 lU) xs⊆ys , ∷∈insert)) - (there p) → case ∈-++⁻ _ (uniqueSubset→subperm xs (drop⁺ 1 lU) (l⊆ ∘ there)) of λ where - (inj₁ v) → xs⊆xs++ys _ _ (∈insert→∷∈insert p (Unique→head∉tail lU) v) - (inj₂ v) → xs⊆ys++xs _ _ (∈-subperm-addhead p (Unique→head∉tail lU) v) - - -- If l is a subpermutation of ys, then l ⊆ ys. - subperm→subset : ∀ {ys : List A} l → l ∈ subpermutations ys → l ⊆ ys - subperm→subset {[]} .[] (here refl) () - subperm→subset {y ∷ ys} l l∈ x∈l = case ∈-++⁻ (concatMap (insert y) (subpermutations ys)) l∈ of λ where - (inj₂ v) → there (subperm→subset l v x∈l) - (inj₁ v) → case insert-decomp l v of λ where - (l' , l'∈sp , l⊆yl') → ∈∷∧⊆→∈ (l⊆yl' x∈l) (subperm→subset l' l'∈sp) - -module _ {a} {p} {A : Set a} {L : List A} {P : Pred (List A) p} where - - ∃uniqueSubset→∃subperm : ∃[ l ] l ⊆ L × Unique l × P l → ∃[ l ] l ∈ subpermutations L × P l - ∃uniqueSubset→∃subperm (l , l⊆L , lU , Pl) = l , uniqueSubset→subperm l lU l⊆L , Pl - - ∃subperm→∃subset : ∃[ l ] l ∈ subpermutations L × P l → ∃[ l ] l ⊆ L × P l - ∃subperm→∃subset (l , l∈spL , Pl) = l , subperm→subset l l∈spL , Pl - - ∃uniqueSubset→∃uniqueSubperm : ∃[ l ] l ⊆ L × Unique l × P l - → ∃[ l ] l ∈ subpermutations L × Unique l × P l - ∃uniqueSubset→∃uniqueSubperm (l , l⊆L , lU , Pl) = l , uniqueSubset→subperm l lU l⊆L , lU , Pl - - ∃uniqueSubperm→∃uniqueSubset : ∃[ l ] l ∈ subpermutations L × Unique l × P l - → ∃[ l ] l ⊆ L × Unique l × P l - ∃uniqueSubperm→∃uniqueSubset (l , l∈spL , lU , Pl) = l , subperm→subset l l∈spL , lU , Pl - - ∃uniqueSubset⇔∃uniqueSubperm : (∃[ l ] l ⊆ L × Unique l × P l) - ⇔ (∃[ l ] l ∈ subpermutations L × Unique l × P l) - ∃uniqueSubset⇔∃uniqueSubperm = mk⇔ ∃uniqueSubset→∃uniqueSubperm ∃uniqueSubperm→∃uniqueSubset diff --git a/docs/agda-spec/src/Data/List/Relation/Binary/Sublist/Ext.agda b/docs/agda-spec/src/Data/List/Relation/Binary/Sublist/Ext.agda deleted file mode 100644 index daecc23fe0..0000000000 --- a/docs/agda-spec/src/Data/List/Relation/Binary/Sublist/Ext.agda +++ /dev/null @@ -1,10 +0,0 @@ -{-# OPTIONS --safe #-} -module Data.List.Relation.Binary.Sublist.Ext where - -open import Data.List.Relation.Binary.Sublist.Propositional public - using (_⊆_; []; _∷_; _∷ʳ_) -open import Data.List using (List; []; _∷_) - -[]⊆ : ∀ {ℓ}{A : Set ℓ} {xs : List A} → [] ⊆ xs -[]⊆ {xs = []} = [] -[]⊆ {xs = _ ∷ _} = _ ∷ʳ []⊆ diff --git a/docs/agda-spec/src/Data/List/Relation/Unary/MOf.agda b/docs/agda-spec/src/Data/List/Relation/Unary/MOf.agda deleted file mode 100644 index 2727804691..0000000000 --- a/docs/agda-spec/src/Data/List/Relation/Unary/MOf.agda +++ /dev/null @@ -1,57 +0,0 @@ -{-# OPTIONS --safe #-} -module Data.List.Relation.Unary.MOf where - -open import Level using (Level; _⊔_) renaming (suc to lsuc) -open import Function using (_$_; case_of_) - -open import Data.Empty using (⊥-elim) -open import Data.List using (List; []; _∷_; length) -open import Data.List.Relation.Unary.All using (All; []; _∷_) -open import Data.Nat using (ℕ; zero; suc) -open import Data.Nat.Properties using (suc-injective) - -open import Relation.Nullary using (Dec; yes; no; ¬_) -open import Relation.Nullary.Decidable using () renaming (map′ to mapDec) -open import Relation.Unary using (Decidable; Pred) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) - -open import Data.List.Relation.Binary.Sublist.Ext - --- States that "m-of-n" elements of a n-element list satisfy a given predicate. -data MOf {ℓ ℓ′}{A : Set ℓ} (m : ℕ) (P : Pred A ℓ′) (xs : List A) : Set (ℓ ⊔ ℓ′) where - mOf : ∀ ys - → m ≡ length ys - → ys ⊆ xs - → All P ys - → MOf m P xs - -private module _ {ℓ ℓ′} {A : Set ℓ} {P : Pred A ℓ′} where - cons : ∀ {x xs m} → P x → MOf m P xs → MOf (suc m) P (x ∷ xs) - cons p (mOf ys refl sub ps) = mOf (_ ∷ ys) refl (refl ∷ sub) (p ∷ ps) - - skip : ∀ {x xs m} → MOf m P xs → MOf m P (x ∷ xs) - skip (mOf ys len sub ps) = mOf ys len (_ ∷ʳ sub) ps - - done : ∀ {xs} → MOf 0 P xs - done = mOf [] refl []⊆ [] - - wk : ∀ {m xs} → MOf (suc m) P xs → MOf m P xs - wk (mOf (_ ∷ ys) refl (_ ∷ sub) (_ ∷ ps)) = mOf ys refl (_ ∷ʳ sub) ps - wk (mOf ys len (_ ∷ʳ sub) ps) = skip (wk (mOf ys len sub ps)) - - uncons : ∀ {m x xs} → MOf (suc m) P (x ∷ xs) → MOf m P xs - uncons (mOf ys len (_ ∷ʳ sub) ps) = wk $ mOf ys len sub ps - uncons (mOf (_ ∷ ys) refl (_ ∷ sub) (_ ∷ ps)) = mOf ys refl sub ps - - unskip : ∀ {m x xs} → ¬ P x → MOf (suc m) P (x ∷ xs) → MOf (suc m) P xs - unskip ¬px (mOf ys len (_ ∷ʳ sub) ps) = mOf ys len sub ps - unskip ¬px (mOf ys len (refl ∷ sub) (px ∷ ps)) = ⊥-elim $ ¬px px - -module _ {ℓ ℓ′} {A : Set ℓ} {P : Pred A ℓ′} (P? : Decidable P) where - MOf? : ∀ m xs → Dec (MOf m P xs) - MOf? zero xs = yes done - MOf? (suc m) [] = no λ where (mOf (_ ∷ _) len≡ () _) - MOf? (suc m) (x ∷ xs) = - case (P? x) of λ where - (yes px) → mapDec (cons px) uncons (MOf? m xs) - (no ¬px) → mapDec skip (unskip ¬px) (MOf? (suc m) xs) diff --git a/docs/agda-spec/src/Data/List/Relation/Unary/Unique/Propositional/Properties/WithK.agda b/docs/agda-spec/src/Data/List/Relation/Unary/Unique/Propositional/Properties/WithK.agda deleted file mode 100644 index 1ed86e59c6..0000000000 --- a/docs/agda-spec/src/Data/List/Relation/Unary/Unique/Propositional/Properties/WithK.agda +++ /dev/null @@ -1,48 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Properties of unique lists (setoid equality) using K ------------------------------------------------------------------------- - -{-# OPTIONS --safe --with-K #-} - -module Data.List.Relation.Unary.Unique.Propositional.Properties.WithK where - -open import Data.Empty -open import Data.List using (List) -open import Data.List.Membership.Propositional -open import Data.List.Relation.Binary.BagAndSetEquality -open import Data.List.Relation.Unary.All.Properties -open import Data.List.Relation.Unary.Any -open import Data.List.Relation.Unary.Unique.Propositional -open import Data.Product -open import Relation.Binary.PropositionalEquality -open import Relation.Nullary -open import Level using (Level) -open import Function.Bundles - -private - variable - a : Level - A : Set a - l l' : List A - ------------------------------------------------------------------------- --- membership - -unique⇒∈-prop : Unique l → (x : A) → Irrelevant (x ∈ l) -unique⇒∈-prop (hx ∷ h) x (here refl) (here refl) = refl -unique⇒∈-prop (hx ∷ h) x (here refl) (there b) = ⊥-elim (All¬⇒¬Any hx b) -unique⇒∈-prop (hx ∷ h) x (there a) (here refl) = ⊥-elim (All¬⇒¬Any hx a) -unique⇒∈-prop (hx ∷ h) x (there a) (there b) rewrite unique⇒∈-prop h x a b = refl - -unique∧set⇒bag : Unique l → Unique l' → l ∼[ set ] l' → l ∼[ bag ] l' -unique∧set⇒bag h h' eq {a} = record - { to = to - ; from = from - ; to-cong = to-cong - ; from-cong = from-cong - ; inverse = (λ {x} {y} _ → unique⇒∈-prop h' a (to y) x) - , (λ {x} {y} _ → unique⇒∈-prop h a (from y) x) - } - where open Equivalence (eq {a}) diff --git a/docs/agda-spec/src/Data/Maybe/Properties/Ext.agda b/docs/agda-spec/src/Data/Maybe/Properties/Ext.agda deleted file mode 100644 index 627eb62d4b..0000000000 --- a/docs/agda-spec/src/Data/Maybe/Properties/Ext.agda +++ /dev/null @@ -1,13 +0,0 @@ -{-# OPTIONS --safe #-} - -module Data.Maybe.Properties.Ext where - -open import Prelude using (Type) - -open import Data.Maybe -open import Function -open import Relation.Binary.PropositionalEquality - -maybe-∘ : ∀ {a} {A B C : Type a} {f : B → C} {g : A → B} {c x} → f (maybe g c x) ≡ maybe (f ∘ g) (f c) x -maybe-∘ {x = just _} = refl -maybe-∘ {x = nothing} = refl diff --git a/docs/agda-spec/src/Data/Nat/Properties/Ext.agda b/docs/agda-spec/src/Data/Nat/Properties/Ext.agda deleted file mode 100644 index b6719f6a66..0000000000 --- a/docs/agda-spec/src/Data/Nat/Properties/Ext.agda +++ /dev/null @@ -1,30 +0,0 @@ -{-# OPTIONS --safe #-} - -module Data.Nat.Properties.Ext where - -open import Data.Nat -open import Data.Nat.Properties -open import Prelude -open import Relation.Nullary.Decidable - --- if P holds for 0 but not for some N, then there exists a k where the induction step fails -negInduction : {P : ℕ → Set} → Decidable¹ P - → P 0 - → ∃[ N ] ¬ P N - → ∃[ k ] P k × ¬ P (suc k) -negInduction {P = P} P? P0 (N , ¬PN) - with anyUpTo? (λ x → P? x ×-dec ¬? (P? $ suc x)) N -... | yes (k , _ , h) = k , h -... | no ¬p = contradiction (k≤N⇒Pk ≤-refl) ¬PN - where - helper : ∀ {k} → k < N → P k → P k × P (suc k) - helper {k} k Date: Wed, 24 Sep 2025 18:01:42 +0000 Subject: [PATCH 2/9] Use `HasAdd`, `HasOrder` and `ToBool` from `stdlib-classes` --- docs/agda-spec/src/Interface/HasAdd.agda | 8 - .../src/Interface/HasAdd/Instance.agda | 17 -- docs/agda-spec/src/Interface/HasOrder.agda | 184 ------------------ .../src/Interface/HasOrder/Instance.agda | 37 ---- docs/agda-spec/src/Interface/ToBool.agda | 44 ----- docs/agda-spec/src/Ledger/Prelude.agda | 8 +- 6 files changed, 3 insertions(+), 295 deletions(-) delete mode 100644 docs/agda-spec/src/Interface/HasAdd.agda delete mode 100644 docs/agda-spec/src/Interface/HasAdd/Instance.agda delete mode 100644 docs/agda-spec/src/Interface/HasOrder.agda delete mode 100644 docs/agda-spec/src/Interface/HasOrder/Instance.agda delete mode 100644 docs/agda-spec/src/Interface/ToBool.agda diff --git a/docs/agda-spec/src/Interface/HasAdd.agda b/docs/agda-spec/src/Interface/HasAdd.agda deleted file mode 100644 index e81cdb0b64..0000000000 --- a/docs/agda-spec/src/Interface/HasAdd.agda +++ /dev/null @@ -1,8 +0,0 @@ -{-# OPTIONS --safe --cubical-compatible #-} -module Interface.HasAdd where - -record HasAdd (A : Set) : Set where - infixl 6 _+_ - field _+_ : A → A → A - -open HasAdd ⦃ ... ⦄ public diff --git a/docs/agda-spec/src/Interface/HasAdd/Instance.agda b/docs/agda-spec/src/Interface/HasAdd/Instance.agda deleted file mode 100644 index 10fcd6cfe0..0000000000 --- a/docs/agda-spec/src/Interface/HasAdd/Instance.agda +++ /dev/null @@ -1,17 +0,0 @@ -{-# OPTIONS --safe #-} -module Interface.HasAdd.Instance where - -open import Interface.HasAdd -open import Data.Integer as ℤ using (ℤ) -open import Data.Nat as ℕ using (ℕ) -open import Data.String as Str - -instance - addInt : HasAdd ℤ - addInt ._+_ = ℤ._+_ - - addNat : HasAdd ℕ - addNat ._+_ = ℕ._+_ - - addString : HasAdd String - addString ._+_ = Str._++_ diff --git a/docs/agda-spec/src/Interface/HasOrder.agda b/docs/agda-spec/src/Interface/HasOrder.agda deleted file mode 100644 index da89ef0f0e..0000000000 --- a/docs/agda-spec/src/Interface/HasOrder.agda +++ /dev/null @@ -1,184 +0,0 @@ -{-# OPTIONS --safe #-} - -module Interface.HasOrder where - -open import Prelude -open import Relation.Binary - -open Equivalence using (from; to) - -module _ {a} {A : Set a} where - module _ {_≈_ : Rel A a} where - - record HasPreorder : Set (sucˡ a) where - infix 4 _≤_ _<_ _≥_ _>_ - field - _≤_ _<_ : Rel A a - ≤-isPreorder : IsPreorder _≈_ _≤_ - <-irrefl : Irreflexive _≈_ _<_ - ≤⇔<∨≈ : ∀ {x y} → x ≤ y ⇔ (x < y ⊎ x ≈ y) - - _≥_ = flip _≤_ - _>_ = flip _<_ - - open IsPreorder ≤-isPreorder public - using () - renaming (isEquivalence to ≈-isEquivalence; refl to ≤-refl; trans to ≤-trans) - - - _≤?_ : ⦃ _≤_ ⁇² ⦄ → Decidable _≤_ - _≤?_ = dec² - - _⊎≈ : ∀ {x y} → x < y → ¬ (y < x ⊎ y ≈ x) - <⇒¬>⊎≈ x⊎≈ x⊎≈ x Date: Wed, 24 Sep 2025 18:29:00 +0000 Subject: [PATCH 3/9] Remove unnecessary files in `Ledger` and `Tactic` --- docs/agda-spec/src/Ledger/Abstract.agda | 24 -- docs/agda-spec/src/Ledger/BaseTypes.lagda | 21 -- docs/agda-spec/src/Tactic/DeriveComp.agda | 245 ---------------- docs/agda-spec/src/Tactic/Inline.agda | 264 ------------------ .../Tactic/MonoidSolver/NonNormalising.agda | 28 -- docs/agda-spec/src/Tactic/Substitute.agda | 47 ---- 6 files changed, 629 deletions(-) delete mode 100644 docs/agda-spec/src/Ledger/Abstract.agda delete mode 100644 docs/agda-spec/src/Ledger/BaseTypes.lagda delete mode 100644 docs/agda-spec/src/Tactic/DeriveComp.agda delete mode 100644 docs/agda-spec/src/Tactic/Inline.agda delete mode 100644 docs/agda-spec/src/Tactic/MonoidSolver/NonNormalising.agda delete mode 100644 docs/agda-spec/src/Tactic/Substitute.agda diff --git a/docs/agda-spec/src/Ledger/Abstract.agda b/docs/agda-spec/src/Ledger/Abstract.agda deleted file mode 100644 index a3ae64a8ec..0000000000 --- a/docs/agda-spec/src/Ledger/Abstract.agda +++ /dev/null @@ -1,24 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Ledger.Prelude -open import Ledger.Transaction - -module Ledger.Abstract (txs : TransactionStructure) where - -open TransactionStructure txs - -record indexOf : Type where - field - indexOfDCert : DCert → List DCert → Maybe Ix - indexOfRwdAddr : RwdAddr → Wdrl → Maybe Ix - indexOfTxIn : TxIn → ℙ TxIn → Maybe Ix - indexOfPolicyId : ScriptHash → ℙ ScriptHash → Maybe Ix - indexOfVote : Voter → List Voter → Maybe Ix - indexOfProposal : GovProposal → List GovProposal → Maybe Ix - -record AbstractFunctions : Type where - field txscriptfee : Prices → ExUnits → Coin - serSize : Value → MemoryEstimate - indexOfImp : indexOf - runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool - scriptSize : Script → ℕ diff --git a/docs/agda-spec/src/Ledger/BaseTypes.lagda b/docs/agda-spec/src/Ledger/BaseTypes.lagda deleted file mode 100644 index 75cea360bb..0000000000 --- a/docs/agda-spec/src/Ledger/BaseTypes.lagda +++ /dev/null @@ -1,21 +0,0 @@ -\section{Base Types} -\begin{code}[hide] -{-# OPTIONS --safe #-} - -module Ledger.BaseTypes where - -open import Prelude using (ℕ) -\end{code} - - -\begin{code}[hide] -private -\end{code} -\begin{figure*}[h] -\begin{code} - Coin = ℕ - Slot = ℕ - Epoch = ℕ -\end{code} -\caption{Some basic types used in many places in the ledger} -\end{figure*} diff --git a/docs/agda-spec/src/Tactic/DeriveComp.agda b/docs/agda-spec/src/Tactic/DeriveComp.agda deleted file mode 100644 index cb520f4230..0000000000 --- a/docs/agda-spec/src/Tactic/DeriveComp.agda +++ /dev/null @@ -1,245 +0,0 @@ -{-# OPTIONS -v allTactics:100 #-} -{-# OPTIONS --safe #-} -module Tactic.DeriveComp where - -open import Prelude hiding (Type) -open import PreludeMeta hiding (TC) renaming (TCI to TC) -open import MetaPrelude using (zipWithIndex) -open import Class.Traversable - -import Data.List.NonEmpty as NE -open import Data.Maybe.Properties using (just-injective) - -open import Interface.ComputationalRelation -open import Interface.HasAdd; open import Interface.HasAdd.Instance -open import Interface.HasSubtract; open import Interface.HasSubtract.Instance - -open import Reflection.Ext using (extendContextTel′) -open import Tactic.ClauseBuilder -open import Tactic.ReduceDec -open import MyDebugOptions - -pattern ``yes x = quote _because_ ◇⟦ quote true ◇ ∣ quote ofʸ ◇⟦ x ⟧ ⟧ -pattern ``no x = quote _because_ ◇⟦ quote false ◇ ∣ quote ofⁿ ◇⟦ x ⟧ ⟧ - -instance _ = ContextMonad-MonadTC - -record STSConstr : Set where - field - name : Name - params : List $ Abs $ Arg Type - clauses : List Type - context : Pattern - state : Pattern - signal : Pattern - result : Term - -conOrVarToPattern : ℕ → Term → Maybe Pattern -conOrVarToPattern k (♯ v) = just (Pattern.var (v - k)) -conOrVarToPattern k (con c args) = - Pattern.con c <$> (sequence $ conOrVarToPattern′ k args) - where - conOrVarToPattern′ : ℕ → List (Arg Term) → List (Maybe (Arg Pattern)) - conOrVarToPattern′ k = λ where - [] → [] - ((arg i x) ∷ l) → (arg i <$> conOrVarToPattern k x) ∷ conOrVarToPattern′ k l -conOrVarToPattern _ _ = nothing - -isArg : (a : Abs (Arg Term)) → Dec _ -isArg a = ¬? (getVisibility (unAbs a) ≟ visible) - -toSTSConstr : Name × TypeView → TC STSConstr -toSTSConstr (n , (cs , def _ args)) - with args | mapMaybe (conOrVarToPattern (length $ dropWhile isArg cs) ∘ unArg) - (take 3 args) -... | _ ∷ _ ∷ _ ∷ r ∷ [] | c ∷ s ∷ sig ∷ [] = - return record - { name = n - ; params = takeWhile isArg cs - ; clauses = zipWithIndex (λ i → mapVars (_- i)) - $ (unArg ∘ unAbs) <$> dropWhile isArg cs - ; context = c - ; state = s - ; signal = sig - ; result = mapVars (_- (length $ dropWhile isArg cs)) $ unArg r } -... | l | l' = - error1 ("toSTSConstr: wrong number of arguments:" - <+> show (length l) <+> "," <+> show (length l')) -toSTSConstr _ = error1 "toSTSConstr: wrong constructor" - -errorIfNothing : ∀ {a} {A : Set a} → Maybe A → String → TC A -errorIfNothing (just x) s = return x -errorIfNothing nothing s = error1 s - -getSTSConstrs : Name → TC (List STSConstr) -getSTSConstrs n = inDebugPath "getSTSConstrs" do - dataDef ← getDataDef n - res ← traverse toSTSConstr (DataDef.constructors dataDef) - debugLogᵐ (res ᵛⁿ ∷ᵈᵐ []ᵐ) - return res - -generatePred : List Term → Term -generatePred clauses = quote ¿_¿ ∙⟦ helper clauses ⟧ - where - helper : List Term → Term - helper [] = quoteTerm ⊤ - helper (x ∷ []) = x - helper (x ∷ x₁ ∷ l) = quote _×_ ∙⟦ x ∣ helper (x₁ ∷ l) ⟧ - -predWitness : ℕ → Term -predWitness 0 = quoteTerm tt -predWitness (suc n) = helper n - where - helper : ℕ → Term - helper 0 = ♯ 0 - helper (suc n) = quote _,_ ◆⟦ ♯ (suc n) ∣ helper n ⟧ - -curryPredProof : ℕ → Term → List (Arg Term) -curryPredProof 0 t = [] -curryPredProof 1 t = [ vArg t ] -curryPredProof 2 t = quote proj₁ ∙⟦ t ⟧ ⟨∷⟩ quote proj₂ ∙⟦ t ⟧ ⟨∷⟩ [] -curryPredProof (suc (suc (suc k))) t = - quote proj₁ ∙⟦ t ⟧ ⟨∷⟩ curryPredProof (suc (suc k)) (quote proj₂ ∙⟦ t ⟧) - -computeFunctionBody : Term → Term → Term -computeFunctionBody g result = - quote if_then_else_ ∙⟦ g ∣ quote just ◆⟦ result ⟧ ∣ quote nothing ◆ ⟧ - where open import Data.Bool - -generateFunctionClause : (List Term → Term) → STSConstr → Clause -generateFunctionClause genPred c = let open STSConstr c in - ⟦ context ∣ state ∣ signal ⦅ (λ { (abs s x) → (s , x) }) <$> params ⦆⇒ - computeFunctionBody (quote ⌊_⌋ ∙⟦ genPred clauses ⟧) result ⟧ - -generateFunction : List STSConstr → Term -generateFunction c = pat-lam (generateFunctionClause generatePred <$> c) [] - -rdOpts : ReductionOptions -rdOpts = onlyReduce [ quote ⌊_⌋ ] - -open ClauseExprM - -derive⇐ : List STSConstr → ITactic -derive⇐ (record { clauses = clauses; result = result } ∷ []) = inDebugPath "derive⇐" do - (constrPat ∷ []) ← currentTyConstrPatterns - where _ → error1 "TODO: Support more than one constructor!" - expr ← singleMatchExpr constrPat $ finishMatch $ withGoalHole $ do - let n = 1 + length clauses - pred = weaken n $ generatePred clauses - scheme = `λ "g" ⇒ (quote _≡_ ∙⟦ computeFunctionBody (♯ 0) (weaken (1 + n) result) - ∣ quote just ◆⟦ weaken (1 + n) result ⟧ ⟧) - eq = quote fromWitness' ∙⟦ pred ∣ predWitness (length clauses) ⟧ - unifyWithGoal $ quote subst ∙⟦ scheme ∣ quote sym ∙⟦ eq ⟧ ∣ quote refl ◆ ⟧ - unifyWithGoal $ clauseExprToPatLam expr -derive⇐ _ = error1 "TODO: support multiple constructors" - -derive⇒ : Name → List STSConstr → ITactic -derive⇒ n - (record { name = stsConstrName ; clauses = clauses; result = result } ∷ []) - = inDebugPath "derive⇒" do - let pred = weaken 3 (generatePred clauses) - expr ← introsExpr (from-just $ NE.fromList ("h" ⟨∷⟩ [])) $ finishMatch $ - caseMatch (mapVars (_+ 2) $ generatePred clauses) $ matchExprM - ((multiSinglePattern [ "" ] (vArg (``no (` 0))) , finishMatch do - let reducedHyp = quote subst - ∙⟦ `λ "g" ⇒ (quote _≡_ ∙⟦ computeFunctionBody (♯ 0) (weaken 4 result) - ∣ quote just ◆⟦ ♯ 3 ⟧ ⟧) - ∣ quote fromWitnessFalse' ∙⟦ pred ∣ ♯ 0 ⟧ - ∣ ♯ 1 - ⟧ - return $ quote case_of_ ∙⟦ reducedHyp ∣ `λ∅ ⟧) ∷ - (multiSinglePattern [ "" ] (vArg (``yes (` 0))) , finishMatch do - let reducedHyp = quote subst - ∙⟦ `λ "g" ⇒ (quote _≡_ ∙⟦ computeFunctionBody (♯ 0) (weaken 4 result) - ∣ quote just ◆⟦ ♯ 3 ⟧ ⟧) - ∣ quote fromWitness' ∙⟦ pred ∣ ♯ 0 ⟧ - ∣ ♯ 1 - ⟧ - ty ∙⟦ c ∣ s ∣ sig ∣ s' ⟧ ← goalTy - where ty → error ("BUG: Unexpected type" ∷ᵈ ty ∷ᵈ []) - return $ quote subst - ∙⟦ ty ∙⟦ c ∣ s ∣ sig ⟧ - ∣ quote just-injective ∙⟦ reducedHyp ⟧ - ∣ con stsConstrName (curryPredProof (length clauses) (♯ 0)) - ⟧) ∷ []) - unifyWithGoal $ clauseExprToPatLam expr -derive⇒ _ _ = error1 "TODO: support multiple constructors" - -module _ ⦃ _ : DebugOptions ⦄ where - derive⇔ : Name → List STSConstr → Tactic - derive⇔ n stsConstrs = initTac $ inDebugPath "derive⇔" do - hole⇒ ← newMeta unknown - hole⇐ ← newMeta unknown - unifyWithGoal $ quote mk⇔ ∙⟦ hole⇒ ∣ hole⇐ ⟧ - runWithHole hole⇐ $ derive⇐ stsConstrs - runWithHole hole⇒ $ derive⇒ n stsConstrs - - deriveComp : Name → List STSConstr → TC ⊤ - deriveComp definedType stsConstrs = do - debugLog ("\nDerive computation function for: " ∷ᵈ definedType ∷ᵈ []) - unifyWithGoal (generateFunction stsConstrs) - - deriveComputational : Name → Name → UnquoteDecl - deriveComputational n compName = - initUnquoteWithGoal (quoteTerm Name) $ inDebugPath "deriveComputational" do - let goalTy = quote Computational ∙⟦ n ∙ ⟧ - debugLog1 goalTy - declareDef (vArg compName) goalTy - stsConstrs ← getSTSConstrs n - compRes ← withSafeReset $ do - compHole ← newMeta unknown - equivHole ← newMeta unknown - definition ← mkRecord (quote Computational) (compHole ⟨∷⟩ equivHole ⟨∷⟩ []) - _ ← checkType definition goalTy - debugLog1ᵐ (compHole ᵗ) - runWithHole compHole $ deriveComp n stsConstrs - reduce compHole - debugLog ("compRes: " ∷ᵈ compRes ∷ᵈ []) - cTy ← newMeta unknown - sTy ← newMeta unknown - sigTy ← newMeta unknown - let isoCxt = Telescope ∋ ("c" , hArg cTy) - ∷ ("s" , hArg (weaken 1 sTy)) - ∷ ("sig" , hArg (weaken 2 sigTy)) - ∷ ("s'" , hArg (weaken 3 sTy)) - ∷ [] - iso ← extendContextTel′ isoCxt $ newMeta unknown - let isolam = `λ⟅ "c" ⟆⇒ `λ⟅ "s" ⟆⇒ `λ⟅ "sig" ⟆⇒ `λ⟅ "s'" ⟆⇒ iso - definition ← mkRecord (quote Computational) (compRes ⟨∷⟩ isolam ⟨∷⟩ []) - defineFun compName [ nonBindingClause definition ] - extendContextTel′ isoCxt $ λ _ → derive⇔ n stsConstrs iso - --- private module _ {A B : Set} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where --- variable --- c : A × B --- s s' : A --- sig : B - --- data Test : A × B → A → B → A → Set where --- test : proj₁ c ≡ s --- → proj₂ c ≡ sig --- ------------------------ --- → Test c s sig (proj₁ c) - --- unquoteDecl Computational-Test = deriveComputational (quote Test) Computational-Test - --- -- Sanity checks --- testFun : A × B → A → B → Maybe A --- testFun c s sig = --- if ⌊ ¿ proj₁ c ≡ s × proj₂ c ≡ sig ¿ ⌋ then just (proj₁ c) else nothing - --- testFunPf⇒ : testFun c s sig ≡ just s' → Test c s sig s' --- testFunPf⇒ {c} {s} {sig} h = case ¿ proj₁ c ≡ s × proj₂ c ≡ sig ¿ of λ where --- (no ¬p) → case by-reduceDec h of λ () --- (yes p) → subst (Test c s sig) (just-injective $ by-reduceDec h) --- $ test (proj₁ p) (proj₂ p) - --- testFunPf⇐ : Test c s sig s' → testFun c s sig ≡ just s' --- testFunPf⇐ {s = s} (test x x₁) = by-reduceDecInGoal (refl {x = just s}) - --- Computational-Test-Manual : Computational Test --- Computational-Test-Manual = record --- { compute = testFun ; ≡-just⇔STS = mk⇔ testFunPf⇒ testFunPf⇐ } - --- _ : ∀ {c s sig} → testFun c s sig ≡ Computational.compute Computational-Test c s sig --- _ = refl diff --git a/docs/agda-spec/src/Tactic/Inline.agda b/docs/agda-spec/src/Tactic/Inline.agda deleted file mode 100644 index b9e1e96916..0000000000 --- a/docs/agda-spec/src/Tactic/Inline.agda +++ /dev/null @@ -1,264 +0,0 @@ -{-# OPTIONS --safe #-} -{-# OPTIONS -v tc.unquote:10 #-} -{-# OPTIONS -v tactic.inline:100 #-} - -module Tactic.Inline where - -open import Prelude hiding (_∷ʳ_) -import Data.Nat as ℕ; import Data.Nat.Properties as ℕ -import Data.List as L -import Data.Fin as F -open import PreludeMeta hiding (All) -open import Interface.ToBool -open import Data.List.Ext using (_⁉_) -open import Reflection.Ext using (apply∗) - -open Debug ("tactic.inline" , 100) -open import Class.Show - -open import Algebra.Core using (Op₁) - -private - pattern `case_of_ x y = quote case_of_ ∙⟦ x ∣ y ⟧ - - $inline : Bool → Name → Term → TC ⊤ - $inline genType n' `e = do - e@(def n xs) ← return `e - where _ → _IMPOSSIBLE_ - printLn $ "** Inlining " ◇ show n ◇ "(" ◇ show xs ◇ ")" - if genType then (declareDef (vArg n') =<< inferType e) else return tt - function cs ← getDefinition n - where _ → _IMPOSSIBLE_ - print $ show n ◇ "'s clauses: " - void $ forM cs λ c → print $ " - " ◇ show c - print "" - let cs' = goᶜ n n' xs <$> cs - print $ "\n" ◇ show n' ◇ "'s clauses: " - void $ forM cs' λ c → print $ " - " ◇ show c - print "" - defineFun n' cs' - - where module _ (n n' : Name) (xs : Args Term) (let ∣xs∣ = length xs) where - - lookupVar : ℕ → ℕ → Maybe Term - lookupVar lvl x - with x ℕ. xs ⁉ (∣xs∣ ∸ suc k) - - -- (B) recursively substitute free variables for the values in given `xs` - mutual - go : ℕ → Op₁ Term - go lvl = λ where - -- * (B1) substitute free variables - (var x as) → let as′ = go∗ lvl as in case lookupVar lvl x of λ where - nothing → var x as′ - (just t) → apply∗ t as′ - -- * (B2) rename (& instantiate) recursive calls - (def 𝕟 as) → let as′ = go∗ lvl as in - if 𝕟 == n then - def n' (drop ∣xs∣ as′) - else - def 𝕟 as′ - (con c as) → con c (go∗ lvl as) - (pi (arg i ty) (abs x t)) → pi (arg i $ go lvl ty) (abs x $ go (suc lvl) t) - (lam v (abs x t)) → lam v (abs x $ go (suc lvl) t) - (pat-lam cs (vArg a ∷ [])) → `case go lvl a of pat-lam (goCls lvl cs) [] - -- ^ use case_of_ for single-argument pattern lambdas (c.f. example 7) - (pat-lam cs as) → pat-lam (goCls lvl cs) (go∗ lvl as) - (agda-sort s) → agda-sort (goSort lvl s) - (meta x as) → meta x (go∗ lvl as) - t → t - - go∗ : ℕ → Op₁ (Args Term) - go∗ lvl = λ where - [] → [] - (arg i x ∷ as) → arg i (go lvl x) ∷ go∗ lvl as - - goSort : ℕ → Op₁ Sort - goSort lvl = λ where - (set t) → set $ go lvl t - (prop t) → prop $ go lvl t - s → s - - goC : ℕ → Op₁ Clause - goC lvl = λ where - (clause tel ps t) → - let lvl' = lvl ℕ.+ length tel - in clause (goTel lvl tel) (goPs lvl' ps) (go lvl' t) - (absurd-clause tel ps) → - let lvl' = lvl ℕ.+ length tel - in absurd-clause (goTel lvl tel) (goPs lvl' ps) - - goCls : ℕ → Op₁ (List Clause) - goCls lvl = λ where - [] → [] - (c ∷ cs) → goC lvl c ∷ goCls lvl cs - - goP : ℕ → Op₁ Pattern - goP lvl = λ where - (con c ps) → con c (goPs lvl ps) - (dot t) → dot (go lvl t) - (var x) → case lookupVar lvl x of λ where - nothing → var x - (just t) → dot t - p → p - - goPs : ℕ → Op₁ (Args Pattern) - goPs lvl = λ where - [] → [] - (arg i p ∷ ps) → arg i (goP lvl p) ∷ goPs lvl ps - - goTel : ℕ → Op₁ Telescope - goTel lvl = λ where - [] → [] - ((x , arg i t) ∷ tel) → (x , arg i (go lvl t)) ∷ goTel (suc lvl) tel - - -- ** Entrypoint (A): instantiating the clauses of a definition - goᶜ : Clause → Clause - goᶜ = λ where - (clause tel ps t) → let n = length tel ∸ ∣xs∣ in - clause (instTel tel) (instPs n ps) (go n t) - (absurd-clause tel ps) → let n = length tel ∸ ∣xs∣ in - absurd-clause (instTel tel) (instPs n ps) - where - -- (A1) instantiating a clause's telescope - instTel : Op₁ Telescope - instTel = goTel 0 ∘ drop ∣xs∣ - - -- (A2) instantiating a clause's parameters - instPs : ℕ → Op₁ (Args Pattern) - instPs n = goPs n ∘ drop ∣xs∣ - -inline inlineDecl : Name → Term → TC ⊤ -inline = $inline false -- for use with `unquoteDef` -inlineDecl = $inline true -- for use with `unquoteDecl` - --- ** Tests - -private - -- (1) specializing the function to be applied by `map` - unquoteDecl sucs = inlineDecl sucs (quoteTerm (L.map suc)) - {- - sucs : List ℕ → List ℕ - sucs [] = [] {_} {_} - sucs (x ∷ xs) = _∷_ {_} {_} (suc x) (sucs xs) - -} - _ = sucs (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) - ∋ refl - - -- (2) specializing the predicate to be checked by `all?`) - data Even : ℕ → Set where - zero : Even 0 - suc : ∀ {n} → Even n → Even (suc (suc n)) - - even? : Decidable¹ Even - even? = λ where - 0 → yes zero - 1 → no λ () - (suc (suc n)) → mapDec suc (λ where (suc p) → p) (even? n) - - open import Data.List.Relation.Unary.All using (All; []; _∷_; all?) - - unquoteDecl evens? = inlineDecl evens? (quoteTerm (all? even?)) - {- - evens? : Decidable¹ (All Even) - evens? [] = yes [] - evens? (x ∷ xs) = mapDec (uncurry _∷_) uncons (even? x ×-dec evens? xs) - -} - _ = evens? (0 ∷ 2 ∷ []) ≡ yes (zero ∷ suc zero ∷ []) - ∋ refl - - -- (3) works under module parameters - module _ (n m : ℕ) where - unquoteDecl ⟫evens? = inlineDecl ⟫evens? (quoteTerm (all? even?)) - _ = ⟫evens? (0 ∷ 2 ∷ []) ≡ yes (zero ∷ suc zero ∷ []) - ∋ refl - - module _ {A B : Set} (f : A → B) where - map' : List A → List B - map' [] = [] - map' (x ∷ xs) = f x ∷ map' xs - - unquoteDecl sucs' = inlineDecl sucs' (quoteTerm (map' {B = ℕ} suc)) - _ = sucs' (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) - ∋ refl - - -- (4) works under mutual blocks - data Odd : ℕ → Set where - one : Odd 1 - suc : ∀ {n} → Odd n → Odd (suc (suc n)) - - mutual - odd? : Decidable¹ Odd - odd? = λ where - 0 → no λ () - 1 → yes one - (suc (suc n)) → mapDec suc (λ where (suc p) → p) (odd? n) - - unquoteDecl mevens? = inlineDecl mevens? (quoteTerm (all? even?)) - unquoteDecl modds? = inlineDecl modds? (quoteTerm (all? odd?)) - _ = mevens? (0 ∷ 2 ∷ []) ≡ yes (zero ∷ suc zero ∷ []) - ∋ refl - - -- [AGDA BUG] cannot use _∋_ (c.f. Agda issue #7028) - _ : modds? (1 ∷ 3 ∷ []) ≡ yes (one ∷ suc one ∷ []) - _ = refl - - -- (5) works with `with`-statements (e.g. for specializing `mapMaybe`) - toEvenOdd : ℕ → ℕ {- even part -} × Maybe ℕ {- odd part -} - toEvenOdd n with even? n - ... | yes _ = n , nothing - ... | no _ = pred n , just 1 - - toOdd : ℕ → Maybe ℕ - toOdd = proj₂ ∘ toEvenOdd - - unquoteDecl toOdds = inlineDecl toOdds (quoteTerm (L.mapMaybe toOdd)) - {- - toOdds : List ℕ → List ℕ - toOdds [] = [] - toOdds (x ∷ xs) with toOdd x - -- ** [LIMITATION] does not recursively inline `with`-statements - -- ... | just y = y ∷ toOdds xs - -- ... | nothing = toOdds xs - ... | just y = y ∷ mapMaybe toOdd xs - ... | nothing = mapMaybe toOdd xs - -} - _ = toOdds (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ≡ (1 ∷ 1 ∷ []) - ∋ refl - - -- (6) test for `MOf?` - open import Data.List.Relation.Unary.MOf using (MOf; mOf; MOf?) - - unquoteDecl MOf-even? = inlineDecl MOf-even? (quoteTerm (MOf? even?)) - {- - MOf?-even? : ∀ m xs → Dec (MOf m Even xs) - MOf?-even? zero xs = yes done - MOf?-even? (suc m) [] = no λ where (mOf (_ ∷ _) len≡ () _) - MOf?-even? (suc m) (x ∷ xs) = - if even? x then - (λ {px} → mapDec (cons px) uncons (MOf?-even? m xs)) - else - (λ {¬px} → mapDec skip (unskip ¬px) (MOf?-even? (suc m) xs)) - -} - - _ = MOf-even? 2 (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) - ≡ yes (mOf (0 ∷ 2 ∷ []) refl (refl ∷ 1 ∷ʳ refl ∷ 3 ∷ʳ []) (zero ∷ suc zero ∷ [])) - ∋ refl - where open import Data.List.Relation.Binary.Sublist.Ext - - -- (7) works on pattern lambdas arising from `case_of_` - refl? : ℕ → Set - refl? n = case n ≟ n of λ where - (yes p) → ⊤ - (no ¬p) → ⊥ - - unquoteDecl refl42 = inlineDecl refl42 (quoteTerm (refl? 42)) - {- - refl42 - = case 42 ℕ.≟ 42 of - (λ { (true because ofʸ p) → ⊤ ; (false because ofⁿ ¬p) → ⊥ }) - -} diff --git a/docs/agda-spec/src/Tactic/MonoidSolver/NonNormalising.agda b/docs/agda-spec/src/Tactic/MonoidSolver/NonNormalising.agda deleted file mode 100644 index 69cd12fa05..0000000000 --- a/docs/agda-spec/src/Tactic/MonoidSolver/NonNormalising.agda +++ /dev/null @@ -1,28 +0,0 @@ -{-# OPTIONS --safe #-} - -module Tactic.MonoidSolver.NonNormalising where - -open import Data.List using ([]; _∷_) -open import Data.Product using (_,_) -open import Data.Maybe using (nothing; just) -open import Reflection -open import Tactic.MonoidSolver hiding (solve-macro; solve) -import Tactic.MonoidSolver as Solver - --- The standard library MonoidSolver normalises the type of the hole --- before solving. This can be very expensive in some scenarios. This --- version tries first without normalising and only if that fails does --- it resort to normalisation. -solve-macro : Term → Term → TC _ -solve-macro mon hole = catchTC (do - hole′ ← inferType hole - names ← findMonoidNames mon - just (lhs , rhs) ← pure (getArgs hole′) - where nothing → typeError (termErr hole′ ∷ []) - let soln = constructSoln mon names lhs rhs - unify hole soln - ) (Solver.solve-macro mon hole) - -macro - solve : Term → Term → TC _ - solve = solve-macro diff --git a/docs/agda-spec/src/Tactic/Substitute.agda b/docs/agda-spec/src/Tactic/Substitute.agda deleted file mode 100644 index f54efdd92d..0000000000 --- a/docs/agda-spec/src/Tactic/Substitute.agda +++ /dev/null @@ -1,47 +0,0 @@ - -module Tactic.Substitute where - -open import MetaPrelude -open import Meta - --- There aren't any nice substitution functions (that I can find) in the standard library or --- stdlib-meta. This one is cheating and only works for closed terms at either never gets --- applied, or where we can safely throw away the arguments (e.g. `unknown`). - -Subst : Set → Set -Subst A = ℕ → Term → A → A - -substTerm : Subst Term -substArgs : Subst (Args Term) -substArg : Subst (Arg Term) -substAbs : Subst (Abs Term) -substSort : Subst Sort - -substTerm x s (var y args) = - case compare x y of λ where - (less _ _) → var (y ∸ 1) (substArgs x s args) - (equal _) → s -- cheating and dropping the args! - (greater _ _) → var y (substArgs x s args) -substTerm x s (con c args) = con c (substArgs x s args) -substTerm x s (def f args) = def f (substArgs x s args) -substTerm x s (lam v t) = lam v (substAbs x s t) -substTerm x s (pat-lam cs args₁) = unknown -- ignoring for now -substTerm x s (pi a b) = pi (substArg x s a) (substAbs x s b) -substTerm x s (agda-sort s₁) = agda-sort (substSort x s s₁) -substTerm x s (lit l) = lit l -substTerm x s (meta m args) = meta m (substArgs x s args) -substTerm x s unknown = unknown - -substArgs x s [] = [] -substArgs x s (a ∷ as) = substArg x s a ∷ substArgs x s as - -substArg x s (arg i t) = arg i (substTerm x s t) - -substAbs x s (abs z t) = abs z (substTerm (ℕ.suc x) s t) - -substSort x s (set t) = set (substTerm x s t) -substSort x s (lit n) = lit n -substSort x s (prop t) = prop (substTerm x s t) -substSort x s (propLit n) = propLit n -substSort x s (inf n) = inf n -substSort x s unknown = unknown From 57d9f56d0353b4716cd22dac7bc822f4376946d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Wed, 24 Sep 2025 22:45:45 +0000 Subject: [PATCH 4/9] Upgrade Agda and libraries --- .../src/Foreign/Convertible/Deriving.agda | 15 ++---- .../src/Foreign/HaskellTypes/Deriving.agda | 5 +- docs/agda-spec/src/Ledger/Prelude.agda | 2 +- docs/agda-spec/src/MyDebugOptions.agda | 2 +- docs/agda-spec/src/PreludeMeta.agda | 47 ------------------- docs/agda-spec/src/Tactic/GenError.agda | 8 +--- docs/agda-spec/src/formal-consensus.agda-lib | 1 + flake.lock | 6 +-- nix/agda.nix | 32 +++++++++---- 9 files changed, 37 insertions(+), 81 deletions(-) delete mode 100644 docs/agda-spec/src/PreludeMeta.agda diff --git a/docs/agda-spec/src/Foreign/Convertible/Deriving.agda b/docs/agda-spec/src/Foreign/Convertible/Deriving.agda index dc85fc206c..8ff4706d00 100644 --- a/docs/agda-spec/src/Foreign/Convertible/Deriving.agda +++ b/docs/agda-spec/src/Foreign/Convertible/Deriving.agda @@ -1,8 +1,8 @@ module Foreign.Convertible.Deriving where open import Level -open import MetaPrelude -open import Meta +open import Meta.Prelude +open import Meta.Init import Data.List as L import Data.List.NonEmpty as NE @@ -29,7 +29,7 @@ open import Class.Traversable open import Class.Show open import Class.MonadReader -open import Tactic.Substitute +open import Reflection.Utils.Substitute open import Foreign.Convertible open import Foreign.HaskellTypes open import Foreign.HaskellTypes.Deriving @@ -37,17 +37,10 @@ open import Foreign.HaskellTypes.Deriving private instance _ = Functor-M {TC} --- TODO: move to agda-stdlib-meta -liftTC : ∀ {a} {A : Set a} → R.TC A → TC A -liftTC m _ = m - private open MonadReader ⦃...⦄ - variable - A B C : Set - TyViewTel = List (Abs (Arg Type)) substTel : Subst TyViewTel @@ -139,7 +132,7 @@ doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole -- Deriving a Convertible instance. Usage -- unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy) deriveConvertible : Name → Name → Name → R.TC ⊤ -deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do +deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (sort (lit 0)) do agdaDef ← getDefinition agdaName hsDef ← getDefinition hsName -- instName ← freshName $ "Convertible" S.++ show hsName diff --git a/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda index 644a74c84f..6195bd8773 100644 --- a/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda +++ b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda @@ -1,7 +1,7 @@ module Foreign.HaskellTypes.Deriving where -open import Meta hiding (TC; Monad-TC; MonadError-TC) +open import Meta.Init hiding (TC; Monad-TC; MonadError-TC) open import Level using (Level; 0ℓ) open import Agda.Builtin.Reflection using (declareData; defineData; pragmaForeign; pragmaCompile; @@ -50,9 +50,6 @@ private variable l : Level A B : Set l --- TODO: somewhere else -`Set = agda-sort (Sort.set (quote 0ℓ ∙)) - -- * Controlling the names of the generated types record NameEnv : Set where diff --git a/docs/agda-spec/src/Ledger/Prelude.agda b/docs/agda-spec/src/Ledger/Prelude.agda index 1093abf511..6d16d17806 100644 --- a/docs/agda-spec/src/Ledger/Prelude.agda +++ b/docs/agda-spec/src/Ledger/Prelude.agda @@ -26,7 +26,7 @@ open import Interface.IsCommutativeMonoid public open import Class.ToBool public open import Ledger.Interface.HasCoin public open import MyDebugOptions public -open import Tactic.Premises public +open import Prelude.STS.GenPremises public open import Class.CommutativeMonoid public open import abstract-set-theory.FiniteSetTheory public diff --git a/docs/agda-spec/src/MyDebugOptions.agda b/docs/agda-spec/src/MyDebugOptions.agda index 9569204bcb..81b3cd9a4d 100644 --- a/docs/agda-spec/src/MyDebugOptions.agda +++ b/docs/agda-spec/src/MyDebugOptions.agda @@ -1,7 +1,7 @@ {-# OPTIONS --safe --without-K #-} module MyDebugOptions where -open import PreludeMeta +open import Meta.Init instance defaultDebugOptionsI : DebugOptions diff --git a/docs/agda-spec/src/PreludeMeta.agda b/docs/agda-spec/src/PreludeMeta.agda deleted file mode 100644 index 9c66242ba1..0000000000 --- a/docs/agda-spec/src/PreludeMeta.agda +++ /dev/null @@ -1,47 +0,0 @@ -{-# OPTIONS --safe --without-K #-} - -module PreludeMeta where - --- ** Re-exporting from stdlib -open import Agda.Builtin.Reflection public - using (withReduceDefs) -open import Reflection public - using (TC; Name; Meta; extendContext; withNormalisation) -open import Reflection.AST.Term public - hiding (_≟_) -open import Reflection.AST.Argument public - using (Arg; arg; unArg; Args; vArg; hArg; iArg; _⟨∷⟩_; _⟅∷⟆_) -open import Reflection.AST.Argument.Visibility public - using (Visibility; visible; hidden; instance′) -open import Reflection.AST.Abstraction public - using (Abs; abs; unAbs) -open import Reflection.AST.DeBruijn public - using (weaken; strengthen; η-expand) - --- ** Re-exporting from stdlib-meta -open import Reflection.Syntax public - hiding (toℕ) -open import Reflection.Utils public - hiding (mkRecord) -open import Reflection.Debug public -open import Reflection.Utils.Debug public - hiding (error) -open import Reflection.Tactic public - --- * MonadTC interface for TC -open import Class.MonadTC public - hiding (extendContext) -open MonadTC ⦃...⦄ public -open import Class.MonadError public - using (MonadError; MonadError-TC) -open MonadError ⦃...⦄ public - using (error; catch) -instance - iTC = MonadTC-TC - iTCE = MonadError-TC - --- * MonadTC interface for TCI -open import Meta public - renaming (TC to TCI) - hiding (Monad-TC; MonadError-TC; toℕ) -open import Reflection.Utils.TCI public diff --git a/docs/agda-spec/src/Tactic/GenError.agda b/docs/agda-spec/src/Tactic/GenError.agda index b358744654..caf2ee7755 100644 --- a/docs/agda-spec/src/Tactic/GenError.agda +++ b/docs/agda-spec/src/Tactic/GenError.agda @@ -7,8 +7,8 @@ module Tactic.GenError where -open import MetaPrelude -open import Meta +open import Meta.Prelude +open import Meta.Init open import Class.Functor open import Class.Monad @@ -35,10 +35,6 @@ instance open ClauseExprM -private - liftTC : {A : Set} → R.TC A → TC A - liftTC x = λ r → applyExtContext (r .TCEnv.localContext) x - genError' : ITactic genError' = inDebugPath "genError" do t ← inferType (♯ 0) diff --git a/docs/agda-spec/src/formal-consensus.agda-lib b/docs/agda-spec/src/formal-consensus.agda-lib index 6ebaaad4bf..b72451f9c5 100644 --- a/docs/agda-spec/src/formal-consensus.agda-lib +++ b/docs/agda-spec/src/formal-consensus.agda-lib @@ -4,4 +4,5 @@ depend: standard-library-classes standard-library-meta abstract-set-theory + iog-prelude include: . diff --git a/flake.lock b/flake.lock index dd007d5741..5948bc68a8 100644 --- a/flake.lock +++ b/flake.lock @@ -35,11 +35,11 @@ }, "agda-nixpkgs": { "locked": { - "lastModified": 1726583932, - "narHash": "sha256-zACxiQx8knB3F8+Ze+1BpiYrI+CbhxyWpcSID9kVhkQ=", + "lastModified": 1758446476, + "narHash": "sha256-5rdAi7CTvM/kSs6fHe1bREIva5W3TbImsto+dxG4mBo=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "658e7223191d2598641d50ee4e898126768fe847", + "rev": "a1f79a1770d05af18111fbbe2a3ab2c42c0f6cd0", "type": "github" }, "original": { diff --git a/nix/agda.nix b/nix/agda.nix index 12f72786c1..88522bc84f 100644 --- a/nix/agda.nix +++ b/nix/agda.nix @@ -19,12 +19,12 @@ let agdaStdlibClasses = customAgda.agdaPackages.mkDerivation { inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; pname = "agda-stdlib-classes"; - version = "2.1.1"; + version = "2.3"; src = pkgs.fetchFromGitHub { owner = "agda"; repo = "agda-stdlib-classes"; - rev = "73f4da05aeea040fea4587629f9fd83a8f04e656"; - hash = "sha256-Uj3bmgMtdBJYGW7K+0rqxexm6M47odBuWyRo0aoYmZg="; + rev = "v2.3"; + sha256 = "0bbgc3nf1b2v3wljrq7974z38apzzsdhfzc1fdmm4fsmnpglmb1m"; }; meta = { }; libraryFile = "agda-stdlib-classes.agda-lib"; @@ -35,16 +35,16 @@ let agdaStdlibMeta = customAgda.agdaPackages.mkDerivation { inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; pname = "agda-stdlib-meta"; - version = "2.1.1"; + version = "2.3"; src = pkgs.fetchFromGitHub { owner = "agda"; repo = "agda-stdlib-meta"; - rev = "v2.1.1"; - hash = "sha256-qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4="; + rev = "v2.3"; + sha256 = "1n41cfkahg2zzfm113dkqlh5m07rvm9jjh8ps50qi3cpkz203gla"; }; meta = { }; libraryFile = "agda-stdlib-meta.agda-lib"; - everythingFile = "Main.agda"; + everythingFile = "standard-library-meta.agda"; buildInputs = [ agdaStdlib agdaStdlibClasses ]; }; @@ -64,7 +64,23 @@ let buildInputs = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ]; }; - deps = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta agdaSets ]; + agdaIOGPrelude = customAgda.agdaPackages.mkDerivation { + inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; + pname = "agda-prelude"; + version = "2.0"; + src = pkgs.fetchFromGitHub { + repo = "iog-agda-prelude"; + owner = "input-output-hk"; + rev = "e25670dcea694f321cbcd7a0bb704b82d5d7b266"; + sha256 = "1r2g7akia33yis8kgw398w0z484zry1q26739wcq6dfdyw7zb8v7"; + }; + meta = { }; + libraryFile = "iog-prelude.agda-lib"; + everythingFile = "src/Everything.agda"; + buildInputs = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ]; + }; + + deps = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta agdaSets agdaIOGPrelude ]; agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; }; attrs = pkgs.recurseIntoAttrs rec { From 84dc3b2e508db5c3cdf496d78d34fdd0a81c7f24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 25 Sep 2025 18:34:49 +0000 Subject: [PATCH 5/9] Relocate extensions to libraries to `src-lib-exts` --- docs/agda-spec/{src => }/formal-consensus.agda-lib | 4 +++- .../{src => src-lib-exts/stdlib}/Data/Rational/Ext.agda | 2 +- docs/agda-spec/src/Ledger/Types/Epoch.agda | 2 +- docs/agda-spec/src/Spec/ChainHead.lagda | 2 +- docs/agda-spec/src/Spec/ChainHead/Properties.agda | 2 +- docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda | 2 +- docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda | 2 +- .../src/Spec/Foreign/HSConsensus/ExternalStructures.agda | 2 +- docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda | 2 +- docs/agda-spec/src/Spec/Protocol.lagda | 2 +- docs/agda-spec/src/Spec/Protocol/Properties.agda | 2 +- 11 files changed, 13 insertions(+), 11 deletions(-) rename docs/agda-spec/{src => }/formal-consensus.agda-lib (82%) rename docs/agda-spec/{src => src-lib-exts/stdlib}/Data/Rational/Ext.agda (98%) diff --git a/docs/agda-spec/src/formal-consensus.agda-lib b/docs/agda-spec/formal-consensus.agda-lib similarity index 82% rename from docs/agda-spec/src/formal-consensus.agda-lib rename to docs/agda-spec/formal-consensus.agda-lib index b72451f9c5..2d36d6b3e3 100644 --- a/docs/agda-spec/src/formal-consensus.agda-lib +++ b/docs/agda-spec/formal-consensus.agda-lib @@ -5,4 +5,6 @@ depend: standard-library-meta abstract-set-theory iog-prelude -include: . +include: + src + src-lib-exts diff --git a/docs/agda-spec/src/Data/Rational/Ext.agda b/docs/agda-spec/src-lib-exts/stdlib/Data/Rational/Ext.agda similarity index 98% rename from docs/agda-spec/src/Data/Rational/Ext.agda rename to docs/agda-spec/src-lib-exts/stdlib/Data/Rational/Ext.agda index a637bfd9ed..1963120707 100644 --- a/docs/agda-spec/src/Data/Rational/Ext.agda +++ b/docs/agda-spec/src-lib-exts/stdlib/Data/Rational/Ext.agda @@ -2,7 +2,7 @@ open import Agda.Primitive renaming (Set to Type) -module Data.Rational.Ext where +module stdlib.Data.Rational.Ext where open import Function using (_∘_; _$_) open import Data.Rational hiding (show) diff --git a/docs/agda-spec/src/Ledger/Types/Epoch.agda b/docs/agda-spec/src/Ledger/Types/Epoch.agda index 5862ded786..42a52cf37a 100644 --- a/docs/agda-spec/src/Ledger/Types/Epoch.agda +++ b/docs/agda-spec/src/Ledger/Types/Epoch.agda @@ -9,7 +9,7 @@ open import Algebra using (Semiring) open import Relation.Binary open import Data.Nat.Properties using (+-*-semiring) open import Data.Rational using (ℚ) -open import Data.Rational.Ext using (InPosUnitInterval) +open import stdlib.Data.Rational.Ext using (InPosUnitInterval) additionVia : ∀{A : Set} → (A → A) → ℕ → A → A additionVia sucFun zero r = r diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda index 28f47da8c7..e33da7c660 100644 --- a/docs/agda-spec/src/Spec/ChainHead.lagda +++ b/docs/agda-spec/src/Spec/ChainHead.lagda @@ -28,7 +28,7 @@ open import Spec.BaseTypes using (Nonces) open import Spec.BlockDefinitions open import Ledger.Crypto open import Ledger.Types.Epoch -open import Data.Rational.Ext +open import stdlib.Data.Rational.Ext module Spec.ChainHead (crypto : _) (open Crypto crypto) diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda index 04a878a1f8..9b70e1cb84 100644 --- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda +++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda @@ -5,7 +5,7 @@ open import Spec.BaseTypes using (Nonces) open import Spec.BlockDefinitions open import Ledger.Crypto open import Ledger.Types.Epoch -open import Data.Rational.Ext +open import stdlib.Data.Rational.Ext module Spec.ChainHead.Properties (crypto : _) (open Crypto crypto) diff --git a/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda index ecafba9e84..8ee1667f80 100644 --- a/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda +++ b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda @@ -28,7 +28,7 @@ dummyExternalFunctions = record ; extLn = λ p → to (rationalExtStructure≈ .ln (from p) ⦃ if (from p) ℚ.> 0ℚ then (λ{p>0} → positive p>0) else error "Not a positive rational number" ⦄) } where - open import Data.Rational.Ext using (RationalExtStructure; rationalExtStructure≈) + open import stdlib.Data.Rational.Ext using (RationalExtStructure; rationalExtStructure≈) open RationalExtStructure open import Data.Rational as ℚ {-# COMPILE GHC dummyExternalFunctions as dummyExternalFunctions #-} diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda index fa8ba59212..b55f7e2694 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda @@ -14,7 +14,7 @@ import Spec.Foreign.HSTypes as F open import Spec.Foreign.Util public open import Data.Rational using (ℚ; mkℚ; 0ℚ; 1ℚ; ½; Positive; positive; _<_) renaming (_≤_ to _≤ℚ_) -open import Data.Rational.Ext using (InPosUnitInterval) +open import stdlib.Data.Rational.Ext using (InPosUnitInterval) open import Data.Integer using (_≤_; _<_) ½-positive : Positive ½ diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda index cf56807788..550621c2bd 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda @@ -110,7 +110,7 @@ instance ; serHashToNonce = id } -open import Data.Rational.Ext using (RationalExtStructure) +open import stdlib.Data.Rational.Ext using (RationalExtStructure) instance HSRationalExtStructure : RationalExtStructure diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda index 6c4e279bdb..7d24e85127 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda @@ -5,7 +5,7 @@ open import Spec.Foreign.ExternalFunctions open import Foreign.Haskell.Coerce open import Data.Rational as ℚ using (ℚ; 0ℚ; 1ℚ; positive) -open import Data.Rational.Ext using (InPosUnitInterval) +open import stdlib.Data.Rational.Ext using (InPosUnitInterval) open import Spec.Foreign.HSConsensus.BaseTypes open import Spec.Protocol DummyCrypto DummyNonces DummyEpochStructure DummyBlockStructure DummyAbstractFunctions DummyRationalExtStructure hiding (lookupPoolDistr) diff --git a/docs/agda-spec/src/Spec/Protocol.lagda b/docs/agda-spec/src/Spec/Protocol.lagda index b31fa90c3c..392d939bdb 100644 --- a/docs/agda-spec/src/Spec/Protocol.lagda +++ b/docs/agda-spec/src/Spec/Protocol.lagda @@ -24,7 +24,7 @@ open import Spec.BaseTypes using (Nonces) open import Spec.BlockDefinitions open import Ledger.Crypto open import Ledger.Types.Epoch -open import Data.Rational.Ext +open import stdlib.Data.Rational.Ext module Spec.Protocol (crypto : _) (open Crypto crypto) diff --git a/docs/agda-spec/src/Spec/Protocol/Properties.agda b/docs/agda-spec/src/Spec/Protocol/Properties.agda index af668e377b..1bc08d5f5f 100644 --- a/docs/agda-spec/src/Spec/Protocol/Properties.agda +++ b/docs/agda-spec/src/Spec/Protocol/Properties.agda @@ -4,7 +4,7 @@ open import Spec.BaseTypes using (Nonces) open import Spec.BlockDefinitions open import Ledger.Crypto open import Ledger.Types.Epoch -open import Data.Rational.Ext +open import stdlib.Data.Rational.Ext module Spec.Protocol.Properties (crypto : _) (open Crypto crypto) From c6843def29d2a205f03dad41479b8916d39deb61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 25 Sep 2025 19:44:35 +0000 Subject: [PATCH 6/9] Relocate test programs to `conformance-example` --- .../{src/Spec/hs-src => conformance-example}/LICENSE | 0 .../{src/Spec/hs-src => conformance-example}/Lib.hs | 0 .../{src/Spec/hs-src => conformance-example}/NOTICE | 0 .../Spec/hs-src => conformance-example}/cabal.project | 0 .../conformance-example.cabal} | 8 ++++---- .../hs-src => conformance-example}/test/ChainHeadSpec.hs | 0 .../test/OperationalCertificateSpec.hs | 0 .../hs-src => conformance-example}/test/ProtocolSpec.hs | 0 .../{src/Spec/hs-src => conformance-example}/test/Spec.hs | 0 .../test/TickForecastSpec.hs | 0 .../hs-src => conformance-example}/test/TickNonceSpec.hs | 0 .../test/UpdateNonceSpec.hs | 0 docs/agda-spec/src/Makefile | 6 +++--- 13 files changed, 7 insertions(+), 7 deletions(-) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/LICENSE (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/Lib.hs (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/NOTICE (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/cabal.project (100%) rename docs/agda-spec/{src/Spec/hs-src/cardano-consensus-executable-spec.cabal => conformance-example/conformance-example.cabal} (79%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/test/ChainHeadSpec.hs (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/test/OperationalCertificateSpec.hs (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/test/ProtocolSpec.hs (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/test/Spec.hs (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/test/TickForecastSpec.hs (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/test/TickNonceSpec.hs (100%) rename docs/agda-spec/{src/Spec/hs-src => conformance-example}/test/UpdateNonceSpec.hs (100%) diff --git a/docs/agda-spec/src/Spec/hs-src/LICENSE b/docs/agda-spec/conformance-example/LICENSE similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/LICENSE rename to docs/agda-spec/conformance-example/LICENSE diff --git a/docs/agda-spec/src/Spec/hs-src/Lib.hs b/docs/agda-spec/conformance-example/Lib.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/Lib.hs rename to docs/agda-spec/conformance-example/Lib.hs diff --git a/docs/agda-spec/src/Spec/hs-src/NOTICE b/docs/agda-spec/conformance-example/NOTICE similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/NOTICE rename to docs/agda-spec/conformance-example/NOTICE diff --git a/docs/agda-spec/src/Spec/hs-src/cabal.project b/docs/agda-spec/conformance-example/cabal.project similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/cabal.project rename to docs/agda-spec/conformance-example/cabal.project diff --git a/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal b/docs/agda-spec/conformance-example/conformance-example.cabal similarity index 79% rename from docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal rename to docs/agda-spec/conformance-example/conformance-example.cabal index 5af036424a..58321a38ec 100644 --- a/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal +++ b/docs/agda-spec/conformance-example/conformance-example.cabal @@ -1,8 +1,8 @@ cabal-version: 3.0 -name: cardano-consensus-executable-spec +name: conformance-example version: 0.1.0.0 -synopsis: Executable Formal Specification of Ouroboros Consensus -description: The Haskell code generated from the Agda executable formal specification of the consensus layer for the Ouroboros blockchain protocol +synopsis: Test programs for the executable formal specification of Ouroboros Consensus +description: Test programs that exercise the Haskell code generated from the Agda executable formal specification of the consensus layer for the Ouroboros blockchain protocol license: Apache-2.0 license-files: LICENSE @@ -34,7 +34,7 @@ test-suite test TickForecastSpec ChainHeadSpec build-depends: - cardano-consensus-executable-spec, + conformance-example, hspec, HUnit, text diff --git a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs b/docs/agda-spec/conformance-example/test/ChainHeadSpec.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs rename to docs/agda-spec/conformance-example/test/ChainHeadSpec.hs diff --git a/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs b/docs/agda-spec/conformance-example/test/OperationalCertificateSpec.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs rename to docs/agda-spec/conformance-example/test/OperationalCertificateSpec.hs diff --git a/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs b/docs/agda-spec/conformance-example/test/ProtocolSpec.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs rename to docs/agda-spec/conformance-example/test/ProtocolSpec.hs diff --git a/docs/agda-spec/src/Spec/hs-src/test/Spec.hs b/docs/agda-spec/conformance-example/test/Spec.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/test/Spec.hs rename to docs/agda-spec/conformance-example/test/Spec.hs diff --git a/docs/agda-spec/src/Spec/hs-src/test/TickForecastSpec.hs b/docs/agda-spec/conformance-example/test/TickForecastSpec.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/test/TickForecastSpec.hs rename to docs/agda-spec/conformance-example/test/TickForecastSpec.hs diff --git a/docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs b/docs/agda-spec/conformance-example/test/TickNonceSpec.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs rename to docs/agda-spec/conformance-example/test/TickNonceSpec.hs diff --git a/docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs b/docs/agda-spec/conformance-example/test/UpdateNonceSpec.hs similarity index 100% rename from docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs rename to docs/agda-spec/conformance-example/test/UpdateNonceSpec.hs diff --git a/docs/agda-spec/src/Makefile b/docs/agda-spec/src/Makefile index d2fe72f313..0c4e889cec 100644 --- a/docs/agda-spec/src/Makefile +++ b/docs/agda-spec/src/Makefile @@ -35,11 +35,11 @@ $(PDF_DIR)/$(PDF_NAME).pdf: $(LATEX_DIR)/Spec/PDF.tex $(latexFiles) $(PRE) # Agda -> Haskell define agdaToHs @echo "Generating $@" - $(eval CABAL_FILE=$(1).cabal) + $(eval CABAL_FILE=conformance-example.cabal) $(eval HS_DIST=$(HS_DIR)/Spec) mkdir -p $(HS_DIST) - cp -r Spec/hs-src/* $(HS_DIST)/ - cp Spec/hs-src/$(CABAL_FILE) $(HS_DIST)/ + cp -r ../conformance-example/* $(HS_DIST)/ + cp ../conformance-example/$(CABAL_FILE) $(HS_DIST)/ $(AGDA_RUN) -c --ghc-dont-call-ghc --compile-dir $(HS_DIST) $< find $(HS_DIST)/MAlonzo -name "*.hs" -print\ | sed "s#^$(HS_DIST)/# #;s#\.hs##;s#/#.#g"\ From df613e0be634148103c105e52b8c3611f61e9ec5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 25 Sep 2025 23:47:18 +0000 Subject: [PATCH 7/9] Relocate `GenError` and `Premises` to `std-lib-exts` --- .../Ext.agda => src-lib-exts/stdlib-meta/Reflection.agda} | 2 +- .../{src => src-lib-exts/stdlib-meta}/Tactic/GenError.agda | 2 +- .../{src => src-lib-exts/stdlib-meta}/Tactic/Premises.agda | 2 +- docs/agda-spec/src/Spec/ChainHead/Properties.agda | 2 +- docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda | 2 +- docs/agda-spec/src/Spec/Protocol/Properties.agda | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) rename docs/agda-spec/{src/Reflection/Ext.agda => src-lib-exts/stdlib-meta/Reflection.agda} (99%) rename docs/agda-spec/{src => src-lib-exts/stdlib-meta}/Tactic/GenError.agda (98%) rename docs/agda-spec/{src => src-lib-exts/stdlib-meta}/Tactic/Premises.agda (99%) diff --git a/docs/agda-spec/src/Reflection/Ext.agda b/docs/agda-spec/src-lib-exts/stdlib-meta/Reflection.agda similarity index 99% rename from docs/agda-spec/src/Reflection/Ext.agda rename to docs/agda-spec/src-lib-exts/stdlib-meta/Reflection.agda index c832d26ec3..c0a700c883 100644 --- a/docs/agda-spec/src/Reflection/Ext.agda +++ b/docs/agda-spec/src-lib-exts/stdlib-meta/Reflection.agda @@ -1,5 +1,5 @@ {-# OPTIONS --safe #-} -module Reflection.Ext where +module stdlib-meta.Reflection where open import Prelude hiding (Type) open import PreludeMeta diff --git a/docs/agda-spec/src/Tactic/GenError.agda b/docs/agda-spec/src-lib-exts/stdlib-meta/Tactic/GenError.agda similarity index 98% rename from docs/agda-spec/src/Tactic/GenError.agda rename to docs/agda-spec/src-lib-exts/stdlib-meta/Tactic/GenError.agda index caf2ee7755..6ea1f7a09d 100644 --- a/docs/agda-spec/src/Tactic/GenError.agda +++ b/docs/agda-spec/src-lib-exts/stdlib-meta/Tactic/GenError.agda @@ -5,7 +5,7 @@ -- genErrors: match on a negated conjunction and return the string of that type -------------------------------------------------------------------------------- -module Tactic.GenError where +module stdlib-meta.Tactic.GenError where open import Meta.Prelude open import Meta.Init diff --git a/docs/agda-spec/src/Tactic/Premises.agda b/docs/agda-spec/src-lib-exts/stdlib-meta/Tactic/Premises.agda similarity index 99% rename from docs/agda-spec/src/Tactic/Premises.agda rename to docs/agda-spec/src-lib-exts/stdlib-meta/Tactic/Premises.agda index b7e839f8c2..97a515bba0 100644 --- a/docs/agda-spec/src/Tactic/Premises.agda +++ b/docs/agda-spec/src-lib-exts/stdlib-meta/Tactic/Premises.agda @@ -1,6 +1,6 @@ {-# OPTIONS --safe #-} -- {-# OPTIONS -v tactic.premises:100 #-} -module Tactic.Premises where +module stdlib-meta.Tactic.Premises where open import Prelude hiding (Type) open import PreludeMeta diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda index 9b70e1cb84..b907d49fe0 100644 --- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda +++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda @@ -17,7 +17,7 @@ module Spec.ChainHead.Properties (rs : _) (open RationalExtStructure rs) where -open import Tactic.GenError +open import stdlib-meta.Tactic.GenError open import Ledger.Prelude open import Ledger.PParams using (PParams; ProtVer) open import Spec.TickForecast crypto es li diff --git a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda index 044ac19d28..254aae78c0 100644 --- a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda +++ b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda @@ -16,7 +16,7 @@ module Spec.OperationalCertificate.Properties open import Ledger.Prelude open import Data.Maybe.Relation.Unary.Any as M open import Spec.OperationalCertificate crypto nonces es bs af -open import Tactic.GenError using (genError) +open import stdlib-meta.Tactic.GenError using (genError) instance diff --git a/docs/agda-spec/src/Spec/Protocol/Properties.agda b/docs/agda-spec/src/Spec/Protocol/Properties.agda index 1bc08d5f5f..937d2b267d 100644 --- a/docs/agda-spec/src/Spec/Protocol/Properties.agda +++ b/docs/agda-spec/src/Spec/Protocol/Properties.agda @@ -17,7 +17,7 @@ module Spec.Protocol.Properties open import Data.Rational as ℚ using (1ℚ) open import Ledger.Prelude -open import Tactic.GenError +open import stdlib-meta.Tactic.GenError open import Spec.Protocol crypto nonces es bs af rs open import Spec.BaseTypes crypto using (OCertCounters; PoolDistr) open import Spec.UpdateNonce crypto nonces es From ec3a969271f08655222d3a084a270f3f3ad5a586 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 26 Sep 2025 17:38:58 +0000 Subject: [PATCH 8/9] Remove unnecessary `Interface\HasEmptySet` --- .../src/Interface/HasEmptySet/Instances.agda | 16 ---------------- 1 file changed, 16 deletions(-) delete mode 100644 docs/agda-spec/src/Interface/HasEmptySet/Instances.agda diff --git a/docs/agda-spec/src/Interface/HasEmptySet/Instances.agda b/docs/agda-spec/src/Interface/HasEmptySet/Instances.agda deleted file mode 100644 index 5141799e52..0000000000 --- a/docs/agda-spec/src/Interface/HasEmptySet/Instances.agda +++ /dev/null @@ -1,16 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Axiom.Set using (Theory) - -module Interface.HasEmptySet.Instances (th : Theory) where - -open import Interface.HasEmptySet -open Theory th renaming (Set to ℙ_; ∅ to ∅ˢ) -open import Axiom.Set.Map th - -instance - HasEmptySet-Set : {A : Set} → HasEmptySet (ℙ A) - HasEmptySet-Set = record { ∅ = ∅ˢ } - - HasEmptySet-Map : {A B : Set} → HasEmptySet (Map A B) - HasEmptySet-Map = record { ∅ = ∅ᵐ } From 907ba072bd2424b0a0c127d115f00fc7db85fd84 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 26 Sep 2025 18:05:04 +0000 Subject: [PATCH 9/9] Update `README.md` --- docs/agda-spec/README.md | 54 ++++++++++++++++++++-------------------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/docs/agda-spec/README.md b/docs/agda-spec/README.md index 58490d2da1..1065dbb897 100644 --- a/docs/agda-spec/README.md +++ b/docs/agda-spec/README.md @@ -8,47 +8,43 @@ The specification is both *formal* (meaning that is machine-checked and amenable The project is comprised by the following subdirectories: -* `Axiom`: The Agda set theory library +* `src`: Files comprising the formal specification -* `Data`: Extensions to the Agda standard library + - `Foreign`: General utilities to automatically generate Haskell code from Agda code -* `Foreign`: General utilities to automatically generate Haskell code from Agda code + - `Interface`: General-purpose type classes not included in the Agda standard library -* `Interface`: General-purpose type classes not included in the Agda standard library + - `InterfaceLibrary`: Interfaces exposed by other Cardano components, currently only for the Ledger Layer -* `InterfaceLibrary`: Interfaces exposed by other Cardano components, currently only for the Ledger Layer + - `Common`: Component-agnostic features (e.g. stake pool distributions) - - `Common`: Component-agnostic features (e.g. stake pool distributions) + - `Ledger`: Components borrowed from the Ledger specification, most of them actually not Ledger-specific (e.g. slots, epochs, cryptographic primitives) -* `Ledger`: Components borrowed from the Ledger specification, most of them actually not Ledger-specific (e.g. slots, epochs, cryptographic primitives) + - `latex`: Auxiliary $$\LaTeX$$-related files required to generate the PDF version of the specification (e.g. fonts, references and static content) -* `Reflection`: Extensions to the reflection support in the Agda standard library + - `Spec`: Root directory of the specification -* `Tactic`: General-purpose tactics not included in the Agda standard library + - `.lagda` (e.g. `TickNonce.lagda` for TICKN): The definition of `` in a human-readable format -* `latex`: Auxiliary $$\LaTeX$$-related files required to generate the PDF version of the specification (e.g. fonts, references and static content) + - `/Properties.agda` (e.g. `TickNonce/Properties.agda` for TICKN): Proofs of properties about ``. In particular, this file contains a proof that `` can be 'computed' by a given function. This means that we have an executable version of `` which is guaranteed to be correct -* `Spec`: Root directory of the specification + - `PDF.lagda`: Source Agda file from which the corresponding PDF file is generated - - `.lagda` (e.g. `TickNonce.lagda` for TICKN): The definition of `` in a human-readable format + - `Foreign`: Machinery required for the automatic generation of an executable (Haskell) version of the Agda specification - - `/Properties.agda` (e.g. `TickNonce/Properties.agda` for TICKN): Proofs of properties about ``. In particular, this file contains a proof that `` can be 'computed' by a given function. This means that we have an executable version of `` which is guaranteed to be correct + - `HSConsensus/.agda` (e.g. `HSConsensus/TickNonce.agda` for TICKN): Contains the code to automatically generate the Haskell types used by `` and a \*`Step` Haskell function to execute `` - - `PDF.lagda`: Source Agda file from which the corresponding PDF file is generated + - `ExternalFunctions.agda`: Automatically generates a Haskell record of 'external functions'. An external function is a function used by the Agda specification whose Haskell version should be provided by the calling environment. Dummy external functions are also available - - `Foreign`: Machinery required for the automatic generation of an executable (Haskell) version of the Agda specification + - `HSTypes.agda`: Generates Haskell versions for common Agda types used in the specification, such as sets and maps - - `HSConsensus/.agda` (e.g. `HSConsensus/TickNonce.agda` for TICKN): Contains the code to automatically generate the Haskell types used by `` and a \*`Step` Haskell function to execute `` + - `HSConsensus.agda`: Top-level Agda module from which the executable specification is generated - - `ExternalFunctions.agda`: Automatically generates a Haskell record of 'external functions'. An external function is a function used by the Agda specification whose Haskell version should be provided by the calling environment. Dummy external functions are also available +* `src-lib-exts`: Extensions to the Agda standard library (`stdlib`), the IOG prelude library (`iog-prelude`), etc - - `HSTypes.agda`: Generates Haskell versions for common Agda types used in the specification, such as sets and maps +* `conformance-example`: A Haskell test suite for the executable specification - - `HSConsensus.agda`: Top-level Agda module from which the executable specification is generated - - - `hs-src`: A Haskell test suite for the executable specification - - - `test/Spec.hs` (e.g. `test/TickNonceSpec.hs` for TICKN): A Haskell program that tests the executable version of `` + - `test/Spec.hs` (e.g. `test/TickNonceSpec.hs` for TICKN): A Haskell program that tests the executable version of `` ## Generating the PDF file @@ -132,22 +128,26 @@ It is possible to perform the above-mentioned tasks without the use of Nix, usin - Install [latexmk](https://ctan.org/pkg/latexmk/) and [XeTeX](https://xetex.sourceforge.net/) -- Install Agda version `2.7.0` (e.g. follow the instructions in +- Install Agda version `2.8.0` (e.g. follow the instructions in ) - In a folder ``, clone the dependencies and checkout the respective commits/tags: | *Dependency* | *Tag/commit* | |--------------------------------------------------------------------|--------------------------------------------| - | [agda-stdlib](https://github.com/agda/agda-stdlib) | `v2.1.1` | - | [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes) | `73f4da05aeea040fea4587629f9fd83a8f04e656` | - | [agda-stdlib-meta](https://github.com/agda/agda-stdlib-meta) | `v2.1.1` | + | [agda-stdlib](https://github.com/agda/agda-stdlib) | `v2.3` | + | [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes) | `v2.3` | + | [agda-stdlib-meta](https://github.com/agda/agda-stdlib-meta) | `v2.3` | + | [agda-sets](https://github.com/input-output-hk/agda-sets) | `31512b000317a577230e9ba5081b693801104851` | + | [iog-prelude](https://github.com/input-output-hk/iog-agda-prelude) | `e25670dcea694f321cbcd7a0bb704b82d5d7b266` | - Create a file `/libraries` with the following content: ``` /agda-stdlib/standard-library.agda-lib /agda-stdlib-classes/agda-stdlib-classes.agda-lib /agda-stdlib-meta/agda-stdlib-meta.agda-lib +/agda-sets/abstract-set-theory.agda-lib +/iog-prelude/iog-prelude.agda-lib ``` - Instead of `agda` use `agda --library-file /libraries`. For example, to typecheck `Everything.agda`: