Skip to content

Commit 33811e5

Browse files
MatthewDaggittjamesmckinna
authored andcommitted
Move ≡-Reasoning from Core to Properties and implement using syntax (agda#2159)
1 parent ef66f77 commit 33811e5

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) =

0 commit comments

Comments
 (0)