Skip to content

Commit 3186ad6

Browse files
Move ≡-Reasoning from Core to Properties and implement using syntax (#2159)
1 parent cc0172d commit 3186ad6

File tree

22 files changed

+70
-50
lines changed

22 files changed

+70
-50
lines changed

CHANGELOG.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1238,6 +1238,12 @@ Major improvements
12381238
pre-existing `Reasoning` module in just a couple of lines
12391239
(e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`)
12401240

1241+
* One pre-requisite for that is that `≡-Reasoning` has been moved from
1242+
`Relation.Binary.PropositionalEquality.Core` (which shouldn't be
1243+
imported anyway as it's a `Core` module) to
1244+
`Relation.Binary.PropositionalEquality.Properties`.
1245+
It is still exported by `Relation.Binary.PropositionalEquality`.
1246+
12411247
Deprecated modules
12421248
------------------
12431249

src/Codata/Guarded/Stream/Properties.agda

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ open import Data.Vec.Base as Vec using (Vec; _∷_)
2121
open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_)
2222
open import Level using (Level)
2323
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong; cong₂)
24+
open import Relation.Binary.PropositionalEquality.Properties
25+
using (module ≡-Reasoning)
2426

2527
private
2628
variable
@@ -218,7 +220,7 @@ lookup-transpose n (as ∷ ass) = begin
218220
lookup as n ∷ lookup (transpose ass) n ≡⟨ cong (lookup as n ∷_) (lookup-transpose n ass) ⟩
219221
lookup as n ∷ List.map (flip lookup n) ass ≡⟨⟩
220222
List.map (flip lookup n) (as ∷ ass) ∎
221-
where open P.≡-Reasoning
223+
where open ≡-Reasoning
222224

223225
lookup-transpose⁺ : n (ass : List⁺ (Stream A))
224226
lookup (transpose⁺ ass) n ≡ List⁺.map (flip lookup n) ass
@@ -228,7 +230,7 @@ lookup-transpose⁺ n (as ∷ ass) = begin
228230
lookup as n ∷ lookup (transpose ass) n ≡⟨ cong (lookup as n ∷_) (lookup-transpose n ass) ⟩
229231
lookup as n ∷ List.map (flip lookup n) ass ≡⟨⟩
230232
List⁺.map (flip lookup n) (as ∷ ass) ∎
231-
where open P.≡-Reasoning
233+
where open ≡-Reasoning
232234

233235
lookup-tails : n (as : Stream A) lookup (tails as) n ≈ ℕ.iterate tail as n
234236
lookup-tails zero as = B.refl

src/Codata/Musical/Colist/Infinite-merge.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,8 @@ open import Level
2626
open import Relation.Unary using (Pred)
2727
import Induction.WellFounded as WF
2828
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
29+
open import Relation.Binary.PropositionalEquality.Properties
30+
using (module ≡-Reasoning)
2931
import Relation.Binary.Construct.On as On
3032

3133
private
@@ -132,7 +134,7 @@ merge xss = ⟦ merge′ xss ⟧P
132134
Any-merge : xss Any P (merge xss) ↔ Any (λ { (x , xs) P x ⊎ Any P xs }) xss
133135
Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂ ∘ to xss)
134136
where
135-
open P.≡-Reasoning
137+
open ≡-Reasoning
136138

137139
-- The from function.
138140

src/Codata/Sized/Stream/Properties.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ open import Data.Vec.Base as Vec using (_∷_)
2525

2626
open import Function.Base using (id; _$_; _∘′_; const)
2727
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_)
28+
open import Relation.Binary.PropositionalEquality.Properties
29+
using (module ≡-Reasoning)
2830

2931
private
3032
variable
@@ -116,7 +118,7 @@ lookup-iterate-identity (suc n) f a = begin
116118
lookup (iterate f (f a)) n ≡⟨ lookup-iterate-identity n f (f a) ⟩
117119
fold (f a) f n ≡⟨ fold-pull a f (const ∘′ f) (f a) P.refl (λ _ P.refl) n ⟩
118120
f (fold a f n) ≡⟨⟩
119-
fold a f (suc n) ∎ where open P.≡-Reasoning
121+
fold a f (suc n) ∎ where open ≡-Reasoning
120122

121123
------------------------------------------------------------------------
122124
-- DEPRECATED

src/Data/Fin/Relation/Unary/Top.agda

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ module Data.Fin.Relation.Unary.Top where
1616
open import Data.Nat.Base using (ℕ; zero; suc)
1717
open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁)
1818
open import Relation.Binary.PropositionalEquality.Core
19+
open import Relation.Binary.PropositionalEquality.Properties
20+
using (module ≡-Reasoning)
1921

2022
private
2123
variable

src/Data/Fin/Substitution/Lemmas.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,11 @@ import Data.Vec.Properties as VecProp
1616
open import Function.Base as Fun using (_∘_; _$_; flip)
1717
open import Relation.Binary.PropositionalEquality.Core as PropEq
1818
using (_≡_; refl; sym; cong; cong₂)
19+
open import Relation.Binary.PropositionalEquality.Properties
20+
using (module ≡-Reasoning)
1921
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
2022
using (Star; ε; _◅_; _▻_)
21-
open PropEq.≡-Reasoning
23+
open ≡-Reasoning
2224
open import Level using (Level; _⊔_)
2325
open import Relation.Unary using (Pred)
2426

src/Data/List/Countdown.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,8 @@ open import Relation.Nullary
3131
open import Relation.Nullary.Decidable using (dec-true; dec-false)
3232
open import Relation.Binary.PropositionalEquality.Core as PropEq
3333
using (_≡_; _≢_; refl; cong)
34-
open PropEq.≡-Reasoning
3534
import Relation.Binary.PropositionalEquality.Properties as PropEq
35+
open PropEq.≡-Reasoning
3636

3737
private
3838
open module D = DecSetoid D

src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010

1111
module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where
1212

13-
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong; subst; module ≡-Reasoning)
13+
open import Relation.Binary.PropositionalEquality
14+
using (_≡_; refl; sym; cong; subst; module ≡-Reasoning)
1415
open ≡-Reasoning
1516

1617
open import Data.List.Base using (List; []; _∷_; [_])

src/Data/List/Relation/Ternary/Interleaving/Properties.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,9 @@ open import Data.List.Relation.Ternary.Interleaving hiding (map)
1616
open import Function.Base using (_$_)
1717
open import Relation.Binary.Core using (REL)
1818
open import Relation.Binary.PropositionalEquality.Core
19-
using (_≡_; refl; sym; cong; module ≡-Reasoning)
19+
using (_≡_; refl; sym; cong)
20+
open import Relation.Binary.PropositionalEquality.Properties
21+
using (module ≡-Reasoning)
2022
open ≡-Reasoning
2123

2224
------------------------------------------------------------------------

src/Data/List/Relation/Unary/Any/Properties.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,8 @@ open import Relation.Binary.Core using (Rel; REL)
4343
open import Relation.Binary.Definitions as B
4444
open import Relation.Binary.PropositionalEquality.Core as P
4545
using (_≡_; refl)
46+
open import Relation.Binary.PropositionalEquality.Properties
47+
using (module ≡-Reasoning)
4648
open import Relation.Unary as U
4749
using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
4850
open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no)
@@ -219,7 +221,7 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
219221
(Any P xs × Any Q ys) ↔ Any (λ x Any (λ y P x × Q y) ys) xs
220222
×↔ {P = P} {Q = Q} {xs} {ys} = mk↔ₛ′ Any-×⁺ Any-×⁻ to∘from from∘to
221223
where
222-
open P.≡-Reasoning
224+
open ≡-Reasoning
223225

224226
from∘to : pq Any-×⁻ (Any-×⁺ pq) ≡ pq
225227
from∘to (p , q) =

src/Data/Nat/Coprimality.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ open import Data.Product.Base as Prod
2020
open import Function.Base using (_∘_)
2121
open import Level using (0ℓ)
2222
open import Relation.Binary.PropositionalEquality.Core as P
23-
using (_≡_; _≢_; refl; trans; cong; subst; module ≡-Reasoning)
23+
using (_≡_; _≢_; refl; trans; cong; subst)
2424
open import Relation.Nullary as Nullary hiding (recompute)
2525
open import Relation.Nullary.Negation using (contradiction)
2626
open import Relation.Binary.Core using (Rel)

src/Data/Nat/GCD.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ open import Induction.Lexicographic using (_⊗_; [_⊗_])
2424
open import Relation.Binary.Definitions using (tri<; tri>; tri≈; Symmetric)
2525
open import Relation.Binary.PropositionalEquality.Core as P
2626
using (_≡_; _≢_; subst; cong)
27+
open import Relation.Binary.PropositionalEquality.Properties
28+
using (module ≡-Reasoning)
2729
open import Relation.Nullary.Decidable using (Dec)
2830
open import Relation.Nullary.Negation using (contradiction)
2931
import Relation.Nullary.Decidable as Dec
@@ -190,7 +192,7 @@ c*gcd[m,n]≡gcd[cm,cn] c@(suc _) m n = begin
190192
c * gcd m n ≡⟨ cong (c *_) (P.sym (gcd[cm,cn]/c≡gcd[m,n] c m n)) ⟩
191193
c * (gcd (c * m) (c * n) / c) ≡⟨ m*[n/m]≡n (gcd-greatest (m∣m*n m) (m∣m*n n)) ⟩
192194
gcd (c * m) (c * n) ∎
193-
where open P.≡-Reasoning
195+
where open ≡-Reasoning
194196

195197
gcd[m,n]≤n : m n .{{_ : NonZero n}} gcd m n ≤ n
196198
gcd[m,n]≤n m n = ∣⇒≤ (gcd[m,n]∣n m n)

src/Data/Nat/LCM.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,9 @@ open import Data.Nat.GCD
1818
open import Data.Product.Base using (_×_; _,_; uncurry′; ∃)
1919
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
2020
open import Relation.Binary.PropositionalEquality.Core as P
21-
using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
21+
using (_≡_; refl; sym; trans; cong; cong₂)
22+
open import Relation.Binary.PropositionalEquality.Properties
23+
using (module ≡-Reasoning)
2224
open import Relation.Nullary.Decidable using (False; fromWitnessFalse)
2325

2426
private

src/Data/String/Unsafe.agda

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,11 @@ open import Data.Product.Base using (proj₂)
1616
open import Data.String.Base
1717
open import Function.Base using (_∘′_)
1818

19-
open import Relation.Binary.PropositionalEquality.Core; open ≡-Reasoning
19+
open import Relation.Binary.PropositionalEquality.Core
20+
open import Relation.Binary.PropositionalEquality.Properties
21+
using (module ≡-Reasoning)
2022
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)
23+
open ≡-Reasoning
2124

2225
------------------------------------------------------------------------
2326
-- Properties of tail

src/Data/Vec/Bounded/Base.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ open import Function.Base using (_∘_; id; _$_)
2222
open import Level using (Level)
2323
open import Relation.Nullary.Decidable.Core using (recompute)
2424
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
25+
open import Relation.Binary.PropositionalEquality.Properties
26+
using (module ≡-Reasoning)
2527

2628
private
2729
variable
@@ -66,7 +68,7 @@ private
6668
m + (⌈ k /2⌉ + ⌊ k /2⌋) ≡⟨ P.cong (m +_) (ℕₚ.+-comm ⌈ k /2⌉ ⌊ k /2⌋) ⟩
6769
m + (⌊ k /2⌋ + ⌈ k /2⌉) ≡⟨ P.cong (m +_) (ℕₚ.⌊n/2⌋+⌈n/2⌉≡n k) ⟩
6870
m + k ≡⟨ eq ⟩
69-
n ∎ where open P.≡-Reasoning
71+
n ∎ where open ≡-Reasoning
7072

7173
padBoth : {n} A A Vec≤ A n Vec A n
7274
padBoth aₗ aᵣ as@(vs , m≤n)

src/Data/Vec/Recursive/Properties.agda

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ open import Data.Vec.Recursive
1515
open import Data.Vec.Base using (Vec; _∷_)
1616
open import Function.Bundles using (_↔_; mk↔ₛ′)
1717
open import Relation.Binary.PropositionalEquality.Core as P
18+
open import Relation.Binary.PropositionalEquality.Properties
19+
using (module ≡-Reasoning)
1820
open ≡-Reasoning
1921

2022
private

src/Data/Vec/Relation/Binary/Equality/Cast.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,9 @@ open import Data.Vec.Base
1818
open import Relation.Binary.Core using (REL; _⇒_)
1919
open import Relation.Binary.Definitions using (Sym; Trans)
2020
open import Relation.Binary.PropositionalEquality.Core
21-
using (_≡_; refl; trans; sym; cong; module ≡-Reasoning)
21+
using (_≡_; refl; trans; sym; cong)
22+
open import Relation.Binary.PropositionalEquality.Properties
23+
using (module ≡-Reasoning)
2224

2325
private
2426
variable

src/Effect/Applicative/Indexed.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ open import Data.Product.Base using (_×_; _,_)
1616
open import Function.Base
1717
open import Level
1818
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
19+
open import Relation.Binary.PropositionalEquality.Properties
20+
using (module ≡-Reasoning)
1921

2022
private
2123
variable
@@ -111,4 +113,4 @@ record Morphism {I : Set i} {F₁ F₂ : IFun I f}
111113
op (A₁._⊛_ (A₁.pure f) x) ≡⟨ op-⊛ _ _ ⟩
112114
A₂._⊛_ (op (A₁.pure f)) (op x) ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl ⟩
113115
A₂._⊛_ (A₂.pure f) (op x) ∎
114-
where open P.≡-Reasoning
116+
where open ≡-Reasoning

src/Function/Related/TypeIsomorphisms.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ open import Function.Related.Propositional
2929
import Function.Construct.Identity as Identity
3030
open import Relation.Binary hiding (_⇔_)
3131
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
32+
open import Relation.Binary.PropositionalEquality.Properties
33+
using (module ≡-Reasoning)
3234
open import Relation.Nullary.Reflects using (invert)
3335
open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ)
3436
import Relation.Nullary.Indexed as I
@@ -284,7 +286,7 @@ private
284286
from C↔D (to C↔D (f (from A↔B (to A↔B x)))) ≡⟨ strictlyInverseʳ C↔D _ ⟩
285287
f (from A↔B (to A↔B x)) ≡⟨ P.cong f $ strictlyInverseʳ A↔B x ⟩
286288
f x ∎)
287-
where open Inverse; open P.≡-Reasoning
289+
where open Inverse; open ≡-Reasoning
288290

289291
→-cong : Extensionality a c Extensionality b d
290292
{k} {A : Set a} {B : Set b} {C : Set c} {D : Set d}

src/Relation/Binary/PropositionalEquality/Core.agda

Lines changed: 0 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -91,35 +91,3 @@ resp₂ _∼_ = respʳ _∼_ , respˡ _∼_
9191

9292
≢-sym : Symmetric {A = A} _≢_
9393
≢-sym x≢y = x≢y ∘ sym
94-
95-
------------------------------------------------------------------------
96-
-- Convenient syntax for equational reasoning
97-
98-
-- This is a special instance of `Relation.Binary.Reasoning.Setoid`.
99-
-- Rather than instantiating the latter with (setoid A), we reimplement
100-
-- equation chains from scratch since then goals are printed much more
101-
-- readably.
102-
103-
module ≡-Reasoning {A : Set a} where
104-
105-
infix 3 _∎
106-
infixr 2 _≡⟨⟩_ step-≡ step-≡˘
107-
infix 1 begin_
108-
109-
begin_ : {x y : A} x ≡ y x ≡ y
110-
begin_ x≡y = x≡y
111-
112-
_≡⟨⟩_ : (x {y} : A) x ≡ y x ≡ y
113-
_ ≡⟨⟩ x≡y = x≡y
114-
115-
step-≡ : (x {y z} : A) y ≡ z x ≡ y x ≡ z
116-
step-≡ _ y≡z x≡y = trans x≡y y≡z
117-
118-
step-≡˘ : (x {y z} : A) y ≡ z y ≡ x x ≡ z
119-
step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z
120-
121-
_∎ : (x : A) x ≡ x
122-
_∎ _ = refl
123-
124-
syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
125-
syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

src/Relation/Binary/PropositionalEquality/Properties.agda

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ open import Relation.Binary.Definitions
2323
import Relation.Binary.Properties.Setoid as Setoid
2424
open import Relation.Binary.PropositionalEquality.Core
2525
open import Relation.Unary using (Pred)
26+
open import Relation.Binary.Reasoning.Syntax
27+
2628

2729
private
2830
variable
@@ -188,3 +190,16 @@ preorder A = Setoid.≈-preorder (setoid A)
188190

189191
poset : Set a Poset _ _ _
190192
poset A = Setoid.≈-poset (setoid A)
193+
194+
------------------------------------------------------------------------
195+
-- Reasoning
196+
197+
-- This is a special instance of `Relation.Binary.Reasoning.Setoid`.
198+
-- Rather than instantiating the latter with (setoid A), we reimplement
199+
-- equation chains from scratch since then goals are printed much more
200+
-- readably.
201+
module ≡-Reasoning {a} {A : Set a} where
202+
203+
open begin-syntax {A = A} _≡_ id public
204+
open ≡-syntax {A = A} _≡_ trans public
205+
open end-syntax {A = A} _≡_ refl public

src/Relation/Binary/Reasoning/Syntax.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ open import Relation.Binary.PropositionalEquality.Core as P
2222
-- Relation/Binary/HeterogeneousEquality
2323
-- Effect/Monad/Partiality
2424
-- Effect/Monad/Partiality/All
25-
-- Relation/Binary/PropositionalEquality/Core
2625
-- Codata/Guarded/Stream/Relation/Binary/Pointwise
2726
-- Codata/Sized/Stream/Bisimilarity
2827
-- Function/Reasoning

0 commit comments

Comments
 (0)