module GeneralLemmas where open import Data.Empty public using (⊥; ⊥-elim) open import Data.List public using (List; _∷_; []; _++_; length; map) open import Data.Maybe public using (Maybe; just; nothing) open import Data.Product public using (_×_; _,_; proj₁; proj₂; ∃; ∃₂; ∄) open import Data.Nat public using (ℕ; suc; zero; _+_) open import Data.Unit public using (⊤; tt) open import Function public using (_∋_; _∘_; id) open import Relation.Binary.PropositionalEquality public using (_≡_; _≢_; refl; cong; cong₂; subst; subst₂; trans; sym; inspect; [_]) open import Relation.Nullary public using (Dec; yes; no; ¬_) ,-inj : {A B : Set}{x y : A × B} → x ≡ y → proj₁ x ≡ proj₁ y × proj₂ x ≡ proj₂ y ,-inj refl = refl , refl ,,-inj : {A B C : Set}{x y : A × B × C} → x ≡ y → proj₁ x ≡ proj₁ y × proj₁ (proj₂ x) ≡ proj₁ (proj₂ y) × proj₂ (proj₂ x) ≡ proj₂ (proj₂ y) ,,-inj refl = refl , refl , refl ∷-inj : {A : Set}{x y : A}{xs ys : List A} → (List A ∋ x ∷ xs) ≡ y ∷ ys → x ≡ y × xs ≡ ys ∷-inj refl = refl , refl suc-inj : ∀ {m n} → suc m ≡ suc n → m ≡ n suc-inj refl = refl just-inj : {A : Set}{x y : A} → (Maybe A ∋ just x) ≡ just y → x ≡ y just-inj refl = refl nothing≠just : ∀ {A : Set}{x : A} → nothing ≢ (Maybe A ∋ just x) nothing≠just () cong₄ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} (f : A → B → C → D → E) {w w' x x' y y' z z'} → w ≡ w' → x ≡ x' → y ≡ y' → z ≡ z' → f w x y z ≡ f w' x' y' z' cong₄ f refl refl refl refl = refl cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} (f : A → B → C → D) {w w' x x' y y'} → w ≡ w' → x ≡ x' → y ≡ y' → f w x y ≡ f w' x' y' cong₃ f refl refl refl = refl lookup : {A : Set} → ℕ → List A → Maybe A lookup n [] = nothing lookup zero (x ∷ xs) = just x lookup (suc n) (x ∷ xs) = lookup n xs