Documentation

Init.WF

inductive Acc {α : Sort u} (r : ααProp) :
αProp

Acc is the accessibility predicate. Given some relation r (e.g. <) and a value x, Acc r x means that x is accessible through r:

x is accessible if there exists no infinite sequence ... < y₂ < y₁ < y₀ < x.

  • intro: ∀ {α : Sort u} {r : ααProp} (x : α), (∀ (y : α), r y xAcc r y)Acc r x

    A value is accessible if for all y such that r y x, y is also accessible. Note that if there exists no y such that r y x, then x is accessible. Such an x is called a base case.

Instances For
    @[reducible, inline]
    noncomputable abbrev Acc.ndrec {α : Sort u2} {r : ααProp} {C : αSort u1} (m : (x : α) → (∀ (y : α), r y xAcc r y)((y : α) → r y xC y)C x) {a : α} (n : Acc r a) :
    C a
    Equations
    Instances For
      @[reducible, inline]
      noncomputable abbrev Acc.ndrecOn {α : Sort u2} {r : ααProp} {C : αSort u1} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y xAcc r y)((y : α) → r y xC y)C x) :
      C a
      Equations
      Instances For
        theorem Acc.inv {α : Sort u} {r : ααProp} {x : α} {y : α} (h₁ : Acc r x) (h₂ : r y x) :
        Acc r y
        inductive WellFounded {α : Sort u} (r : ααProp) :

        A relation r is WellFounded if all elements of α are accessible within r. If a relation is WellFounded, it does not allow for an infinite descent along the relation.

        If the arguments of the recursive calls in a function definition decrease according to a well founded relation, then the function terminates. Well-founded relations are sometimes called Artinian or said to satisfy the “descending chain condition”.

        Instances For
          class WellFoundedRelation (α : Sort u) :
          Sort (max 1 u)
          Instances
            theorem WellFoundedRelation.wf {α : Sort u} [self : WellFoundedRelation α] :
            WellFounded WellFoundedRelation.rel
            theorem WellFounded.apply {α : Sort u} {r : ααProp} (wf : WellFounded r) (a : α) :
            Acc r a
            noncomputable def WellFounded.recursion {α : Sort u} {r : ααProp} (hwf : WellFounded r) {C : αSort v} (a : α) (h : (x : α) → ((y : α) → r y xC y)C x) :
            C a
            Equations
            • hwf.recursion a h = Acc.rec (fun (x₁ : α) (h_1 : ∀ (y : α), r y x₁Acc r y) (ih : (y : α) → r y x₁C y) => h x₁ ih)
            Instances For
              theorem WellFounded.induction {α : Sort u} {r : ααProp} (hwf : WellFounded r) {C : αProp} (a : α) (h : ∀ (x : α), (∀ (y : α), r y xC y)C x) :
              C a
              noncomputable def WellFounded.fixF {α : Sort u} {r : ααProp} {C : αSort v} (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) (a : Acc r x) :
              C x
              Equations
              • WellFounded.fixF F x a = Acc.rec (fun (x₁ : α) (h : ∀ (y : α), r y x₁Acc r y) (ih : (y : α) → r y x₁C y) => F x₁ ih) a
              Instances For
                theorem WellFounded.fixFEq {α : Sort u} {r : ααProp} {C : αSort v} (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) (acx : Acc r x) :
                WellFounded.fixF F x acx = F x fun (y : α) (p : r y x) => WellFounded.fixF F y
                noncomputable def WellFounded.fix {α : Sort u} {C : αSort v} {r : ααProp} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
                C x
                Equations
                Instances For
                  theorem WellFounded.fix_eq {α : Sort u} {C : αSort v} {r : ααProp} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
                  hwf.fix F x = F x fun (y : α) (x : r y x) => hwf.fix F y
                  Equations
                  • emptyWf = { rel := emptyRelation, wf := }
                  Instances For
                    theorem Subrelation.accessible {α : Sort u} {r : ααProp} {q : ααProp} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) :
                    Acc q a
                    theorem Subrelation.wf {α : Sort u} {r : ααProp} {q : ααProp} (h₁ : Subrelation q r) (h₂ : WellFounded r) :
                    theorem InvImage.accessible {α : Sort u} {β : Sort v} {r : ββProp} {a : α} (f : αβ) (ac : Acc r (f a)) :
                    Acc (InvImage r f) a
                    theorem InvImage.wf {α : Sort u} {β : Sort v} {r : ββProp} (f : αβ) (h : WellFounded r) :
                    @[reducible]
                    def invImage {α : Sort u_1} {β : Sort u_2} (f : αβ) (h : WellFoundedRelation β) :
                    Equations
                    Instances For
                      theorem Acc.transGen :
                      ∀ {α : Sort u_1} {r : ααProp} {a : α}, Acc r aAcc (Relation.TransGen r) a
                      theorem acc_transGen_iff :
                      ∀ {α : Sort u_1} {r : ααProp} {a : α}, Acc (Relation.TransGen r) a Acc r a
                      theorem WellFounded.transGen :
                      ∀ {α : Sort u_1} {r : ααProp}, WellFounded rWellFounded (Relation.TransGen r)
                      @[reducible, inline, deprecated Acc.transGen]
                      abbrev TC.accessible :
                      ∀ {α : Sort u_1} {r : ααProp} {a : α}, Acc r aAcc (Relation.TransGen r) a
                      Equations
                      Instances For
                        @[reducible, inline, deprecated WellFounded.transGen]
                        abbrev TC.wf :
                        ∀ {α : Sort u_1} {r : ααProp}, WellFounded rWellFounded (Relation.TransGen r)
                        Equations
                        Instances For
                          noncomputable def Nat.strongInductionOn {motive : NatSort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) :
                          motive n
                          Equations
                          Instances For
                            noncomputable def Nat.caseStrongInductionOn {motive : NatSort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m nmotive m)motive n.succ) :
                            motive a
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[reducible, inline]
                              abbrev measure {α : Sort u} (f : αNat) :
                              Equations
                              Instances For
                                @[reducible, inline]
                                abbrev sizeOfWFRel {α : Sort u} [SizeOf α] :
                                Equations
                                Instances For
                                  @[instance 100]
                                  Equations
                                  • instWellFoundedRelationOfSizeOf = sizeOfWFRel
                                  inductive Prod.Lex {α : Type u} {β : Type v} (ra : ααProp) (rb : ββProp) :
                                  α × βα × βProp
                                  • left: ∀ {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β), ra a₁ a₂Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
                                  • right: ∀ {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} (a : α) {b₁ b₂ : β}, rb b₁ b₂Prod.Lex ra rb (a, b₁) (a, b₂)
                                  Instances For
                                    theorem Prod.lex_def {α : Type u} {β : Type v} (r : ααProp) (s : ββProp) {p : α × β} {q : α × β} :
                                    Prod.Lex r s p q r p.fst q.fst p.fst = q.fst s p.snd q.snd
                                    instance Prod.Lex.instDecidableRelOfDecidableEq {α : Type u} {β : Type v} [αeqDec : DecidableEq α] {r : ααProp} [rDec : DecidableRel r] {s : ββProp} [sDec : DecidableRel s] :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    theorem Prod.Lex.right' {β : Type v} (rb : ββProp) {a₂ : Nat} {b₂ : β} {a₁ : Nat} {b₁ : β} (h₁ : a₁ a₂) (h₂ : rb b₁ b₂) :
                                    Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)
                                    inductive Prod.RProd {α : Type u} {β : Type v} (ra : ααProp) (rb : ββProp) :
                                    α × βα × βProp
                                    • intro: ∀ {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, ra a₁ a₂rb b₁ b₂Prod.RProd ra rb (a₁, b₁) (a₂, b₂)
                                    Instances For
                                      theorem Prod.lexAccessible {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} {a : α} (aca : Acc ra a) (acb : ∀ (b : β), Acc rb b) (b : β) :
                                      Acc (Prod.Lex ra rb) (a, b)
                                      @[reducible]
                                      def Prod.lex {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
                                      Equations
                                      • Prod.lex ha hb = { rel := Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel, wf := }
                                      Instances For
                                        Equations
                                        • Prod.instWellFoundedRelation = Prod.lex ha hb
                                        theorem Prod.RProdSubLex {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} (a : α × β) (b : α × β) (h : Prod.RProd ra rb a b) :
                                        Prod.Lex ra rb a b
                                        def Prod.rprod {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
                                        Equations
                                        Instances For
                                          inductive PSigma.Lex {α : Sort u} {β : αSort v} (r : ααProp) (s : (a : α) → β aβ aProp) :
                                          PSigma βPSigma βProp
                                          • left: ∀ {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂PSigma.Lex r s a₁, b₁ a₂, b₂
                                          • right: ∀ {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} (a : α) {b₁ b₂ : β a}, s a b₁ b₂PSigma.Lex r s a, b₁ a, b₂
                                          Instances For
                                            theorem PSigma.lexAccessible {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} {a : α} (aca : Acc r a) (acb : ∀ (a : α), WellFounded (s a)) (b : β a) :
                                            Acc (PSigma.Lex r s) a, b
                                            @[reducible]
                                            def PSigma.lex {α : Sort u} {β : αSort v} (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) :
                                            Equations
                                            • PSigma.lex ha hb = { rel := PSigma.Lex WellFoundedRelation.rel fun (a : α) => WellFoundedRelation.rel, wf := }
                                            Instances For
                                              instance PSigma.instWellFoundedRelation {α : Sort u} {β : αSort v} [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] :
                                              Equations
                                              def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : ααProp) (s : ββProp) :
                                              (_ : α) ×' β(_ : α) ×' βProp
                                              Equations
                                              Instances For
                                                theorem PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
                                                inductive PSigma.RevLex {α : Sort u} {β : Sort v} (r : ααProp) (s : ββProp) :
                                                (_ : α) ×' β(_ : α) ×' βProp
                                                • left: ∀ {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} {a₁ a₂ : α} (b : β), r a₁ a₂PSigma.RevLex r s a₁, b a₂, b
                                                • right: ∀ {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂PSigma.RevLex r s a₁, b₁ a₂, b₂
                                                Instances For
                                                  theorem PSigma.revLexAccessible {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} {b : β} (acb : Acc s b) (aca : ∀ (a : α), Acc r a) (a : α) :
                                                  Acc (PSigma.RevLex r s) a, b
                                                  theorem PSigma.revLex {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
                                                  def PSigma.SkipLeft (α : Type u) {β : Type v} (s : ββProp) :
                                                  (_ : α) ×' β(_ : α) ×' βProp
                                                  Equations
                                                  Instances For
                                                    def PSigma.skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) :
                                                    WellFoundedRelation ((_ : α) ×' β)
                                                    Equations
                                                    Instances For
                                                      theorem PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {s : ββProp} (a₁ : α) (a₂ : α) (h : s b₁ b₂) :
                                                      PSigma.SkipLeft α s a₁, b₁ a₂, b₂