Skip to content

Instantly share code, notes, and snippets.

@collares
Last active May 22, 2019 02:35
Show Gist options
  • Save collares/f6f12fffe04488f8f89a7a6e3de59ce5 to your computer and use it in GitHub Desktop.
Save collares/f6f12fffe04488f8f89a7a6e3de59ce5 to your computer and use it in GitHub Desktop.
module plfa.Minimized where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open import Function using (_∘_)
open import Data.List using (List; []; _∷_)
open import Data.List.All using (All; []; _∷_)
open import Data.List.Any using (Any; here; there)
open import Data.List.Membership.Propositional using (_∈_)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)
open import Level using (Level)
postulate
extensionality : ∀ {A : Set} {B : A → Set} {C : A → Set} {f g : {x : A} → B x → C x}
→ (∀ {x : A} (bx : B x) → f {x} bx ≡ g {x} bx)
--------------------------------------------
→ (λ {x} → f {x}) ≡ (λ {x} → g {x})
All-∀-to : ∀ {A : Set} {P : A → Set} (xs : List A)
→ All P xs → (∀ {x} → x ∈ xs → P x)
All-∀-to [] [] ()
All-∀-to (x ∷ xs) (ap ∷ aps) (here refl) = ap
All-∀-to (x ∷ xs) (ap ∷ aps) (there pf) = All-∀-to xs aps pf
All-∀-from : ∀ {A : Set} {P : A → Set} (xs : List A)
→ (∀ {x} → x ∈ xs → P x) → All P xs
All-∀-from [] f = []
All-∀-from (x ∷ xs) f = f (here refl) ∷ All-∀-from xs (f ∘ there)
All-∀-to∘from : ∀ {A : Set} {P : A → Set} (xs : List A) (f : (∀ {x} → x ∈ xs → P x))
→ (λ {x} → All-∀-to xs (All-∀-from xs f) {x}) ≡ (λ {x} → f {x})
All-∀-to∘from [] f = extensionality λ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment