From ee5adcb505173a16ec7bdbb81ec395663208c5ff Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 7 Mar 2024 17:19:39 +0000 Subject: [PATCH 1/2] tidying up `README` imports --- doc/README/Data/Container/FreeMonad.agda | 10 +- doc/README/Data/List/Membership.agda | 8 +- .../Data/List/Relation/Binary/Equality.agda | 4 +- doc/README/Data/Tree/AVL.agda | 6 +- doc/README/Data/Trie/NonDependent.agda | 18 +-- .../Vec/Relation/Binary/Equality/Cast.agda | 146 +++++++++++------- doc/README/Function/Reasoning.agda | 2 +- doc/README/Tactic/Cong.agda | 14 +- doc/README/Tactic/MonoidSolver.agda | 4 +- 9 files changed, 118 insertions(+), 94 deletions(-) diff --git a/doc/README/Data/Container/FreeMonad.agda b/doc/README/Data/Container/FreeMonad.agda index ab302c90f5..cedc1e7069 100644 --- a/doc/README/Data/Container/FreeMonad.agda +++ b/doc/README/Data/Container/FreeMonad.agda @@ -16,12 +16,12 @@ open import Data.Unit open import Data.Bool.Base using (Bool; true) open import Data.Nat open import Data.Sum.Base using (inj₁; inj₂) -open import Data.Product.Base renaming (_×_ to _⟨×⟩_) +open import Data.Product.Base as Product hiding (_×_) open import Data.Container using (Container; _▷_) open import Data.Container.Combinator -open import Data.Container.FreeMonad as FreeMonad +open import Data.Container.FreeMonad open import Data.W -open import Relation.Binary.PropositionalEquality as P +open import Relation.Binary.PropositionalEquality as ≡ ------------------------------------------------------------------------ -- Defining the signature of an effect and building trees describing @@ -51,13 +51,13 @@ prog = where open RawMonad monad using (_>>_) -runState : {S X : Set} → State S ⋆ X → (S → X ⟨×⟩ S) +runState : {S X : Set} → State S ⋆ X → (S → X Product.× S) runState (pure x) = λ s → x , s runState (impure ((inj₁ _) , k)) = λ s → runState (k s) s runState (impure ((inj₂ s) , k)) = λ _ → runState (k _) s test : runState prog 0 ≡ (true , 1) -test = P.refl +test = ≡.refl -- It should be noted that @State S ⋆ X@ is not the state monad. If we -- could quotient @State S ⋆ X@ by the seven axioms of state (see diff --git a/doc/README/Data/List/Membership.agda b/doc/README/Data/List/Membership.agda index 9cb89a8159..38732fe631 100644 --- a/doc/README/Data/List/Membership.agda +++ b/doc/README/Data/List/Membership.agda @@ -7,11 +7,11 @@ module README.Data.List.Membership where open import Data.Char.Base using (Char; fromℕ) -open import Data.Char.Properties as CharProp hiding (setoid) -open import Data.Nat as ℕ using (ℕ; _+_; _<_; s≤s; z≤n; _*_; _∸_; _≤_) +open import Data.Char.Properties as Char hiding (setoid) open import Data.List.Base using (List; []; _∷_; map) +open import Data.Nat as ℕ using (ℕ) open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; cong; setoid) + using (_≡_; refl; cong; setoid) ------------------------------------------------------------------------ -- Membership @@ -66,7 +66,7 @@ import Data.List.Membership.Propositional.Properties as PropProperties -- following the first `∈` refers to lists of type `List ℕ` whereas -- the second `∈` refers to lists of type `List Char`. -open DecPropMembership CharProp._≟_ renaming (_∈_ to _∈ᶜ_) +open DecPropMembership Char._≟_ renaming (_∈_ to _∈ᶜ_) open SetoidProperties using (∈-map⁺) lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs diff --git a/doc/README/Data/List/Relation/Binary/Equality.agda b/doc/README/Data/List/Relation/Binary/Equality.agda index 4ce5fe2478..5820501564 100644 --- a/doc/README/Data/List/Relation/Binary/Equality.agda +++ b/doc/README/Data/List/Relation/Binary/Equality.agda @@ -9,10 +9,8 @@ module README.Data.List.Relation.Binary.Equality where open import Data.Nat using (ℕ; _+_; _<_; s≤s; z≤n; _*_; _∸_; _≤_) -open import Data.Nat.Properties as NatProp +open import Data.Nat.Properties as ℕ open import Data.List.Base -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; cong; setoid) ------------------------------------------------------------------------ -- Pointwise equality diff --git a/doc/README/Data/Tree/AVL.agda b/doc/README/Data/Tree/AVL.agda index 0955887f23..7e29f09f17 100644 --- a/doc/README/Data/Tree/AVL.agda +++ b/doc/README/Data/Tree/AVL.agda @@ -20,7 +20,7 @@ import Data.Tree.AVL -- natural numbers as keys and vectors of strings as values. open import Data.Nat.Properties using (<-strictTotalOrder) -open import Data.Product.Base as Prod using (_,_; _,′_) +open import Data.Product.Base as Product using (_,_; _,′_) open import Data.String.Base using (String) open import Data.Vec.Base using (Vec; _∷_; []) open import Relation.Binary.PropositionalEquality @@ -111,14 +111,14 @@ open import Function.Base using (id) v₆ : headTail t₀ ≡ nothing v₆ = refl -v₇ : Maybe.map (Prod.map₂ toList) (headTail t₂) ≡ +v₇ : Maybe.map (Product.map₂ toList) (headTail t₂) ≡ just ((1 , v₁) , ((2 , v₂) ∷ [])) v₇ = refl v₈ : initLast t₀ ≡ nothing v₈ = refl -v₉ : Maybe.map (Prod.map₁ toList) (initLast t₄) ≡ +v₉ : Maybe.map (Product.map₁ toList) (initLast t₄) ≡ just (((1 , v₁) ∷ []) ,′ (2 , v₂)) v₉ = refl diff --git a/doc/README/Data/Trie/NonDependent.agda b/doc/README/Data/Trie/NonDependent.agda index 0484e6005a..385e981880 100644 --- a/doc/README/Data/Trie/NonDependent.agda +++ b/doc/README/Data/Trie/NonDependent.agda @@ -51,15 +51,15 @@ module README.Data.Trie.NonDependent where open import Level open import Data.Unit open import Data.Bool -open import Data.Char as Char -import Data.Char.Properties as Char -open import Data.List.Base as List using (List; []; _∷_) -open import Data.List.Fresh as List# using (List#; []; _∷#_) -open import Data.Maybe as Maybe -open import Data.Product.Base as Prod using (_×_; ∃; proj₁; _,_) -open import Data.String.Base as String using (String) +open import Data.Char as Char +import Data.Char.Properties as Char +open import Data.List.Base as List using (List; []; _∷_) +open import Data.List.Fresh as List# using (List#; []; _∷#_) +open import Data.Maybe as Maybe +open import Data.Product.Base as Product using (_×_; ∃; proj₁; _,_) +open import Data.String.Base as String using (String) open import Data.String.Properties as String using (_≟_) -open import Data.These as These +open import Data.These as These open import Function.Base using (case_of_; _$_; _∘′_; id; _on_) open import Relation.Nary @@ -127,7 +127,7 @@ module _ {t} (L : Lexer t) where -- characters one by one init : Keywords - init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords + init = fromList $ List.map (Product.map₁ String.toList) $ proj₁ $ List#.toList keywords -- Kickstart the tokeniser with an empty accumulator and the initial -- trie. diff --git a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda index 42cd8bfd3d..e06cdb49f0 100644 --- a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda +++ b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda @@ -3,6 +3,9 @@ -- -- An equational reasoning library for propositional equality over -- vectors of different indices using cast. +-- +-- To see example usages of this library, scroll to the `Combinators` +-- section. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -10,15 +13,15 @@ module README.Data.Vec.Relation.Binary.Equality.Cast where open import Agda.Primitive -open import Data.List.Base as L using (List) -import Data.List.Properties as Lₚ +open import Data.List.Base as List using (List) +import Data.List.Properties as List open import Data.Nat.Base open import Data.Nat.Properties open import Data.Vec.Base open import Data.Vec.Properties open import Data.Vec.Relation.Binary.Equality.Cast open import Relation.Binary.PropositionalEquality - using (_≡_; refl; trans; sym; cong; subst; module ≡-Reasoning) + using (_≡_; refl; sym; cong; module ≡-Reasoning) private variable a : Level @@ -27,10 +30,6 @@ private variable xs ys zs ws : Vec A n --- To see example usages of this library, scroll to the combinators --- section. - - ------------------------------------------------------------------------ -- Motivation -- @@ -60,20 +59,20 @@ private variable -- Although `cast` makes it possible to prove vector identities by ind- -- uction, the explicit type-casting nature poses a significant barrier -- to code reuse in larger proofs. For example, consider the identity --- ‘fromList (xs L.∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `L._∷ʳ_` is the +-- ‘fromList (xs List.∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `List._∷ʳ_` is the -- snoc function of lists. We have -- --- fromList (xs L.∷ʳ x) : Vec A (L.length (xs L.∷ʳ x)) +-- fromList (xs List.∷ʳ x) : Vec A (List.length (xs List.∷ʳ x)) -- = {- by definition -} --- fromList (xs L.++ L.[ x ]) : Vec A (L.length (xs L.++ L.[ x ])) +-- fromList (xs List.++ List.[ x ]) : Vec A (List.length (xs List.++ List.[ x ])) -- = {- by fromList-++ -} --- fromList xs ++ fromList L.[ x ] : Vec A (L.length xs + L.length [ x ]) +-- fromList xs ++ fromList List.[ x ] : Vec A (List.length xs + List.length [ x ]) -- = {- by definition -} --- fromList xs ++ [ x ] : Vec A (L.length xs + 1) +-- fromList xs ++ [ x ] : Vec A (List.length xs + 1) -- = {- by unfold-∷ʳ -} --- fromList xs ∷ʳ x : Vec A (suc (L.length xs)) +-- fromList xs ∷ʳ x : Vec A (suc (List.length xs)) -- where --- fromList-++ : cast _ (fromList (xs L.++ ys)) ≡ fromList xs ++ fromList ys +-- fromList-++ : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys -- unfold-∷ʳ : cast _ (xs ∷ʳ x) ≡ xs ++ [ x ] -- -- Although the identity itself is simple, the reasoning process changes @@ -82,31 +81,42 @@ private variable -- rearrange (the Agda version of) the identity into one with two -- `cast`s, resulting in lots of boilerplate code as demonstrated by -- `example1a-fromList-∷ʳ`. -example1a-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) → - cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x +example1a-fromList-∷ʳ : ∀ (x : A) xs → + .(eq : List.length (xs List.∷ʳ x) ≡ suc (List.length xs)) → + cast eq (fromList (xs List.∷ʳ x)) ≡ fromList xs ∷ʳ x example1a-fromList-∷ʳ x xs eq = begin - cast eq (fromList (xs L.∷ʳ x)) ≡⟨⟩ - cast eq (fromList (xs L.++ L.[ x ])) ≡⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟨ - cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩ - cast eq₂ (fromList xs ++ [ x ]) ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩ - fromList xs ∷ʳ x ∎ + cast eq (fromList (xs List.∷ʳ x)) + ≡⟨⟩ + cast eq (fromList (xs List.++ List.[ x ])) + ≡⟨ cast-trans eq₁ eq₂ (fromList (xs List.++ List.[ x ])) ⟨ + cast eq₂ (cast eq₁ (fromList (xs List.++ List.[ x ]))) + ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩ + cast eq₂ (fromList xs ++ [ x ]) + ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩ + fromList xs ∷ʳ x + ∎ where open ≡-Reasoning - eq₁ = Lₚ.length-++ xs {L.[ x ]} - eq₂ = +-comm (L.length xs) 1 + eq₁ = List.length-++ xs {List.[ x ]} + eq₂ = +-comm (List.length xs) 1 -- The `cast`s are irrelevant to core of the proof. At the same time, -- they can be inferred from the lemmas used during the reasoning steps -- (e.g. `fromList-++` and `unfold-∷ʳ`). To eliminate the boilerplate, -- this library provides a set of equational reasoning combinators for -- equality of the form `cast eq xs ≡ ys`. -example1b-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) → - cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x +example1b-fromList-∷ʳ : ∀ (x : A) xs → + .(eq : List.length (xs List.∷ʳ x) ≡ suc (List.length xs)) → + cast eq (fromList (xs List.∷ʳ x)) ≡ fromList xs ∷ʳ x example1b-fromList-∷ʳ x xs eq = begin - fromList (xs L.∷ʳ x) ≈⟨⟩ - fromList (xs L.++ L.[ x ]) ≈⟨ fromList-++ xs ⟩ - fromList xs ++ [ x ] ≈⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟨ - fromList xs ∷ʳ x ∎ + fromList (xs List.∷ʳ x) + ≈⟨⟩ + fromList (xs List.++ List.[ x ]) + ≈⟨ fromList-++ xs ⟩ + fromList xs ++ [ x ] + ≈⟨ unfold-∷ʳ (+-comm 1 (List.length xs)) x (fromList xs) ⟨ + fromList xs ∷ʳ x + ∎ where open CastReasoning @@ -149,7 +159,7 @@ example2b eq xs a ys = begin (a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩ -- index: suc m + n reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩ -- index: suc m + n (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n - reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨ -- index: m + suc n + reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨ -- index: m + suc n xs ʳ++ (a ∷ ys) ∎ -- index: m + suc n where open CastReasoning @@ -169,29 +179,35 @@ example2b eq xs a ys = begin -- Note. Technically, `A` and `B` should be vectors of different length -- and that `ys`, `zs` are vectors of non-definitionally equal index. example3a-fromList-++-++ : {xs ys zs : List A} → - .(eq : L.length (xs L.++ ys L.++ zs) ≡ - L.length xs + (L.length ys + L.length zs)) → - cast eq (fromList (xs L.++ ys L.++ zs)) ≡ + .(eq : List.length (xs List.++ ys List.++ zs) ≡ + List.length xs + (List.length ys + List.length zs)) → + cast eq (fromList (xs List.++ ys List.++ zs)) ≡ fromList xs ++ fromList ys ++ fromList zs example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin - fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩ - fromList xs ++ fromList (ys L.++ zs) ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (Lₚ.length-++ ys) (fromList xs)) - (fromList-++ ys) ⟩ - fromList xs ++ fromList ys ++ fromList zs ∎ + fromList (xs List.++ ys List.++ zs) + ≈⟨ fromList-++ xs ⟩ + fromList xs ++ fromList (ys List.++ zs) + ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (List.length-++ ys) (fromList xs)) (fromList-++ ys) ⟩ + fromList xs ++ fromList ys ++ fromList zs + ∎ where open CastReasoning -- As an alternative, one can manually apply `cast-++ʳ` to expose `cast` -- in the subterm. However, this unavoidably duplicates the proof term. example3b-fromList-++-++′ : {xs ys zs : List A} → - .(eq : L.length (xs L.++ ys L.++ zs) ≡ - L.length xs + (L.length ys + L.length zs)) → - cast eq (fromList (xs L.++ ys L.++ zs)) ≡ + .(eq : List.length (xs List.++ ys List.++ zs) ≡ + List.length xs + (List.length ys + List.length zs)) → + cast eq (fromList (xs List.++ ys List.++ zs)) ≡ fromList xs ++ fromList ys ++ fromList zs example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin - fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩ - fromList xs ++ fromList (ys L.++ zs) ≈⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩ - fromList xs ++ cast _ (fromList (ys L.++ zs)) ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩ - fromList xs ++ fromList ys ++ fromList zs ∎ + fromList (xs List.++ ys List.++ zs) + ≈⟨ fromList-++ xs ⟩ + fromList xs ++ fromList (ys List.++ zs) + ≈⟨ cast-++ʳ (List.length-++ ys) (fromList xs) ⟩ + fromList xs ++ cast _ (fromList (ys List.++ zs)) + ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩ + fromList xs ++ fromList ys ++ fromList zs + ∎ where open CastReasoning -- `≈-cong` can be chained together much like how `cong` can be nested. @@ -201,12 +217,16 @@ example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys → cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a) example4-cong² {m = m} {n} eq a xs ys = begin - reverse ((xs ++ [ a ]) ++ ys) ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys)) + reverse ((xs ++ [ a ]) ++ ys) + ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys)) (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a)) (unfold-∷ʳ _ a xs)) ⟨ - reverse ((xs ∷ʳ a) ++ ys) ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩ - reverse ys ++ reverse (xs ∷ʳ a) ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨ - ys ʳ++ reverse (xs ∷ʳ a) ∎ + reverse ((xs ∷ʳ a) ++ ys) + ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩ + reverse ys ++ reverse (xs ∷ʳ a) + ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨ + ys ʳ++ reverse (xs ∷ʳ a) + ∎ where open CastReasoning ------------------------------------------------------------------------ @@ -222,25 +242,33 @@ example4-cong² {m = m} {n} eq a xs ys = begin -- reasoning system of `_≈[_]_` and switches back to the reasoning -- system of `_≡_`. example5-fromList-++-++′ : {xs ys zs : List A} → - .(eq : L.length (xs L.++ ys L.++ zs) ≡ - L.length xs + (L.length ys + L.length zs)) → - cast eq (fromList (xs L.++ ys L.++ zs)) ≡ + .(eq : List.length (xs List.++ ys List.++ zs) ≡ + List.length xs + (List.length ys + List.length zs)) → + cast eq (fromList (xs List.++ ys List.++ zs)) ≡ fromList xs ++ fromList ys ++ fromList zs example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin - fromList (xs L.++ ys L.++ zs) ≈⟨ fromList-++ xs ⟩ - fromList xs ++ fromList (ys L.++ zs) ≃⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩ - fromList xs ++ cast _ (fromList (ys L.++ zs)) ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩ - fromList xs ++ fromList ys ++ fromList zs ≡-∎ + fromList (xs List.++ ys List.++ zs) + ≈⟨ fromList-++ xs ⟩ + fromList xs ++ fromList (ys List.++ zs) + ≃⟨ cast-++ʳ (List.length-++ ys) (fromList xs) ⟩ + fromList xs ++ cast _ (fromList (ys List.++ zs)) + ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩ + fromList xs ++ fromList ys ++ fromList zs + ≡-∎ where open CastReasoning -- Of course, it is possible to start with the reasoning system of `_≡_` -- and then switch to the reasoning system of `_≈[_]_`. example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs example6a-reverse-∷ʳ {n = n} x xs = begin-≡ - reverse (xs ∷ʳ x) ≡⟨ ≈-reflexive refl ⟨ - reverse (xs ∷ʳ x) ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩ - reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩ - x ∷ reverse xs ∎ + reverse (xs ∷ʳ x) + ≡⟨ ≈-reflexive refl ⟨ + reverse (xs ∷ʳ x) + ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩ + reverse (xs ++ [ x ]) + ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩ + x ∷ reverse xs + ∎ where open CastReasoning example6b-reverse-∷ʳ-by-induction : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs diff --git a/doc/README/Function/Reasoning.agda b/doc/README/Function/Reasoning.agda index 0125fa9d99..86e4c3891c 100644 --- a/doc/README/Function/Reasoning.agda +++ b/doc/README/Function/Reasoning.agda @@ -39,7 +39,7 @@ open import Data.String.Base as String using (String; toList; fromList) open import Data.String.Properties as String using (_==_) open import Function.Base using (_∘_) open import Data.Bool hiding (_≤?_) -open import Data.Product.Base as P using (_×_; <_,_>; uncurry; proj₁) +open import Data.Product.Base as Product using (_×_; <_,_>; uncurry; proj₁) open import Agda.Builtin.Equality -- This can give us for instance this decomposition of a function diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda index 20cb5ad7d9..2a775f06e7 100644 --- a/doc/README/Tactic/Cong.agda +++ b/doc/README/Tactic/Cong.agda @@ -5,8 +5,8 @@ module README.Tactic.Cong where open import Data.Nat open import Data.Nat.Properties -open import Relation.Binary.PropositionalEquality as Eq -import Relation.Binary.Reasoning.Preorder as PR +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; cong; module ≡-Reasoning) open import Tactic.Cong using (cong!) @@ -26,7 +26,7 @@ open import Tactic.Cong using (cong!) verbose-example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0) verbose-example m n eq = - let open Eq.≡-Reasoning in + let open ≡-Reasoning in begin suc (suc (m + 0)) + m ≡⟨ cong (λ ϕ → suc (suc (ϕ + m))) (+-identityʳ m) ⟩ @@ -44,7 +44,7 @@ verbose-example m n eq = succinct-example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0) succinct-example m n eq = - let open Eq.≡-Reasoning in + let open ≡-Reasoning in begin suc (suc (m + 0)) + m ≡⟨ cong! (+-identityʳ m) ⟩ @@ -117,7 +117,7 @@ module EquationalReasoningTests where test₁ : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0) test₁ m n eq = - let open Eq.≡-Reasoning in + let open ≡-Reasoning in begin suc (suc (m + 0)) + m ≡⟨ cong! (+-identityʳ m) ⟩ @@ -130,11 +130,11 @@ module EquationalReasoningTests where test₂ : ∀ m n → m ≡ n → suc (m + m) ≤ suc (suc (n + n)) test₂ m n eq = - let open PR ≤-preorder in + let open ≤-Reasoning in begin suc (m + m) ≡⟨ cong! eq ⟩ suc (n + n) - ∼⟨ ≤-step ≤-refl ⟩ + ≤⟨ n≤1+n _ ⟩ suc (suc (n + n)) ∎ diff --git a/doc/README/Tactic/MonoidSolver.agda b/doc/README/Tactic/MonoidSolver.agda index 530091bc97..4631d67089 100644 --- a/doc/README/Tactic/MonoidSolver.agda +++ b/doc/README/Tactic/MonoidSolver.agda @@ -10,11 +10,9 @@ module README.Tactic.MonoidSolver {a ℓ} (M : Monoid a ℓ) where open Monoid M -open import Data.Nat as Nat using (ℕ; suc; zero; _+_) -open import Data.Nat.Properties as Properties using (+-0-monoid; +-comm) open import Relation.Binary.Reasoning.Setoid setoid -open import Tactic.MonoidSolver using (solve; solve-macro) +open import Tactic.MonoidSolver using (solve) -- The monoid solver is capable to of solving equations without having -- to specify the equation itself in the proof. From 4880e8e0bbb203fe160129faf31b033e4a64596a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 12 Mar 2024 17:19:05 +0000 Subject: [PATCH 2/2] address Matthew's review comments --- doc/README/Data/Container/FreeMonad.agda | 6 +++--- doc/README/Function/Reasoning.agda | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/README/Data/Container/FreeMonad.agda b/doc/README/Data/Container/FreeMonad.agda index cedc1e7069..3d3b2d5ff4 100644 --- a/doc/README/Data/Container/FreeMonad.agda +++ b/doc/README/Data/Container/FreeMonad.agda @@ -16,9 +16,9 @@ open import Data.Unit open import Data.Bool.Base using (Bool; true) open import Data.Nat open import Data.Sum.Base using (inj₁; inj₂) -open import Data.Product.Base as Product hiding (_×_) +open import Data.Product.Base open import Data.Container using (Container; _▷_) -open import Data.Container.Combinator +open import Data.Container.Combinator hiding (_×_) open import Data.Container.FreeMonad open import Data.W open import Relation.Binary.PropositionalEquality as ≡ @@ -51,7 +51,7 @@ prog = where open RawMonad monad using (_>>_) -runState : {S X : Set} → State S ⋆ X → (S → X Product.× S) +runState : {S X : Set} → State S ⋆ X → (S → X × S) runState (pure x) = λ s → x , s runState (impure ((inj₁ _) , k)) = λ s → runState (k s) s runState (impure ((inj₂ s) , k)) = λ _ → runState (k _) s diff --git a/doc/README/Function/Reasoning.agda b/doc/README/Function/Reasoning.agda index 86e4c3891c..810f048aa3 100644 --- a/doc/README/Function/Reasoning.agda +++ b/doc/README/Function/Reasoning.agda @@ -1,9 +1,9 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some examples showing how the Function.Reasoning module --- can be used to perform "functional reasoning" similar to what is being --- described in: https://stackoverflow.com/q/22676703/3168666 +-- Some examples showing how the Function.Reasoning module can be used +-- to perform "functional reasoning" similar to what is being described +-- in: https://stackoverflow.com/q/22676703/3168666 ------------------------------------------------------------------------ {-# OPTIONS --with-K #-} @@ -39,7 +39,7 @@ open import Data.String.Base as String using (String; toList; fromList) open import Data.String.Properties as String using (_==_) open import Function.Base using (_∘_) open import Data.Bool hiding (_≤?_) -open import Data.Product.Base as Product using (_×_; <_,_>; uncurry; proj₁) +open import Data.Product.Base using (_×_; <_,_>; uncurry; proj₁) open import Agda.Builtin.Equality -- This can give us for instance this decomposition of a function