FixedPoint

Difficulty: optional — 6 definitions, 0 abbreviations, 7 lemmas, 2 theorems, 2 examples.

definition lemma theorem examples
legend
BitSequence.Dominates {n : ℕ} (a b : BitSequence n) : Prop
Show details 
fun {n} a b => ∀ (i : Fin n), a i = true → b i = true

Complexity: 33 (size of the value term)

Outer dependencies: BitSequence

Inner dependencies: Bit

Lean core dependencies: Eq, Fin, Nat

Used by: BitFunction.Monotone, BitFunction.exists_settle, BitFunction.iterate_dominates_succ, BitSequence.Dominates.bot, BitSequence.trueCount_strict

BitSequence.Dominates.bot {n : ℕ} (a : BitSequence n) : BitSequence.Dominates (fun x => false) a
Show details 
fun {n} a x h =>
  absurd h
    (of_eq_true
      (Eq.trans (congrArg Not (eq_false' fun h => False.elim (noConfusion_of_Nat Bool.ctorIdx h)))
        not_false_eq_true))

Complexity: 155 (size of the value term)

Dependencies: BitSequence, BitSequence.Dominates

Proof dependencies: Bit

Lean core dependencies: Bool, Eq, Eq.trans, False, False.elim, Fin, Nat, Not, True, absurd, congrArg, eq_false', noConfusion_of_Nat, not_false_eq_true, of_eq_true

Used by: BitFunction.iterate_dominates_succ

BitFunction.Monotone {n : ℕ} (f : BitFunction n n) : Prop
Show details 
fun {n} f => ∀ (a b : BitSequence n), a.Dominates b → BitSequence.Dominates (f a) (f b)

Complexity: 35 (size of the value term)

Outer dependencies: BitFunction

Inner dependencies: BitSequence, BitSequence.Dominates

Lean core dependencies: Nat

Used by: BitFunction.exists_isFixedPoint, BitFunction.exists_settle, BitFunction.fixedPoint, BitFunction.fixedPoint_isFixed, BitFunction.iterate_dominates_succ, BitFunction.iterate_settles

BitSequence.trueCount {n : ℕ} (x : BitSequence n) : ℕ
Show details 
fun {n} x => {i | x i = true}.card

Complexity: 53 (size of the value term)

Outer dependencies: BitSequence

Inner dependencies: Bit

Mathlib dependencies: Finset.card, Finset.filter, Finset.univ

Lean core dependencies: Eq, Fin, Nat

Used by: BitFunction.exists_settle, BitSequence.trueCount_le, BitSequence.trueCount_strict

BitSequence.trueCount_le {n : ℕ} (x : BitSequence n) : x.trueCount ≤ n
Show details 
fun {n} x =>
  Trans.trans (Finset.card_filter_le Finset.univ fun i => x i = true)
    (of_eq_true (Eq.trans (congrFun' (congrArg Eq (Fintype.card_fin n)) n) (eq_self n)))

Complexity: 241 (size of the value term)

Dependencies: BitSequence, BitSequence.trueCount

Proof dependencies: Bit

Mathlib dependencies: Finset.card, Finset.card_filter_le, Finset.univ, Fintype.card_fin

Lean core dependencies: Eq, Eq.trans, Fin, Nat, True, congrArg, congrFun', eq_self, of_eq_true

Used by: BitFunction.exists_settle

BitSequence.trueCount_strict {n : ℕ} {a b : BitSequence n} (h : a.Dominates b) (hne : a ≠ b) :
  a.trueCount < b.trueCount
Show details 
fun {n} {a b} h hne =>
  have hsub := fun i hi =>
    Eq.mpr
      (id
        (Eq.trans BitSequence.trueCount_strict._simp_1_1
          (Eq.trans
            (congrFun' (congrArg And (BitSequence.trueCount_strict._simp_1_2 i)) (b i = true))
            (true_and (b i = true)))))
      (h i
        (Eq.mp
          (Eq.trans BitSequence.trueCount_strict._simp_1_1
            (Eq.trans
              (congrFun' (congrArg And (BitSequence.trueCount_strict._simp_1_2 i)) (a i = true))
              (true_and (a i = true))))
          hi));
  Or.casesOn (LE.le.eq_or_ssubset hsub)
    (fun heq =>
      False.elim
        (hne
          (funext fun i =>
            have this :=
              have this := Finset.ext_iff.mp heq i;
              Eq.mpr (id eq_iff_iff._simp_1)
                (Eq.mp
                  (congr
                    (congrArg Iff
                      (Eq.trans Finset.mem_filter._simp_1
                        (Eq.trans
                          (congrFun' (congrArg And (Finset.mem_univ._simp_1 i)) (a i = true))
                          (true_and (a i = true)))))
                    (Eq.trans Finset.mem_filter._simp_1
                      (Eq.trans (congrFun' (congrArg And (Finset.mem_univ._simp_1 i)) (b i = true))
                        (true_and (b i = true)))))
                  this);
            Bool.casesOn (motive := fun t => a i = t → a i = b i) (a i)
              (fun h =>
                Eq.ndrec (motive := fun x => a i = x → x = b i)
                  (fun ha =>
                    Bool.casesOn (motive := fun t => b i = t → false = b i) (b i)
                      (fun h =>
                        Eq.ndrec (motive := fun x => b i = x → false = x)
                          (fun hb => of_eq_true (eq_self false)) (Eq.symm h) (Eq.refl (b i)))
                      (fun h =>
                        Eq.ndrec (motive := fun x => b i = x → false = x)
                          (fun hb =>
                            False.elim
                              (Eq.mp
                                (Eq.trans
                                  (Eq.trans
                                    (congr
                                      (congrArg Eq
                                        (Eq.trans (congrFun' (congrArg Eq ha) true)
                                          (eq_false' fun h =>
                                            False.elim (noConfusion_of_Nat Bool.ctorIdx h))))
                                      (Eq.trans (congrFun' (congrArg Eq hb) true) (eq_self true)))
                                    eq_iff_iff._simp_1)
                                  (iff_true False))
                                this))
                          (Eq.symm h) (Eq.refl (b i)))
                      (Eq.refl (b i)))
                  (Eq.symm h) (Eq.refl (a i)))
              (fun h =>
                Eq.ndrec (motive := fun x => a i = x → x = b i)
                  (fun ha =>
                    Bool.casesOn (motive := fun t => b i = t → true = b i) (b i)
                      (fun h =>
                        Eq.ndrec (motive := fun x => b i = x → true = x)
                          (fun hb =>
                            False.elim
                              (Eq.mp
                                (Eq.trans
                                  (Eq.trans
                                    (congr
                                      (congrArg Eq
                                        (Eq.trans (congrFun' (congrArg Eq ha) true) (eq_self true)))
                                      (Eq.trans (congrFun' (congrArg Eq hb) true)
                                        (eq_false' fun h =>
                                          False.elim (noConfusion_of_Nat Bool.ctorIdx h))))
                                    eq_iff_iff._simp_1)
                                  (Eq.trans (iff_false True) not_true_eq_false))
                                this))
                          (Eq.symm h) (Eq.refl (b i)))
                      (fun h =>
                        Eq.ndrec (motive := fun x => b i = x → true = x)
                          (fun hb => of_eq_true (eq_self true)) (Eq.symm h) (Eq.refl (b i)))
                      (Eq.refl (b i)))
                  (Eq.symm h) (Eq.refl (a i)))
              (Eq.refl (a i)))))
    fun hssub => Finset.card_lt_card hssub

Complexity: 5398 (size of the value term)

Dependencies: BitSequence, BitSequence.Dominates, BitSequence.trueCount

Proof dependencies: Bit

Mathlib dependencies: Finset, Finset.card_lt_card, Finset.ext_iff, Finset.filter, Finset.mem_filter, Finset.mem_univ, Finset.univ, Fintype

Lean core dependencies: And, Bool, DecidablePred, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, False.elim, Fin, Iff, Nat, Ne, Not, Or, True, congr, congrArg, congrFun', eq_false', eq_self, eq_true, funext, id, iff_false, iff_true, noConfusion_of_Nat, not_true_eq_false, of_eq_true, true_and

Used by: BitFunction.exists_settle

BitFunction.iterate {n : ℕ} (f : BitFunction n n) (k : ℕ) : BitSequence n
Show details 
fun {n} f k => f^[k] fun x => false

Complexity: 27 (size of the value term)

Outer dependencies: BitFunction, BitSequence

Inner dependencies: Bit

Mathlib dependencies: Nat.iterate

Lean core dependencies: Fin, Nat

Used by: BitFunction.exists_settle, BitFunction.fixedPoint, BitFunction.fixedPoint_isFixed, BitFunction.iterate_dominates_succ, BitFunction.iterate_settles, BitFunction.iterate_stays

BitFunction.iterate_dominates_succ {n : ℕ} {f : BitFunction n n} (hf : f.Monotone) (k : ℕ) :
  (f.iterate k).Dominates (f.iterate (k + 1))
Show details 
fun {n} {f} hf k =>
  Nat.recAux (BitSequence.Dominates.bot (f.iterate (0 + 1)))
    (fun k ih =>
      id
        (Eq.mpr
          (id
            (congrArg (fun _a => BitSequence.Dominates _a (f^[k + 1 + 1] fun x => false))
              (Function.iterate_succ_apply' f k fun x => false)))
          (Eq.mpr
            (id
              (congrArg (fun _a => BitSequence.Dominates (f (f^[k] fun x => false)) _a)
                (Function.iterate_succ_apply' f (k + 1) fun x => false)))
            (hf (f^[k] fun x => false) (f^[k + 1] fun x => false) ih))))
    k

Complexity: 1367 (size of the value term)

Dependencies: BitFunction, BitFunction.Monotone, BitFunction.iterate, BitSequence.Dominates

Proof dependencies: Bit, BitSequence.Dominates.bot

Mathlib dependencies: Function.iterate_succ_apply', Nat.iterate

Lean core dependencies: Eq, Eq.mpr, Fin, Nat, Nat.recAux, congrArg, id

Used by: BitFunction.exists_settle

BitFunction.iterate_stays {n : ℕ} (f : BitFunction n n) {k : ℕ}
  (hk : f.iterate (k + 1) = f.iterate k) (j : ℕ) : k ≤ j → f.iterate j = f.iterate k
Show details 
fun {n} f {k} hk j hj =>
  Nat.le_induction (Eq.refl (f.iterate k))
    (fun j hmn ih =>
      have hstep :=
        of_eq_true
          (Eq.trans
            (congrFun' (congrArg Eq (Function.iterate_succ_apply' f j fun x => false))
              (f (f^[j] fun x => false)))
            (eq_self (f (f^[j] fun x => false))));
      have hfix :=
        id
          (Eq.mp
            (congrFun' (congrArg Eq (Function.iterate_succ_apply' f k fun x => false))
              (f^[k] fun x => false))
            hk);
      Eq.mpr (id (congrArg (fun _a => _a = f.iterate k) hstep))
        (Eq.mpr (id (congrArg (fun _a => f _a = f.iterate k) ih))
          (Eq.mpr (id (congrArg (fun _a => _a = f.iterate k) hfix)) (Eq.refl (f.iterate k)))))
    j hj

Complexity: 1445 (size of the value term)

Dependencies: BitFunction, BitFunction.iterate, BitSequence

Proof dependencies: Bit

Mathlib dependencies: Function.iterate_succ_apply', Nat.iterate, Nat.le_induction

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.trans, Fin, Nat, True, congrArg, congrFun', eq_self, id, of_eq_true

Used by: BitFunction.iterate_settles

BitFunction.exists_settle {n : ℕ} {f : BitFunction n n} (hf : f.Monotone) :
  ∃ k ≤ n, f.iterate (k + 1) = f.iterate k
Show details 
fun {n} {f} hf =>
  Decidable.byContradiction fun hnone =>
    have hgrow := fun k hk =>
      Nat.recAux (motive := fun k => k ≤ n + 1 → k ≤ (f.iterate k).trueCount)
        (fun hk => Nat.zero_le (f.iterate 0).trueCount)
        (fun k ih hk =>
          have hk' := Nat.le_of_succ_le hk;
          have hkn :=
            Decidable.byContradiction fun a => BitFunction.exists_settle._proof_1_1 k hk a;
          have hne := fun h =>
            Eq.mp
              (Eq.trans
                (Mathlib.Tactic.Push.not_exists._simp_1 fun k =>
                  k ≤ n ∧ f.iterate (k + 1) = f.iterate k)
                (forall_congr fun k =>
                  Mathlib.Tactic.Push.not_and_eq (k ≤ n) (f.iterate (k + 1) = f.iterate k)))
              hnone k hkn h;
          have hdom := BitFunction.iterate_dominates_succ hf k;
          have hstrict := BitSequence.trueCount_strict hdom (Ne.symm hne);
          have this := ih hk';
          Decidable.byContradiction fun a => BitFunction.exists_settle._proof_1_2 k hstrict this a)
        k hk;
    have h1 := hgrow (n + 1) (le_refl (n + 1));
    have h2 := BitSequence.trueCount_le (f.iterate (n + 1));
    BitFunction.exists_settle._proof_1_3 h1 h2

Complexity: 2102 (size of the value term)

Dependencies: BitFunction, BitFunction.Monotone, BitFunction.iterate, BitSequence

Proof dependencies: Bit, BitFunction.iterate_dominates_succ, BitSequence.Dominates, BitSequence.trueCount, BitSequence.trueCount_le, BitSequence.trueCount_strict

Mathlib dependencies: Mathlib.Tactic.Push.not_and_eq, le_refl

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mp, Eq.symm, Eq.trans, Exists, Fin, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_of_succ_le, Nat.lt_of_not_le, Nat.recAux, Nat.zero_le, Ne, Ne.symm, Not, binderNameHint, forall_congr, id, le_of_le_of_eq, of_decide_eq_true

Used by: BitFunction.iterate_settles

BitFunction.iterate_settles {n : ℕ} {f : BitFunction n n} (hf : f.Monotone) :
  f.iterate (n + 1) = f.iterate n
Show details 
fun {n} {f} hf =>
  Exists.casesOn (BitFunction.exists_settle hf) fun k h =>
    And.casesOn h fun hkn hk =>
      Eq.mpr
        (id (congrArg (fun _a => f.iterate (n + 1) = _a) (BitFunction.iterate_stays f hk n hkn)))
        (Eq.mpr
          (id
            (congrArg (fun _a => _a = f.iterate k)
              (BitFunction.iterate_stays f hk (n + 1) (Nat.le_succ_of_le hkn))))
          (Eq.refl (f.iterate k)))

Complexity: 1019 (size of the value term)

Dependencies: BitFunction, BitFunction.Monotone, BitFunction.iterate, BitSequence

Proof dependencies: BitFunction.exists_settle, BitFunction.iterate_stays

Lean core dependencies: And, Eq, Eq.mpr, Exists, Nat, Nat.le_succ_of_le, congrArg, id

Used by: BitFunction.fixedPoint_isFixed

BitFunction.fixedPoint {n : ℕ} (f : BitFunction n n) : f.Monotone → BitSequence n
Show details 
fun {n} f x => f.iterate n

Complexity: 21 (size of the value term)

Outer dependencies: BitFunction, BitFunction.Monotone, BitSequence

Inner dependencies: BitFunction.iterate

Lean core dependencies: Nat

Used by: BitFunction.exists_isFixedPoint, BitFunction.fixedPoint_isFixed

BitFunction.fixedPoint_isFixed {n : ℕ} {f : BitFunction n n} (hf : f.Monotone) :
  f (f.fixedPoint hf) = f.fixedPoint hf
Show details 
fun {n} {f} hf =>
  id
    (have this :=
      of_eq_true
        (Eq.trans
          (congrArg (Eq (f (f^[n] fun x => false)))
            (Function.iterate_succ_apply' f n fun x => false))
          (eq_self (f (f^[n] fun x => false))));
    Eq.mpr (id (congrArg (fun _a => _a = f.iterate n) this))
      (Eq.mpr (id (congrArg (fun _a => _a = f.iterate n) (BitFunction.iterate_settles hf)))
        (Eq.refl (f.iterate n))))

Complexity: 880 (size of the value term)

Dependencies: Bit, BitFunction, BitFunction.Monotone, BitFunction.fixedPoint

Proof dependencies: BitFunction.iterate, BitFunction.iterate_settles, BitSequence

Mathlib dependencies: Function.iterate_succ_apply', Nat.iterate

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Fin, Nat, True, congrArg, eq_self, id, of_eq_true

Used by: BitFunction.exists_isFixedPoint

BitFunction.IsFixedPoint {n : ℕ} (f : BitFunction n n) (o : BitSequence n) : Prop
Show details 
fun {n} f o => f o = o

Complexity: 25 (size of the value term)

Outer dependencies: BitFunction, BitSequence

Inner dependencies: Bit

Lean core dependencies: Eq, Fin, Nat

Used by: BitFunction.exists_isFixedPoint, notRule_no_fixedPoint

BitFunction.exists_isFixedPoint {n : ℕ} {f : BitFunction n n} (hf : f.Monotone) :
  ∃ o, f.IsFixedPoint o
Show details 
fun {n} {f} hf => Exists.intro (f.fixedPoint hf) (BitFunction.fixedPoint_isFixed hf)

Complexity: 47 (size of the value term)

Dependencies: BitFunction, BitFunction.IsFixedPoint, BitFunction.Monotone, BitSequence

Proof dependencies: BitFunction.fixedPoint, BitFunction.fixedPoint_isFixed

Lean core dependencies: Exists, Nat

Used by: (none)

notRule : BitFunction 1 1
Show details 
fun iv x => !iv 0

Complexity: 61 (size of the value term)

Outer dependencies: BitFunction

Inner dependencies: Bit

Lean core dependencies: Bool.not, Fin, Nat

Used by: notRule_no_fixedPoint

notRule_no_fixedPoint : ¬∃ o, notRule.IsFixedPoint o
Show details 
fun a =>
  Exists.casesOn a fun o ho =>
    have ho0 := congrFun ho 0;
    Bool.casesOn (motive := fun t => o 0 = t → (!o 0) = o 0 → False) (o 0)
      (fun h =>
        Eq.ndrec (motive := fun b => (!b) = b → False) (of_decide_eq_true (id (Eq.refl true)))
          (Eq.symm h))
      (fun h =>
        Eq.ndrec (motive := fun b => (!b) = b → False) (of_decide_eq_true (id (Eq.refl true)))
          (Eq.symm h))
      (Eq.refl (o 0)) ho0

Complexity: 1164 (size of the value term)

Dependencies: BitFunction.IsFixedPoint, BitSequence, notRule

Proof dependencies: Bit

Lean core dependencies: Bool, Bool.not, Decidable.decide, Eq, Eq.symm, Exists, False, Fin, Nat, Not, congrFun, id, of_decide_eq_true

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremexampledeclared elsewheredependencyproof dependency
legend