<commit_before>-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: <NAME>
import logic.eq

inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
intro : ∀x, (∀ y, R y x → acc R y) → acc R x

namespace acc
  variables {A : Type} {R : A → A → Prop}

  definition inv {x y : A} (H₁ : acc R x) (H₂ : R y x) : acc R y :=
  acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂
end acc

inductive well_founded [class] {A : Type} (R : A → A → Prop) : Prop :=
intro : (∀ a, acc R a) → well_founded R

namespace well_founded
  definition apply [coercion] {A : Type} {R : A → A → Prop} (wf : well_founded R) : ∀a, acc R a :=
  take a, well_founded.rec_on wf (λp, p) a

  context
  parameters {A : Type} {R : A → A → Prop}
  infix `≺`:50    := R

  hypothesis [Hwf : well_founded R]

  theorem recursion {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a :=
  acc.rec_on (Hwf a) (λ x₁ ac₁ iH, H x₁ iH)

  theorem indunction {C : A → Prop} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a :=
  recursion a H

  variable {C : A → Type}
  variable F : Πx, (Πy, y ≺ x → C y) → C x

  definition fix_F (x : A) (a : acc R x) : C x :=
  acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH)

  theorem fix_F_eq (x : A) (r : acc R x) :
    fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
  have gen : Π r : acc R x, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)), from
  acc.rec_on r
    (λ x₁ ac iH (r₁ : acc R x₁),
      -- The proof is straightforward after we replace r₁ with acc.intro (to "unblock" evaluation).
      calc fix_F F x₁ r₁
           = fix_F F x₁ (acc.intro x₁ ac)             : proof_irrel r₁
       ... = F x₁ (λ y ay, fix_F F y (acc.inv r₁ ay)) : rfl),
  gen r
  end

  variables {A : Type} {C : A → Type} {R : A → A → Prop}

  -- Well-founded fixpoint
  definition fix [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) : C x :=
  fix_F F x (Hwf x)

  -- Well-founded fixpoint satisfies fixpoint equation
  theorem fix_eq [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) :
    fix F x = F x (λy h, fix F y) :=
  calc
    -- The proof is straightforward, it just uses fix_F_eq and proof irrelevance
    fix F x
        = F x (λy h, fix_F F y (acc.inv (Hwf x) h)) : fix_F_eq F x (Hwf x)
    ... = F x (λy h, fix F y)                       : rfl  -- proof irrelevance is used here

end well_founded
<commit_msg>feat(library/logic/wf): some basic definitions for constructing well_founded relations<commit_after>-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: <NAME>
import logic.eq

inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
intro : ∀x, (∀ y, R y x → acc R y) → acc R x

namespace acc
  variables {A : Type} {R : A → A → Prop}

  definition inv {x y : A} (H₁ : acc R x) (H₂ : R y x) : acc R y :=
  acc.rec_on H₁ (λ x₁ ac₁ iH H₂, ac₁ y H₂) H₂
end acc

inductive well_founded [class] {A : Type} (R : A → A → Prop) : Prop :=
intro : (∀ a, acc R a) → well_founded R

definition well_founded.apply [coercion] {A : Type} {R : A → A → Prop} (wf : well_founded R) : ∀a, acc R a :=
take a, well_founded.rec_on wf (λp, p) a

namespace well_founded
  context
  parameters {A : Type} {R : A → A → Prop}
  infix `≺`:50    := R

  hypothesis [Hwf : well_founded R]

  theorem recursion {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a :=
  acc.rec_on (Hwf a) (λ x₁ ac₁ iH, H x₁ iH)

  theorem indunction {C : A → Prop} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a :=
  recursion a H

  variable {C : A → Type}
  variable F : Πx, (Πy, y ≺ x → C y) → C x

  definition fix_F (x : A) (a : acc R x) : C x :=
  acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH)

  theorem fix_F_eq (x : A) (r : acc R x) :
    fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
  have gen : Π r : acc R x, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)), from
  acc.rec_on r
    (λ x₁ ac iH (r₁ : acc R x₁),
      -- The proof is straightforward after we replace r₁ with acc.intro (to "unblock" evaluation).
      calc fix_F F x₁ r₁
           = fix_F F x₁ (acc.intro x₁ ac)             : proof_irrel r₁
       ... = F x₁ (λ y ay, fix_F F y (acc.inv r₁ ay)) : rfl),
  gen r
  end

  variables {A : Type} {C : A → Type} {R : A → A → Prop}

  -- Well-founded fixpoint
  definition fix [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) : C x :=
  fix_F F x (Hwf x)

  -- Well-founded fixpoint satisfies fixpoint equation
  theorem fix_eq [Hwf : well_founded R] (F : Πx, (Πy, R y x → C y) → C x) (x : A) :
    fix F x = F x (λy h, fix F y) :=
  calc
    -- The proof is straightforward, it just uses fix_F_eq and proof irrelevance
    fix F x
        = F x (λy h, fix_F F y (acc.inv (Hwf x) h)) : fix_F_eq F x (Hwf x)
    ... = F x (λy h, fix F y)                       : rfl  -- proof irrelevance is used here

end well_founded

-- Empty relation is well-founded
definition empty.wf {A : Type} : well_founded (λa b : A, false) :=
well_founded.intro (λ (a : A),
  acc.intro a (λ (b : A) (lt : false), false.rec _ lt))

-- Subrelation of a well-founded relation is well-founded
namespace subrel
context
  parameters {A : Type} {R Q : A → A → Prop}
  parameters (H₁ : ∀{x y}, Q x y → R x y)
  parameters (H₂ : well_founded R)

  definition accessible {a : A} (ac : acc R a) : acc Q a :=
  acc.rec_on ac
    (λ (x : A) (ax : _) (iH : ∀ (y : A), R y x → acc Q y),
      acc.intro x (λ (y : A) (lt : Q y x), iH y (H₁ lt)))

  definition wf : well_founded Q :=
  well_founded.intro (λ a, accessible (H₂ a))
end
end subrel

definition inv_image {A B : Type} (R : B → B → Prop) (f : A → B) : A → A → Prop :=
λa₁ a₂, R (f a₁) (f a₂)

-- The inverse image of a well-founded relation is well-founded
namespace inv_image
context
  parameters {A B : Type} {R : B → B → Prop}
  parameters (f : A → B)
  parameters (H : well_founded R)

  definition accessible {a : A} (ac : acc R (f a)) : acc (inv_image R f) a :=
  have gen : ∀x, f x = f a → acc (inv_image R f) x, from
    acc.rec_on ac
      (λ (x : B) (ax : _)
         (iH : ∀y, R y x → (∀z, f z = y → acc (inv_image R f) z))
         (z : A) (eq₁ : f z = x),
        acc.intro z (λ (y : A) (lt : R (f y) (f z)),
          iH (f y) (eq.rec_on eq₁ lt) y rfl)),
  gen a rfl

  definition wf : well_founded (inv_image R f) :=
  well_founded.intro (λ a, accessible (H (f a)))
end
end inv_image

{'fraction_non_alphanumeric': 0.14482970236268794, 'fraction_numerical': 0.00245474071801166, 'mean_word_length': 2.254618072890664, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '730663', 'n_tokens_mistral': 2858, 'n_tokens_neox': 2754, 'n_words': 1228}