Documentation

Lake.Util.Compare

class Lake.EqOfCmp (α : Type u) (cmp : ααOrdering) :

Proof that the equality of a compare function corresponds to propositional equality.

Instances
    class Lake.LawfulCmpEq (α : Type u) (cmp : ααOrdering) extends Lake.EqOfCmp :

    Proof that the equality of a compare function corresponds to propositional equality and vice versa.

    Instances
      @[simp]
      theorem Lake.cmp_iff_eq {α : Type u_1} {cmp : ααOrdering} {a : α} {a' : α} [Lake.LawfulCmpEq α cmp] :
      cmp a a' = Ordering.eq a = a'
      class Lake.EqOfCmpWrt (α : Type u) {β : Type v} (f : αβ) (cmp : ααOrdering) :

      Proof that the equality of a compare function corresponds to propositional equality with respect to a given function.

      • eq_of_cmp_wrt : ∀ {a a' : α}, cmp a a' = Ordering.eqf a = f a'
      Instances
        instance Lake.instEqOfCmpWrtType {α : Type u_1} {cmp : ααOrdering} :
        Lake.EqOfCmpWrt α (fun (x : α) => α) cmp
        Equations
        • Lake.instEqOfCmpWrtType = { eq_of_cmp_wrt := (_ : ∀ {a a' : α}, cmp a a' = Ordering.eqα = α) }
        instance Lake.instEqOfCmpWrt {α : Type u_1} {cmp : ααOrdering} :
        {β : Type u_2} → {f : αβ} → [inst : Lake.EqOfCmp α cmp] → Lake.EqOfCmpWrt α f cmp
        Equations
        • Lake.instEqOfCmpWrt = { eq_of_cmp_wrt := (_ : ∀ {a a' : α}, cmp a a' = Ordering.eqf a = f a') }
        instance Lake.instEqOfCmp {α : Type u_1} {cmp : ααOrdering} [Lake.EqOfCmpWrt α (fun (a : α) => a) cmp] :
        Equations
        • Lake.instEqOfCmp = { eq_of_cmp := (_ : ∀ {a a' : α}, cmp a a' = Ordering.eqa = a') }
        theorem Lake.eq_of_compareOfLessAndEq {α : Type u_1} [LT α] [DecidableEq α] {a : α} {a' : α} [Decidable (a < a')] (h : compareOfLessAndEq a a' = Ordering.eq) :
        a = a'
        theorem Lake.compareOfLessAndEq_rfl {α : Type u_1} [LT α] [DecidableEq α] {a : α} [Decidable (a < a)] (lt_irrefl : ¬a < a) :
        theorem Lake.Fin.eq_of_compare {m : Nat} {n : Fin m} {n' : Fin m} (h : compare n n' = Ordering.eq) :
        n = n'
        Equations
        theorem Lake.List.lt_irrefl {α : Type u_1} [LT α] (irrefl_α : ∀ (a : α), ¬a < a) (a : List α) :
        ¬a < a
        @[simp]
        theorem Lake.String.lt_irrefl (s : String) :
        ¬s < s
        @[macro_inline]
        def Lake.Option.compareWith {α : Type u_1} (cmp : ααOrdering) :
        Option αOption αOrdering
        Equations
        Instances For
          instance Lake.instEqOfCmpOptionCompareWith {α : Type u_1} {cmp : ααOrdering} [Lake.EqOfCmp α cmp] :
          Equations
          Equations
          def Lake.Prod.compareWith {α : Type u_1} {β : Type u_2} (cmpA : ααOrdering) (cmpB : ββOrdering) :
          α × βα × βOrdering
          Equations
          • Lake.Prod.compareWith cmpA cmpB x✝ x = match x✝ with | (a, b) => match x with | (a', b') => match cmpA a a' with | Ordering.eq => cmpB b b' | ord => ord
          Instances For
            instance Lake.instEqOfCmpProdCompareWith {α : Type u_1} {cmpA : ααOrdering} {β : Type u_2} {cmpB : ββOrdering} [Lake.EqOfCmp α cmpA] [Lake.EqOfCmp β cmpB] :
            Equations
            instance Lake.instLawfulCmpEqProdCompareWith {α : Type u_1} {cmpA : ααOrdering} {β : Type u_2} {cmpB : ββOrdering} [Lake.LawfulCmpEq α cmpA] [Lake.LawfulCmpEq β cmpB] :
            Equations
            • One or more equations did not get rendered due to their size.