From f4cd47fb7a9d1596c84d393a4db3597f52bc48f0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 19:08:50 +0000 Subject: [PATCH 01/31] `List.Relation.Unary.Any.Properties` --- src/Data/List/Relation/Unary/Any/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 479741fb93..76792578a3 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -42,7 +42,7 @@ open import Function.Related as Related using (Kind; Related; SK-sym) open import Level using (Level) open import Relation.Binary as B hiding (_⇔_) open import Relation.Binary.PropositionalEquality as P - using (_≡_; refl; inspect) + using (_≡_; refl) open import Relation.Unary as U using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_) open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no) @@ -172,9 +172,9 @@ any⁺ p (there {x = x} pxs) with p x ... | false = any⁺ p pxs any⁻ : ∀ (p : A → Bool) xs → T (any p xs) → Any (T ∘ p) xs -any⁻ p (x ∷ xs) px∷xs with p x | inspect p x -... | true | P.[ eq ] = here (Equivalence.from T-≡ ⟨$⟩ eq) -... | false | _ = there (any⁻ p xs px∷xs) +any⁻ p (x ∷ xs) px∷xs with p x in eq +... | true = here (Equivalence.from T-≡ ⟨$⟩ eq) +... | false = there (any⁻ p xs px∷xs) any⇔ : ∀ {p : A → Bool} → Any (T ∘ p) xs ⇔ T (any p xs) any⇔ = equivalence (any⁺ _) (any⁻ _ _) From f32505e364879a5d33c6677e1b6d1c522ce35304 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 19:11:33 +0000 Subject: [PATCH 02/31] `Vec.Relation.Unary.Any.Properties` --- src/Data/Vec/Relation/Unary/Any/Properties.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index 17040a4862..cfcb00b32e 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -333,12 +333,12 @@ module _ {P : Pred A p} where concat⁺∘concat⁻ : ∀ {n m} (xss : Vec (Vec A n) m) (p : Any P (concat xss)) → concat⁺ (concat⁻ xss p) ≡ p - concat⁺∘concat⁻ (xs ∷ xss) p with ++⁻ xs p | P.inspect (++⁻ xs) p - ... | inj₁ pxs | P.[ p=inj₁ ] - = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₁)) + concat⁺∘concat⁻ (xs ∷ xss) p with ++⁻ xs p in eq + ... | inj₁ pxs + = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym eq)) $ ++⁺∘++⁻ xs p - ... | inj₂ pxss | P.[ p=inj₂ ] rewrite concat⁺∘concat⁻ xss pxss - = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₂)) + ... | inj₂ pxss rewrite concat⁺∘concat⁻ xss pxss + = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym eq)) $ ++⁺∘++⁻ xs p concat⁻∘concat⁺ : ∀ {n m} {xss : Vec (Vec A n) m} (p : Any (Any P) xss) → From 0510b05c861be5d2d11c1f3b707baf47a58546d5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 19:15:58 +0000 Subject: [PATCH 03/31] `Rational.Properties` --- src/Data/Rational/Properties.agda | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 805b2786a8..abf5963ef4 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -1304,24 +1304,24 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i ------------------------------------------------------------------------ p≤q⇒p⊔q≡q : p ≤ q → p ⊔ q ≡ q -p≤q⇒p⊔q≡q {p@record{}} {q@record{}} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊔q≡q {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) p≥q⇒p⊔q≡p : p ≥ q → p ⊔ q ≡ p -p≥q⇒p⊔q≡p {p@record{}} {q@record{}} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) -... | false | [ p≤q ] = refl +p≥q⇒p⊔q≡p {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q +... | true = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) +... | false = refl p≤q⇒p⊓q≡p : p ≤ q → p ⊓ q ≡ p -p≤q⇒p⊓q≡p {p@record{}} {q@record{}} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊓q≡p {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) p≥q⇒p⊓q≡q : p ≥ q → p ⊓ q ≡ q -p≥q⇒p⊓q≡q {p@record{}} {q@record{}} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q -... | false | [ p≤q ] = refl +p≥q⇒p⊓q≡q {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q +... | true = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q +... | false = refl ⊓-operator : MinOperator ≤-totalPreorder ⊓-operator = record From 45d675db3c0c6082c2c7acd36c1dea0944c90948 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 19:28:55 +0000 Subject: [PATCH 04/31] `List.Properties` but `Fin.Properties` a problem: 'panic: pattern violation' --- src/Data/Fin/Properties.agda | 6 +++--- src/Data/List/Properties.agda | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index cb19ae7ab4..8323068109 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -612,13 +612,13 @@ remQuot-combine {suc n} {k} (suc i) j rewrite splitAt-↑ʳ k (n ℕ.* k) (com cong (Data.Product.map₁ suc) (remQuot-combine i j) combine-remQuot : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (remQuot {n} k i) ≡ i -combine-remQuot {suc n} k i with splitAt k i | P.inspect (splitAt k) i -... | inj₁ j | P.[ eq ] = begin +combine-remQuot {suc n} k i with splitAt k i in eq +... | inj₁ j = begin join k (n ℕ.* k) (inj₁ j) ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩ join k (n ℕ.* k) (splitAt k i) ≡⟨ join-splitAt k (n ℕ.* k) i ⟩ i ∎ where open ≡-Reasoning -... | inj₂ j | P.[ eq ] = begin +... | inj₂ j = begin k ↑ʳ (uncurry combine (remQuot {n} k j)) ≡⟨ cong (k ↑ʳ_) (combine-remQuot {n} k j) ⟩ join k (n ℕ.* k) (inj₂ j) ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩ join k (n ℕ.* k) (splitAt k i) ≡⟨ join-splitAt k (n ℕ.* k) i ⟩ diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 304eca74dc..4db334333a 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -856,9 +856,9 @@ module _ {P : Pred A p} (P? : Decidable P) where filter-idem : filter P? ∘ filter P? ≗ filter P? filter-idem [] = refl - filter-idem (x ∷ xs) with does (P? x) | inspect does (P? x) - ... | false | _ = filter-idem xs - ... | true | P.[ eq ] rewrite eq = cong (x ∷_) (filter-idem xs) + filter-idem (x ∷ xs) with does (P? x) in eq + ... | false = filter-idem xs + ... | true rewrite eq = cong (x ∷_) (filter-idem xs) filter-++ : ∀ xs ys → filter P? (xs ++ ys) ≡ filter P? xs ++ filter P? ys filter-++ [] ys = refl From 10141964f0663ff4d265cf4641641cda34927aea Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 19:33:21 +0000 Subject: [PATCH 05/31] unused appeals to `inspect` --- .../Relation/Binary/Permutation/Propositional/Properties.agda | 2 +- .../List/Relation/Binary/Permutation/Setoid/Properties.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 7ac00bac5b..21b7625aa7 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -29,7 +29,7 @@ open import Level using (Level) open import Relation.Unary using (Pred) open import Relation.Binary open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_ ; refl ; cong; cong₂; _≢_; inspect) + using (_≡_ ; refl ; cong; cong₂; _≢_) open import Relation.Nullary open PermutationReasoning diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index fe2a4620ae..23de930bdd 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -37,7 +37,7 @@ open import Level using (Level; _⊔_) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_; inspect) + using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_) open import Relation.Nullary.Decidable using (yes; no; does) open import Relation.Nullary.Negation using (contradiction) From c9e9f34bf6dc3e2d83e9a543aa43de58ebb31967 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 19:50:07 +0000 Subject: [PATCH 06/31] `Codata.Sized.Colist.Properties` --- src/Codata/Sized/Colist/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda index 17f6a70ff2..4ed10b13de 100644 --- a/src/Codata/Sized/Colist/Properties.agda +++ b/src/Codata/Sized/Colist/Properties.agda @@ -144,10 +144,10 @@ module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where scanl-unfold : ∀ nil a → i ⊢ scanl cons nil (unfold alg a) ≈ nil ∷ (λ where .force → unfold alg′ (a , nil)) - scanl-unfold nil a with alg a | Eq.inspect alg a - ... | nothing | [ eq ] = Eq.refl ∷ λ { .force → + scanl-unfold nil a with alg a in eq + ... | nothing = Eq.refl ∷ λ { .force → sym (fromEq (unfold-nothing (Maybeₚ.map-nothing eq))) } - ... | just (a′ , b) | [ eq ] = Eq.refl ∷ λ { .force → begin + ... | just (a′ , b) = Eq.refl ∷ λ { .force → begin scanl cons (cons nil b) (unfold alg a′) ≈⟨ scanl-unfold (cons nil b) a′ ⟩ (cons nil b ∷ _) From b4a665e07b2f46d15293f4e5507cac48cec441ae Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 23:22:04 +0000 Subject: [PATCH 07/31] a new proof of the errant lemma, plus two new lemmas to enable it --- src/Data/Fin/Properties.agda | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 8323068109..bd27a0e973 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -562,10 +562,20 @@ splitAt-↑ˡ : ∀ m i n → splitAt m (i ↑ˡ n) ≡ inj₁ i splitAt-↑ˡ (suc m) zero n = refl splitAt-↑ˡ (suc m) (suc i) n rewrite splitAt-↑ˡ m i n = refl +splitAt-↑ˡ⁻¹ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i +splitAt-↑ˡ⁻¹ {suc m} {n} {0F} {.0F} refl = refl +splitAt-↑ˡ⁻¹ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ +... | inj₁ k with refl ← eq = cong suc (splitAt-↑ˡ⁻¹ {i = i} {j = k} EQ) + splitAt-↑ʳ : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i splitAt-↑ʳ zero n i = refl splitAt-↑ʳ (suc m) n i rewrite splitAt-↑ʳ m n i = refl +splitAt-↑ʳ⁻¹ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i +splitAt-↑ʳ⁻¹ {zero} {n} {i} {j} refl = refl +splitAt-↑ʳ⁻¹ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ +... | inj₂ k with refl ← eq = cong suc (splitAt-↑ʳ⁻¹ {i = i} {j = k} EQ) + splitAt-join : ∀ m n i → splitAt m (join m n i) ≡ i splitAt-join m n (inj₁ x) = splitAt-↑ˡ m x n splitAt-join m n (inj₂ y) = splitAt-↑ʳ m n y @@ -677,7 +687,7 @@ combine-injective : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) → combine-injective i j k l cᵢⱼ≡cₖₗ = combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ , combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ - +{- combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i combine-surjective {m} {n} i with remQuot {m} n i | P.inspect (remQuot {m} n) i ... | j , k | P.[ eq ] = j , k , (begin @@ -685,6 +695,13 @@ combine-surjective {m} {n} i with remQuot {m} n i | P.inspect (remQuot {m} n) i uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ i ∎) where open ≡-Reasoning +-} +combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i +combine-surjective {m = suc m} {n} i with splitAt n i in eq +... | inj₁ j rewrite (splitAt-↑ˡ _ j (m ℕ.* n)) + = zero , j , splitAt-↑ˡ⁻¹ eq +... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjective {m} {n} k + = suc j₁ , k₁ , splitAt-↑ʳ⁻¹ eq ------------------------------------------------------------------------ -- Bundles From 4e93ab4038fda627556c5c9fd4718a55a1f8eaa7 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 15 Feb 2023 12:42:05 +0000 Subject: [PATCH 08/31] a bit more commentary on the bug --- src/Data/Fin/Properties.agda | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index bd27a0e973..d0d62c6981 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -687,13 +687,20 @@ combine-injective : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) → combine-injective i j k l cᵢⱼ≡cₖₗ = combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ , combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ + {- -combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i -combine-surjective {m} {n} i with remQuot {m} n i | P.inspect (remQuot {m} n) i -... | j , k | P.[ eq ] = j , k , (begin +-- [agda issue #6507](https://github.com/agda/agda/issues/6507) +-- +-- The use of `with remQuot {m} n i in eq` causes Agda to signal +-- "Panic: uncaught pattern violation" +-- even *before* attempting to decompose the pattern variable `p` + +combine-surjectiveOLD : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i +combine-surjectiveOLD {m} {n} i with remQuot {m} n i in eq +... | p = {!j , k , (begin combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ - i ∎) + i ∎)!} where open ≡-Reasoning -} combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i From 1b4daa645d8e33fc90fb0434d8af620a5f1e6b66 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 15 Feb 2023 16:54:38 +0000 Subject: [PATCH 09/31] shorter, if not minimal, working (counter)example --- src/Data/Fin/MWE.agda | 250 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 250 insertions(+) create mode 100644 src/Data/Fin/MWE.agda diff --git a/src/Data/Fin/MWE.agda b/src/Data/Fin/MWE.agda new file mode 100644 index 0000000000..8e02c20cdf --- /dev/null +++ b/src/Data/Fin/MWE.agda @@ -0,0 +1,250 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties related to Fin, and operations making use of these +-- properties (or other properties not available in Data.Fin) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Fin.MWE where + +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Fin.Base +open import Data.Fin.Patterns +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; z) +open import Data.Product.Properties using (,-injective) +open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) +open import Data.Sum.Properties using ([,]-map; [,]-∘) +open import Function.Base using (_∘_; id; _$_; flip) +open import Level using (Level) +open import Relation.Binary as B hiding (Decidable; _⇔_) +open import Relation.Binary.PropositionalEquality as P + using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning) + +private + variable + a : Level + A : Set a + m n o : ℕ + i j : Fin n + +------------------------------------------------------------------------ +-- suc +------------------------------------------------------------------------ + +suc-injective : Fin.suc i ≡ suc j → i ≡ j +suc-injective refl = refl + +------------------------------------------------------------------------ +-- toℕ +------------------------------------------------------------------------ + +toℕ-injective : toℕ i ≡ toℕ j → i ≡ j +toℕ-injective {zero} {} {} _ +toℕ-injective {suc n} {zero} {zero} eq = refl +toℕ-injective {suc n} {suc i} {suc j} eq = + cong suc (toℕ-injective (cong ℕ.pred eq)) + +------------------------------------------------------------------------ +-- toℕ-↑ˡ: "i" ↑ˡ n = "i" in Fin (m + n) +------------------------------------------------------------------------ + +toℕ-↑ˡ : ∀ (i : Fin m) n → toℕ (i ↑ˡ n) ≡ toℕ i +toℕ-↑ˡ zero n = refl +toℕ-↑ˡ (suc i) n = cong suc (toℕ-↑ˡ i n) + +------------------------------------------------------------------------ +-- toℕ-↑ʳ: n ↑ʳ "i" = "n + i" in Fin (n + m) +------------------------------------------------------------------------ + +toℕ-↑ʳ : ∀ n (i : Fin m) → toℕ (n ↑ʳ i) ≡ n ℕ.+ toℕ i +toℕ-↑ʳ zero i = refl +toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i) + +------------------------------------------------------------------------ +-- toℕ and the ordering relations +------------------------------------------------------------------------ + +toℕ≤pred[n] : ∀ (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n +toℕ≤pred[n] zero = z≤n +toℕ≤pred[n] (suc {n = suc n} i) = s≤s (toℕ≤pred[n] i) + +toℕ (λ()) (λ()) z i≮j i≢j j (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s _ _ i>k with () ← <⇒≢ (combine-monoˡ-< l j i>k) (sym cᵢⱼ≡cₖₗ) + +combine-injectiveʳ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) → + combine i j ≡ combine k l → j ≡ l +combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ with combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ +... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin + n ℕ.* toℕ i ℕ.+ toℕ j ≡˘⟨ toℕ-combine i j ⟩ + toℕ (combine i j) ≡⟨ cong toℕ cᵢⱼ≡cₖₗ ⟩ + toℕ (combine i l) ≡⟨ toℕ-combine i l ⟩ + n ℕ.* toℕ i ℕ.+ toℕ l ∎)) + where open ≡-Reasoning + +combine-injective : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) → + combine i j ≡ combine k l → i ≡ k × j ≡ l +combine-injective i j k l cᵢⱼ≡cₖₗ = + combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ , + combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ + +combine-surjectiveOLD : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i +combine-surjectiveOLD {m} {n} i with remQuot {m} n i | P.inspect (remQuot {m} n) i +... | j , k | P.[ eq ] = j , k , (begin + combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ + uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ + i ∎) + where open ≡-Reasoning + +combine-surjectiveNEW : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i +combine-surjectiveNEW {m = suc m} {n} i with splitAt n i in eq +... | inj₁ j rewrite (splitAt-↑ˡ _ j (m ℕ.* n)) + = zero , j , splitAt-↑ˡ⁻¹ eq +... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjectiveNEW {m} {n} k + = suc j₁ , k₁ , splitAt-↑ʳ⁻¹ eq + +combine-surjectiveBUG : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i +combine-surjectiveBUG {m} {n} i with remQuot {m} n i in eq +{- +... | j , k | P.[ eq ] = j , k , (begin + combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ + uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ + i ∎) + where open ≡-Reasoning +-} +... | p = ? From 57b90e8912d8f43462ac059972ea31cbf8a34fb4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 21 Feb 2023 13:31:19 +0000 Subject: [PATCH 10/31] working under Agda-2.6.2.2 --- CHANGELOG.md | 3 +++ src/Data/Fin/Properties.agda | 33 +++++++++++++-------------------- 2 files changed, 16 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1c23ceb055..8e3e126d87 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1797,6 +1797,9 @@ Other minor changes toℕ-cancel-≤ : toℕ i ℕ.≤ toℕ j → i ≤ j toℕ-cancel-< : toℕ i ℕ.< toℕ j → i < j + splitAt⁻¹-↑ˡ : splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i + splitAt⁻¹-↑ʳ : splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i + toℕ-combine : toℕ (combine i j) ≡ k ℕ.* toℕ i ℕ.+ toℕ j combine-injectiveˡ : combine i j ≡ combine k l → i ≡ k combine-injectiveʳ : combine i j ≡ combine k l → j ≡ l diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index d0d62c6981..46410dac67 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -562,19 +562,19 @@ splitAt-↑ˡ : ∀ m i n → splitAt m (i ↑ˡ n) ≡ inj₁ i splitAt-↑ˡ (suc m) zero n = refl splitAt-↑ˡ (suc m) (suc i) n rewrite splitAt-↑ˡ m i n = refl -splitAt-↑ˡ⁻¹ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i -splitAt-↑ˡ⁻¹ {suc m} {n} {0F} {.0F} refl = refl -splitAt-↑ˡ⁻¹ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ -... | inj₁ k with refl ← eq = cong suc (splitAt-↑ˡ⁻¹ {i = i} {j = k} EQ) +splitAt⁻¹-↑ˡ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i +splitAt⁻¹-↑ˡ {suc m} {n} {0F} {.0F} refl = refl +splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ +... | inj₁ k with refl ← eq = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} EQ) splitAt-↑ʳ : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i splitAt-↑ʳ zero n i = refl splitAt-↑ʳ (suc m) n i rewrite splitAt-↑ʳ m n i = refl -splitAt-↑ʳ⁻¹ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i -splitAt-↑ʳ⁻¹ {zero} {n} {i} {j} refl = refl -splitAt-↑ʳ⁻¹ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ -... | inj₂ k with refl ← eq = cong suc (splitAt-↑ʳ⁻¹ {i = i} {j = k} EQ) +splitAt⁻¹-↑ʳ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i +splitAt⁻¹-↑ʳ {zero} {n} {i} {j} refl = refl +splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ +... | inj₂ k with refl ← eq = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} EQ) splitAt-join : ∀ m n i → splitAt m (join m n i) ≡ i splitAt-join m n (inj₁ x) = splitAt-↑ˡ m x n @@ -688,27 +688,20 @@ combine-injective i j k l cᵢⱼ≡cₖₗ = combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ , combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ -{- --- [agda issue #6507](https://github.com/agda/agda/issues/6507) --- --- The use of `with remQuot {m} n i in eq` causes Agda to signal --- "Panic: uncaught pattern violation" --- even *before* attempting to decompose the pattern variable `p` - combine-surjectiveOLD : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i combine-surjectiveOLD {m} {n} i with remQuot {m} n i in eq -... | p = {!j , k , (begin +... | j , k = j , k , (begin combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ - i ∎)!} + i ∎) where open ≡-Reasoning --} + combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i combine-surjective {m = suc m} {n} i with splitAt n i in eq ... | inj₁ j rewrite (splitAt-↑ˡ _ j (m ℕ.* n)) - = zero , j , splitAt-↑ˡ⁻¹ eq + = zero , j , splitAt⁻¹-↑ˡ eq ... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjective {m} {n} k - = suc j₁ , k₁ , splitAt-↑ʳ⁻¹ eq + = suc j₁ , k₁ , splitAt⁻¹-↑ʳ eq ------------------------------------------------------------------------ -- Bundles From 4cb44ad24bb61199e2fd916b56b6a3d98be509f5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 21 Feb 2023 13:40:39 +0000 Subject: [PATCH 11/31] removed MWE; solution working under 2.6.2.2 --- src/Data/Fin/MWE.agda | 250 ----------------------------------- src/Data/Fin/Properties.agda | 10 +- 2 files changed, 5 insertions(+), 255 deletions(-) delete mode 100644 src/Data/Fin/MWE.agda diff --git a/src/Data/Fin/MWE.agda b/src/Data/Fin/MWE.agda deleted file mode 100644 index 8e02c20cdf..0000000000 --- a/src/Data/Fin/MWE.agda +++ /dev/null @@ -1,250 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Properties related to Fin, and operations making use of these --- properties (or other properties not available in Data.Fin) ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Data.Fin.MWE where - -open import Data.Empty using (⊥; ⊥-elim) -open import Data.Fin.Base -open import Data.Fin.Patterns -open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; z) -open import Data.Product.Properties using (,-injective) -open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) -open import Data.Sum.Properties using ([,]-map; [,]-∘) -open import Function.Base using (_∘_; id; _$_; flip) -open import Level using (Level) -open import Relation.Binary as B hiding (Decidable; _⇔_) -open import Relation.Binary.PropositionalEquality as P - using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning) - -private - variable - a : Level - A : Set a - m n o : ℕ - i j : Fin n - ------------------------------------------------------------------------- --- suc ------------------------------------------------------------------------- - -suc-injective : Fin.suc i ≡ suc j → i ≡ j -suc-injective refl = refl - ------------------------------------------------------------------------- --- toℕ ------------------------------------------------------------------------- - -toℕ-injective : toℕ i ≡ toℕ j → i ≡ j -toℕ-injective {zero} {} {} _ -toℕ-injective {suc n} {zero} {zero} eq = refl -toℕ-injective {suc n} {suc i} {suc j} eq = - cong suc (toℕ-injective (cong ℕ.pred eq)) - ------------------------------------------------------------------------- --- toℕ-↑ˡ: "i" ↑ˡ n = "i" in Fin (m + n) ------------------------------------------------------------------------- - -toℕ-↑ˡ : ∀ (i : Fin m) n → toℕ (i ↑ˡ n) ≡ toℕ i -toℕ-↑ˡ zero n = refl -toℕ-↑ˡ (suc i) n = cong suc (toℕ-↑ˡ i n) - ------------------------------------------------------------------------- --- toℕ-↑ʳ: n ↑ʳ "i" = "n + i" in Fin (n + m) ------------------------------------------------------------------------- - -toℕ-↑ʳ : ∀ n (i : Fin m) → toℕ (n ↑ʳ i) ≡ n ℕ.+ toℕ i -toℕ-↑ʳ zero i = refl -toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i) - ------------------------------------------------------------------------- --- toℕ and the ordering relations ------------------------------------------------------------------------- - -toℕ≤pred[n] : ∀ (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n -toℕ≤pred[n] zero = z≤n -toℕ≤pred[n] (suc {n = suc n} i) = s≤s (toℕ≤pred[n] i) - -toℕ (λ()) (λ()) z i≮j i≢j j (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s _ _ i>k with () ← <⇒≢ (combine-monoˡ-< l j i>k) (sym cᵢⱼ≡cₖₗ) - -combine-injectiveʳ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) → - combine i j ≡ combine k l → j ≡ l -combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ with combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ -... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin - n ℕ.* toℕ i ℕ.+ toℕ j ≡˘⟨ toℕ-combine i j ⟩ - toℕ (combine i j) ≡⟨ cong toℕ cᵢⱼ≡cₖₗ ⟩ - toℕ (combine i l) ≡⟨ toℕ-combine i l ⟩ - n ℕ.* toℕ i ℕ.+ toℕ l ∎)) - where open ≡-Reasoning - -combine-injective : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) → - combine i j ≡ combine k l → i ≡ k × j ≡ l -combine-injective i j k l cᵢⱼ≡cₖₗ = - combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ , - combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ - -combine-surjectiveOLD : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i -combine-surjectiveOLD {m} {n} i with remQuot {m} n i | P.inspect (remQuot {m} n) i -... | j , k | P.[ eq ] = j , k , (begin - combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ - uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ - i ∎) - where open ≡-Reasoning - -combine-surjectiveNEW : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i -combine-surjectiveNEW {m = suc m} {n} i with splitAt n i in eq -... | inj₁ j rewrite (splitAt-↑ˡ _ j (m ℕ.* n)) - = zero , j , splitAt-↑ˡ⁻¹ eq -... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjectiveNEW {m} {n} k - = suc j₁ , k₁ , splitAt-↑ʳ⁻¹ eq - -combine-surjectiveBUG : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i -combine-surjectiveBUG {m} {n} i with remQuot {m} n i in eq -{- -... | j , k | P.[ eq ] = j , k , (begin - combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ - uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ - i ∎) - where open ≡-Reasoning --} -... | p = ? diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 46410dac67..708c20c56e 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -688,19 +688,19 @@ combine-injective i j k l cᵢⱼ≡cₖₗ = combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ , combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ -combine-surjectiveOLD : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i -combine-surjectiveOLD {m} {n} i with remQuot {m} n i in eq +combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i +combine-surjective {m} {n} i with remQuot {m} n i in eq ... | j , k = j , k , (begin combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ i ∎) where open ≡-Reasoning -combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i -combine-surjective {m = suc m} {n} i with splitAt n i in eq +combine-surjectiveNEW : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i +combine-surjectiveNEW {m = suc m} {n} i with splitAt n i in eq ... | inj₁ j rewrite (splitAt-↑ˡ _ j (m ℕ.* n)) = zero , j , splitAt⁻¹-↑ˡ eq -... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjective {m} {n} k +... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjectiveNEW {m} {n} k = suc j₁ , k₁ , splitAt⁻¹-↑ʳ eq ------------------------------------------------------------------------ From 960a64d9360b9393fa17abedf9e75e290a6c99cb Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Tue, 21 Feb 2023 18:14:07 +0000 Subject: [PATCH 12/31] [ ci ] upgrade Agda version --- .github/workflows/ci-ubuntu.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index f2dffff775..5c0c4aec92 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -74,12 +74,12 @@ jobs: if [[ '${{ github.ref }}' == 'refs/heads/master' \ || '${{ github.base_ref }}' == 'master' ]]; then # Pick Agda version for master - echo "AGDA_COMMIT=tags/v2.6.2" >> $GITHUB_ENV; + echo "AGDA_COMMIT=tags/v2.6.2.2" >> $GITHUB_ENV; echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \ || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental - echo "AGDA_COMMIT=tags/v2.6.2" >> $GITHUB_ENV; + echo "AGDA_COMMIT=tags/v2.6.2.2" >> $GITHUB_ENV; echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV fi From d36d730b33d1d7ebf5bd0ab42460fa86c17b5a9d Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Tue, 21 Feb 2023 18:21:42 +0000 Subject: [PATCH 13/31] [ ci ] bump haskell-ci's ubuntu dep --- .github/workflows/haskell-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index f83b527faa..6dcf86c4c6 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -25,7 +25,7 @@ on: jobs: linux: name: Haskell-CI - Linux - ${{ matrix.compiler }} - runs-on: ubuntu-18.04 + runs-on: ubuntu-latest timeout-minutes: 60 container: From 3ff33cc89481126cf330d826232e6cf746f1e44c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 22 Feb 2023 13:21:51 +0000 Subject: [PATCH 14/31] added a new `README`; delted the old one --- README/{Inspect.agda => WithIn.agda} | 77 ++++++++++------------------ 1 file changed, 27 insertions(+), 50 deletions(-) rename README/{Inspect.agda => WithIn.agda} (54%) diff --git a/README/Inspect.agda b/README/WithIn.agda similarity index 54% rename from README/Inspect.agda rename to README/WithIn.agda index 22f11e5d4d..a3eb1addfc 100644 --- a/README/Inspect.agda +++ b/README/WithIn.agda @@ -1,13 +1,12 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Explaining how to use the inspect idiom and elaborating on the way --- it is implemented in the standard library. +-- Explaining how to use the `with ... in ...` idiom. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -module README.Inspect where +module README.WithIn where open import Data.Nat.Base open import Data.Nat.Properties @@ -15,7 +14,7 @@ open import Data.Product open import Relation.Binary.PropositionalEquality ------------------------------------------------------------------------ --- Using inspect +-- Using `with ... in ...` -- We start with the definition of a (silly) predicate: `Plus m n p` states -- that `m + n` is equal to `p` in a rather convoluted way. Crucially, it @@ -60,8 +59,8 @@ plus-eq-+ (suc m) n = refl -- when we would have wanted a more precise type of the form: -- `plus-eq-aux : ∀ m n p → m + n ≡ p → Plus-eq m n p`. --- This is where we can use `inspect`. By using `with f x | inspect f x`, --- we get both a `y` which is the result of `f x` and a proof that `f x ≡ y`. +-- This is where we can use `with ... in ...`. By using `with f x in eq`, we get +-- *both* a `y` which is the result of `f x` *and* a proof `eq` that `f x ≡ y`. -- Splitting on the result of `m + n`, we get two cases: -- 1. `m ≡ 0 × n ≡ 0` under the assumption that `m + n ≡ zero` @@ -70,18 +69,20 @@ plus-eq-+ (suc m) n = refl -- The first one can be discharged using lemmas from Data.Nat.Properties and -- the second one is trivial. -plus-eq-with : ∀ m n → Plus-eq m n (m + n) -plus-eq-with m n with m + n | inspect (m +_) n -... | zero | [ m+n≡0 ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 -... | suc p | [ m+n≡1+p ] = m+n≡1+p +plus-eq-with-in : ∀ m n → Plus-eq m n (m + n) +plus-eq-with-in m n with m + n in eq +... | zero = m+n≡0⇒m≡0 m eq , m+n≡0⇒n≡0 m eq +... | suc p = eq +-- NB. What has been lost? the new syntax binds `eq` once and for all, +-- whereas the old `with ... inspect` syntax allowed pattern-matching on +-- *different names* for the equation in each possible branch after a `with`. ------------------------------------------------------------------------ --- Understanding the implementation of inspect +-- Understanding the implementation of `with ... in ...` --- So why is it that we have to go through the record type `Reveal_·_is_` --- and the ̀inspect` function? The fact is: we don't have to if we write --- our own auxiliary lemma: +-- What happens if we try to avoid use of the ̀with ... in ...` syntax? +-- The fact is: we don't have to if we write our own auxiliary lemma: plus-eq-aux : ∀ m n → Plus-eq m n (m + n) plus-eq-aux m n = aux m n (m + n) refl where @@ -90,43 +91,19 @@ plus-eq-aux m n = aux m n (m + n) refl where aux m n zero m+n≡0 = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 aux m n (suc p) m+n≡1+p = m+n≡1+p --- The problem is that when we write ̀with f x | pr`, `with` decides to call `y` --- the result `f x` and to replace *all* of the occurences of `f x` in the type --- of `pr` with `y`. That is to say that if we were to write: +-- NB. Here we can choose alternative names in each branch of `aux` +-- for the proof of the auxiliary hypothesis `m + n ≡ p` --- plus-eq-naïve : ∀ m n → Plus-eq m n (m + n) --- plus-eq-naïve m n with m + n | refl {x = m + n} --- ... | p | eq = {!!} +-- We could likewise emulate the general behaviour of `with ... in ...` +-- using an auxiliary function as follows, using the `with p ← ...` syntax +-- to bind the subexpression `m + n` to (pattern) variable `p`: --- then `with` would abstract `m + n` as `p` on *both* sides of the equality --- proven by `refl` thus giving us the following goal with an extra, useless, --- assumption: +plus-eq-with-in-aux : ∀ m n → Plus-eq m n (m + n) +plus-eq-with-in-aux m n with p ← m + n in eq = aux m n p eq where --- 1. `Plus-eq m n p` under the assumption that `p ≡ p` - --- So how does `inspect` work? The standard library uses a more general version --- of the following type and function: - -record MyReveal_·_is_ (f : ℕ → ℕ) (x y : ℕ) : Set where - constructor [_] - field eq : f x ≡ y - -my-inspect : ∀ f n → MyReveal f · n is (f n) -my-inspect f n = [ refl ] - --- Given that `inspect` has the type `∀ f n → Reveal f · n is (f n)`, when we --- write `with f n | inspect f n`, the only `f n` that can be abstracted in the --- type of `inspect f n` is the third argument to `Reveal_·_is_`. - --- That is to say that the auxiliary definition generated looks like this: - -plus-eq-reveal : ∀ m n → Plus-eq m n (m + n) -plus-eq-reveal m n = aux m n (m + n) (my-inspect (m +_) n) where - - aux : ∀ m n p → MyReveal (m +_) · n is p → Plus-eq m n p - aux m n zero [ m+n≡0 ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 - aux m n (suc p) [ m+n≡1+p ] = m+n≡1+p + aux : ∀ m n p → m + n ≡ p → Plus-eq m n p + aux m n zero m+n≡0 = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 + aux m n (suc p) m+n≡1+p = m+n≡1+p --- At the cost of having to unwrap the constructor `[_]` around the equality --- we care about, we can keep relying on `with` and avoid having to roll out --- handwritten auxiliary definitions. +-- That is, more or less, what the Agda-generated definition corresponding to +-- `plus-eq-with-in` would look like. From 2ba26d4433dc71bc05cb2bc225e6d201c727c755 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 22 Feb 2023 15:42:23 +0000 Subject: [PATCH 15/31] added deprecation warnings; updated `CHANGELOG` --- CHANGELOG.md | 9 ++++ .../Binary/PropositionalEquality.agda | 51 ++++++++++++------- 2 files changed, 42 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8e3e126d87..97c29c56d1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1285,6 +1285,15 @@ Deprecated names * This fixes the fact we had picked the wrong name originally. The erased modality corresponds to @0 whereas the irrelevance one corresponds to `.`. +### Deprecated `Relation.Binary.PropositionalEquality.inspect` + in favour of `with ... in ...` syntax (issue #1580; PRs #1630, #1930) + +* In `Relation.Binary.PropositionalEquality` + both the record type `Reveal_·_is_` + and its principal mode of use, `inspect`, + have been deprecated in favour of the new `with ... in ...` syntax. + + New modules ----------- diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 4c7e71b2cd..0582a70b95 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -60,24 +60,6 @@ _≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B) (A → Setoid.Carrier B) → setoid A ⟶ B →-to-⟶ = :→-to-Π ------------------------------------------------------------------------- --- Inspect - --- Inspect can be used when you want to pattern match on the result r --- of some expression e, and you also need to "remember" that r ≡ e. - --- See README.Inspect for an explanation of how/why to use this. - -record Reveal_·_is_ {A : Set a} {B : A → Set b} - (f : (x : A) → B x) (x : A) (y : B x) : - Set (a ⊔ b) where - constructor [_] - field eq : f x ≡ y - -inspect : ∀ {A : Set a} {B : A → Set b} - (f : (x : A) → B x) (x : A) → Reveal f · x is f x -inspect f x = [ refl ] - ------------------------------------------------------------------------ -- Propositionality @@ -120,3 +102,36 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y ≢-≟-identity = dec-no (x ≟ y) + + + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +record Reveal_·_is_ {A : Set a} {B : A → Set b} + (f : (x : A) → B x) (x : A) (y : B x) : + Set (a ⊔ b) where + constructor [_] + field eq : f x ≡ y + +inspect : ∀ {A : Set a} {B : A → Set b} + (f : (x : A) → B x) (x : A) → Reveal f · x is f x +inspect f x = [ refl ] + +{-# WARNING_ON_USAGE Reveal_·_is_ +"Warning: Reveal_·_is_ was deprecated in v2.0. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality instead. +See also README.WithIn" +#-} +{-# WARNING_ON_USAGE inspect +"Warning: inspect was deprecated in v2.0. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality instead. +See also README.WithIn" +#-} + From 883018aa35605f922b2ef4488e84bf7ecd8da417 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 22 Feb 2023 16:05:37 +0000 Subject: [PATCH 16/31] fix-whitespace; updated to version 2.6.2.2 in `CHANGELOG` --- CHANGELOG.md | 2 +- README/WithIn.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 97c29c56d1..acc7a2466d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ Version 2.0-dev =============== -The library has been tested using Agda 2.6.2. +The library has been tested using Agda 2.6.2.2. Highlights ---------- diff --git a/README/WithIn.agda b/README/WithIn.agda index a3eb1addfc..0e103c60bf 100644 --- a/README/WithIn.agda +++ b/README/WithIn.agda @@ -76,7 +76,7 @@ plus-eq-with-in m n with m + n in eq -- NB. What has been lost? the new syntax binds `eq` once and for all, -- whereas the old `with ... inspect` syntax allowed pattern-matching on --- *different names* for the equation in each possible branch after a `with`. +-- *different names* for the equation in each possible branch after a `with`. ------------------------------------------------------------------------ -- Understanding the implementation of `with ... in ...` From 383f59c409c7771793333b053813f16d14f8b992 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 22 Feb 2023 16:14:28 +0000 Subject: [PATCH 17/31] updated `README` and `CHANGELOG` to reflect version 2.6.2.2 --- README.agda | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/README.agda b/README.agda index 2d87cb56d2..313daec5df 100644 --- a/README.agda +++ b/README.agda @@ -12,13 +12,14 @@ module README where -- Liang-Ting Chen, Dominique Devriese, Dan Doel, Érdi Gergő, -- Zack Grannan, Helmut Grohne, Simon Foster, Liyang Hu, Jason Hu, -- Patrik Jansson, Alan Jeffrey, Wen Kokke, Evgeny Kotelnikov, --- Sergei Meshveliani, Eric Mertens, Darin Morrison, Guilhem Moulin, --- Shin-Cheng Mu, Ulf Norell, Noriyuki Ohkawa, Nicolas Pouillard, --- Andrés Sicard-Ramírez, Lex van der Stoep, Sandro Stucki, Milo Turner, --- Noam Zeilberger and other anonymous contributors. +-- James McKinna, Sergei Meshveliani, Eric Mertens, Darin Morrison, +-- Guilhem Moulin, Shin-Cheng Mu, Ulf Norell, Noriyuki Ohkawa, +-- Nicolas Pouillard, Andrés Sicard-Ramírez, Lex van der Stoep, +-- Sandro Stucki, Milo Turner, Noam Zeilberger +-- and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.2. +-- This version of the library has been tested using Agda 2.6.2.2. -- The library comes with a .agda-lib file, for use with the library -- management system. @@ -236,11 +237,6 @@ import README.Debug.Trace import README.Nary --- Explaining the inspect idiom: use case, equivalent handwritten --- auxiliary definitions, and implementation details. - -import README.Inspect - -- Explaining how to use the automatic solvers import README.Tactic.MonoidSolver @@ -266,6 +262,11 @@ import README.Text.Regex import README.Text.Tabular +-- Explaining the `with ... in ...` syntax: use case, equivalent handwritten +-- auxiliary definitions, and implementation details. + +import README.WithIn + ------------------------------------------------------------------------ -- All library modules ------------------------------------------------------------------------ From f17885727172ef7fbcd5f4b25ec0e82d42a86833 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 23 Apr 2023 19:41:08 +0100 Subject: [PATCH 18/31] removed redundant parentheses --- src/Data/Fin/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 20da3d0075..c3c30e1f8a 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -698,7 +698,7 @@ combine-surjective {m} {n} i with remQuot {m} n i in eq combine-surjectiveNEW : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i combine-surjectiveNEW {m = suc m} {n} i with splitAt n i in eq -... | inj₁ j rewrite (splitAt-↑ˡ _ j (m ℕ.* n)) +... | inj₁ j rewrite splitAt-↑ˡ _ j (m ℕ.* n) = zero , j , splitAt⁻¹-↑ˡ eq ... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjectiveNEW {m} {n} k = suc j₁ , k₁ , splitAt⁻¹-↑ʳ eq From 4c5034266cc252a71b15d7fdf3c30c9a179ec56b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 09:22:01 +0100 Subject: [PATCH 19/31] removed `combine-surjectiveNEW`; renamed `EQ` proofs --- src/Data/Fin/Properties.agda | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index f2e9b1bc2d..d7a963f9fd 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -564,8 +564,8 @@ splitAt-↑ˡ (suc m) (suc i) n rewrite splitAt-↑ˡ m i n = refl splitAt⁻¹-↑ˡ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i splitAt⁻¹-↑ˡ {suc m} {n} {0F} {.0F} refl = refl -splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ -... | inj₁ k with refl ← eq = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} EQ) +splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₁[j] +... | inj₁ k with refl ← eq = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} splitAt[m][i]≡inj₁[j]) splitAt-↑ʳ : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i splitAt-↑ʳ zero n i = refl @@ -573,8 +573,8 @@ splitAt-↑ʳ (suc m) n i rewrite splitAt-↑ʳ m n i = refl splitAt⁻¹-↑ʳ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i splitAt⁻¹-↑ʳ {zero} {n} {i} {j} refl = refl -splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq with splitAt m i in EQ -... | inj₂ k with refl ← eq = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} EQ) +splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₂[k] +... | inj₂ k with refl ← eq = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} splitAt[m][i]≡inj₂[k]) splitAt-join : ∀ m n i → splitAt m (join m n i) ≡ i splitAt-join m n (inj₁ x) = splitAt-↑ˡ m x n @@ -696,13 +696,6 @@ combine-surjective {m} {n} i with remQuot {m} n i in eq i ∎) where open ≡-Reasoning -combine-surjectiveNEW : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i -combine-surjectiveNEW {m = suc m} {n} i with splitAt n i in eq -... | inj₁ j rewrite splitAt-↑ˡ _ j (m ℕ.* n) - = zero , j , splitAt⁻¹-↑ˡ eq -... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjectiveNEW {m} {n} k - = suc j₁ , k₁ , splitAt⁻¹-↑ʳ eq - ------------------------------------------------------------------------ -- Bundles From 0722e6e88a6c8c86ffdf726de10d8764410f3e6a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 09:25:07 +0100 Subject: [PATCH 20/31] `CHANGELOG` --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 346a354e66..4fc7aa0b6d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ Version 2.0-dev =============== -The library has been tested using Agda 2.6.2.2. +The library has been tested using Agda 2.6.3. Highlights ---------- From daeae9c4c455e51d62db9f21194d68361e534b35 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 09:27:07 +0100 Subject: [PATCH 21/31] `Agda 2.6.3` --- README.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.agda b/README.agda index 313daec5df..6949c27ab8 100644 --- a/README.agda +++ b/README.agda @@ -19,7 +19,7 @@ module README where -- and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.2.2. +-- This version of the library has been tested using Agda 2.6.3. -- The library comes with a .agda-lib file, for use with the library -- management system. From 3d846659eac3814b72422363deb3db89628fa1ae Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 10:04:42 +0100 Subject: [PATCH 22/31] link to Agda documentation --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4fc7aa0b6d..119890627f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1305,7 +1305,7 @@ Deprecated names both the record type `Reveal_·_is_` and its principal mode of use, `inspect`, have been deprecated in favour of the new `with ... in ...` syntax. - + See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#id16) New modules ----------- From 5f5dc678cb3e2871da29bb4a0b6a43b590e851ca Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 10:09:15 +0100 Subject: [PATCH 23/31] corrected link to Agda documentation --- CHANGELOG.md | 2 +- src/Relation/Binary/PropositionalEquality.agda | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 119890627f..36f8ee04b5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1305,7 +1305,7 @@ Deprecated names both the record type `Reveal_·_is_` and its principal mode of use, `inspect`, have been deprecated in favour of the new `with ... in ...` syntax. - See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#id16) + See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality) New modules ----------- diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 3d3a3787d2..6adfac91b3 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -126,12 +126,10 @@ inspect f x = [ refl ] {-# WARNING_ON_USAGE Reveal_·_is_ "Warning: Reveal_·_is_ was deprecated in v2.0. -Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality instead. -See also README.WithIn" +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead. #-} {-# WARNING_ON_USAGE inspect "Warning: inspect was deprecated in v2.0. -Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality instead. -See also README.WithIn" +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead. #-} From d040c7e389b5447bedd999baa1eb160c038e29ed Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 10:24:31 +0100 Subject: [PATCH 24/31] restored `README.Inspect`; removed `README.WithIn` --- README/{WithIn.agda => Inspect.agda} | 80 ++++++++++++++++++---------- 1 file changed, 53 insertions(+), 27 deletions(-) rename README/{WithIn.agda => Inspect.agda} (54%) diff --git a/README/WithIn.agda b/README/Inspect.agda similarity index 54% rename from README/WithIn.agda rename to README/Inspect.agda index 4269c517c0..79a9439217 100644 --- a/README/WithIn.agda +++ b/README/Inspect.agda @@ -1,12 +1,16 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Explaining how to use the `with ... in ...` idiom. +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} -module README.WithIn where +module README.Inspect where + +{-# WARNING_ON_IMPORT +"README.Inspect was deprecated in v2.0. +#-} open import Data.Nat.Base open import Data.Nat.Properties @@ -14,7 +18,7 @@ open import Data.Product open import Relation.Binary.PropositionalEquality ------------------------------------------------------------------------ --- Using `with ... in ...` +-- Using inspect -- We start with the definition of a (silly) predicate: `Plus m n p` states -- that `m + n` is equal to `p` in a rather convoluted way. Crucially, it @@ -59,8 +63,8 @@ plus-eq-+ (suc m) n = refl -- when we would have wanted a more precise type of the form: -- `plus-eq-aux : ∀ m n p → m + n ≡ p → Plus-eq m n p`. --- This is where we can use `with ... in ...`. By using `with f x in eq`, we get --- *both* a `y` which is the result of `f x` *and* a proof `eq` that `f x ≡ y`. +-- This is where we can use `inspect`. By using `with f x | inspect f x`, +-- we get both a `y` which is the result of `f x` and a proof that `f x ≡ y`. -- Splitting on the result of `m + n`, we get two cases: -- 1. `m ≡ 0 × n ≡ 0` under the assumption that `m + n ≡ zero` @@ -69,20 +73,18 @@ plus-eq-+ (suc m) n = refl -- The first one can be discharged using lemmas from Data.Nat.Properties and -- the second one is trivial. -plus-eq-with-in : ∀ m n → Plus-eq m n (m + n) -plus-eq-with-in m n with m + n in eq -... | zero = m+n≡0⇒m≡0 m eq , m+n≡0⇒n≡0 m eq -... | suc p = eq +plus-eq-with : ∀ m n → Plus-eq m n (m + n) +plus-eq-with m n with m + n | inspect (m +_) n +... | zero | [ m+n≡0 ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 +... | suc p | [ m+n≡1+p ] = m+n≡1+p --- NB. What has been lost? the new syntax binds `eq` once and for all, --- whereas the old `with ... inspect` syntax allowed pattern-matching on --- *different names* for the equation in each possible branch after a `with`. ------------------------------------------------------------------------ --- Understanding the implementation of `with ... in ...` +-- Understanding the implementation of inspect --- What happens if we try to avoid use of the ̀with ... in ...` syntax? --- The fact is: we don't have to if we write our own auxiliary lemma: +-- So why is it that we have to go through the record type `Reveal_·_is_` +-- and the ̀inspect` function? The fact is: we don't have to if we write +-- our own auxiliary lemma: plus-eq-aux : ∀ m n → Plus-eq m n (m + n) plus-eq-aux m n = aux m n (m + n) refl where @@ -91,19 +93,43 @@ plus-eq-aux m n = aux m n (m + n) refl where aux m n zero m+n≡0 = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 aux m n (suc p) m+n≡1+p = m+n≡1+p --- NB. Here we can choose alternative names in each branch of `aux` --- for the proof of the auxiliary hypothesis `m + n ≡ p` +-- The problem is that when we write ̀with f x | pr`, `with` decides to call `y` +-- the result `f x` and to replace *all* of the occurences of `f x` in the type +-- of `pr` with `y`. That is to say that if we were to write: --- We could likewise emulate the general behaviour of `with ... in ...` --- using an auxiliary function as follows, using the `with p ← ...` syntax --- to bind the subexpression `m + n` to (pattern) variable `p`: +-- plus-eq-naïve : ∀ m n → Plus-eq m n (m + n) +-- plus-eq-naïve m n with m + n | refl {x = m + n} +-- ... | p | eq = {!!} -plus-eq-with-in-aux : ∀ m n → Plus-eq m n (m + n) -plus-eq-with-in-aux m n with p ← m + n in eq = aux m n p eq where +-- then `with` would abstract `m + n` as `p` on *both* sides of the equality +-- proven by `refl` thus giving us the following goal with an extra, useless, +-- assumption: - aux : ∀ m n p → m + n ≡ p → Plus-eq m n p - aux m n zero m+n≡0 = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 - aux m n (suc p) m+n≡1+p = m+n≡1+p +-- 1. `Plus-eq m n p` under the assumption that `p ≡ p` + +-- So how does `inspect` work? The standard library uses a more general version +-- of the following type and function: + +record MyReveal_·_is_ (f : ℕ → ℕ) (x y : ℕ) : Set where + constructor [_] + field eq : f x ≡ y + +my-inspect : ∀ f n → MyReveal f · n is (f n) +my-inspect f n = [ refl ] + +-- Given that `inspect` has the type `∀ f n → Reveal f · n is (f n)`, when we +-- write `with f n | inspect f n`, the only `f n` that can be abstracted in the +-- type of `inspect f n` is the third argument to `Reveal_·_is_`. + +-- That is to say that the auxiliary definition generated looks like this: + +plus-eq-reveal : ∀ m n → Plus-eq m n (m + n) +plus-eq-reveal m n = aux m n (m + n) (my-inspect (m +_) n) where + + aux : ∀ m n p → MyReveal (m +_) · n is p → Plus-eq m n p + aux m n zero [ m+n≡0 ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0 + aux m n (suc p) [ m+n≡1+p ] = m+n≡1+p --- That is, more or less, what the Agda-generated definition corresponding to --- `plus-eq-with-in` would look like. +-- At the cost of having to unwrap the constructor `[_]` around the equality +-- we care about, we can keep relying on `with` and avoid having to roll out +-- handwritten auxiliary definitions. From 92bd3a43cdfa25548c204a8c41f44bde8e01d834 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 11:09:10 +0100 Subject: [PATCH 25/31] fixed missing quote marks in deprecation warnings --- src/Relation/Binary/PropositionalEquality.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 6adfac91b3..4764635449 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -126,10 +126,10 @@ inspect f x = [ refl ] {-# WARNING_ON_USAGE Reveal_·_is_ "Warning: Reveal_·_is_ was deprecated in v2.0. -Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead." #-} {-# WARNING_ON_USAGE inspect "Warning: inspect was deprecated in v2.0. -Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead." #-} From 8d8ba254c1e95c375b898ae64a92f355181d95c8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 11:55:39 +0100 Subject: [PATCH 26/31] fixed `README` --- README.agda | 4 ---- 1 file changed, 4 deletions(-) diff --git a/README.agda b/README.agda index 6949c27ab8..ab12e226c0 100644 --- a/README.agda +++ b/README.agda @@ -262,10 +262,6 @@ import README.Text.Regex import README.Text.Tabular --- Explaining the `with ... in ...` syntax: use case, equivalent handwritten --- auxiliary definitions, and implementation details. - -import README.WithIn ------------------------------------------------------------------------ -- All library modules From 169583a3846248bf8ac077216f2d4b15aff9b6a0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 15:13:36 +0100 Subject: [PATCH 27/31] fixed `README.Inspect` --- README.agda | 2 +- README/Inspect.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.agda b/README.agda index ab12e226c0..350641e06e 100644 --- a/README.agda +++ b/README.agda @@ -262,7 +262,7 @@ import README.Text.Regex import README.Text.Tabular - +import README.Inspect ------------------------------------------------------------------------ -- All library modules ------------------------------------------------------------------------ diff --git a/README/Inspect.agda b/README/Inspect.agda index 79a9439217..64213410af 100644 --- a/README/Inspect.agda +++ b/README/Inspect.agda @@ -9,7 +9,7 @@ module README.Inspect where {-# WARNING_ON_IMPORT -"README.Inspect was deprecated in v2.0. +"README.Inspect was deprecated in v2.0." #-} open import Data.Nat.Base From d1b72183f9158cfd416936b127458195c23b686e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 15:14:19 +0100 Subject: [PATCH 28/31] fixed `README`, again --- README.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.agda b/README.agda index 350641e06e..ab12e226c0 100644 --- a/README.agda +++ b/README.agda @@ -262,7 +262,7 @@ import README.Text.Regex import README.Text.Tabular -import README.Inspect + ------------------------------------------------------------------------ -- All library modules ------------------------------------------------------------------------ From f883ab96895fa436515aa7bf40b59e3426a58fec Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 15:21:11 +0100 Subject: [PATCH 29/31] `fix-whitespace` --- README/Inspect.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README/Inspect.agda b/README/Inspect.agda index 64213410af..cff492d008 100644 --- a/README/Inspect.agda +++ b/README/Inspect.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- This module is DEPRECATED. +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} From c744b1cbefe420e478286f8204f67c2c3358bf1f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 14 May 2023 09:43:02 +0100 Subject: [PATCH 30/31] (vertical) whitespace --- README.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.agda b/README.agda index ab12e226c0..350641e06e 100644 --- a/README.agda +++ b/README.agda @@ -262,7 +262,7 @@ import README.Text.Regex import README.Text.Tabular - +import README.Inspect ------------------------------------------------------------------------ -- All library modules ------------------------------------------------------------------------ From eea641d63a1fedf2add7eea46a043436a20304c9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 14 May 2023 09:47:16 +0100 Subject: [PATCH 31/31] unsaved changes --- README.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/README.agda b/README.agda index 350641e06e..6fee0aeffa 100644 --- a/README.agda +++ b/README.agda @@ -262,7 +262,6 @@ import README.Text.Regex import README.Text.Tabular -import README.Inspect ------------------------------------------------------------------------ -- All library modules ------------------------------------------------------------------------