-
Notifications
You must be signed in to change notification settings - Fork 248
Some preparatory proofs for proving sorting+permutation is equality #2724 #2725
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
|
@@ -235,6 +235,23 @@ Additions to existing modules | |||||
∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b | ||||||
``` | ||||||
|
||||||
* In `Data.Fin.Base`: | ||||||
```agda | ||||||
_≰_ : ∀ {n} → Rel (Fin n) 0ℓ | ||||||
_≮_ : ∀ {n} → Rel (Fin n) 0ℓ | ||||||
``` | ||||||
|
||||||
* In `Data.Fin.Permutation`: | ||||||
```agda | ||||||
cast-id : .(m ≡ n) → Permutation m n | ||||||
swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n)) | ||||||
``` | ||||||
|
||||||
* In `Data.Fin.Properties`: | ||||||
```agda | ||||||
cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k | ||||||
``` | ||||||
|
||||||
* In `Data.Fin.Subset`: | ||||||
```agda | ||||||
_⊇_ : Subset n → Subset n → Set | ||||||
|
@@ -266,14 +283,31 @@ Additions to existing modules | |||||
map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n | ||||||
``` | ||||||
|
||||||
* In `Data.List.Relation.Binary.Permutation.Homogeneous`: | ||||||
```agda | ||||||
onIndices : Permutation R xs ys → Fin.Permutation (length xs) (length ys) | ||||||
``` | ||||||
|
||||||
* In `Data.List.Relation.Binary.Permutation.Propositional`: | ||||||
```agda | ||||||
↭⇒↭ₛ′ : IsEquivalence _≈_ → _↭_ ⇒ _↭ₛ′_ | ||||||
``` | ||||||
|
||||||
* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: | ||||||
```agda | ||||||
xs↭ys⇒|xs|≡|ys| : xs ↭ ys → length xs ≡ length ys | ||||||
¬x∷xs↭[] : ¬ (x ∷ xs ↭ []) | ||||||
toFin-lookup : ∀ i → lookup xs i ≈ lookup ys (Inverse.to (toFin xs↭ys) i) | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this should be:
Suggested change
and again, do we need the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. (explicit arguments should definitely be in the changelog - but does There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. @Taneb I'm surprised to learn that (is it documented?): given that As for whether |
||||||
``` | ||||||
|
||||||
* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: | ||||||
```agda | ||||||
filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys | ||||||
``` | ||||||
|
||||||
* In `Data.List.Relation.Binary.Pointwise.Properties`: | ||||||
```agda | ||||||
lookup-cast : Pointwise R xs ys → .(∣xs∣≡∣ys∣ : length xs ≡ length ys) → ∀ i → R (lookup xs i) (lookup ys (cast ∣xs∣≡∣ys∣ i)) | ||||||
``` | ||||||
|
||||||
* In `Data.Product.Function.Dependent.Propositional`: | ||||||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -19,7 +19,7 @@ open import Level using (0ℓ) | |
open import Relation.Binary.Core using (Rel) | ||
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) | ||
open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) | ||
open import Relation.Nullary.Negation.Core using (contradiction) | ||
open import Relation.Nullary.Negation.Core using (¬_; contradiction) | ||
|
||
private | ||
variable | ||
|
@@ -271,7 +271,7 @@ pinch {suc n} (suc i) (suc j) = suc (pinch i j) | |
------------------------------------------------------------------------ | ||
-- Order relations | ||
|
||
infix 4 _≤_ _≥_ _<_ _>_ | ||
infix 4 _≤_ _≥_ _<_ _>_ _≰_ _≮_ | ||
|
||
_≤_ : IRel Fin 0ℓ | ||
i ≤ j = toℕ i ℕ.≤ toℕ j | ||
|
@@ -285,6 +285,11 @@ i < j = toℕ i ℕ.< toℕ j | |
_>_ : IRel Fin 0ℓ | ||
i > j = toℕ i ℕ.> toℕ j | ||
|
||
_≰_ : ∀ {n} → Rel (Fin n) 0ℓ | ||
i ≰ j = ¬ (i ≤ j) | ||
|
||
_≮_ : ∀ {n} → Rel (Fin n) 0ℓ | ||
i ≮ j = ¬ (i < j) | ||
Comment on lines
+288
to
+292
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
|
||
------------------------------------------------------------------------ | ||
-- An ordering view. | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -9,10 +9,10 @@ | |
module Data.Fin.Permutation where | ||
|
||
open import Data.Bool.Base using (true; false) | ||
open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut) | ||
open import Data.Fin.Patterns using (0F) | ||
open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut) | ||
open import Data.Fin.Patterns using (0F; 1F) | ||
open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn; | ||
punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0) | ||
punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; cast-involutive) | ||
import Data.Fin.Permutation.Components as PC | ||
open import Data.Nat.Base using (ℕ; suc; zero) | ||
open import Data.Product.Base using (_,_; proj₂) | ||
|
@@ -22,7 +22,7 @@ open import Function.Construct.Identity using (↔-id) | |
open import Function.Construct.Symmetry using (↔-sym) | ||
open import Function.Definitions using (StrictlyInverseˡ; StrictlyInverseʳ) | ||
open import Function.Properties.Inverse using (↔⇒↣) | ||
open import Function.Base using (_∘_) | ||
open import Function.Base using (_∘_; _∘′_) | ||
open import Level using (0ℓ) | ||
open import Relation.Binary.Core using (Rel) | ||
open import Relation.Nullary using (does; ¬_; yes; no) | ||
|
@@ -57,11 +57,15 @@ Permutation′ n = Permutation n n | |
------------------------------------------------------------------------ | ||
-- Helper functions | ||
|
||
permutation : ∀ (f : Fin m → Fin n) (g : Fin n → Fin m) → | ||
StrictlyInverseˡ _≡_ f g → StrictlyInverseʳ _≡_ f g → Permutation m n | ||
permutation : ∀ (f : Fin m → Fin n) | ||
(g : Fin n → Fin m) → | ||
StrictlyInverseˡ _≡_ f g → | ||
StrictlyInverseʳ _≡_ f g → | ||
Permutation m n | ||
permutation = mk↔ₛ′ | ||
|
||
infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ_ | ||
|
||
_⟨$⟩ʳ_ : Permutation m n → Fin m → Fin n | ||
_⟨$⟩ʳ_ = Inverse.to | ||
|
||
|
@@ -75,44 +79,61 @@ inverseʳ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡ | |
inverseʳ π = Inverse.inverseˡ π refl | ||
|
||
------------------------------------------------------------------------ | ||
-- Equality | ||
-- Equality over permutations | ||
|
||
infix 6 _≈_ | ||
|
||
_≈_ : Rel (Permutation m n) 0ℓ | ||
π ≈ ρ = ∀ i → π ⟨$⟩ʳ i ≡ ρ ⟨$⟩ʳ i | ||
|
||
------------------------------------------------------------------------ | ||
-- Example permutations | ||
|
||
-- Identity | ||
-- Permutation properties | ||
|
||
id : Permutation′ n | ||
id : Permutation n n | ||
id = ↔-id _ | ||
|
||
-- Transpose two indices | ||
|
||
transpose : Fin n → Fin n → Permutation′ n | ||
transpose i j = permutation (PC.transpose i j) (PC.transpose j i) (λ _ → PC.transpose-inverse _ _) (λ _ → PC.transpose-inverse _ _) | ||
flip : Permutation m n → Permutation n m | ||
flip = ↔-sym | ||
|
||
-- Reverse the order of indices | ||
infixr 9 _∘ₚ_ | ||
|
||
reverse : Permutation′ n | ||
reverse = permutation opposite opposite PC.reverse-involutive PC.reverse-involutive | ||
_∘ₚ_ : Permutation m n → Permutation n o → Permutation m o | ||
π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁ | ||
|
||
------------------------------------------------------------------------ | ||
-- Operations | ||
-- Non-trivial identity | ||
|
||
-- Composition | ||
cast-id : .(m ≡ n) → Permutation m n | ||
cast-id m≡n = permutation | ||
(cast m≡n) | ||
(cast (sym m≡n)) | ||
(cast-involutive m≡n (sym m≡n)) | ||
(cast-involutive (sym m≡n) m≡n) | ||
|
||
infixr 9 _∘ₚ_ | ||
_∘ₚ_ : Permutation m n → Permutation n o → Permutation m o | ||
π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁ | ||
------------------------------------------------------------------------ | ||
-- Transposition | ||
|
||
-- Flip | ||
-- Transposes two elements in the permutation, keeping the remainder | ||
-- of the permutation the same | ||
transpose : Fin n → Fin n → Permutation n n | ||
transpose i j = permutation | ||
(PC.transpose i j) | ||
(PC.transpose j i) | ||
(λ _ → PC.transpose-inverse _ _) | ||
(λ _ → PC.transpose-inverse _ _) | ||
|
||
flip : Permutation m n → Permutation n m | ||
flip = ↔-sym | ||
------------------------------------------------------------------------ | ||
-- Reverse | ||
|
||
-- Reverses a permutation | ||
reverse : Permutation n n | ||
reverse = permutation | ||
opposite | ||
opposite | ||
PC.reverse-involutive | ||
PC.reverse-involutive | ||
|
||
------------------------------------------------------------------------ | ||
-- Element removal | ||
-- | ||
-- `remove k [0 ↦ i₀, …, k ↦ iₖ, …, n ↦ iₙ]` yields | ||
|
@@ -159,8 +180,14 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′ | |
punchOut {i = πʳ i} {punchIn (πʳ i) j} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩ | ||
j ∎ | ||
|
||
-- lift: takes a permutation m → n and creates a permutation (suc m) → (suc n) | ||
------------------------------------------------------------------------ | ||
-- Lifting | ||
|
||
-- Takes a permutation m → n and creates a permutation (suc m) → (suc n) | ||
-- by mapping 0 to 0 and applying the input permutation to everything else | ||
-- | ||
-- Note: should be refactored as a special-case when we add the | ||
-- concatenation of two permutations | ||
lift₀ : Permutation m n → Permutation (suc m) (suc n) | ||
lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′ | ||
where | ||
|
@@ -180,6 +207,9 @@ lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′ | |
inverseˡ′ 0F = refl | ||
inverseˡ′ (suc j) = cong suc (inverseʳ π) | ||
|
||
------------------------------------------------------------------------ | ||
-- Insertion | ||
|
||
-- insert i j π is the permutation that maps i to j and otherwise looks like π | ||
-- it's roughly an inverse of remove | ||
insert : ∀ {m n} → Fin (suc m) → Fin (suc n) → Permutation m n → Permutation (suc m) (suc n) | ||
|
@@ -221,6 +251,38 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ | |
punchIn j (punchOut j≢k) ≡⟨ punchIn-punchOut j≢k ⟩ | ||
k ∎ | ||
|
||
------------------------------------------------------------------------ | ||
-- Swapping | ||
|
||
-- Takes a permutation m → n and creates a permutation | ||
-- suc (suc m) → suc (suc n) by mapping 0 to 1 and 1 to 0 and | ||
-- then applying the input permutation to everything else | ||
-- | ||
-- Note: should be refactored as a special-case when we add the | ||
-- concatenation of two permutations | ||
swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n)) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is a special case of \oplus of two permutations. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I agree ( There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I have it buried in my Rig Categories repo. I need to port the basic operations on permutations over. I've got the full semiring defined there. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. But also: There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Plus, of course: we only need this operation because There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, absolutely, there is some great stuff in |
||
swap {m} {n} π = permutation to from inverseˡ′ inverseʳ′ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is this definition easier to describe/define indirectly, via the composition of
or indeed (more) directly, as |
||
where | ||
to : Fin (suc (suc m)) → Fin (suc (suc n)) | ||
to 0F = 1F | ||
to 1F = 0F | ||
to (suc (suc i)) = suc (suc (π ⟨$⟩ʳ i)) | ||
|
||
from : Fin (suc (suc n)) → Fin (suc (suc m)) | ||
from 0F = 1F | ||
from 1F = 0F | ||
from (suc (suc i)) = suc (suc (π ⟨$⟩ˡ i)) | ||
|
||
inverseʳ′ : StrictlyInverseʳ _≡_ to from | ||
inverseʳ′ 0F = refl | ||
inverseʳ′ 1F = refl | ||
inverseʳ′ (suc (suc j)) = cong (suc ∘′ suc) (inverseˡ π) | ||
|
||
inverseˡ′ : StrictlyInverseˡ _≡_ to from | ||
inverseˡ′ 0F = refl | ||
inverseˡ′ 1F = refl | ||
inverseˡ′ (suc (suc j)) = cong (suc ∘′ suc) (inverseʳ π) | ||
|
||
------------------------------------------------------------------------ | ||
-- Other properties | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we, by convention, avoid writing the
∀ {n} →
prefix here?