Minimized.agda

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 λ()