-
Notifications
You must be signed in to change notification settings - Fork 233
/
Permutation.agda
70 lines (52 loc) · 2.52 KB
/
Permutation.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
------------------------------------------------------------------------
-- The Agda standard library
--
-- Documentation for permutation over `List`s
------------------------------------------------------------------------
module README.Data.List.Relation.Binary.Permutation where
open import Algebra.Structures using (IsCommutativeMonoid)
open import Data.List.Base
open import Data.Nat using (ℕ; _+_)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; sym; cong; setoid)
------------------------------------------------------------------------
-- Permutations
-- As an alternative to pointwise equality you might consider two lists
-- to be equal if they contain the same elements regardless of the order
-- of the elements. This is known as either "set equality" or a
-- "permutation".
-- The easiest-to-use formalisation of this relation is found in the
-- module:
open import Data.List.Relation.Binary.Permutation.Propositional
-- The permutation relation is written as `_↭_` and has four
-- constructors. The first `refl` says that a list is always
-- a permutation of itself, the second `prep` says that if the
-- heads of the lists are the same they can be skipped, the third
-- `swap` says that the first two elements of the lists can be
-- swapped and the fourth `trans` says that permutation proofs
-- can be chained transitively.
-- For example a proof that two lists are a permutation of one
-- another can be written as follows:
lem₁ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
lem₁ = trans (prep 1 (swap 2 3 refl)) (swap 1 3 refl)
-- In practice it is difficult to parse the constructors in the
-- proof above and hence understand why it holds. The
-- `PermutationReasoning` module can be used to write this proof
-- in a much more readable form:
open PermutationReasoning
lem₂ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
lem₂ = begin
1 ∷ 2 ∷ 3 ∷ [] ↭⟨ prep 1 (swap 2 3 refl) ⟩
1 ∷ 3 ∷ 2 ∷ [] ↭⟨ swap 1 3 refl ⟩
3 ∷ 1 ∷ 2 ∷ [] ∎
-- As might be expected, properties of the permutation relation may be
-- found in:
open import Data.List.Relation.Binary.Permutation.Propositional.Properties
using (map⁺; ++-isCommutativeMonoid)
lem₃ : ∀ (f : ℕ → ℕ) {xs ys : List ℕ} → xs ↭ ys → map f xs ↭ map f ys
lem₃ = map⁺
lem₄ : IsCommutativeMonoid {A = List ℕ} _↭_ _++_ []
lem₄ = ++-isCommutativeMonoid
-- Alternatively permutations using non-propositional equality can be
-- found in:
import Data.List.Relation.Binary.Permutation.Setoid