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
        def Acc.inv {α : Sort u} {r : ααProp} {x : α} {y : α} (h₁ : Acc r x) (h₂ : r y x) :
        Acc r y
        Equations
        • =
        Instances For
          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
              def WellFounded.apply {α : Sort u} {r : ααProp} (wf : WellFounded r) (a : α) :
              Acc r a
              Equations
              • =
              Instances For
                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
                    def 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
                    Equations
                    • =
                    Instances For
                      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
                          def Subrelation.accessible {α : Sort u} {r : ααProp} {q : ααProp} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) :
                          Acc q a
                          Equations
                          • =
                          Instances For
                            def Subrelation.wf {α : Sort u} {r : ααProp} {q : ααProp} (h₁ : Subrelation q r) (h₂ : WellFounded r) :
                            Equations
                            • =
                            Instances For
                              def InvImage.accessible {α : Sort u} {β : Sort v} {r : ββProp} {a : α} (f : αβ) (ac : Acc r (f a)) :
                              Acc (InvImage r f) a
                              Equations
                              • =
                              Instances For
                                def InvImage.wf {α : Sort u} {β : Sort v} {r : ββProp} (f : αβ) (h : WellFounded r) :
                                Equations
                                • =
                                Instances For
                                  @[reducible]
                                  def invImage {α : Sort u_1} {β : Sort u_2} (f : αβ) (h : WellFoundedRelation β) :
                                  Equations
                                  Instances For
                                    def TC.accessible {α : Sort u} {r : ααProp} {z : α} (ac : Acc r z) :
                                    Acc (TC r) z
                                    Equations
                                    • =
                                    Instances For
                                      def TC.wf {α : Sort u} {r : ααProp} (h : WellFounded 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.
                                                  def 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₂)
                                                  Equations
                                                  • =
                                                  Instances For
                                                    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
                                                      def 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)
                                                      Equations
                                                      • =
                                                      Instances For
                                                        @[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
                                                          def 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
                                                          Equations
                                                          • =
                                                          Instances For
                                                            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
                                                                def 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
                                                                Equations
                                                                • =
                                                                Instances For
                                                                  @[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
                                                                      def PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
                                                                      Equations
                                                                      • =
                                                                      Instances For
                                                                        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
                                                                          def 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
                                                                          Equations
                                                                          • =
                                                                          Instances For
                                                                            def PSigma.revLex {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
                                                                            Equations
                                                                            • =
                                                                            Instances For
                                                                              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
                                                                                  def PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {s : ββProp} (a₁ : α) (a₂ : α) (h : s b₁ b₂) :
                                                                                  PSigma.SkipLeft α s a₁, b₁ a₂, b₂
                                                                                  Equations
                                                                                  • =
                                                                                  Instances For