-
Notifications
You must be signed in to change notification settings - Fork 236
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add two lemmas to
Data.List.Membership.Setoid.Properties (#2465)
* fixes first part of issue #2463; second part creates dependency cycle * refactor to break dependency cycle * renamed in line with review suggestions * fix bug
- Loading branch information
1 parent
41001ea
commit 9a5ec9f
Showing
4 changed files
with
128 additions
and
60 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,96 @@ | ||
| ------------------------------------------------------------------------ | ||
| -- The Agda standard library | ||
| -- | ||
| -- Properties related to All | ||
| ------------------------------------------------------------------------ | ||
|
|
||
| {-# OPTIONS --cubical-compatible --safe #-} | ||
|
|
||
| module Data.List.Relation.Unary.All.Properties.Core where | ||
|
|
||
| open import Axiom.Extensionality.Propositional using (Extensionality) | ||
| open import Data.Bool.Base using (true; false) | ||
| open import Data.List.Base using (List; []; _∷_) | ||
| open import Data.List.Relation.Unary.All as All using (All; []; _∷_) | ||
| open import Data.List.Relation.Unary.Any as Any using (Any; here; there) | ||
| open import Data.Product.Base as Product using (_,_) | ||
| open import Function.Base using (_∘_; _$_) | ||
| open import Function.Bundles using (_↠_; mk↠ₛ; _⇔_; mk⇔) | ||
| open import Level using (Level) | ||
| open import Relation.Binary.Core using (REL) | ||
| open import Relation.Binary.PropositionalEquality.Core | ||
| using (_≡_; refl; cong; cong₂) | ||
| open import Relation.Nullary.Reflects using (invert) | ||
| open import Relation.Nullary.Negation.Core using (¬_; contradiction) | ||
| open import Relation.Nullary.Decidable.Core using (_because_) | ||
| open import Relation.Unary using (Decidable; Pred; Universal) | ||
|
|
||
| private | ||
| variable | ||
| a b p ℓ : Level | ||
| A : Set a | ||
| B : Set b | ||
| P : Pred A p | ||
| x y : A | ||
| xs ys : List A | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Lemmas relating Any, All and negation. | ||
|
|
||
| ¬Any⇒All¬ : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs | ||
| ¬Any⇒All¬ [] ¬p = [] | ||
| ¬Any⇒All¬ (x ∷ xs) ¬p = ¬p ∘ here ∷ ¬Any⇒All¬ xs (¬p ∘ there) | ||
|
|
||
| All¬⇒¬Any : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs | ||
| All¬⇒¬Any (¬p ∷ _) (here p) = ¬p p | ||
| All¬⇒¬Any (_ ∷ ¬p) (there p) = All¬⇒¬Any ¬p p | ||
|
|
||
| ¬All⇒Any¬ : Decidable P → ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs | ||
| ¬All⇒Any¬ dec [] ¬∀ = contradiction [] ¬∀ | ||
| ¬All⇒Any¬ dec (x ∷ xs) ¬∀ with dec x | ||
| ... | true because [p] = there (¬All⇒Any¬ dec xs (¬∀ ∘ _∷_ (invert [p]))) | ||
| ... | false because [¬p] = here (invert [¬p]) | ||
|
|
||
| Any¬⇒¬All : ∀ {xs} → Any (¬_ ∘ P) xs → ¬ All P xs | ||
| Any¬⇒¬All (here ¬p) = ¬p ∘ All.head | ||
| Any¬⇒¬All (there ¬p) = Any¬⇒¬All ¬p ∘ All.tail | ||
|
|
||
| ¬Any↠All¬ : ∀ {xs} → (¬ Any P xs) ↠ All (¬_ ∘ P) xs | ||
| ¬Any↠All¬ = mk↠ₛ {to = ¬Any⇒All¬ _} (λ y → All¬⇒¬Any y , to∘from y) | ||
| where | ||
| to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → ¬Any⇒All¬ xs (All¬⇒¬Any ¬p) ≡ ¬p | ||
| to∘from [] = refl | ||
| to∘from (¬p ∷ ¬ps) = cong₂ _∷_ refl (to∘from ¬ps) | ||
|
|
||
| -- If equality of functions were extensional, then the surjection | ||
| -- could be strengthened to a bijection. | ||
|
|
||
| from∘to : Extensionality _ _ → | ||
| ∀ xs → (¬p : ¬ Any P xs) → All¬⇒¬Any (¬Any⇒All¬ xs ¬p) ≡ ¬p | ||
| from∘to ext [] ¬p = ext λ () | ||
| from∘to ext (x ∷ xs) ¬p = ext λ | ||
| { (here p) → refl | ||
| ; (there p) → cong (λ f → f p) $ from∘to ext xs (¬p ∘ there) | ||
| } | ||
|
|
||
| Any¬⇔¬All : ∀ {xs} → Decidable P → Any (¬_ ∘ P) xs ⇔ (¬ All P xs) | ||
| Any¬⇔¬All dec = mk⇔ Any¬⇒¬All (¬All⇒Any¬ dec _) | ||
|
|
||
| private | ||
| -- If equality of functions were extensional, then the logical | ||
| -- equivalence could be strengthened to a surjection. | ||
| to∘from : Extensionality _ _ → (dec : Decidable P) → | ||
| (¬∀ : ¬ All P xs) → Any¬⇒¬All (¬All⇒Any¬ dec xs ¬∀) ≡ ¬∀ | ||
| to∘from ext P ¬∀ = ext λ ∀P → contradiction ∀P ¬∀ | ||
|
|
||
| module _ {_~_ : REL A B ℓ} where | ||
|
|
||
| All-swap : ∀ {xs ys} → | ||
| All (λ x → All (x ~_) ys) xs → | ||
| All (λ y → All (_~ y) xs) ys | ||
| All-swap {ys = []} _ = [] | ||
| All-swap {ys = y ∷ ys} [] = All.universal (λ _ → []) (y ∷ ys) | ||
| All-swap {ys = y ∷ ys} ((x~y ∷ x~ys) ∷ pxs) = | ||
| (x~y ∷ (All.map All.head pxs)) ∷ | ||
| All-swap (x~ys ∷ (All.map All.tail pxs)) | ||
|
|