Documentation

Init.GetElem

@[never_extract]
def outOfBounds {α : Type u_1} [Inhabited α] :
α
Equations
Instances For
    theorem outOfBounds_eq_default {α : Type u_1} [Inhabited α] :
    outOfBounds = default
    class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (collidxProp)) :
    Type (max (max u v) w)

    The classes GetElem and GetElem? implement lookup notation, specifically xs[i], xs[i]?, xs[i]!, and xs[i]'p.

    Both classes are indexed by types coll, idx, and elem which are the collection, the index, and the element types. A single collection may support lookups with multiple index types. The relation valid determines when the index is guaranteed to be valid; lookups of valid indices are guaranteed not to fail.

    For example, an instance for arrays looks like GetElem (Array α) Nat α (fun xs i => i < xs.size). In other words, given an array xs and a natural number i, xs[i] will return an α when valid xs i holds, which is true when i is less than the size of the array. Array additionally supports indexing with USize instead of Nat. In either case, because the bounds are checked at compile time, no runtime check is required.

    Given xs[i] with xs : coll and i : idx, Lean looks for an instance of GetElem coll idx elem valid and uses this to infer the type of the return value elem and side condition valid required to ensure xs[i] yields a valid value of type elem. The tactic get_elem_tactic is invoked to prove validity automatically. The xs[i]'p notation uses the proof p to satisfy the validity condition. If the proof p is long, it is often easier to place the proof in the context using have, because get_elem_tactic tries assumption.

    The proof side-condition valid xs i is automatically dispatched by the get_elem_tactic tactic; this tactic can be extended by adding more clauses to get_elem_tactic_trivial using macro_rules.

    xs[i]? and xs[i]! do not impose a proof obligation; the former returns an Option elem, with none signalling that the value isn't present, and the latter returns elem but panics if the value isn't there, returning default : elem based on the Inhabited elem instance. These are provided by the GetElem? class, for which there is a default instance generated from a GetElem class as long as valid xs i is always decidable.

    Important instances include:

    • arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no runtime bounds check and a proof side goal i < arr.size.
    • l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.
    • getElem : (xs : coll) → (i : idx) → valid xs ielem

      The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

    Instances

      The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible, inline]
          abbrev decidableGetElem? {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : collidxProp} [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
          Option elem

          Helper function for implementation of GetElem?.getElem?.

          Equations
          Instances For
            class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (collidxProp)) extends GetElem :
            Type (max (max u v) w)

            The classes GetElem and GetElem? implement lookup notation, specifically xs[i], xs[i]?, xs[i]!, and xs[i]'p.

            Both classes are indexed by types coll, idx, and elem which are the collection, the index, and the element types. A single collection may support lookups with multiple index types. The relation valid determines when the index is guaranteed to be valid; lookups of valid indices are guaranteed not to fail.

            For example, an instance for arrays looks like GetElem (Array α) Nat α (fun xs i => i < xs.size). In other words, given an array xs and a natural number i, xs[i] will return an α when valid xs i holds, which is true when i is less than the size of the array. Array additionally supports indexing with USize instead of Nat. In either case, because the bounds are checked at compile time, no runtime check is required.

            Given xs[i] with xs : coll and i : idx, Lean looks for an instance of GetElem coll idx elem valid and uses this to infer the type of the return value elem and side condition valid required to ensure xs[i] yields a valid value of type elem. The tactic get_elem_tactic is invoked to prove validity automatically. The xs[i]'p notation uses the proof p to satisfy the validity condition. If the proof p is long, it is often easier to place the proof in the context using have, because get_elem_tactic tries assumption.

            The proof side-condition valid xs i is automatically dispatched by the get_elem_tactic tactic; this tactic can be extended by adding more clauses to get_elem_tactic_trivial using macro_rules.

            xs[i]? and xs[i]! do not impose a proof obligation; the former returns an Option elem, with none signalling that the value isn't present, and the latter returns elem but panics if the value isn't there, returning default : elem based on the Inhabited elem instance. These are provided by the GetElem? class, for which there is a default instance generated from a GetElem class as long as valid xs i is always decidable.

            Important instances include:

            • arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no runtime bounds check and a proof side goal i < arr.size.
            • l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.
            • getElem : (xs : coll) → (i : idx) → valid xs ielem
            • getElem? : collidxOption elem

              The syntax arr[i]? gets the i'th element of the collection arr, if it is present (and wraps it in some), and otherwise returns none.

            • getElem! : [inst : Inhabited elem] → collidxelem

              The syntax arr[i]! gets the i'th element of the collection arr, if it is present, and otherwise panics at runtime and returns the default term from Inhabited elem.

            Instances

              The syntax arr[i]? gets the i'th element of the collection arr or returns none if i is out of bounds.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The syntax arr[i]! gets the i'th element of the collection arr and panics i is out of bounds.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[instance 100]
                  instance instGetElem?OfGetElemOfDecidable {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : collidxProp} [GetElem coll idx elem valid] [(xs : coll) → (i : idx) → Decidable (valid xs i)] :
                  GetElem? coll idx elem valid
                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem getElem_congr_coll {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : collidxProp} [GetElem coll idx elem valid] {c : coll} {d : coll} {i : idx} {h : valid c i} (h' : c = d) :
                  c[i] = d[i]
                  theorem getElem_congr {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : collidxProp} [GetElem coll idx elem valid] {c : coll} {i : idx} {j : idx} {h : valid c i} (h' : i = j) :
                  c[i] = c[j]
                  class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (contidxProp)) [ge : GetElem? cont idx elem dom] :
                  • getElem?_def : ∀ (c : cont) (i : idx) [inst : Decidable (dom c i)], c[i]? = if h : dom c i then some c[i] else none
                  • getElem!_def : ∀ [inst : Inhabited elem] (c : cont) (i : idx), c[i]! = match c[i]? with | some e => e | none => default
                  Instances
                    theorem LawfulGetElem.getElem?_def {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (contidxProp)} {ge : GetElem? cont idx elem dom} [self : LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] :
                    c[i]? = if h : dom c i then some c[i] else none
                    theorem LawfulGetElem.getElem!_def {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (contidxProp)} {ge : GetElem? cont idx elem dom} [self : LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) :
                    c[i]! = match c[i]? with | some e => e | none => default
                    @[instance 100]
                    instance instLawfulGetElem {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : collidxProp} [GetElem coll idx elem valid] [(xs : coll) → (i : idx) → Decidable (valid xs i)] :
                    LawfulGetElem coll idx elem valid
                    Equations
                    • =
                    theorem getElem?_pos {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
                    c[i]? = some c[i]
                    theorem getElem?_neg {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] :
                    c[i]? = none
                    theorem getElem!_pos {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
                    c[i]! = c[i]
                    theorem getElem!_neg {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] :
                    c[i]! = default
                    instance Fin.instGetElemFinVal {cont : Type u_1} {elem : Type u_2} {dom : contNatProp} {n : Nat} [GetElem cont Nat elem dom] :
                    GetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs i
                    Equations
                    • Fin.instGetElemFinVal = { getElem := fun (xs : cont) (i : Fin n) (h : dom xs i) => xs[i] }
                    instance Fin.instGetElem?FinVal {cont : Type u_1} {elem : Type u_2} {dom : contNatProp} {n : Nat} [GetElem? cont Nat elem dom] :
                    GetElem? cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs i
                    Equations
                    • Fin.instGetElem?FinVal = GetElem?.mk (fun (xs : cont) (i : Fin n) => xs[i]?) fun [Inhabited elem] (xs : cont) (i : Fin n) => xs[i]!
                    instance Fin.instLawfulGetElemValOfNat {cont : Type u_1} {elem : Type u_2} {dom : contNatProp} {n : Nat} [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
                    LawfulGetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs i
                    Equations
                    • =
                    @[simp]
                    theorem Fin.getElem_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : ContNatProp} {n : Nat} [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
                    a[i] = a[i]
                    @[simp]
                    theorem Fin.getElem?_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : ContNatProp} {n : Nat} [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) :
                    a[i]? = a[i]?
                    @[simp]
                    theorem Fin.getElem!_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : ContNatProp} {n : Nat} [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] :
                    a[i]! = a[i]!
                    instance List.instGetElemNatLtLength {α : Type u_1} :
                    GetElem (List α) Nat α fun (as : List α) (i : Nat) => i < as.length
                    Equations
                    • List.instGetElemNatLtLength = { getElem := fun (as : List α) (i : Nat) (h : i < as.length) => as.get i, h }
                    @[simp]
                    theorem List.getElem_cons_zero {α : Type u_1} (a : α) (as : List α) (h : 0 < (a :: as).length) :
                    (a :: as)[0] = a
                    @[reducible, inline, deprecated]
                    abbrev List.cons_getElem_zero {α : Type u_1} (a : α) (as : List α) (h : 0 < (a :: as).length) :
                    (a :: as)[0] = a
                    Equations
                    Instances For
                      @[simp]
                      theorem List.getElem_cons_succ {α : Type u_1} (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) :
                      (a :: as)[i + 1] = as[i]
                      @[reducible, inline, deprecated]
                      abbrev List.cons_getElem_succ {α : Type u_1} (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) :
                      (a :: as)[i + 1] = as[i]
                      Equations
                      Instances For
                        theorem List.get_drop_eq_drop {α : Type u_1} (as : List α) (i : Nat) (h : i < as.length) :
                        as[i] :: List.drop (i + 1) as = List.drop i as
                        instance Array.instGetElemNatLtSize {α : Type u_1} :
                        GetElem (Array α) Nat α fun (xs : Array α) (i : Nat) => i < xs.size
                        Equations
                        • Array.instGetElemNatLtSize = { getElem := fun (xs : Array α) (i : Nat) (h : i < xs.size) => xs.get i, h }
                        Equations