getElem?_neg
theorem getElem?_neg :
∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem cont idx elem dom]
[inst_1 : LawfulGetElem cont idx elem dom] (c : cont) (i : idx),
¬dom c i → ∀ [inst_2 : Decidable (dom c i)], c[i]? = none
This theorem, `getElem?_neg`, states that for any given types `Cont`, `Idx`, and `Elem`, and a predicate `Dom` of type `Cont → Idx → Prop`, given an instance of `GetElem` typeclass for these types and predicate, and an instance `a` of `Cont` and `i` of `Idx` such that the predicate `Dom a i` is not true (denoted by `¬Dom a i`), then for any instance `inst_1` that can decide the truth value of `Dom a i`, the indexed getter function `a[i]?` applied to `a` and `i` will always return `none`. Essentially, it says that if the domain predicate doesn't hold for an index and a container, then the getter function returns `none` for that index in the container.
More concisely: If `Dom` is a predicate on containers `Cont` and indices `Idx` such that for any `a : Cont` and `i : Idx` with `¬Dom a i`, the getter function `a[i]?` always returns `none`.
|
getElem?_pos
theorem getElem?_pos :
∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem cont idx elem dom]
[inst_1 : LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : dom c i) [inst_2 : Decidable (dom c i)],
c[i]? = some c[i]
The theorem `getElem?_pos` states that for any types `Cont`, `Idx`, and `Elem`, and any predicate `Dom` that describes a relationship between `Cont` and `Idx`, given an instance of `GetElem` typeclass for `Cont`, `Idx`, `Elem`, and `Dom`, and any elements `a` of `Cont` and `i` of `Idx` such that `Dom a i` holds, if `Dom a i` is decidable, then the optional retrieving of an element at index `i` from `a` using the `?` operator is equal to the definite retrieval of that element using the square bracket notation. In other words, if we know that an element exists at a certain index, the optional and definite retrieval methods give the same result.
More concisely: Given types `Cont`, `Idx`, `Elem`, and a predicate `Dom`, if `Cont` has a `GetElem` instance, `Dom a i` is decidable, and `Dom a i` holds, then `getElem? a i = some (getElem a i)`.
|