From 4b32a5c0910a5a158a7cff5a6d6ab3837e73e990 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 7 Oct 2025 07:30:18 +0200 Subject: [PATCH 1/4] Simplify Sublist/Heterogeneous/antisym: collapse two cases --- .../Binary/Sublist/Heterogeneous/Properties.agda | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index a80d689ec5..e5b5881bd2 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -401,25 +401,20 @@ module Antisymmetry open ℕ.≤-Reasoning antisym : Antisym (Sublist R) (Sublist S) (Pointwise E) - antisym [] [] = [] - antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss -- impossible cases - antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷ʳ_ {ys₂} {zs} z ss) = + antisym (_∷ʳ_ {xs} {ys₁} y rs) ss = contradiction (begin length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ - length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩ - length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ + length xs ≤⟨ length-mono-≤ rs ⟩ length ys₁ ∎) $ ℕ.<-irrefl ≡.refl - antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss) = - contradiction (begin - length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ≤⟨ length-mono-≤ ss ⟩ - length zs ∎) $ ℕ.<-irrefl ≡.refl antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) = contradiction (begin length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ length xs ≤⟨ length-mono-≤ rs ⟩ length ys₁ ∎) $ ℕ.<-irrefl ≡.refl + -- diagonal cases + antisym [] [] = [] + antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss open Antisymmetry public From 94e2bfbd3925c6707fc37cb432e6c0181952422e Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 7 Oct 2025 07:43:29 +0200 Subject: [PATCH 2/4] Simplify Sublist/Heterogeneous/antisym: factor out contradiction --- .../Sublist/Heterogeneous/Properties.agda | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index e5b5881bd2..b10816fa79 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -400,18 +400,19 @@ module Antisymmetry open ℕ.≤-Reasoning + private + antisym-lemma : ∀ xs ys₁ y → Sublist R xs ys₁ → ¬ Sublist S (y ∷ ys₁) xs + antisym-lemma xs ys₁ y rs ss = ℕ.<-irrefl ≡.refl (begin + length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ + length xs ≤⟨ length-mono-≤ rs ⟩ + length ys₁ ∎) + antisym : Antisym (Sublist R) (Sublist S) (Pointwise E) -- impossible cases antisym (_∷ʳ_ {xs} {ys₁} y rs) ss = - contradiction (begin - length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ - length xs ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎) $ ℕ.<-irrefl ≡.refl + case (antisym-lemma xs ys₁ y rs ss) of λ() antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) = - contradiction (begin - length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ - length xs ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎) $ ℕ.<-irrefl ≡.refl + case (antisym-lemma xs ys₁ y rs ss) of λ() -- diagonal cases antisym [] [] = [] antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss From 90ec3757f789cff04a8b48e5293896903223e341 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 7 Oct 2025 15:36:58 +0200 Subject: [PATCH 3/4] Review comment: use contradiction --- .../Relation/Binary/Sublist/Heterogeneous/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index b10816fa79..ed1ae55cbb 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -29,7 +29,7 @@ open import Function.Base open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔) open import Function.Consequences.Propositional using (strictlySurjective⇒surjective) open import Relation.Nullary.Decidable as Dec using (Dec; does; _because_; yes; no; ¬?) -open import Relation.Nullary.Negation using (¬_; contradiction) +open import Relation.Nullary.Negation using (¬_; contradiction; contradiction′) open import Relation.Nullary.Reflects using (invert) open import Relation.Unary as U using (Pred) open import Relation.Binary.Core using (Rel; REL; _⇒_) @@ -410,9 +410,9 @@ module Antisymmetry antisym : Antisym (Sublist R) (Sublist S) (Pointwise E) -- impossible cases antisym (_∷ʳ_ {xs} {ys₁} y rs) ss = - case (antisym-lemma xs ys₁ y rs ss) of λ() + contradiction′ (antisym-lemma xs ys₁ y rs) ss antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) = - case (antisym-lemma xs ys₁ y rs ss) of λ() + contradiction′ (antisym-lemma xs ys₁ y rs) ss -- diagonal cases antisym [] [] = [] antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss From 8eecaeac5cb588f196983660876fc15ed6ca5997 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Wed, 8 Oct 2025 22:38:48 +0200 Subject: [PATCH 4/4] Apply suggestions from code review Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- .../Binary/Sublist/Heterogeneous/Properties.agda | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index ed1ae55cbb..af3675fb9c 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -401,18 +401,17 @@ module Antisymmetry open ℕ.≤-Reasoning private - antisym-lemma : ∀ xs ys₁ y → Sublist R xs ys₁ → ¬ Sublist S (y ∷ ys₁) xs - antisym-lemma xs ys₁ y rs ss = ℕ.<-irrefl ≡.refl (begin - length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ - length xs ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎) + antisym-lemma : Sublist R xs ys → ¬ Sublist S (y ∷ ys) xs + antisym-lemma {xs} {ys} {y} rs ss = ℕ.<-irrefl ≡.refl $ begin + length (y ∷ ys) ≤⟨ length-mono-≤ ss ⟩ + length xs ≤⟨ length-mono-≤ rs ⟩ + length ys ∎ antisym : Antisym (Sublist R) (Sublist S) (Pointwise E) -- impossible cases - antisym (_∷ʳ_ {xs} {ys₁} y rs) ss = - contradiction′ (antisym-lemma xs ys₁ y rs) ss + antisym (_ ∷ʳ rs) ss = contradiction′ (antisym-lemma rs) ss antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) = - contradiction′ (antisym-lemma xs ys₁ y rs) ss + contradiction′ (antisym-lemma rs) ss -- diagonal cases antisym [] [] = [] antisym (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs ss