From a54d331278609a0b3888817dcbd82a1cd20b2e8d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 24 Jan 2023 09:48:03 +0100 Subject: [PATCH 1/3] punchOut preserves ordering --- CHANGELOG.md | 3 +++ src/Data/Fin/Properties.agda | 16 ++++++++++++++++ 2 files changed, 19 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e56fc6dcd8..a52ea2d01e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1790,6 +1790,9 @@ Other minor changes ℕ-ℕ≡toℕ‿ℕ- : n ℕ-ℕ i ≡ toℕ (n ℕ- i) + punchOut-mono-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → j ≤ k → punchOut i≢j ≤ punchOut i≢k + punchOut-cancel-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≤ punchOut i≢k → j ≤ k + lower₁-injective : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j pinch-injective : suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index cb19ae7ab4..02262e802d 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -835,6 +835,22 @@ punchOut-injective {suc n} {suc i} {zero} {zero} _ _ _ = refl punchOut-injective {suc n} {suc i} {suc j} {suc k} i≢j i≢k pⱼ≡pₖ = cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ)) +punchOut-mono-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → + j ≤ k → punchOut i≢j ≤ punchOut i≢k +punchOut-mono-≤ {_ } {zero } {zero } {_ } 0≢0 _ z≤n = contradiction refl 0≢0 +punchOut-mono-≤ {_ } {zero } {suc j} {suc k} _ _ (s≤s j≤k) = j≤k +punchOut-mono-≤ {suc _} {suc i} {zero } {_ } _ _ z≤n = z≤n +punchOut-mono-≤ {suc _} {suc i} {suc j} {suc k} i≢j i≢k (s≤s j≤k) = s≤s (punchOut-mono-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) j≤k) + +punchOut-cancel-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → + punchOut i≢j ≤ punchOut i≢k → j ≤ k +punchOut-cancel-≤ {_ } {zero } {zero } {_ } i≢j i≢k pⱼ≤pₖ = contradiction refl i≢j +punchOut-cancel-≤ {_ } {zero } {suc j} {zero } i≢j i≢k pⱼ≤pₖ = contradiction refl i≢k +punchOut-cancel-≤ {suc _} {zero } {suc j} {suc k} i≢j i≢k pⱼ≤pₖ = s≤s pⱼ≤pₖ +punchOut-cancel-≤ {_ } {suc i} {zero } {_ } i≢j i≢k pⱼ≤pₖ = z≤n +punchOut-cancel-≤ {suc n} {suc i} {suc j} {zero } i≢j i≢k () +punchOut-cancel-≤ {suc n} {suc i} {suc j} {suc k} i≢j i≢k (s≤s pⱼ≤pₖ) = s≤s (punchOut-cancel-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) pⱼ≤pₖ) + punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) → punchIn i (punchOut i≢j) ≡ j punchIn-punchOut {_} {zero} {zero} 0≢0 = contradiction refl 0≢0 From 30c5af664cc8ce00291fb8d7b0dd460fc8139427 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 24 Jan 2023 11:15:57 +0100 Subject: [PATCH 2/3] Add the corresponding properties for punchIn too --- CHANGELOG.md | 2 ++ src/Data/Fin/Properties.agda | 10 ++++++++++ 2 files changed, 12 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a52ea2d01e..01966abff4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1790,6 +1790,8 @@ Other minor changes ℕ-ℕ≡toℕ‿ℕ- : n ℕ-ℕ i ≡ toℕ (n ℕ- i) + punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k + punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k punchOut-mono-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → j ≤ k → punchOut i≢j ≤ punchOut i≢k punchOut-cancel-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≤ punchOut i≢k → j ≤ k diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 02262e802d..86c47711af 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -802,6 +802,16 @@ punchIn-injective (suc i) (suc j) (suc k) ↑j+1≡↑k+1 = punchInᵢ≢i : ∀ i (j : Fin n) → punchIn i j ≢ i punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective +punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k +punchIn-mono-≤ zero _ _ j≤k = s≤s j≤k +punchIn-mono-≤ (suc _) zero _ z≤n = z≤n +punchIn-mono-≤ (suc i) (suc j) (suc k) (s≤s j≤k) = s≤s (punchIn-mono-≤ i j k j≤k) + +punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k +punchIn-cancel-≤ zero _ _ (s≤s j≤k) = j≤k +punchIn-cancel-≤ (suc _) zero _ z≤n = z≤n +punchIn-cancel-≤ (suc i) (suc j) (suc k) (s≤s ↑j≤↑k) = s≤s (punchIn-cancel-≤ i j k ↑j≤↑k) + ------------------------------------------------------------------------ -- punchOut ------------------------------------------------------------------------ From 65f60d197edf9d30972df2c2d058cfd175a09a94 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 24 Jan 2023 11:21:04 +0100 Subject: [PATCH 3/3] Name fewer pattern matches and name them better --- src/Data/Fin/Properties.agda | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 86c47711af..f730458038 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -848,18 +848,18 @@ punchOut-injective {suc n} {suc i} {suc j} {suc k} i≢j i≢k pⱼ≡pₖ = punchOut-mono-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → j ≤ k → punchOut i≢j ≤ punchOut i≢k punchOut-mono-≤ {_ } {zero } {zero } {_ } 0≢0 _ z≤n = contradiction refl 0≢0 -punchOut-mono-≤ {_ } {zero } {suc j} {suc k} _ _ (s≤s j≤k) = j≤k -punchOut-mono-≤ {suc _} {suc i} {zero } {_ } _ _ z≤n = z≤n -punchOut-mono-≤ {suc _} {suc i} {suc j} {suc k} i≢j i≢k (s≤s j≤k) = s≤s (punchOut-mono-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) j≤k) +punchOut-mono-≤ {_ } {zero } {suc _} {suc _} _ _ (s≤s j≤k) = j≤k +punchOut-mono-≤ {suc _} {suc _} {zero } {_ } _ _ z≤n = z≤n +punchOut-mono-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s j≤k) = s≤s (punchOut-mono-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) j≤k) punchOut-cancel-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≤ punchOut i≢k → j ≤ k -punchOut-cancel-≤ {_ } {zero } {zero } {_ } i≢j i≢k pⱼ≤pₖ = contradiction refl i≢j -punchOut-cancel-≤ {_ } {zero } {suc j} {zero } i≢j i≢k pⱼ≤pₖ = contradiction refl i≢k -punchOut-cancel-≤ {suc _} {zero } {suc j} {suc k} i≢j i≢k pⱼ≤pₖ = s≤s pⱼ≤pₖ -punchOut-cancel-≤ {_ } {suc i} {zero } {_ } i≢j i≢k pⱼ≤pₖ = z≤n -punchOut-cancel-≤ {suc n} {suc i} {suc j} {zero } i≢j i≢k () -punchOut-cancel-≤ {suc n} {suc i} {suc j} {suc k} i≢j i≢k (s≤s pⱼ≤pₖ) = s≤s (punchOut-cancel-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) pⱼ≤pₖ) +punchOut-cancel-≤ {_ } {zero } {zero } {_ } 0≢0 _ _ = contradiction refl 0≢0 +punchOut-cancel-≤ {_ } {zero } {suc _} {zero } _ 0≢0 _ = contradiction refl 0≢0 +punchOut-cancel-≤ {suc _} {zero } {suc _} {suc _} _ _ pⱼ≤pₖ = s≤s pⱼ≤pₖ +punchOut-cancel-≤ {_ } {suc _} {zero } {_ } _ _ _ = z≤n +punchOut-cancel-≤ {suc _} {suc _} {suc _} {zero } _ _ () +punchOut-cancel-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s pⱼ≤pₖ) = s≤s (punchOut-cancel-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) pⱼ≤pₖ) punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) → punchIn i (punchOut i≢j) ≡ j