text:
/-
Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel, Yury Kudryashov
-/
import topology.uniform_space.basic
import topology.separation

/-!
# `Gδ` sets

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

In this file we define `Gδ` sets and prove their basic properties.

## Main definitions

* `is_Gδ`: a set `s` is a `Gδ` set if it can be represented as an intersection
  of countably many open sets;

* `residual`: the filter of residual sets. A set `s` is called *residual* if it includes a dense
  `Gδ` set. In a Baire space (e.g., in a complete (e)metric space), residual sets form a filter.

  For technical reasons, we define `residual` in any topological space but the definition agrees
  with the description above only in Baire spaces.

## Main results

We prove that finite or countable intersections of Gδ sets is a Gδ set. We also prove that the
continuity set of a function from a topological space to an (e)metric space is a Gδ set.

## Tags

Gδ set, residual set
-/

noncomputable theory
open_locale classical topology filter uniformity

open filter encodable set

variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}

section is_Gδ
variable [topological_space α]

/-- A Gδ set is a countable intersection of open sets. -/
def is_Gδ (s : set α) : Prop :=
  ∃T : set (set α), (∀t ∈ T, is_open t) ∧ T.countable ∧ s = (⋂₀ T)

/-- An open set is a Gδ set. -/
lemma is_open.is_Gδ {s : set α} (h : is_open s) : is_Gδ s :=
⟨{s}, by simp [h], countable_singleton _, (set.sInter_singleton _).symm⟩

@[simp] lemma is_Gδ_empty : is_Gδ (∅ : set α) := is_open_empty.is_Gδ

@[simp] lemma is_Gδ_univ : is_Gδ (univ : set α) := is_open_univ.is_Gδ

lemma is_Gδ_bInter_of_open {I : set ι} (hI : I.countable) {f : ι → set α}
  (hf : ∀i ∈ I, is_open (f i)) : is_Gδ (⋂i∈I, f i) :=
⟨f '' I, by rwa ball_image_iff, hI.image _, by rw sInter_image⟩

lemma is_Gδ_Inter_of_open [encodable ι] {f : ι → set α}
  (hf : ∀i, is_open (f i)) : is_Gδ (⋂i, f i) :=
⟨range f, by rwa forall_range_iff, countable_range _, by rw sInter_range⟩

/-- The intersection of an encodable family of Gδ sets is a Gδ set. -/
lemma is_Gδ_Inter [encodable ι] {s : ι → set α} (hs : ∀ i, is_Gδ (s i)) : is_Gδ (⋂ i, s i) :=
begin
  choose T hTo hTc hTs using hs,
  obtain rfl : s = λ i, ⋂₀ T i := funext hTs,
  refine ⟨⋃ i, T i, _, countable_Union hTc, (sInter_Union _).symm⟩,
  simpa [@forall_swap ι] using hTo
end

lemma is_Gδ_bInter {s : set ι} (hs : s.countable) {t : Π i ∈ s, set α}
  (ht : ∀ i ∈ s, is_Gδ (t i ‹_›)) : is_Gδ (⋂ i ∈ s, t i ‹_›) :=
begin
  rw [bInter_eq_Inter],
  haveI := hs.to_encodable,
  exact is_Gδ_Inter (λ x, ht x x.2)
end

/-- A countable intersection of Gδ sets is a Gδ set. -/
lemma is_Gδ_sInter {S : set (set α)} (h : ∀s∈S, is_Gδ s) (hS : S.countable) : is_Gδ (⋂₀ S) :=
by simpa only [sInter_eq_bInter] using is_Gδ_bInter hS h

lemma is_Gδ.inter {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) : is_Gδ (s ∩ t) :=
by { rw inter_eq_Inter, exact is_Gδ_Inter (bool.forall_bool.2 ⟨ht, hs⟩) }

/-- The union of two Gδ sets is a Gδ set. -/
lemma is_Gδ.union {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) : is_Gδ (s ∪ t) :=
begin
  rcases hs with ⟨S, Sopen, Scount, rfl⟩,
  rcases ht with ⟨T, Topen, Tcount, rfl⟩,
  rw [sInter_union_sInter],
  apply is_Gδ_bInter_of_open (Scount.prod Tcount),
  rintros ⟨a, b⟩ ⟨ha, hb⟩,
  exact (Sopen a ha).union (Topen b hb)
end

/-- The union of finitely many Gδ sets is a Gδ set. -/
lemma is_Gδ_bUnion {s : set ι} (hs : s.finite) {f : ι → set α} (h : ∀ i ∈ s, is_Gδ (f i)) :
  is_Gδ (⋃ i ∈ s, f i) :=
begin
  refine finite.induction_on hs (by simp) _ h,
  simp only [ball_insert_iff, bUnion_insert],
  exact λ a s _ _ ihs H, H.1.union (ihs H.2)
end

lemma is_closed.is_Gδ {α} [uniform_space α] [is_countably_generated (𝓤 α)]
  {s : set α} (hs : is_closed s) : is_Gδ s :=
begin
  rcases (@uniformity_has_basis_open α _).exists_antitone_subbasis  with ⟨U, hUo, hU, -⟩,
  rw [← hs.closure_eq, ← hU.bInter_bUnion_ball],
  refine is_Gδ_bInter (to_countable _) (λ n hn, is_open.is_Gδ _),
  exact is_open_bUnion (λ x hx, uniform_space.is_open_ball _ (hUo _).2)
end

section t1_space

variable [t1_space α]

lemma is_Gδ_compl_singleton (a : α) : is_Gδ ({a}ᶜ : set α) :=
is_open_compl_singleton.is_Gδ

lemma set.countable.is_Gδ_compl {s : set α} (hs : s.countable) : is_Gδ sᶜ :=
begin
  rw [← bUnion_of_singleton s, compl_Union₂],
  exact is_Gδ_bInter hs (λ x _, is_Gδ_compl_singleton x)
end

lemma set.finite.is_Gδ_compl {s : set α} (hs : s.finite) : is_Gδ sᶜ :=
hs.countable.is_Gδ_compl

lemma set.subsingleton.is_Gδ_compl {s : set α} (hs : s.subsingleton) : is_Gδ sᶜ :=
hs.finite.is_Gδ_compl

lemma finset.is_Gδ_compl (s : finset α) : is_Gδ (sᶜ : set α) :=
s.finite_to_set.is_Gδ_compl

open topological_space

variables [first_countable_topology α]

lemma is_Gδ_singleton (a : α) : is_Gδ ({a} : set α) :=
begin
  rcases (nhds_basis_opens a).exists_antitone_subbasis with ⟨U, hU, h_basis⟩,
  rw [← bInter_basis_nhds h_basis.to_has_basis],
  exact is_Gδ_bInter (to_countable _) (λ n hn, (hU n).2.is_Gδ),
end

lemma set.finite.is_Gδ {s : set α} (hs : s.finite) : is_Gδ s :=
finite.induction_on hs is_Gδ_empty $ λ a s _ _ hs, (is_Gδ_singleton a).union hs

end t1_space

end is_Gδ

section continuous_at

open topological_space
open_locale uniformity

variables [topological_space α]

/-- The set of points where a function is continuous is a Gδ set. -/
lemma is_Gδ_set_of_continuous_at [uniform_space β] [is_countably_generated (𝓤 β)] (f : α → β) :
  is_Gδ {x | continuous_at f x} :=
begin
  obtain ⟨U, hUo, hU⟩ := (@uniformity_has_basis_open_symmetric β _).exists_antitone_subbasis,
  simp only [uniform.continuous_at_iff_prod, nhds_prod_eq],
  simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.to_has_basis, forall_prop_of_true,
    set_of_forall, id],
  refine is_Gδ_Inter (λ k, is_open.is_Gδ $ is_open_iff_mem_nhds.2 $ λ x, _),
  rintros ⟨s, ⟨hsx, hso⟩, hsU⟩,
  filter_upwards [is_open.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩,
end

end continuous_at

/-- A set `s` is called *residual* if it includes a dense `Gδ` set. If `α` is a Baire space
(e.g., a complete metric space), then residual sets form a filter, see `mem_residual`.

For technical reasons we define the filter `residual` in any topological space but in a non-Baire
space it is not useful because it may contain some non-residual sets. -/
def residual (α : Type*) [topological_space α] : filter α :=
⨅ t (ht : is_Gδ t) (ht' : dense t), 𝓟 t

repo: mathlib


text:
import category_theory.limits.shapes.finite_products
import category_theory.products.basic
import for_mathlib.category_theory.functor_misc
import for_mathlib.category_theory.limits
import category_theory.limits.opposites
import category_theory.adjunction.limits

noncomputable theory

namespace category_theory

open category

section
variables {C D : Type*} [category C] [category D]

namespace limits

variable (C)

def is_left_adjoint_diag_of_has_binary_products [has_binary_products C] :
  is_left_adjoint (functor.diag C) :=
{ right := uncurry.obj prod.functor,
  adj :=
  { hom_equiv := λ X Y,
    { to_fun := λ f, prod.lift f.1 f.2,
      inv_fun := λ g, ⟨g ≫ prod.fst, g ≫ prod.snd⟩,
      left_inv := by tidy,
      right_inv := by tidy, },
    unit := { app := λ X, prod.lift (𝟙 X) (𝟙 X), },
    counit := { app := λ Y, ⟨prod.fst, prod.snd⟩, }, }, }

variable {C}

lemma limit_cone_pair_of_is_left_adjoint_diag [is_left_adjoint (functor.diag C)]
  (X₁ X₂ : C) : limit_cone (pair X₁ X₂) :=
begin
  let Δ := functor.diag C,
  let R := right_adjoint Δ,
  let adj : Δ ⊣ R := is_left_adjoint.adj,
  let η := adj.counit.app ⟨X₁, X₂⟩,
  refine limit_cone.mk (binary_fan.mk η.1 η.2) _,
  refine binary_fan.is_limit.mk _ (λ A f₁ f₂, (adj.hom_equiv A ⟨X₁, X₂⟩) ⟨f₁, f₂⟩)
    (λ A f₁ f₂, _) (λ A f₁ f₂, _) (λ A f₁ f₂ φ hφ₁ hφ₂, _),
  { dsimp [η],
    simpa only [adjunction.hom_equiv_unit, category.assoc]
      using congr_arg (λ x : (_ × _), x.1) (adj.compatibility (⟨f₁, f₂⟩ : Δ.obj A ⟶ ⟨X₁, X₂⟩)), },
  { dsimp [η],
    simpa only [adjunction.hom_equiv_unit, category.assoc]
      using congr_arg (λ x : (_ × _), x.2) (adj.compatibility (⟨f₁, f₂⟩ : Δ.obj A ⟶ ⟨X₁, X₂⟩)), },
  { dsimp,
    symmetry,
    rw [adj.hom_equiv_apply_eq, ← hφ₁, ← hφ₂],
    simp only [binary_fan.mk_fst, binary_fan.mk_snd, adjunction.hom_equiv_counit,
      functor.diag_map, prod_comp], },
end

variable (C)

lemma has_binary_products_of_is_left_adjoint_diag [is_left_adjoint (functor.diag C)] :
  has_binary_products C :=
begin
  haveI : ∀ (X₁ X₂ : C), has_limit (pair X₁ X₂) := λ X₁ X₂,
    has_limit.mk (limit_cone_pair_of_is_left_adjoint_diag X₁ X₂),
  apply has_binary_products_of_has_limit_pair,
end

lemma is_left_adjoint_const_of_has_terminal [has_terminal C]
  {T : Type*} (t : T) [subsingleton T] :
    is_left_adjoint ((functor.const C).obj (discrete.mk t)) :=
{ right := (functor.const (discrete T)).obj (terminal C),
  adj :=
  { hom_equiv := λ X Y,
    { to_fun := λ f, terminal.from _,
      inv_fun := λ f, eq_to_hom (subsingleton.elim _ _),
      left_inv := by tidy,
      right_inv := by tidy, },
    unit := { app := terminal.from, },
    counit := { app := λ Y, eq_to_hom (subsingleton.elim _ _), }, }, }

lemma has_terminal_of_is_left_adjoint_const {T : Type*} (t : T) [subsingleton T]
    [is_left_adjoint ((functor.const C).obj (discrete.mk t))] : has_terminal C :=
begin
  let G := ((functor.const C).obj (discrete.mk t)),
  let F := right_adjoint G,
  let adj : G ⊣ F := is_left_adjoint.adj,
  haveI : ∀ (X : C), unique (X ⟶ F.obj (discrete.mk t)),
  { intro X,
    haveI : subsingleton (X ⟶ F.obj (discrete.mk t)),
    { constructor,
      intros x y,
      apply (adj.hom_equiv _ _).symm.injective,
      apply subsingleton.elim, },
    exact unique_of_subsingleton
      (adj.hom_equiv _ _ (eq_to_hom (subsingleton.elim _ _))), },
  exact has_terminal_of_unique (F.obj (discrete.mk t)),
end

variable {C}

lemma limit.congr_π {J : Type*} [category J] (F : J ⥤ C) [has_limit F] {j₁ j₂ : J}
  (h : j₁ = j₂) : limit.π F j₁ ≫ eq_to_hom (by rw h) = limit.π F j₂ :=
by { subst h, rw [eq_to_hom_refl, category.comp_id], }

variable (C)

lemma has_finite_products_of_has_binary_products
  [has_terminal C] [has_binary_products C] : has_finite_products C :=
begin
  constructor,
  intro n,
  induction n with n hn,
  { exact has_limits_of_shape_of_equivalence (discrete.equivalence
      (equiv.equiv_of_is_empty (pempty : Type) (fin 0))), },
  { constructor,
    intro F,
    have hF : ∃ (φ : fin (n+1) → C), nonempty (F ≅ discrete.functor φ) :=
      ⟨F.obj ∘ discrete.mk, nonempty.intro discrete.nat_iso_functor⟩,
    rcases hF with ⟨φ, hφ⟩,
    suffices : has_limit (discrete.functor φ),
    { haveI := this,
      exact has_limit_of_iso hφ.some.symm, },
    clear hφ F,
    haveI := hn,
    let L := prod (φ 0) (limit (discrete.functor (λ (i : fin n), φ i.succ))),
    let π : Π (i : fin (n+1)), L ⟶ φ i,
    { intro i,
      by_cases i = 0,
      { subst h,
        exact prod.fst, },
      { exact prod.snd ≫ limit.π _ (discrete.mk (i.pred h)) ≫
        eq_to_hom (by { dsimp, rw i.succ_pred h,}), }, },
    have hπ₀ : π 0 = prod.fst := rfl,
    have hπ : ∀ (i : fin n), π i.succ = prod.snd ≫ limit.π _ (discrete.mk i),
    { intro i,
      dsimp [π],
      rw dif_neg i.succ_ne_zero,
      congr' 1,
      exact limit.congr_π (discrete.functor (λ (i : fin n), φ i.succ))
        (congr_arg discrete.mk i.pred_succ), },
    let c : fan φ := fan.mk L π,
    have hc : is_limit c,
    { refine mk_fan_limit _ (λ s, prod.lift (s.proj 0) (pi.lift (λ i, s.proj i.succ)))
         _ _,
      { intros s i,
        by_cases i = 0,
        { subst h,
          simp only [hπ₀, fan_mk_proj, prod.lift_fst], },
        { cases fin.eq_succ_of_ne_zero h with j hj,
          subst hj,
          simp only [hπ, fan_mk_proj, prod.lift_snd_assoc, limit.lift_π, fan.mk_π_app], }, },
      { intros s f hs,
        ext,
        { simpa only [prod.lift_fst] using hs 0, },
        { discrete_cases,
          rw [assoc, assoc, prod.lift_snd_assoc, limit.lift_π, fan.mk_π_app, ← hs j.succ],
          dsimp [c],
          rw hπ, }, }, },
    exact has_limit.mk ⟨c, hc⟩, },
end

local attribute [instance] has_limits_of_shape_op_of_has_colimits_of_shape

lemma has_binary_products_opposite [has_binary_coproducts C] : has_binary_products Cᵒᵖ :=
begin
  resetI,
  haveI : has_colimits_of_shape (discrete walking_pair)ᵒᵖ C :=
    has_colimits_of_shape_of_equivalence (discrete.opposite _).symm,
  apply_instance,
end

lemma has_finite_coproducts_of_has_binary_coproducts
  [has_initial C] [has_binary_coproducts C] : has_finite_coproducts C :=
⟨λ J, begin
  suffices : has_finite_products Cᵒᵖ,
  { haveI := this,
    exact adjunction.has_colimits_of_shape_of_equivalence (op_op_equivalence C).inverse, },
  haveI : has_terminal Cᵒᵖ := infer_instance,
  haveI : has_binary_products Cᵒᵖ := has_binary_products_opposite _,
  exact has_finite_products_of_has_binary_products Cᵒᵖ,
end⟩

end limits

end

section

variables {J : Type*} {C : J → Type*} {D : J → Type*}
  [Π j, category (C j)] [Π j, category (D j)] {E : Type*} [category E]

instance : category (Π j, C j) :=
{ hom := λ X Y, Π j, X j ⟶ Y j,
  id := λ X j, 𝟙 (X j),
  comp := λ X Y Z f g j, f j ≫ g j, }

@[simps]
def functor.pi_ (F : Π j, C j ⥤ D j) : (Π j, C j) ⥤ (Π j, D j) :=
{ obj := λ X j, (F j).obj (X j),
  map := λ X Y f j, (F j).map (f j), }

@[simps]
def functor.pi'_ (F : Π j, E ⥤ D j) : E ⥤ (Π j, D j) :=
{ obj := λ X j, (F j).obj X,
  map := λ X Y f j, (F j).map f, }

@[simps]
def nat_trans.pi_ {F G : Π j, C j ⥤ D j} (e : Π j, F j ⟶ G j) :
  functor.pi_ F ⟶ functor.pi_ G :=
{ app := λ X j, (e j).app (X j), }

@[simps]
def nat_iso.pi {F G : Π j, C j ⥤ D j} (e : Π j, F j ≅ G j) :
  functor.pi_ F ≅ functor.pi_ G :=
{ hom := nat_trans.pi_ (λ j, (e j).hom),
  inv := nat_trans.pi_ (λ j, (e j).inv), }

@[simps]
def nat_trans.pi'_ {F G : Π j, E ⥤ D j} (e : Π j, F j ⟶ G j) :
  functor.pi'_ F ⟶ functor.pi'_ G :=
{ app := λ X j, (e j).app X, }

@[simps]
def nat_iso.pi'_ {F G : Π j, E ⥤ D j} (e : Π j, F j ≅ G j) :
  functor.pi'_ F ≅ functor.pi'_ G :=
{ hom := nat_trans.pi'_ (λ j, (e j).hom),
  inv := nat_trans.pi'_ (λ j, (e j).inv), }

@[simps]
def equivalence.pi (e : Π j, C j ≌ D j) : (Π j, C j) ≌ (Π j, D j) :=
{ functor := functor.pi_ (λ j, (e j).functor),
  inverse := functor.pi_ (λ j, (e j).inverse),
  unit_iso := nat_iso.pi (λ j, (e j).unit_iso),
  counit_iso := nat_iso.pi (λ j, (e j).counit_iso), }

variable (C)

@[simps]
def functor.pi_.eval (j : J) : (Π j, C j) ⥤ C j :=
{ obj := λ X, X j,
  map := λ X Y f, f j, }

variable {C}

@[simp]
lemma functor.pi_eval (F : Π j, C j ⥤ D j) (j : J) :
  functor.pi_ F ⋙ functor.pi_.eval _ j = functor.pi_.eval _ j ⋙ F j := rfl

@[simp]
def functor.pi'__eval (F : Π j, E ⥤ D j) (j : J) :
  functor.pi'_ F ⋙ functor.pi_.eval _ j = F j :=
functor.ext (λ X, rfl) (by tidy)

@[simp]
def functor.pi'__eval_iso (F : Π j, E ⥤ D j) (j : J) :
  functor.pi'_ F ⋙ functor.pi_.eval _ j ≅ F j :=
eq_to_iso (functor.pi'__eval F j)

lemma functor.pi_.ext {F₁ F₂ : E ⥤ (Π j, C j)}
  (h : ∀ (j : J), F₁ ⋙ functor.pi_.eval _ j = F₂ ⋙ functor.pi_.eval _ j) : F₁ = F₂ :=
begin
  refine functor.ext (λ X, _) (λ X Y f, _),
  { ext j,
    exact functor.congr_obj (h j) X, },
  { ext j,
    simpa only [pi.comp_apply, functor.eq_to_hom_proj]
      using functor.congr_map_conjugate (h j) f, },
end

@[simps]
def functor.pi_.mk_nat_trans {F₁ F₂ : E ⥤ (Π j, C j)}
  (τ : Π (j : J), F₁ ⋙ functor.pi_.eval _ j ⟶ F₂ ⋙ functor.pi_.eval _ j) : F₁ ⟶ F₂ :=
{ app := λ X j, (τ j).app X,
  naturality' := λ X Y f, by { ext j, exact (τ j).naturality f, }, }

@[simps]
def functor.pi_.mk_nat_iso {F₁ F₂ : E ⥤ (Π j, C j)}
  (e : Π (j : J), F₁ ⋙ functor.pi_.eval _ j ≅ F₂ ⋙ functor.pi_.eval _ j) : F₁ ≅ F₂ :=
{ hom := functor.pi_.mk_nat_trans (λ j, (e j).hom),
  inv := functor.pi_.mk_nat_trans (λ j, (e j).inv), }

variable (C)

def pi.equivalence_of_eq {j j' : J} (eq : j = j') : C j ≌ C j' := by subst eq

def pi.equivalence_of_eq_functor_eq {J' : Type*} {j'₁ j'₂ : J'} (f : J' → J) (eq : j'₁ = j'₂) :
  (pi.equivalence_of_eq (λ j', C (f j')) eq).functor = (pi.equivalence_of_eq C (by rw eq)).functor :=
by { subst eq, refl, }

def pi.equivalence_of_eq_functor_iso {J' : Type*} {j'₁ j'₂ : J'} (f : J' → J) (eq : j'₁ = j'₂) :
  (pi.equivalence_of_eq (λ j', C (f j')) eq).functor ≅ (pi.equivalence_of_eq C (by rw eq)).functor :=
by { subst eq, refl, }

@[simp]
def pi.equivalence_of_eq_functor_iso_hom_app {J' : Type*} {j'₁ j'₂ : J'} (f : J' → J) (eq : j'₁ = j'₂)
  (X : C (f j'₁)) :
  (pi.equivalence_of_eq_functor_iso C f eq).hom.app X = eq_to_hom (by { subst eq, refl, }) :=
by { subst eq, refl, }

@[simp]
lemma pi.equivalence_of_eq_functor_iso_refl {J' : Type*} (j' : J') (f : J' → J) :
  pi.equivalence_of_eq_functor_iso C f (show j' = j', by refl) = iso.refl _ := rfl

def functor.pi_.eval_eq_of_eq {j j' : J} (eq : j = j') :
  functor.pi_.eval C j ⋙ (pi.equivalence_of_eq C eq).functor = functor.pi_.eval C j' :=
by { subst eq, refl, }

@[simps]
def functor.pi_.eval_iso_of_eq {j j' : J} (eq : j = j') :
  functor.pi_.eval C j ⋙ (pi.equivalence_of_eq C eq).functor ≅ functor.pi_.eval C j' :=
by { apply eq_to_iso, subst eq, refl, }

lemma functor.pi_.eval_iso_of_eq_refl (j : J) :
  functor.pi_.eval_iso_of_eq C (show j = j, by refl) = iso.refl _ := rfl

@[simp]
lemma functor.pi_.eval_iso_of_eq_eq_to_hom {j j' : J} (eq : j = j') (X : Π j, C j) :
  (functor.pi_.eval_iso_of_eq C eq).hom.app X = eq_to_hom (by { subst eq, refl, }) :=
by simp only [functor.pi_.eval_iso_of_eq_hom, eq_to_hom_app]

variable {C}

def functor.pi_.lift (F : Π j, E ⥤ C j) : E ⥤ Π j, C j :=
{ obj := λ X j, (F j).obj X,
  map := λ X Y f j, (F j).map f, }

end

variables (C : Type*) [category C]

@[simps]
def pi_equivalence_functors_from_discrete (J : Type*) :
  (Π (j : J), C) ≌ (discrete J ⥤ C) :=
{ functor :=
  { obj := λ F, discrete.functor F,
    map := λ F₁ F₂ f, discrete.nat_trans (by { rintro ⟨i⟩, exact f i}),
    map_id' := λ F, by { ext j, cases j, refl, },
    map_comp' := λ F₁ F₂ F₃ f g, by { ext j, cases j, refl, }, },
  inverse :=
  { obj := λ F j, F.obj (discrete.mk j),
    map := λ F₁ F₂ f j, f.app (discrete.mk j), },
  unit_iso := eq_to_iso rfl,
  counit_iso := eq_to_iso begin
    refine functor.ext (λ F, _) (λ F₁ F₂ f, _),
    { refine functor.ext _ _,
      { rintro ⟨j⟩, refl, },
      { rintros ⟨j⟩ ⟨j'⟩ f,
        have h := discrete.eq_of_hom f,
        dsimp at h,
        subst h,
        have h' : f = 𝟙 _ := by tidy,
        subst h',
        dsimp,
        simpa, }, },
    { ext j,
      cases j,
      dsimp,
      simp,
      erw id_comp, },
  end,
  functor_unit_iso_comp' := λ X, begin
    ext j,
    cases j,
    dsimp,
    simpa,
  end, }

def functor.pi.diag (J : Type*) : C ⥤ Π (j : J), C := functor.pi_.lift (λ j, 𝟭 C)

namespace limits

def is_left_adjoint_of_has_limits_of_shape_discrete (J : Type*)
  [has_limits_of_shape (discrete J) C] : is_left_adjoint (functor.pi.diag C J) :=
⟨_, const_lim_adj.comp (pi_equivalence_functors_from_discrete C J).symm.to_adjunction⟩

variable {C}

@[simps]
lemma pi.limit_cone_of_adjunction_diag {J : Type*} {R : (Π (j : J), C) ⥤ C}
  (adj : (functor.pi.diag C J) ⊣ R) (X : J → C) : limit_cone (discrete.functor X) :=
begin
  refine limit_cone.mk (fan.mk (R.obj X) (λ j, adj.counit.app X j)) _,
  refine mk_fan_limit _ (λ s, adj.hom_equiv s.X X (λ j, s.proj j)) (λ s, _) (λ s m hm, _),
  { intro j,
    dsimp,
    simpa only [adjunction.hom_equiv_unit, assoc] using congr_arg
      (λ (f : Π j, s.X ⟶ X j), f j) (adj.compatibility (λ j, s.proj j : (functor.pi.diag C J).obj s.X ⟶ X)), },
  { dsimp,
    symmetry,
    simp only [adj.hom_equiv_apply_eq],
    ext j,
    rw ← hm,
    simpa only [adjunction.hom_equiv_counit], },
end

variable (C)

lemma has_limits_of_shape_discrete_of_is_left_adjoint_diag (J : Type*)
  [h : is_left_adjoint (functor.pi.diag C J)] : has_limits_of_shape (discrete J) C :=
⟨λ F, begin
  haveI : has_limit (discrete.functor (F.obj ∘ discrete.mk)),
  { exact ⟨nonempty.intro (pi.limit_cone_of_adjunction_diag h.adj _)⟩, },
  exact has_limit_of_iso discrete.nat_iso_functor.symm,
end⟩

lemma has_finite_products_of_is_left_adjoint_diag
  [Π (J : Type) [fintype J], is_left_adjoint (functor.pi.diag C J)] : has_finite_products C :=
⟨λ J, by { apply has_limits_of_shape_discrete_of_is_left_adjoint_diag, }⟩

end limits

end category_theory

author: joelriou


text:
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import data.num.bitwise
import data.int.char_zero
import data.nat.gcd
import data.nat.psub

/-!
# Properties of the binary representation of integers
-/

local attribute [simp] add_assoc

namespace pos_num
variables {α : Type*}

@[simp, norm_cast] theorem cast_one [has_one α] [has_add α] :
  ((1 : pos_num) : α) = 1 := rfl
@[simp] theorem cast_one' [has_one α] [has_add α] : (pos_num.one : α) = 1 := rfl
@[simp, norm_cast] theorem cast_bit0 [has_one α] [has_add α] (n : pos_num) :
  (n.bit0 : α) = _root_.bit0 n := rfl
@[simp, norm_cast] theorem cast_bit1 [has_one α] [has_add α] (n : pos_num) :
  (n.bit1 : α) = _root_.bit1 n := rfl

@[simp, norm_cast] theorem cast_to_nat [add_monoid α] [has_one α] :
  ∀ n : pos_num, ((n : ℕ) : α) = n
| 1        := nat.cast_one
| (bit0 p) := (nat.cast_bit0 _).trans $ congr_arg _root_.bit0 p.cast_to_nat
| (bit1 p) := (nat.cast_bit1 _).trans $ congr_arg _root_.bit1 p.cast_to_nat

@[simp, norm_cast] theorem to_nat_to_int (n : pos_num) : ((n : ℕ) : ℤ) = n :=
by rw [← int.nat_cast_eq_coe_nat, cast_to_nat]

@[simp, norm_cast] theorem cast_to_int [add_group α] [has_one α] (n : pos_num) :
  ((n : ℤ) : α) = n :=
by rw [← to_nat_to_int, int.cast_coe_nat, cast_to_nat]

theorem succ_to_nat : ∀ n, (succ n : ℕ) = n + 1
| 1        := rfl
| (bit0 p) := rfl
| (bit1 p) := (congr_arg _root_.bit0 (succ_to_nat p)).trans $
  show ↑p + 1 + ↑p + 1 = ↑p + ↑p + 1 + 1, by simp [add_left_comm]

theorem one_add (n : pos_num) : 1 + n = succ n := by cases n; refl
theorem add_one (n : pos_num) : n + 1 = succ n := by cases n; refl

@[norm_cast]
theorem add_to_nat : ∀ m n, ((m + n : pos_num) : ℕ) = m + n
| 1        b        := by rw [one_add b, succ_to_nat, add_comm]; refl
| a        1        := by rw [add_one a, succ_to_nat]; refl
| (bit0 a) (bit0 b) := (congr_arg _root_.bit0 (add_to_nat a b)).trans $
  show ((a + b) + (a + b) : ℕ) = (a + a) + (b + b), by simp [add_left_comm]
| (bit0 a) (bit1 b) := (congr_arg _root_.bit1 (add_to_nat a b)).trans $
  show ((a + b) + (a + b) + 1 : ℕ) = (a + a) + (b + b + 1), by simp [add_left_comm]
| (bit1 a) (bit0 b) := (congr_arg _root_.bit1 (add_to_nat a b)).trans $
  show ((a + b) + (a + b) + 1 : ℕ) = (a + a + 1) + (b + b), by simp [add_comm, add_left_comm]
| (bit1 a) (bit1 b) :=
  show (succ (a + b) + succ (a + b) : ℕ) = (a + a + 1) + (b + b + 1),
  by rw [succ_to_nat, add_to_nat]; simp [add_left_comm]

theorem add_succ : ∀ (m n : pos_num), m + succ n = succ (m + n)
| 1        b        := by simp [one_add]
| (bit0 a) 1        := congr_arg bit0 (add_one a)
| (bit1 a) 1        := congr_arg bit1 (add_one a)
| (bit0 a) (bit0 b) := rfl
| (bit0 a) (bit1 b) := congr_arg bit0 (add_succ a b)
| (bit1 a) (bit0 b) := rfl
| (bit1 a) (bit1 b) := congr_arg bit1 (add_succ a b)

theorem bit0_of_bit0 : Π n, _root_.bit0 n = bit0 n
| 1        := rfl
| (bit0 p) := congr_arg bit0 (bit0_of_bit0 p)
| (bit1 p) := show bit0 (succ (_root_.bit0 p)) = _, by rw bit0_of_bit0; refl

theorem bit1_of_bit1 (n : pos_num) : _root_.bit1 n = bit1 n :=
show _root_.bit0 n + 1 = bit1 n, by rw [add_one, bit0_of_bit0]; refl

@[norm_cast]
theorem mul_to_nat (m) : ∀ n, ((m * n : pos_num) : ℕ) = m * n
| 1        := (mul_one _).symm
| (bit0 p) := show (↑(m * p) + ↑(m * p) : ℕ) = ↑m * (p + p), by rw [mul_to_nat, left_distrib]
| (bit1 p) := (add_to_nat (bit0 (m * p)) m).trans $
  show (↑(m * p) + ↑(m * p) + ↑m : ℕ) = ↑m * (p + p) + m, by rw [mul_to_nat, left_distrib]

theorem to_nat_pos : ∀ n : pos_num, 0 < (n : ℕ)
| 1        := zero_lt_one
| (bit0 p) := let h := to_nat_pos p in add_pos h h
| (bit1 p) := nat.succ_pos _

theorem cmp_to_nat_lemma {m n : pos_num} : (m:ℕ) < n → (bit1 m : ℕ) < bit0 n :=
show (m:ℕ) < n → (m + m + 1 + 1 : ℕ) ≤ n + n,
by intro h; rw [nat.add_right_comm m m 1, add_assoc]; exact add_le_add h h

theorem cmp_swap (m) : ∀n, (cmp m n).swap = cmp n m :=
by induction m with m IH m IH; intro n;
   cases n with n n; try {unfold cmp}; try {refl}; rw ←IH; cases cmp m n; refl

theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((n:ℕ) < m) : Prop)
| 1        1        := rfl
| (bit0 a) 1        := let h : (1:ℕ) ≤ a := to_nat_pos a in add_le_add h h
| (bit1 a) 1        := nat.succ_lt_succ $ to_nat_pos $ bit0 a
| 1        (bit0 b) := let h : (1:ℕ) ≤ b := to_nat_pos b in add_le_add h h
| 1        (bit1 b) := nat.succ_lt_succ $ to_nat_pos $ bit0 b
| (bit0 a) (bit0 b) := begin
    have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
    { exact add_lt_add this this },
    { rw this },
    { exact add_lt_add this this }
  end
| (bit0 a) (bit1 b) := begin dsimp [cmp],
    have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
    { exact nat.le_succ_of_le (add_lt_add this this) },
    { rw this, apply nat.lt_succ_self },
    { exact cmp_to_nat_lemma this }
  end
| (bit1 a) (bit0 b) := begin dsimp [cmp],
    have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
    { exact cmp_to_nat_lemma this },
    { rw this, apply nat.lt_succ_self },
    { exact nat.le_succ_of_le (add_lt_add this this) },
  end
| (bit1 a) (bit1 b) := begin
    have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
    { exact nat.succ_lt_succ (add_lt_add this this) },
    { rw this },
    { exact nat.succ_lt_succ (add_lt_add this this) }
  end

@[norm_cast]
theorem lt_to_nat {m n : pos_num} : (m:ℕ) < n ↔ m < n :=
show (m:ℕ) < n ↔ cmp m n = ordering.lt, from
match cmp m n, cmp_to_nat m n with
| ordering.lt, h := by simp at h; simp [h]
| ordering.eq, h := by simp at h; simp [h, lt_irrefl]; exact dec_trivial
| ordering.gt, h := by simp [not_lt_of_gt h]; exact dec_trivial
end

@[norm_cast]
theorem le_to_nat {m n : pos_num} : (m:ℕ) ≤ n ↔ m ≤ n :=
by rw ← not_lt; exact not_congr lt_to_nat

end pos_num

namespace num
variables {α : Type*}
open pos_num

theorem add_zero (n : num) : n + 0 = n := by cases n; refl
theorem zero_add (n : num) : 0 + n = n := by cases n; refl

theorem add_one : ∀ n : num, n + 1 = succ n
| 0       := rfl
| (pos p) := by cases p; refl

theorem add_succ : ∀ (m n : num), m + succ n = succ (m + n)
| 0       n       := by simp [zero_add]
| (pos p) 0       := show pos (p + 1) = succ (pos p + 0),
                     by rw [pos_num.add_one, add_zero]; refl
| (pos p) (pos q) := congr_arg pos (pos_num.add_succ _ _)

@[simp, norm_cast] theorem add_of_nat (m) : ∀ n, ((m + n : ℕ) : num) = m + n
| 0     := (add_zero _).symm
| (n+1) := show ((m + n : ℕ) + 1 : num) = m + (↑ n + 1),
           by rw [add_one, add_one, add_succ, add_of_nat]

theorem bit0_of_bit0 : ∀ n : num, bit0 n = n.bit0
| 0       := rfl
| (pos p) := congr_arg pos p.bit0_of_bit0

theorem bit1_of_bit1 : ∀ n : num, bit1 n = n.bit1
| 0       := rfl
| (pos p) := congr_arg pos p.bit1_of_bit1

@[simp, norm_cast] theorem cast_zero [has_zero α] [has_one α] [has_add α] :
  ((0 : num) : α) = 0 := rfl

@[simp] theorem cast_zero' [has_zero α] [has_one α] [has_add α] :
  (num.zero : α) = 0 := rfl

@[simp, norm_cast] theorem cast_one [has_zero α] [has_one α] [has_add α] :
  ((1 : num) : α) = 1 := rfl

@[simp] theorem cast_pos [has_zero α] [has_one α] [has_add α]
  (n : pos_num) : (num.pos n : α) = n := rfl

theorem succ'_to_nat : ∀ n, (succ' n : ℕ) = n + 1
| 0       := (_root_.zero_add _).symm
| (pos p) := pos_num.succ_to_nat _

theorem succ_to_nat (n) : (succ n : ℕ) = n + 1 := succ'_to_nat n

@[simp, norm_cast] theorem cast_to_nat [add_monoid α] [has_one α] : ∀ n : num, ((n : ℕ) : α) = n
| 0       := nat.cast_zero
| (pos p) := p.cast_to_nat

@[simp, norm_cast] theorem to_nat_to_int (n : num) : ((n : ℕ) : ℤ) = n :=
by rw [← int.nat_cast_eq_coe_nat, cast_to_nat]

@[simp, norm_cast] theorem cast_to_int [add_group α] [has_one α] (n : num) : ((n : ℤ) : α) = n :=
by rw [← to_nat_to_int, int.cast_coe_nat, cast_to_nat]

@[norm_cast]
theorem to_of_nat : Π (n : ℕ), ((n : num) : ℕ) = n
| 0     := rfl
| (n+1) := by rw [nat.cast_add_one, add_one, succ_to_nat, to_of_nat]

@[simp, norm_cast]
theorem of_nat_cast [add_monoid α] [has_one α] (n : ℕ) : ((n : num) : α) = n :=
by rw [← cast_to_nat, to_of_nat]

@[norm_cast] theorem of_nat_inj {m n : ℕ} : (m : num) = n ↔ m = n :=
⟨λ h, function.left_inverse.injective to_of_nat h, congr_arg _⟩

@[norm_cast]
theorem add_to_nat : ∀ m n, ((m + n : num) : ℕ) = m + n
| 0       0       := rfl
| 0       (pos q) := (_root_.zero_add _).symm
| (pos p) 0       := rfl
| (pos p) (pos q) := pos_num.add_to_nat _ _

@[norm_cast]
theorem mul_to_nat : ∀ m n, ((m * n : num) : ℕ) = m * n
| 0       0       := rfl
| 0       (pos q) := (zero_mul _).symm
| (pos p) 0       := rfl
| (pos p) (pos q) := pos_num.mul_to_nat _ _

theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((n:ℕ) < m) : Prop)
| 0       0       := rfl
| 0       (pos b) := to_nat_pos _
| (pos a) 0       := to_nat_pos _
| (pos a) (pos b) :=
  by { have := pos_num.cmp_to_nat a b; revert this; dsimp [cmp];
       cases pos_num.cmp a b, exacts [id, congr_arg pos, id] }

@[norm_cast]
theorem lt_to_nat {m n : num} : (m:ℕ) < n ↔ m < n :=
show (m:ℕ) < n ↔ cmp m n = ordering.lt, from
match cmp m n, cmp_to_nat m n with
| ordering.lt, h := by simp at h; simp [h]
| ordering.eq, h := by simp at h; simp [h, lt_irrefl]; exact dec_trivial
| ordering.gt, h := by simp [not_lt_of_gt h]; exact dec_trivial
end

@[norm_cast]
theorem le_to_nat {m n : num} : (m:ℕ) ≤ n ↔ m ≤ n :=
by rw ← not_lt; exact not_congr lt_to_nat

end num

namespace pos_num
@[simp] theorem of_to_nat : Π (n : pos_num), ((n : ℕ) : num) = num.pos n
| 1        := rfl
| (bit0 p) :=
  show ↑(p + p : ℕ) = num.pos p.bit0,
  by rw [num.add_of_nat, of_to_nat];
    exact congr_arg num.pos p.bit0_of_bit0
| (bit1 p) :=
  show ((p + p : ℕ) : num) + 1 = num.pos p.bit1,
  by rw [num.add_of_nat, of_to_nat];
    exact congr_arg num.pos p.bit1_of_bit1
end pos_num

namespace num

@[simp, norm_cast] theorem of_to_nat : Π (n : num), ((n : ℕ) : num) = n
| 0           := rfl
| (pos p) := p.of_to_nat

@[norm_cast] theorem to_nat_inj {m n : num} : (m : ℕ) = n ↔ m = n :=
⟨λ h, function.left_inverse.injective of_to_nat h, congr_arg _⟩

/--
This tactic tries to turn an (in)equality about `num`s to one about `nat`s by rewriting.
```lean
example (n : num) (m : num) : n ≤ n + m :=
begin
  num.transfer_rw,
  exact nat.le_add_right _ _
end
```
-/
meta def transfer_rw : tactic unit :=
`[repeat {rw ← to_nat_inj <|> rw ← lt_to_nat <|> rw ← le_to_nat},
  repeat {rw add_to_nat <|> rw mul_to_nat <|> rw cast_one <|> rw cast_zero}]

/--
This tactic tries to prove (in)equalities about `num`s by transfering them to the `nat` world and
then trying to call `simp`.
```lean
example (n : num) (m : num) : n ≤ n + m := by num.transfer
```
-/
meta def transfer : tactic unit := `[intros, transfer_rw, try {simp}]

instance : comm_semiring num :=
by refine_struct {
  add      := (+),
  zero     := 0,
  zero_add := zero_add,
  add_zero := add_zero,
  mul      := (*),
  one      := 1,
  nsmul    := @nsmul_rec _ ⟨0⟩ ⟨(+)⟩,
  npow     := @npow_rec _ ⟨1⟩ ⟨(*)⟩ };
try { intros, refl }; try { transfer }; simp [mul_add, mul_left_comm, mul_comm, add_comm]

instance : ordered_cancel_add_comm_monoid num :=
{ add_left_cancel            := by {intros a b c, transfer_rw, apply add_left_cancel},
  lt                         := (<),
  lt_iff_le_not_le           := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
  le                         := (≤),
  le_refl                    := by transfer,
  le_trans                   := by {intros a b c, transfer_rw, apply le_trans},
  le_antisymm                := by {intros a b, transfer_rw, apply le_antisymm},
  add_le_add_left            := by {intros a b h c, revert h, transfer_rw,
    exact λ h, add_le_add_left h c},
  le_of_add_le_add_left      := by {intros a b c, transfer_rw, apply le_of_add_le_add_left},
  ..num.comm_semiring }

instance : linear_ordered_semiring num :=
{ le_total                   := by {intros a b, transfer_rw, apply le_total},
  zero_le_one                := dec_trivial,
  mul_lt_mul_of_pos_left     := by {intros a b c, transfer_rw, apply mul_lt_mul_of_pos_left},
  mul_lt_mul_of_pos_right    := by {intros a b c, transfer_rw, apply mul_lt_mul_of_pos_right},
  decidable_lt               := num.decidable_lt,
  decidable_le               := num.decidable_le,
  decidable_eq               := num.decidable_eq,
  exists_pair_ne             := ⟨0, 1, dec_trivial⟩,
  ..num.comm_semiring, ..num.ordered_cancel_add_comm_monoid }

@[norm_cast]
theorem dvd_to_nat (m n : num) : (m : ℕ) ∣ n ↔ m ∣ n :=
⟨λ ⟨k, e⟩, ⟨k, by rw [← of_to_nat n, e]; simp⟩,
 λ ⟨k, e⟩, ⟨k, by simp [e, mul_to_nat]⟩⟩

end num

namespace pos_num
variables {α : Type*}
open num

@[norm_cast] theorem to_nat_inj {m n : pos_num} : (m : ℕ) = n ↔ m = n :=
⟨λ h, num.pos.inj $ by rw [← pos_num.of_to_nat, ← pos_num.of_to_nat, h],
 congr_arg _⟩

theorem pred'_to_nat : ∀ n, (pred' n : ℕ) = nat.pred n
| 1        := rfl
| (bit0 n) :=
  have nat.succ ↑(pred' n) = ↑n,
  by rw [pred'_to_nat n, nat.succ_pred_eq_of_pos (to_nat_pos n)],
  match pred' n, this : ∀ k : num, nat.succ ↑k = ↑n →
    ↑(num.cases_on k 1 bit1 : pos_num) = nat.pred (_root_.bit0 n) with
  | 0, (h : ((1:num):ℕ) = n) := by rw ← to_nat_inj.1 h; refl
  | num.pos p, (h : nat.succ ↑p = n) :=
    by rw ← h; exact (nat.succ_add p p).symm
  end
| (bit1 n) := rfl

@[simp] theorem pred'_succ' (n) : pred' (succ' n) = n :=
num.to_nat_inj.1 $ by rw [pred'_to_nat, succ'_to_nat,
  nat.add_one, nat.pred_succ]

@[simp] theorem succ'_pred' (n) : succ' (pred' n) = n :=
to_nat_inj.1 $ by rw [succ'_to_nat, pred'_to_nat,
  nat.add_one, nat.succ_pred_eq_of_pos (to_nat_pos _)]

instance : has_dvd pos_num := ⟨λ m n, pos m ∣ pos n⟩

@[norm_cast] theorem dvd_to_nat {m n : pos_num} : (m:ℕ) ∣ n ↔ m ∣ n :=
num.dvd_to_nat (pos m) (pos n)

theorem size_to_nat : ∀ n, (size n : ℕ) = nat.size n
| 1        := nat.size_one.symm
| (bit0 n) := by rw [size, succ_to_nat, size_to_nat, cast_bit0,
                     nat.size_bit0 $ ne_of_gt $ to_nat_pos n]
| (bit1 n) := by rw [size, succ_to_nat, size_to_nat, cast_bit1,
                     nat.size_bit1]

theorem size_eq_nat_size : ∀ n, (size n : ℕ) = nat_size n
| 1        := rfl
| (bit0 n) := by rw [size, succ_to_nat, nat_size, size_eq_nat_size]
| (bit1 n) := by rw [size, succ_to_nat, nat_size, size_eq_nat_size]

theorem nat_size_to_nat (n) : nat_size n = nat.size n :=
by rw [← size_eq_nat_size, size_to_nat]

theorem nat_size_pos (n) : 0 < nat_size n :=
by cases n; apply nat.succ_pos

/--
This tactic tries to turn an (in)equality about `pos_num`s to one about `nat`s by rewriting.
```lean
example (n : pos_num) (m : pos_num) : n ≤ n + m :=
begin
  pos_num.transfer_rw,
  exact nat.le_add_right _ _
end
```
-/
meta def transfer_rw : tactic unit :=
`[repeat {rw ← to_nat_inj <|> rw ← lt_to_nat <|> rw ← le_to_nat},
  repeat {rw add_to_nat <|> rw mul_to_nat <|> rw cast_one <|> rw cast_zero}]

/--
This tactic tries to prove (in)equalities about `pos_num`s by transferring them to the `nat` world
and then trying to call `simp`.
```lean
example (n : pos_num) (m : pos_num) : n ≤ n + m := by pos_num.transfer
```
-/
meta def transfer : tactic unit :=
`[intros, transfer_rw, try {simp [add_comm, add_left_comm, mul_comm, mul_left_comm]}]

instance : add_comm_semigroup pos_num :=
by refine {add := (+), ..}; transfer

instance : comm_monoid pos_num :=
by refine_struct {mul := (*), one := (1 : pos_num), npow := @npow_rec _ ⟨1⟩ ⟨(*)⟩};
try { intros, refl }; transfer

instance : distrib pos_num :=
by refine {add := (+), mul := (*), ..}; {transfer, simp [mul_add, mul_comm]}

instance : linear_order pos_num :=
{ lt              := (<),
  lt_iff_le_not_le := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
  le              := (≤),
  le_refl         := by transfer,
  le_trans        := by {intros a b c, transfer_rw, apply le_trans},
  le_antisymm     := by {intros a b, transfer_rw, apply le_antisymm},
  le_total        := by {intros a b, transfer_rw, apply le_total},
  decidable_lt    := by apply_instance,
  decidable_le    := by apply_instance,
  decidable_eq    := by apply_instance }

@[simp] theorem cast_to_num (n : pos_num) : ↑n = num.pos n :=
by rw [← cast_to_nat, ← of_to_nat n]

@[simp, norm_cast]
theorem bit_to_nat (b n) : (bit b n : ℕ) = nat.bit b n :=
by cases b; refl

@[simp, norm_cast]
theorem cast_add [add_monoid α] [has_one α] (m n) : ((m + n : pos_num) : α) = m + n :=
by rw [← cast_to_nat, add_to_nat, nat.cast_add, cast_to_nat, cast_to_nat]

@[simp, norm_cast, priority 500]
theorem cast_succ [add_monoid α] [has_one α] (n : pos_num) : (succ n : α) = n + 1 :=
by rw [← add_one, cast_add, cast_one]

@[simp, norm_cast]
theorem cast_inj [add_monoid α] [has_one α] [char_zero α] {m n : pos_num} : (m:α) = n ↔ m = n :=
by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_inj, to_nat_inj]

@[simp]
theorem one_le_cast [linear_ordered_semiring α] (n : pos_num) : (1 : α) ≤ n :=
by rw [← cast_to_nat, ← nat.cast_one, nat.cast_le]; apply to_nat_pos

@[simp]
theorem cast_pos [linear_ordered_semiring α] (n : pos_num) : 0 < (n : α) :=
lt_of_lt_of_le zero_lt_one (one_le_cast n)

@[simp, norm_cast]
theorem cast_mul [semiring α] (m n) : ((m * n : pos_num) : α) = m * n :=
by rw [← cast_to_nat, mul_to_nat, nat.cast_mul, cast_to_nat, cast_to_nat]

@[simp]
theorem cmp_eq (m n) : cmp m n = ordering.eq ↔ m = n :=
begin
  have := cmp_to_nat m n,
  cases cmp m n; simp at this ⊢; try {exact this};
  { simp [show m ≠ n, from λ e, by rw e at this; exact lt_irrefl _ this] }
end

@[simp, norm_cast]
theorem cast_lt [linear_ordered_semiring α] {m n : pos_num} : (m:α) < n ↔ m < n :=
by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_lt, lt_to_nat]

@[simp, norm_cast]
theorem cast_le [linear_ordered_semiring α] {m n : pos_num} : (m:α) ≤ n ↔ m ≤ n :=
by rw ← not_lt; exact not_congr cast_lt

end pos_num

namespace num
variables {α : Type*}
open pos_num

theorem bit_to_nat (b n) : (bit b n : ℕ) = nat.bit b n :=
by cases b; cases n; refl

theorem cast_succ' [add_monoid α] [has_one α] (n) : (succ' n : α) = n + 1 :=
by rw [← pos_num.cast_to_nat, succ'_to_nat, nat.cast_add_one, cast_to_nat]

theorem cast_succ [add_monoid α] [has_one α] (n) : (succ n : α) = n + 1 := cast_succ' n

@[simp, norm_cast] theorem cast_add [semiring α] (m n) : ((m + n : num) : α) = m + n :=
by rw [← cast_to_nat, add_to_nat, nat.cast_add, cast_to_nat, cast_to_nat]

@[simp, norm_cast] theorem cast_bit0 [semiring α] (n : num) : (n.bit0 : α) = _root_.bit0 n :=
by rw [← bit0_of_bit0, _root_.bit0, cast_add]; refl

@[simp, norm_cast] theorem cast_bit1 [semiring α] (n : num) : (n.bit1 : α) = _root_.bit1 n :=
by rw [← bit1_of_bit1, _root_.bit1, bit0_of_bit0, cast_add, cast_bit0]; refl

@[simp, norm_cast] theorem cast_mul [semiring α] : ∀ m n, ((m * n : num) : α) = m * n
| 0       0       := (zero_mul _).symm
| 0       (pos q) := (zero_mul _).symm
| (pos p) 0       := (mul_zero _).symm
| (pos p) (pos q) := pos_num.cast_mul _ _

theorem size_to_nat : ∀ n, (size n : ℕ) = nat.size n
| 0       := nat.size_zero.symm
| (pos p) := p.size_to_nat

theorem size_eq_nat_size : ∀ n, (size n : ℕ) = nat_size n
| 0       := rfl
| (pos p) := p.size_eq_nat_size

theorem nat_size_to_nat (n) : nat_size n = nat.size n :=
by rw [← size_eq_nat_size, size_to_nat]

@[simp] theorem of_nat'_zero : num.of_nat' 0 = 0 :=
by simp [num.of_nat']

@[simp, priority 999] theorem of_nat'_eq : ∀ n, num.of_nat' n = n :=
nat.binary_rec (by simp) $ λ b n IH, begin
  rw of_nat' at IH ⊢,
  rw [nat.binary_rec_eq, IH],
  { cases b; simp [nat.bit, bit0_of_bit0, bit1_of_bit1] },
  { refl }
end

theorem zneg_to_znum (n : num) : -n.to_znum = n.to_znum_neg := by cases n; refl
theorem zneg_to_znum_neg (n : num) : -n.to_znum_neg = n.to_znum := by cases n; refl

theorem to_znum_inj {m n : num} : m.to_znum = n.to_znum ↔ m = n :=
⟨λ h, by cases m; cases n; cases h; refl, congr_arg _⟩

@[simp, norm_cast squash] theorem cast_to_znum [has_zero α] [has_one α] [has_add α] [has_neg α] :
  ∀ n : num, (n.to_znum : α) = n
| 0           := rfl
| (num.pos p) := rfl

@[simp] theorem cast_to_znum_neg [add_group α] [has_one α] :
  ∀ n : num, (n.to_znum_neg : α) = -n
| 0           := neg_zero.symm
| (num.pos p) := rfl

@[simp] theorem add_to_znum (m n : num) : num.to_znum (m + n) = m.to_znum + n.to_znum :=
by cases m; cases n; refl

end num

namespace pos_num
open num

theorem pred_to_nat {n : pos_num} (h : 1 < n) : (pred n : ℕ) = nat.pred n :=
begin
  unfold pred,
  have := pred'_to_nat n,
  cases e : pred' n,
  { have : (1:ℕ) ≤ nat.pred n :=
      nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h),
    rw [← pred'_to_nat, e] at this,
    exact absurd this dec_trivial },
  { rw [← pred'_to_nat, e], refl }
end

theorem sub'_one (a : pos_num) : sub' a 1 = (pred' a).to_znum :=
by cases a; refl

theorem one_sub' (a : pos_num) : sub' 1 a = (pred' a).to_znum_neg :=
by cases a; refl

theorem lt_iff_cmp {m n} : m < n ↔ cmp m n = ordering.lt := iff.rfl

theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ ordering.gt :=
not_congr $ lt_iff_cmp.trans $
by rw ← cmp_swap; cases cmp m n; exact dec_trivial

end pos_num

namespace num
variables {α : Type*}
open pos_num

theorem pred_to_nat : ∀ (n : num), (pred n : ℕ) = nat.pred n
| 0       := rfl
| (pos p) := by rw [pred, pos_num.pred'_to_nat]; refl

theorem ppred_to_nat : ∀ (n : num), coe <$> ppred n = nat.ppred n
| 0       := rfl
| (pos p) := by rw [ppred, option.map_some, nat.ppred_eq_some.2];
  rw [pos_num.pred'_to_nat, nat.succ_pred_eq_of_pos (pos_num.to_nat_pos _)]; refl

theorem cmp_swap (m n) : (cmp m n).swap = cmp n m :=
by cases m; cases n; try {unfold cmp}; try {refl}; apply pos_num.cmp_swap

theorem cmp_eq (m n) : cmp m n = ordering.eq ↔ m = n :=
begin
  have := cmp_to_nat m n,
  cases cmp m n; simp at this ⊢; try {exact this};
  { simp [show m ≠ n, from λ e, by rw e at this; exact lt_irrefl _ this] }
end

@[simp, norm_cast]
theorem cast_lt [linear_ordered_semiring α] {m n : num} : (m:α) < n ↔ m < n :=
by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_lt, lt_to_nat]

@[simp, norm_cast]
theorem cast_le [linear_ordered_semiring α] {m n : num} : (m:α) ≤ n ↔ m ≤ n :=
by rw ← not_lt; exact not_congr cast_lt

@[simp, norm_cast]
theorem cast_inj [linear_ordered_semiring α] {m n : num} : (m:α) = n ↔ m = n :=
by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_inj, to_nat_inj]

theorem lt_iff_cmp {m n} : m < n ↔ cmp m n = ordering.lt := iff.rfl

theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ ordering.gt :=
not_congr $ lt_iff_cmp.trans $
by rw ← cmp_swap; cases cmp m n; exact dec_trivial

theorem bitwise_to_nat {f : num → num → num} {g : bool → bool → bool}
  (p : pos_num → pos_num → num)
  (gff : g ff ff = ff)
  (f00 : f 0 0 = 0)
  (f0n : ∀ n, f 0 (pos n) = cond (g ff tt) (pos n) 0)
  (fn0 : ∀ n, f (pos n) 0 = cond (g tt ff) (pos n) 0)
  (fnn : ∀ m n, f (pos m) (pos n) = p m n)
  (p11 : p 1 1 = cond (g tt tt) 1 0)
  (p1b : ∀ b n, p 1 (pos_num.bit b n) = bit (g tt b) (cond (g ff tt) (pos n) 0))
  (pb1 : ∀ a m, p (pos_num.bit a m) 1 = bit (g a tt) (cond (g tt ff) (pos m) 0))
  (pbb : ∀ a b m n, p (pos_num.bit a m) (pos_num.bit b n) = bit (g a b) (p m n))
  : ∀ m n : num, (f m n : ℕ) = nat.bitwise g m n :=
begin
  intros, cases m with m; cases n with n;
  try { change zero with 0 };
  try { change ((0:num):ℕ) with 0 },
  { rw [f00, nat.bitwise_zero]; refl },
  { unfold nat.bitwise, rw [f0n, nat.binary_rec_zero],
    cases g ff tt; refl },
  { unfold nat.bitwise,
    generalize h : (pos m : ℕ) = m', revert h,
    apply nat.bit_cases_on m' _, intros b m' h,
    rw [fn0, nat.binary_rec_eq, nat.binary_rec_zero, ←h],
    cases g tt ff; refl,
    apply nat.bitwise_bit_aux gff },
  { rw fnn,
    have : ∀b (n : pos_num), (cond b ↑n 0 : ℕ) = ↑(cond b (pos n) 0 : num) :=
      by intros; cases b; refl,
    induction m with m IH m IH generalizing n; cases n with n n,
    any_goals { change one with 1 },
    any_goals { change pos 1 with 1 },
    any_goals { change pos_num.bit0 with pos_num.bit ff },
    any_goals { change pos_num.bit1 with pos_num.bit tt },
    any_goals { change ((1:num):ℕ) with nat.bit tt 0 },
    all_goals {
      repeat {
        rw show ∀ b n, (pos (pos_num.bit b n) : ℕ) = nat.bit b ↑n,
           by intros; cases b; refl },
      rw nat.bitwise_bit },
    any_goals { assumption },
    any_goals { rw [nat.bitwise_zero, p11], cases g tt tt; refl },
    any_goals { rw [nat.bitwise_zero_left, this, ← bit_to_nat, p1b] },
    any_goals { rw [nat.bitwise_zero_right _ gff, this, ← bit_to_nat, pb1] },
    all_goals { rw [← show ∀ n, ↑(p m n) = nat.bitwise g ↑m ↑n, from IH],
      rw [← bit_to_nat, pbb] } }
end

@[simp, norm_cast] theorem lor_to_nat   : ∀ m n, (lor    m n : ℕ) = nat.lor    m n :=
by apply bitwise_to_nat (λx y, pos (pos_num.lor x y)); intros; try {cases a}; try {cases b}; refl
@[simp, norm_cast] theorem land_to_nat  : ∀ m n, (land   m n : ℕ) = nat.land   m n :=
by apply bitwise_to_nat pos_num.land; intros; try {cases a}; try {cases b}; refl
@[simp, norm_cast] theorem ldiff_to_nat : ∀ m n, (ldiff  m n : ℕ) = nat.ldiff  m n :=
by apply bitwise_to_nat pos_num.ldiff; intros; try {cases a}; try {cases b}; refl
@[simp, norm_cast] theorem lxor_to_nat  : ∀ m n, (lxor   m n : ℕ) = nat.lxor   m n :=
by apply bitwise_to_nat pos_num.lxor; intros; try {cases a}; try {cases b}; refl

@[simp, norm_cast] theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = nat.shiftl m n :=
begin
  cases m; dunfold shiftl, {symmetry, apply nat.zero_shiftl},
  simp, induction n with n IH, {refl},
  simp [pos_num.shiftl, nat.shiftl_succ], rw ←IH
end

@[simp, norm_cast] theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = nat.shiftr m n :=
begin
  cases m with m; dunfold shiftr, {symmetry, apply nat.zero_shiftr},
  induction n with n IH generalizing m, {cases m; refl},
  cases m with m m; dunfold pos_num.shiftr,
  { rw [nat.shiftr_eq_div_pow], symmetry, apply nat.div_eq_of_lt,
    exact @nat.pow_lt_pow_of_lt_right 2 dec_trivial 0 (n+1) (nat.succ_pos _) },
  { transitivity, apply IH,
    change nat.shiftr m n = nat.shiftr (bit1 m) (n+1),
    rw [add_comm n 1, nat.shiftr_add],
    apply congr_arg (λx, nat.shiftr x n), unfold nat.shiftr,
    change (bit1 ↑m : ℕ) with nat.bit tt m,
    rw nat.div2_bit },
  { transitivity, apply IH,
    change nat.shiftr m n = nat.shiftr (bit0 m) (n + 1),
    rw [add_comm n 1, nat.shiftr_add],
    apply congr_arg (λx, nat.shiftr x n), unfold nat.shiftr,
    change (bit0 ↑m : ℕ) with nat.bit ff m,
    rw nat.div2_bit }
end

@[simp] theorem test_bit_to_nat (m n) : test_bit m n = nat.test_bit m n :=
begin
  cases m with m; unfold test_bit nat.test_bit,
  { change (zero : nat) with 0, rw nat.zero_shiftr, refl },
  induction n with n IH generalizing m;
  cases m; dunfold pos_num.test_bit, {refl},
  { exact (nat.bodd_bit _ _).symm },
  { exact (nat.bodd_bit _ _).symm },
  { change ff = nat.bodd (nat.shiftr 1 (n + 1)),
    rw [add_comm, nat.shiftr_add], change nat.shiftr 1 1 with 0,
    rw nat.zero_shiftr; refl },
  { change pos_num.test_bit m n = nat.bodd (nat.shiftr (nat.bit tt m) (n + 1)),
    rw [add_comm, nat.shiftr_add], unfold nat.shiftr,
    rw nat.div2_bit, apply IH },
  { change pos_num.test_bit m n = nat.bodd (nat.shiftr (nat.bit ff m) (n + 1)),
    rw [add_comm, nat.shiftr_add], unfold nat.shiftr,
    rw nat.div2_bit, apply IH },
end

end num

namespace znum
variables {α : Type*}
open pos_num

@[simp, norm_cast] theorem cast_zero [has_zero α] [has_one α] [has_add α] [has_neg α] :
  ((0 : znum) : α) = 0 := rfl

@[simp] theorem cast_zero' [has_zero α] [has_one α] [has_add α] [has_neg α] :
  (znum.zero : α) = 0 := rfl

@[simp, norm_cast] theorem cast_one [has_zero α] [has_one α] [has_add α] [has_neg α] :
  ((1 : znum) : α) = 1 := rfl

@[simp] theorem cast_pos [has_zero α] [has_one α] [has_add α] [has_neg α]
  (n : pos_num) : (pos n : α) = n := rfl

@[simp] theorem cast_neg [has_zero α] [has_one α] [has_add α] [has_neg α]
  (n : pos_num) : (neg n : α) = -n := rfl

@[simp, norm_cast] theorem cast_zneg [add_group α] [has_one α] : ∀ n, ((-n : znum) : α) = -n
| 0       := neg_zero.symm
| (pos p) := rfl
| (neg p) := (neg_neg _).symm

theorem neg_zero : (-0 : znum) = 0 := rfl
theorem zneg_pos (n : pos_num) : -pos n = neg n := rfl
theorem zneg_neg (n : pos_num) : -neg n = pos n := rfl
theorem zneg_zneg (n : znum) : - -n = n := by cases n; refl
theorem zneg_bit1 (n : znum) : -n.bit1 = (-n).bitm1 := by cases n; refl
theorem zneg_bitm1 (n : znum) : -n.bitm1 = (-n).bit1 := by cases n; refl

theorem zneg_succ (n : znum) : -n.succ = (-n).pred :=
by cases n; try {refl}; rw [succ, num.zneg_to_znum_neg]; refl

theorem zneg_pred (n : znum) : -n.pred = (-n).succ :=
by rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]

@[simp, norm_cast]

@[simp] theorem abs_to_nat : ∀ n, (abs n : ℕ) = int.nat_abs n
| 0       := rfl
| (pos p) := congr_arg int.nat_abs p.to_nat_to_int
| (neg p) := show int.nat_abs ((p:ℕ):ℤ) = int.nat_abs (- p),
  by rw [p.to_nat_to_int, int.nat_abs_neg]

@[simp] theorem abs_to_znum : ∀ n : num, abs n.to_znum = n
| 0           := rfl
| (num.pos p) := rfl

@[simp, norm_cast] theorem cast_to_int [add_group α] [has_one α] : ∀ n : znum, ((n : ℤ) : α) = n
| 0       := rfl
| (pos p) := by rw [cast_pos, cast_pos, pos_num.cast_to_int]
| (neg p) := by rw [cast_neg, cast_neg, int.cast_neg, pos_num.cast_to_int]

theorem bit0_of_bit0 : ∀ n : znum, _root_.bit0 n = n.bit0
| 0       := rfl
| (pos a) := congr_arg pos a.bit0_of_bit0
| (neg a) := congr_arg neg a.bit0_of_bit0

theorem bit1_of_bit1 : ∀ n : znum, _root_.bit1 n = n.bit1
| 0       := rfl
| (pos a) := congr_arg pos a.bit1_of_bit1
| (neg a) := show pos_num.sub' 1 (_root_.bit0 a) = _,
  by rw [pos_num.one_sub', a.bit0_of_bit0]; refl

@[simp, norm_cast] theorem cast_bit0 [add_group α] [has_one α] :
  ∀ n : znum, (n.bit0 : α) = bit0 n
| 0       := (add_zero _).symm
| (pos p) := by rw [znum.bit0, cast_pos, cast_pos]; refl
| (neg p) := by rw [znum.bit0, cast_neg, cast_neg, pos_num.cast_bit0,
                    _root_.bit0, _root_.bit0, neg_add_rev]

@[simp, norm_cast] theorem cast_bit1 [add_group α] [has_one α] :
  ∀ n : znum, (n.bit1 : α) = bit1 n
| 0       := by simp [znum.bit1, _root_.bit1, _root_.bit0]
| (pos p) := by rw [znum.bit1, cast_pos, cast_pos]; refl
| (neg p) := begin
    rw [znum.bit1, cast_neg, cast_neg],
    cases e : pred' p with a;
    have : p = _ := (succ'_pred' p).symm.trans
      (congr_arg num.succ' e),
    { change p=1 at this, subst p,
      simp [_root_.bit1, _root_.bit0] },
    { rw [num.succ'] at this, subst p,
      have : (↑(-↑a:ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ), {simp [add_comm]},
      simpa [_root_.bit1, _root_.bit0, -add_comm] },
  end

@[simp] theorem cast_bitm1 [add_group α] [has_one α]
  (n : znum) : (n.bitm1 : α) = bit0 n - 1 :=
begin
  conv { to_lhs, rw ← zneg_zneg n },
  rw [← zneg_bit1, cast_zneg, cast_bit1],
  have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ), {simp [add_comm, add_left_comm]},
  simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg, -int.add_neg_one]
end

theorem add_zero (n : znum) : n + 0 = n := by cases n; refl
theorem zero_add (n : znum) : 0 + n = n := by cases n; refl

theorem add_one : ∀ n : znum, n + 1 = succ n
| 0       := rfl
| (pos p) := congr_arg pos p.add_one
| (neg p) := by cases p; refl

end znum

namespace pos_num
variables {α : Type*}

theorem cast_to_znum : ∀ n : pos_num, (n : znum) = znum.pos n
| 1        := rfl
| (bit0 p) := (znum.bit0_of_bit0 p).trans $ congr_arg _ (cast_to_znum p)
| (bit1 p) := (znum.bit1_of_bit1 p).trans $ congr_arg _ (cast_to_znum p)

local attribute [-simp] int.add_neg_one

theorem cast_sub' [add_group α] [has_one α] : ∀ m n : pos_num, (sub' m n : α) = m - n
| a        1        := by rw [sub'_one, num.cast_to_znum,
                              ← num.cast_to_nat, pred'_to_nat, ← nat.sub_one];
                          simp [pos_num.cast_pos]
| 1        b        := by rw [one_sub', num.cast_to_znum_neg, ← neg_sub, neg_inj,
                              ← num.cast_to_nat, pred'_to_nat, ← nat.sub_one];
                          simp [pos_num.cast_pos]
| (bit0 a) (bit0 b) := begin
    rw [sub', znum.cast_bit0, cast_sub'],
    have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b), {simp [add_left_comm]},
    simpa [_root_.bit0, sub_eq_add_neg]
  end
| (bit0 a) (bit1 b) := begin
    rw [sub', znum.cast_bitm1, cast_sub'],
    have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b):ℤ),
    { simp [add_comm, add_left_comm] },
    simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg]
  end
| (bit1 a) (bit0 b) := begin
    rw [sub', znum.cast_bit1, cast_sub'],
    have : ((-b + (a + (-b + 1)) : ℤ) : α) = (a + 1 + (-b + -b):ℤ),
    { simp [add_comm, add_left_comm] },
    simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg]
  end
| (bit1 a) (bit1 b) := begin
    rw [sub', znum.cast_bit0, cast_sub'],
    have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b), {simp [add_left_comm]},
    simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg]
  end

theorem to_nat_eq_succ_pred (n : pos_num) : (n:ℕ) = n.pred' + 1 :=
by rw [← num.succ'_to_nat, n.succ'_pred']

theorem to_int_eq_succ_pred (n : pos_num) : (n:ℤ) = (n.pred' : ℕ) + 1 :=
by rw [← n.to_nat_to_int, to_nat_eq_succ_pred]; refl

end pos_num

namespace num
variables {α : Type*}

@[simp] theorem cast_sub' [add_group α] [has_one α] : ∀ m n : num, (sub' m n : α) = m - n
| 0       0       := (sub_zero _).symm
| (pos a) 0       := (sub_zero _).symm
| 0       (pos b) := (zero_sub _).symm
| (pos a) (pos b) := pos_num.cast_sub' _ _

@[simp] theorem of_nat_to_znum : ∀ n : ℕ, to_znum n = n
| 0     := rfl
| (n+1) := by rw [nat.cast_add_one, nat.cast_add_one,
  znum.add_one, add_one, ← of_nat_to_znum]; cases (n:num); refl

@[simp] theorem of_nat_to_znum_neg (n : ℕ) : to_znum_neg n = -n :=
by rw [← of_nat_to_znum, zneg_to_znum]

theorem mem_of_znum' : ∀ {m : num} {n : znum}, m ∈ of_znum' n ↔ n = to_znum m
| 0       0      := ⟨λ _, rfl, λ _, rfl⟩
| (pos m) 0      := ⟨λ h, by cases h, λ h, by cases h⟩
| m (znum.pos p) := option.some_inj.trans $
  by cases m; split; intro h; try {cases h}; refl
| m (znum.neg p) := ⟨λ h, by cases h, λ h, by cases m; cases h⟩

theorem of_znum'_to_nat : ∀ (n : znum), coe <$> of_znum' n = int.to_nat' n
| 0            := rfl
| (znum.pos p) := show _ = int.to_nat' p, by rw [← pos_num.to_nat_to_int p]; refl
| (znum.neg p) := congr_arg (λ x, int.to_nat' (-x)) $
  show ((p.pred' + 1 : ℕ) : ℤ) = p, by rw ← succ'_to_nat; simp

@[simp] theorem of_znum_to_nat : ∀ (n : znum), (of_znum n : ℕ) = int.to_nat n
| 0            := rfl
| (znum.pos p) := show _ = int.to_nat p, by rw [← pos_num.to_nat_to_int p]; refl
| (znum.neg p) := congr_arg (λ x, int.to_nat (-x)) $
  show ((p.pred' + 1 : ℕ) : ℤ) = p, by rw ← succ'_to_nat; simp

@[simp] theorem cast_of_znum [add_group α] [has_one α] (n : znum) :
  (of_znum n : α) = int.to_nat n :=
by rw [← cast_to_nat, of_znum_to_nat]

@[simp, norm_cast] theorem sub_to_nat (m n) : ((m - n : num) : ℕ) = m - n :=
show (of_znum _ : ℕ) = _, by rw [of_znum_to_nat, cast_sub',
  ← to_nat_to_int, ← to_nat_to_int, int.to_nat_sub]

end num

namespace znum
variables {α : Type*}

@[simp, norm_cast] theorem cast_add [add_group α] [has_one α] : ∀ m n, ((m + n : znum) : α) = m + n
| 0       a       := by cases a; exact (_root_.zero_add _).symm
| b       0       := by cases b; exact (_root_.add_zero _).symm
| (pos a) (pos b) := pos_num.cast_add _ _
| (pos a) (neg b) := by simpa only [sub_eq_add_neg] using pos_num.cast_sub' _ _
| (neg a) (pos b) :=
have (↑b + -↑a : α) = -↑a + ↑b, by rw [← pos_num.cast_to_int a, ← pos_num.cast_to_int b,
  ← int.cast_neg, ← int.cast_add (-a)]; simp [add_comm],
(pos_num.cast_sub' _ _).trans $ (sub_eq_add_neg _ _).trans this
| (neg a) (neg b) := show -(↑(a + b) : α) = -a + -b, by rw [
  pos_num.cast_add, neg_eq_iff_neg_eq, neg_add_rev, neg_neg, neg_neg,
  ← pos_num.cast_to_int a, ← pos_num.cast_to_int b, ← int.cast_add]; simp [add_comm]

@[simp] theorem cast_succ [add_group α] [has_one α] (n) : ((succ n : znum) : α) = n + 1 :=
by rw [← add_one, cast_add, cast_one]

@[simp, norm_cast] theorem mul_to_int : ∀ m n, ((m * n : znum) : ℤ) = m * n
| 0       a       := by cases a; exact (_root_.zero_mul _).symm
| b       0       := by cases b; exact (_root_.mul_zero _).symm
| (pos a) (pos b) := pos_num.cast_mul a b
| (pos a) (neg b) := show -↑(a * b) = ↑a * -↑b, by rw [pos_num.cast_mul, neg_mul_eq_mul_neg]
| (neg a) (pos b) := show -↑(a * b) = -↑a * ↑b, by rw [pos_num.cast_mul, neg_mul_eq_neg_mul]
| (neg a) (neg b) := show ↑(a * b) = -↑a * -↑b, by rw [pos_num.cast_mul, neg_mul_neg]

theorem cast_mul [ring α] (m n) : ((m * n : znum) : α) = m * n :=
by rw [← cast_to_int, mul_to_int, int.cast_mul, cast_to_int, cast_to_int]

@[simp, norm_cast] theorem of_to_int : Π (n : znum), ((n : ℤ) : znum) = n
| 0       := rfl
| (pos a) := by rw [cast_pos, ← pos_num.cast_to_nat,
  int.cast_coe_nat', ← num.of_nat_to_znum, pos_num.of_to_nat]; refl
| (neg a) := by rw [cast_neg, neg_of_int, ← pos_num.cast_to_nat,
  int.cast_coe_nat', ← num.of_nat_to_znum_neg, pos_num.of_to_nat]; refl

@[norm_cast]
theorem to_of_int : Π (n : ℤ), ((n : znum) : ℤ) = n
| (n : ℕ) := by rw [int.cast_coe_nat,
  ← num.of_nat_to_znum, num.cast_to_znum, ← num.cast_to_nat,
  int.nat_cast_eq_coe_nat, num.to_of_nat]
| -[1+ n] := by rw [int.cast_neg_succ_of_nat, cast_zneg,
  add_one, cast_succ, int.neg_succ_of_nat_eq,
  ← num.of_nat_to_znum, num.cast_to_znum, ← num.cast_to_nat,
  int.nat_cast_eq_coe_nat, num.to_of_nat]

theorem to_int_inj {m n : znum} : (m : ℤ) = n ↔ m = n :=
⟨λ h, function.left_inverse.injective of_to_int h, congr_arg _⟩

@[simp, norm_cast] theorem of_int_cast [add_group α] [has_one α] (n : ℤ) : ((n : znum) : α) = n :=
by rw [← cast_to_int, to_of_int]

@[simp, norm_cast] theorem of_nat_cast [add_group α] [has_one α] (n : ℕ) : ((n : znum) : α) = n :=
of_int_cast n

@[simp] theorem of_int'_eq : ∀ n, znum.of_int' n = n
| (n : ℕ) := to_int_inj.1 $ by simp [znum.of_int']
| -[1+ n] := to_int_inj.1 $ by simp [znum.of_int']

theorem cmp_to_int : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℤ) < n) (m = n) ((n:ℤ) < m) : Prop)
| 0       0       := rfl
| (pos a) (pos b) := begin
    have := pos_num.cmp_to_nat a b; revert this; dsimp [cmp];
    cases pos_num.cmp a b; dsimp;
    [simp, exact congr_arg pos, simp [gt]]
  end
| (neg a) (neg b) := begin
    have := pos_num.cmp_to_nat b a; revert this; dsimp [cmp];
    cases pos_num.cmp b a; dsimp;
    [simp, simp {contextual := tt}, simp [gt]]
  end
| (pos a) 0       := pos_num.cast_pos _
| (pos a) (neg b) := lt_trans (neg_lt_zero.2 $ pos_num.cast_pos _) (pos_num.cast_pos _)
| 0       (neg b) := neg_lt_zero.2 $ pos_num.cast_pos _
| (neg a) 0       := neg_lt_zero.2 $ pos_num.cast_pos _
| (neg a) (pos b) := lt_trans (neg_lt_zero.2 $ pos_num.cast_pos _) (pos_num.cast_pos _)
| 0       (pos b) := pos_num.cast_pos _

@[norm_cast]
theorem lt_to_int {m n : znum} : (m:ℤ) < n ↔ m < n :=
show (m:ℤ) < n ↔ cmp m n = ordering.lt, from
match cmp m n, cmp_to_int m n with
| ordering.lt, h := by simp at h; simp [h]
| ordering.eq, h := by simp at h; simp [h, lt_irrefl]; exact dec_trivial
| ordering.gt, h := by simp [not_lt_of_gt h]; exact dec_trivial
end

theorem le_to_int {m n : znum} : (m:ℤ) ≤ n ↔ m ≤ n :=
by rw ← not_lt; exact not_congr lt_to_int

@[simp, norm_cast]
theorem cast_lt [linear_ordered_ring α] {m n : znum} : (m:α) < n ↔ m < n :=
by rw [← cast_to_int m, ← cast_to_int n, int.cast_lt, lt_to_int]

@[simp, norm_cast]
theorem cast_le [linear_ordered_ring α] {m n : znum} : (m:α) ≤ n ↔ m ≤ n :=
by rw ← not_lt; exact not_congr cast_lt

@[simp, norm_cast]
theorem cast_inj [linear_ordered_ring α] {m n : znum} : (m:α) = n ↔ m = n :=
by rw [← cast_to_int m, ← cast_to_int n, int.cast_inj, to_int_inj]

/--
This tactic tries to turn an (in)equality about `znum`s to one about `int`s by rewriting.
```lean
example (n : znum) (m : znum) : n ≤ n + m * m :=
begin
  znum.transfer_rw,
  exact le_add_of_nonneg_right (mul_self_nonneg _)
end
```
-/
meta def transfer_rw : tactic unit :=
`[repeat {rw ← to_int_inj <|> rw ← lt_to_int <|> rw ← le_to_int},
  repeat {rw cast_add <|> rw mul_to_int <|> rw cast_one <|> rw cast_zero}]

/--
This tactic tries to prove (in)equalities about `znum`s by transfering them to the `int` world and
then trying to call `simp`.
```lean
example (n : znum) (m : znum) : n ≤ n + m * m :=
begin
  znum.transfer,
  exact mul_self_nonneg _
end
```
-/
meta def transfer : tactic unit :=
`[intros, transfer_rw, try {simp [add_comm, add_left_comm, mul_comm, mul_left_comm]}]

instance : linear_order znum :=
{ lt               := (<),
  lt_iff_le_not_le := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
  le               := (≤),
  le_refl          := by transfer,
  le_trans         := by {intros a b c, transfer_rw, apply le_trans},
  le_antisymm      := by {intros a b, transfer_rw, apply le_antisymm},
  le_total         := by {intros a b, transfer_rw, apply le_total},
  decidable_eq     := znum.decidable_eq,
  decidable_le     := znum.decidable_le,
  decidable_lt     := znum.decidable_lt }

instance : add_comm_group znum :=
{ add              := (+),
  add_assoc        := by transfer,
  zero             := 0,
  zero_add         := zero_add,
  add_zero         := add_zero,
  add_comm         := by transfer,
  neg              := has_neg.neg,
  add_left_neg     := by transfer }

instance : linear_ordered_comm_ring znum :=
{ mul              := (*),
  mul_assoc        := by transfer,
  one              := 1,
  one_mul          := by transfer,
  mul_one          := by transfer,
  left_distrib     := by {transfer, simp [mul_add]},
  right_distrib    := by {transfer, simp [mul_add, mul_comm]},
  mul_comm         := by transfer,
  exists_pair_ne   := ⟨0, 1, dec_trivial⟩,
  add_le_add_left  := by {intros a b h c, revert h, transfer_rw, exact λ h, add_le_add_left h c},
  mul_pos          := λ a b, show 0 < a → 0 < b → 0 < a * b, by {transfer_rw, apply mul_pos},
  zero_le_one      := dec_trivial,
  ..znum.linear_order, ..znum.add_comm_group }

@[simp, norm_cast] theorem dvd_to_int (m n : znum) : (m : ℤ) ∣ n ↔ m ∣ n :=
⟨λ ⟨k, e⟩, ⟨k, by rw [← of_to_int n, e]; simp⟩,
 λ ⟨k, e⟩, ⟨k, by simp [e]⟩⟩

end znum

namespace pos_num

theorem divmod_to_nat_aux {n d : pos_num} {q r : num}
  (h₁ : (r:ℕ) + d * _root_.bit0 q = n)
  (h₂ : (r:ℕ) < 2 * d) :
  ((divmod_aux d q r).2 + d * (divmod_aux d q r).1 : ℕ) = ↑n ∧
  ((divmod_aux d q r).2 : ℕ) < d :=
begin
  unfold divmod_aux,
  have : ∀ {r₂}, num.of_znum' (num.sub' r (num.pos d)) = some r₂ ↔ (r : ℕ) = r₂ + d,
  { intro r₂,
    apply num.mem_of_znum'.trans,
    rw [← znum.to_int_inj, num.cast_to_znum,
      num.cast_sub', sub_eq_iff_eq_add, ← int.coe_nat_inj'],
    simp },
  cases e : num.of_znum' (num.sub' r (num.pos d)) with r₂;
    simp [divmod_aux],
  { refine ⟨h₁, lt_of_not_ge (λ h, _)⟩,
    cases nat.le.dest h with r₂ e',
    rw [← num.to_of_nat r₂, add_comm] at e',
    cases e.symm.trans (this.2 e'.symm) },
  { have := this.1 e,
    split,
    { rwa [_root_.bit1, add_comm _ 1, mul_add, mul_one,
        ← add_assoc, ← this] },
    { rwa [this, two_mul, add_lt_add_iff_right] at h₂ } }
end

theorem divmod_to_nat (d n : pos_num) :
  (n / d : ℕ) = (divmod d n).1 ∧
  (n % d : ℕ) = (divmod d n).2 :=
begin
  rw nat.div_mod_unique (pos_num.cast_pos _),
  induction n with n IH n IH,
  { exact divmod_to_nat_aux (by simp; refl)
      (nat.mul_le_mul_left 2
        (pos_num.cast_pos d : (0 : ℕ) < d)) },
  { unfold divmod,
    cases divmod d n with q r, simp only [divmod] at IH ⊢,
    apply divmod_to_nat_aux; simp,
    { rw [_root_.bit1, _root_.bit1, add_right_comm,
        bit0_eq_two_mul ↑n, ← IH.1,
        mul_add, ← bit0_eq_two_mul,
        mul_left_comm, ← bit0_eq_two_mul] },
    { rw ← bit0_eq_two_mul,
      exact nat.bit1_lt_bit0 IH.2 } },
  { unfold divmod,
    cases divmod d n with q r, simp only [divmod] at IH ⊢,
    apply divmod_to_nat_aux; simp,
    { rw [bit0_eq_two_mul ↑n, ← IH.1,
        mul_add, ← bit0_eq_two_mul,
        mul_left_comm, ← bit0_eq_two_mul] },
    { rw ← bit0_eq_two_mul,
      exact nat.bit0_lt IH.2 } }
end

@[simp] theorem div'_to_nat (n d) : (div' n d : ℕ) = n / d :=
(divmod_to_nat _ _).1.symm

@[simp] theorem mod'_to_nat (n d) : (mod' n d : ℕ) = n % d :=
(divmod_to_nat _ _).2.symm

end pos_num

namespace num

@[simp] protected lemma div_zero (n : num) : n / 0 = 0 :=
show n.div 0 = 0, by { cases n, refl, simp [num.div] }

@[simp, norm_cast] theorem div_to_nat : ∀ n d, ((n / d : num) : ℕ) = n / d
| 0       0       := by simp
| 0       (pos d) := (nat.zero_div _).symm
| (pos n) 0       := (nat.div_zero _).symm
| (pos n) (pos d) := pos_num.div'_to_nat _ _

@[simp] protected lemma mod_zero (n : num) : n % 0 = n :=
show n.mod 0 = n, by { cases n, refl, simp [num.mod] }

@[simp, norm_cast] theorem mod_to_nat : ∀ n d, ((n % d : num) : ℕ) = n % d
| 0       0       := by simp
| 0       (pos d) := (nat.zero_mod _).symm
| (pos n) 0       := (nat.mod_zero _).symm
| (pos n) (pos d) := pos_num.mod'_to_nat _ _

theorem gcd_to_nat_aux : ∀ {n} {a b : num},
  a ≤ b → (a * b).nat_size ≤ n → (gcd_aux n a b : ℕ) = nat.gcd a b
| 0            0       b       ab h := (nat.gcd_zero_left _).symm
| 0            (pos a) 0       ab h := (not_lt_of_ge ab).elim rfl
| 0            (pos a) (pos b) ab h :=
  (not_lt_of_le h).elim $ pos_num.nat_size_pos _
| (nat.succ n) 0       b       ab h := (nat.gcd_zero_left _).symm
| (nat.succ n) (pos a) b       ab h := begin
  simp [gcd_aux],
  rw [nat.gcd_rec, gcd_to_nat_aux, mod_to_nat], {refl},
  { rw [← le_to_nat, mod_to_nat],
    exact le_of_lt (nat.mod_lt _ (pos_num.cast_pos _)) },
  rw [nat_size_to_nat, mul_to_nat, nat.size_le] at h ⊢,
  rw [mod_to_nat, mul_comm],
  rw [pow_succ', ← nat.mod_add_div b (pos a)] at h,
  refine lt_of_mul_lt_mul_right (lt_of_le_of_lt _ h) (nat.zero_le 2),
  rw [mul_two, mul_add],
  refine add_le_add_left (nat.mul_le_mul_left _
    (le_trans (le_of_lt (nat.mod_lt _ (pos_num.cast_pos _))) _)) _,
  suffices : 1 ≤ _, simpa using nat.mul_le_mul_left (pos a) this,
  rw [nat.le_div_iff_mul_le _ _ a.cast_pos, one_mul],
  exact le_to_nat.2 ab
end

@[simp] theorem gcd_to_nat : ∀ a b, (gcd a b : ℕ) = nat.gcd a b :=
have ∀ a b : num, (a * b).nat_size ≤ a.nat_size + b.nat_size,
begin
  intros,
  simp [nat_size_to_nat],
  rw [nat.size_le, pow_add],
  exact mul_lt_mul'' (nat.lt_size_self _)
    (nat.lt_size_self _) (nat.zero_le _) (nat.zero_le _)
end,
begin
  intros, unfold gcd, split_ifs,
  { exact gcd_to_nat_aux h (this _ _) },
  { rw nat.gcd_comm,
    exact gcd_to_nat_aux (le_of_not_le h) (this _ _) }
end

theorem dvd_iff_mod_eq_zero {m n : num} : m ∣ n ↔ n % m = 0 :=
by rw [← dvd_to_nat, nat.dvd_iff_mod_eq_zero,
  ← to_nat_inj, mod_to_nat]; refl

instance decidable_dvd : decidable_rel ((∣) : num → num → Prop)
| a b := decidable_of_iff' _ dvd_iff_mod_eq_zero

end num

instance pos_num.decidable_dvd : decidable_rel ((∣) : pos_num → pos_num → Prop)
| a b := num.decidable_dvd _ _

namespace znum

@[simp] protected lemma div_zero (n : znum) : n / 0 = 0 :=
show n.div 0 = 0, by cases n; refl <|> simp [znum.div]

@[simp, norm_cast] theorem div_to_int : ∀ n d, ((n / d : znum) : ℤ) = n / d
| 0       0       := by simp [int.div_zero]
| 0       (pos d) := (int.zero_div _).symm
| 0       (neg d) := (int.zero_div _).symm
| (pos n) 0       := (int.div_zero _).symm
| (neg n) 0       := (int.div_zero _).symm
| (pos n) (pos d) := (num.cast_to_znum _).trans $
  by rw ← num.to_nat_to_int; simp
| (pos n) (neg d) := (num.cast_to_znum_neg _).trans $
  by rw ← num.to_nat_to_int; simp
| (neg n) (pos d) := show - _ = (-_/↑d), begin
    rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred,
      ← pos_num.to_nat_to_int, num.succ'_to_nat,
      num.div_to_nat],
    change -[1+ n.pred' / ↑d] = -[1+ n.pred' / (d.pred' + 1)],
    rw d.to_nat_eq_succ_pred
  end
| (neg n) (neg d) := show ↑(pos_num.pred' n / num.pos d).succ' = (-_ / -↑d), begin
    rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred,
      ← pos_num.to_nat_to_int, num.succ'_to_nat,
      num.div_to_nat],
    change (nat.succ (_/d) : ℤ) = nat.succ (n.pred'/(d.pred' + 1)),
    rw d.to_nat_eq_succ_pred
  end

@[simp, norm_cast] theorem mod_to_int : ∀ n d, ((n % d : znum) : ℤ) = n % d
| 0       d := (int.zero_mod _).symm
| (pos n) d := (num.cast_to_znum _).trans $
  by rw [← num.to_nat_to_int, cast_pos, num.mod_to_nat,
    ← pos_num.to_nat_to_int, abs_to_nat]; refl
| (neg n) d := (num.cast_sub' _ _).trans $
  by rw [← num.to_nat_to_int, cast_neg, ← num.to_nat_to_int,
    num.succ_to_nat, num.mod_to_nat, abs_to_nat,
    ← int.sub_nat_nat_eq_coe, n.to_int_eq_succ_pred]; refl

@[simp] theorem gcd_to_nat (a b) : (gcd a b : ℕ) = int.gcd a b :=
(num.gcd_to_nat _ _).trans $ by simpa

theorem dvd_iff_mod_eq_zero {m n : znum} : m ∣ n ↔ n % m = 0 :=
by rw [← dvd_to_int, int.dvd_iff_mod_eq_zero,
  ← to_int_inj, mod_to_int]; refl

instance : decidable_rel ((∣) : znum → znum → Prop)
| a b := decidable_of_iff' _ dvd_iff_mod_eq_zero

end znum

namespace int

/-- Cast a `snum` to the corresponding integer. -/
def of_snum : snum → ℤ :=
snum.rec' (λ a, cond a (-1) 0) (λa p IH, cond a (bit1 IH) (bit0 IH))

instance snum_coe : has_coe snum ℤ := ⟨of_snum⟩
end int

instance : has_lt snum := ⟨λa b, (a : ℤ) < b⟩
instance : has_le snum := ⟨λa b, (a : ℤ) ≤ b⟩

author: JLimperg


text:
import Mathlib.Tactic.Relation.Trans
import Std.Data.Nat.Lemmas

-- testing that the attribute is recognized and used
def nleq (a b : Nat) : Prop := a ≤ b

@[trans] def nleq_trans : nleq a b → nleq b c → nleq a c := Nat.le_trans

example (a b c : Nat) : nleq a b → nleq b c → nleq a c := by
  intro h₁ h₂
  trans b
  assumption
  assumption

example (a b c : Nat) : nleq a b → nleq b c → nleq a c := by intros; trans <;> assumption

-- using `Trans` typeclass
@[trans] def eq_trans {a b c : α} : a = b → b = c → a = c := by
  intro h₁ h₂
  apply Eq.trans h₁ h₂

example (a b c : Nat) : a = b → b = c → a = c := by intros; trans <;> assumption

example (a b c : Nat) : a = b → b = c → a = c := by
  intro h₁ h₂
  trans b
  assumption
  assumption

example : @Trans Nat Nat Nat (. ≤ .) (. ≤ .) (. ≤ .) := inferInstance

example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
  intros h₁ h₂
  trans ?b
  case b => exact b
  exact h₁
  exact h₂

example (a b c : α) (R : α → α → Prop) [Trans R R R] : R a b → R b c → R a c := by
  intros h₁ h₂
  trans ?b
  case b => exact b
  exact h₁
  exact h₂

example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
  intros h₁ h₂
  trans
  exact h₁
  exact h₂

example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by intros; trans <;> assumption

example (a b c : Nat) : a < b → b < c → a < c := by
  intro h₁ h₂
  trans b
  assumption
  assumption

example (a b c : Nat) : a < b → b < c → a < c := by intros; trans <;> assumption

example (x n p : Nat) (h₁ : n * Nat.succ p ≤ x) : n * p ≤ x := by
  trans
  · apply Nat.mul_le_mul_left; apply Nat.le_succ
  · apply h₁

example (a : α)(c : γ) : ∀ b : β, HEq a b → HEq b c → HEq a c := by
    intro b h₁ h₂
    trans b
    assumption
    assumption

author: leanprover-community


text:
/-
Copyright (c) 2020 Shing Tak Lam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shing Tak Lam
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.data.zmod.basic
import Mathlib.group_theory.order_of_element
import Mathlib.PostPort

universes l

namespace Mathlib

/-!
# Dihedral Groups

We define the dihedral groups `dihedral n`, with elements `r i` and `sr i` for `i : zmod n`.

For `n ≠ 0`, `dihedral n` represents the symmetry group of the regular `n`-gon. `r i` represents
the rotations of the `n`-gon by `2πi/n`, and `sr i` represents the reflections of the `n`-gon.
`dihedral 0` corresponds to the infinite dihedral group.
-/

/--
For `n ≠ 0`, `dihedral n` represents the symmetry group of the regular `n`-gon. `r i` represents
the rotations of the `n`-gon by `2πi/n`, and `sr i` represents the reflections of the `n`-gon.
`dihedral 0` corresponds to the infinite dihedral group.
-/
inductive dihedral (n : ℕ) where
| r : zmod n → dihedral n
| sr : zmod n → dihedral n

namespace dihedral

/--
Multiplication of the dihedral group.
-/
/--
The identity `1` is the rotation by `0`.
-/
protected instance inhabited {n : ℕ} : Inhabited (dihedral n) := { default := one }

/--
The inverse of a an element of the dihedral group.
-/
/--
The group structure on `dihedral n`.
-/
protected instance group {n : ℕ} : group (dihedral n) :=
  group.mk mul sorry one sorry sorry inv (div_inv_monoid.div._default mul sorry one sorry sorry inv)
    sorry

@[simp] theorem r_mul_r {n : ℕ} (i : zmod n) (j : zmod n) : r i * r j = r (i + j) := rfl

@[simp] theorem r_mul_sr {n : ℕ} (i : zmod n) (j : zmod n) : r i * sr j = sr (j - i) := rfl

@[simp] theorem sr_mul_r {n : ℕ} (i : zmod n) (j : zmod n) : sr i * r j = sr (i + j) := rfl

@[simp] theorem sr_mul_sr {n : ℕ} (i : zmod n) (j : zmod n) : sr i * sr j = r (j - i) := rfl

theorem one_def {n : ℕ} : 1 = r 0 := rfl

/--
If `0 < n`, then `dihedral n` is a finite group.
-/
protected instance fintype {n : ℕ} [fact (0 < n)] : fintype (dihedral n) :=
  fintype.of_equiv (zmod n ⊕ zmod n) fintype_helper

protected instance nontrivial {n : ℕ} : nontrivial (dihedral n) :=
  nontrivial.mk (Exists.intro (r 0) (Exists.intro (sr 0) (of_as_true trivial)))

/--
If `0 < n`, then `dihedral n` has `2n` elements.
-/
theorem card {n : ℕ} [fact (0 < n)] : fintype.card (dihedral n) = bit0 1 * n := sorry

@[simp] theorem r_one_pow {n : ℕ} (k : ℕ) : r 1 ^ k = r ↑k := sorry

@[simp] theorem r_one_pow_n {n : ℕ} : r 1 ^ n = 1 := sorry

@[simp] theorem sr_mul_self {n : ℕ} (i : zmod n) : sr i * sr i = 1 :=
  eq.mpr (id (Eq._oldrec (Eq.refl (sr i * sr i = 1)) (sr_mul_sr i i)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (r (i - i) = 1)) (sub_self i)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (r 0 = 1)) one_def)) (Eq.refl (r 0))))

/--
If `0 < n`, then `sr i` has order 2.
-/
@[simp] theorem order_of_sr {n : ℕ} [fact (0 < n)] (i : zmod n) : order_of (sr i) = bit0 1 := sorry

/--
If `0 < n`, then `r 1` has order `n`.
-/
@[simp] theorem order_of_r_one {n : ℕ} [hnpos : fact (0 < n)] : order_of (r 1) = n := sorry

/--
If `0 < n`, then `i : zmod n` has order `n / gcd n i`
-/
theorem order_of_r {n : ℕ} [fact (0 < n)] (i : zmod n) :
    order_of (r i) = n / nat.gcd n (zmod.val i) :=
  sorry

end Mathlib

author: AurelienSaue


text:
-- ---------------------------------------------------------------------
-- Ejercicio 1. Realizar las siguientes acciones:
-- 1. Importar la teoría Definicion_de_funciones_acotadas
-- 2. Declarar f y g como variable de funciones de ℝ en ℝ.
-- 3. Declarar a y c como variables sobre ℝ.
-- ----------------------------------------------------------------------

import .Definicion_de_funciones_acotadas -- 1

variables {f g : ℝ → ℝ}                  -- 2
variables {a b : ℝ}                      -- 3

-- ---------------------------------------------------------------------
-- Ejercicio 2. Demostrar que si a es una cota superior de f y b es una
-- cota superior de g, entonces a + b lo es de f + g.
-- ----------------------------------------------------------------------

theorem fn_ub_add
  (hfa : fn_ub f a)
  (hgb : fn_ub g b)
  : fn_ub (λ x, f x + g x) (a + b) :=
λ x, add_le_add (hfa x) (hgb x)

-- ---------------------------------------------------------------------
-- Ejercicio 3. Demostrar que si f y g está acotadas superiormente,
-- entonces f + g también lo está.
-- ----------------------------------------------------------------------

-- 1ª demostración
-- ===============

example
  (ubf : fn_has_ub f)
  (ubg : fn_has_ub g)
  : fn_has_ub (λ x, f x + g x) :=
begin
  rcases ubf with ⟨a, ubfa⟩,
  rcases ubg with ⟨b, ubfb⟩,
  exact ⟨a + b, fn_ub_add ubfa ubfb⟩,
end

-- Su desarrollo es
--
-- f g : ℝ → ℝ,
-- ubf : fn_has_ub f,
-- ubg : fn_has_ub g
-- ⊢ fn_has_ub (λ (x : ℝ), f x + g x)
--    >> rcases ubf with ⟨a, ubfa⟩,
-- f g : ℝ → ℝ,
-- ubg : fn_has_ub g,
-- a : ℝ,
-- ubfa : fn_ub f a
-- ⊢ fn_has_ub (λ (x : ℝ), f x + g x)
--    >> rcases ubg with ⟨b, ubfb⟩,
-- f g : ℝ → ℝ,
-- a : ℝ,
-- ubfa : fn_ub f a,
-- b : ℝ,
-- ubfb : fn_ub g b
-- ⊢ fn_has_ub (λ (x : ℝ), f x + g x)
--    >> exact ⟨a + b, fn_ub_add ubfa ubfb⟩
-- no goals

-- 2ª demostración
-- ===============

example :
  fn_has_ub f →
  fn_has_ub g →
  fn_has_ub (λ x, f x + g x) :=
begin
  rintros ⟨a, ubfa⟩ ⟨b, ubfb⟩,
  exact ⟨a + b, fn_ub_add ubfa ubfb⟩,
end

-- Su desarrollo es
--
-- f g : ℝ → ℝ
-- ⊢ fn_has_ub f → fn_has_ub g → fn_has_ub (λ (x : ℝ), f x + g x)
--    >> rintros ⟨a, ubfa⟩ ⟨b, ubfb⟩,
-- f g : ℝ → ℝ,
-- a : ℝ,
-- ubfa : fn_ub f a,
-- b : ℝ,
-- ubfb : fn_ub g b
-- ⊢ fn_has_ub (λ (x : ℝ), f x + g x)
--    >> exact ⟨a + b, fn_ub_add ubfa ubfb⟩
-- no goals

-- 3ª demostración
-- ===============

example : fn_has_ub f → fn_has_ub g →
  fn_has_ub (λ x, f x + g x) :=
λ ⟨a, ubfa⟩ ⟨b, ubfb⟩, ⟨a + b, fn_ub_add ubfa ubfb⟩

author: jaalonso


text:
-- Razonamiento sobre arboles binarios: Aplanamiento e imagen especular
-- ====================================================================

import tactic
open list

variable {α : Type}

-- Para que no use la notación con puntos
set_option pp.structure_projections false

-- ----------------------------------------------------
-- Nota. Se usarán las definiciones de árboles e
-- imagen especular estudiadas anteriormente.
-- ----------------------------------------------------

inductive arbol (α : Type) : Type
| hoja : α → arbol
| nodo : α → arbol → arbol → arbol

namespace arbol

--        3
--       / \
--      2   4
--     / \
--    1   5
def ejArbol : arbol ℕ :=
  nodo 3 (nodo 2 (hoja 1) (hoja 5)) (hoja 4)

def repr [has_repr α] : arbol α → string
| (hoja x)     := "H " ++ has_repr.repr x
| (nodo x i d) := "N " ++ has_repr.repr x ++ " (" ++ repr i ++ ") (" ++ repr d ++ ")"

instance [has_repr α] : has_repr (arbol α) := ⟨repr⟩

def espejo : arbol α → arbol α
| (hoja x)     := hoja x
| (nodo x i d) := nodo x (espejo d) (espejo i)

variables (a i d : arbol α)
variable  (x : α)

@[simp]
lemma espejo_1 :
  espejo (hoja x) = hoja x :=
rfl

@[simp]
lemma espejo_2 :
  espejo (nodo x i d) = nodo x (espejo d) (espejo i) :=
rfl

-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    aplana : arbol α → list α
-- tal que (aplana a) es la lista obtenida aplanando
-- el árbole a recorriéndolo en orden infijo. Por
-- ejemplo,
--    #eval aplana ejArbol
--    Da: [1, 2, 5, 3, 4]
--
--        3
--       / \
--      2   4
--     / \
--    1   5
-- ----------------------------------------------------

def aplana : arbol α → list α
| (hoja x)     := [x]
| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)

-- #eval aplana ejArbol
-- -- Da: [1, 2, 5, 3, 4]

-- ----------------------------------------------------
-- Ejercicio 7. Demostrar los siguientes lemas
-- + aplana_1 :
--      aplana (hoja x) = [x]
-- + aplana_2 :
--      aplana (nodo x i d) = (aplana i) ++ [x] ++ (aplana d)
-- ----------------------------------------------------

@[simp]
lemma aplana_1 :
  aplana (hoja x) = [x] :=
rfl

@[simp]
lemma aplana_2 :
  aplana (nodo x i d) = (aplana i) ++ [x] ++ (aplana d) :=
rfl

-- ----------------------------------------------------
-- Ejercicio 3. Demostrar que
--    aplana (espejo a) = rev (aplana a)
-- ----------------------------------------------------

-- 1ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { rw espejo_1,
    rw aplana_1,
    rw reverse_singleton, },
  { rw espejo_2,
    rw aplana_2,
    rw [Hi, Hd],
    rw aplana_2,
    rw reverse_append,
    rw reverse_append,
    rw reverse_singleton,
    rw append_assoc, },
end

-- 2ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { calc aplana (espejo (hoja x))
         = aplana (hoja x)
             :by simp only [espejo_1]
     ... = [x]
             :by rw aplana_1
     ... = reverse [x]
             :by rw reverse_singleton
     ... = reverse (aplana (hoja x))
             :by simp only [aplana_1], },
  { calc aplana (espejo (nodo x i d))
         = aplana (nodo x (espejo d) (espejo i))
             :by simp only [espejo_2]
     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)
             :by rw aplana_2
     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)
             :by rw [Hi, Hd]
     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)
             :by simp only [reverse_singleton]
     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)
             :by simp only [reverse_append]
     ... = reverse (aplana i ++ ([x] ++ aplana d))
             :by simp only [reverse_append]
     ... = reverse (aplana i ++ [x] ++ aplana d)
             :by simp only [append_assoc]
     ... = reverse (aplana (nodo x i d))
             :by simp only [aplana_2], },
end

-- 3ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { simp, },
  { simp [Hi, Hd], },
end

-- 4ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
by induction a ; simp [*]

-- 5ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
arbol.rec_on a
  ( assume x,
    calc aplana (espejo (hoja x))
         = aplana (hoja x)
             :by simp only [espejo_1]
     ... = [x]
             :by rw aplana_1
     ... = reverse [x]
             :by rw reverse_singleton
     ... = reverse (aplana (hoja x))
             :by simp only [aplana_1])
  ( assume x i d,
    assume Hi : aplana (espejo i) = reverse (aplana i),
    assume Hd : aplana (espejo d) = reverse (aplana d),
    calc aplana (espejo (nodo x i d))
         = aplana (nodo x (espejo d) (espejo i))
             :by simp only [espejo_2]
     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)
             :by rw aplana_2
     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)
             :by rw [Hi, Hd]
     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)
             :by simp only [reverse_singleton]
     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)
             :by simp only [reverse_append]
     ... = reverse (aplana i ++ ([x] ++ aplana d))
             :by simp only [reverse_append]
     ... = reverse (aplana i ++ [x] ++ aplana d)
             :by simp only [append_assoc]
     ... = reverse (aplana (nodo x i d))
             :by simp only [aplana_2])

-- 6ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
arbol.rec_on a
  (λ x, by simp)
  (λ x i d Hi Hd, by simp [Hi, Hd])

-- 7ª demostración
lemma aplana_espejo :
  ∀ a : arbol α, aplana (espejo a) = reverse (aplana a)
| (hoja x)     := by simp
| (nodo x i d) := by simp [aplana_espejo i,
                           aplana_espejo d]

-- ----------------------------------------------------
-- Ejercicio 4. Cerrar el espacio de nombres arbol.
-- ----------------------------------------------------

end arbol


text:
/-
Theorem 2: uniqueness of the entropy function

Hypotheses:

1. H is continuous in p
2. If p is uniform, H is monotonically increasing in n
3. Partitioning/coarse-graining - I think the proper way to express this is through conditional probabilities like:
    Let X be a random variable with probabilities p_0, ..., p_N
    Pick any j ≤ N
    Define X_coarse j = if (X = j) then 1 else 0
    Define X_hat = X | X_coarse = 1
    Then H X = H X_coarse + (1-p_j) * H X_hat

Proof sketch:

1. Let p be uniform. Use 3 iteratively to decompose the process into a series of N steps.
2. This implies that H restricted to uniform distributions is "essentially" a logarithm since A(s^m) = m * A(s) - proving this requires manipulating some inequalities, & using 2
3. Use 3 to reduce the non-uniform (but rational) to the uniform case
4. Continuity argument to extend it from the rationals to the reals
-/

/-
Binary coarse graining of a finite random variable
-/
def coarse (X : ι → ℝ) (j : ι) [rnd_var X] : (ι → ℝ) := λ i, if (i = j) then (X j) else (1 - (X j))

/-
Conditional probability of X given coarse X i = 1
Assumes X j != 0
-/
-- TODO: maybe define this invoking the p_cond method instead of writing custom code
def cond_coarse (X : ι → ℝ) (j : ι) [rnd_var X] : (ι → ℝ) := λ i, (X i) / (1 - (X j))

/--
Definition: Shannon's H
-/
class Shannons_H (N : ℕ) (X : ι → ℝ) [rnd_var X] :=
-- We have defined X : ι → ℝ
-- This is isomorphic to X : ℝ^|ι|
-- But maybe Lean cannot infer that - and there is no obvious topology for the first type
(continuous : topology.basic.continuous_def λ X, Shannons_H N X)
-- If we want to state monotonicity in N maybe we'll have to make H's dependence on N explicit in the type definition. Otherwise, we may be able to use fintype.card ι ? Yes, I think you're right.
(monotonic : is_uniform X → λ N, order.basic.monotone Shannons_H N X)
(coarse_graining : ∀ (i : ι), Shannons_H X = Shannons_H (coarse X i) + (1 - X j) * Shannons_H (cond_coarse X i) )

/--
Theorem: Shannon_entropy of Shannon's H
-/
theorem theorem2 (H : ι → ℝ) [Shannons_H H] :
-- K cannot be a free variable. I see two choices:
-- 1. define a family of H's parametrized by K (same entropy in diff units)
-- 2. Re-state the theorem with an existential quant on K
∀ (K : ℝ>0), H = - K * ∑ i, pᵢ * real.log(pᵢ) :=
begin
    sorry
end

/--
Theorem: Shannon_entropy of Shannon's H with existential quantifier
-/
theorem theorem2' (H : ι → ℝ) [Shannons_H H] :
-- K cannot be a free variable. I see two choices:
-- 1. define a family of H's parametrized by K (same entropy in diff units)
-- 2. Re-state the theorem with an existential quant on K
∃ (K : ℝ>0), H = - K * ∑ i, pᵢ * real.log(pᵢ) :=
begin
    sorry
end

/--
Theorem: Shannon_entropy of Shannon's H
-/
theorem theorem2'' (H : ι → ℝ) [Shannons_H H] {K : ℝ>0} :
-- K cannot be a free variable. I see two choices:
-- 1. define a family of H's parametrized by K (same entropy in diff units)
-- 2. Re-state the theorem with an existential quant on K
H = - K * ∑ i, pᵢ * real.log(pᵢ) :=
begin
    sorry
end

/--
Consider the expression H(p₁, ..., pₙ).
We have an unordered set of probabilities? i.e. a point in the (n-1)-simplex modulo permutations (random variables or outcomes from the sample space?)
-/
theorem H (...) :
continuous H over p₁, .. pₙ
→
(∀ i, pᵢ = 1/n → monotonically_increasing H)
→
(...)
→
H = - K * ∑ i, pᵢ * real.log(pᵢ) :=
begin
    sorry
end

---- Theorem 3

/--
Definition: probability expression (helper definition)
-/
def helper_prop (p : ℝ) (N : ℕ) (H : ...) (δ : ℝ>0) :=
|real.log(p⁻¹) / N - H| ≤ δ

/--
Theorem 3
-/
theorem theorem3 :
∀ ε>0, ∀ δ>0, ∃ N₀, ∀ N ≥ N₀
p < ε
∨
helper_prop p N H δ
:=
begin
    sorry
end

---- Theorem 4

/--
"Consider again the sequences of length N and let them be arranged in order of decreasing probabilities.

We define n(q) to be the number we must take from this set starting with the most probable one in order to accumulate a total probability q for those "
-/
def n (q : ℝ) (hq1 : q > 0) (hq2 : q < 1)

/--
Theorem 4
-/
theorem theorem4 (q : ℝ) (hq1 : q > 0) (hq2 : q < 1) :
lim N → ∞ real.log(n(q)) / N = H :=
begin
    sorry
end

author: BassemSafieldeen

repo: Shannon-theory


text:
import Mathlib
import RSACryptosystems

/-Fermat's Little theorem Proof -/
theorem fermat_little_theorem (p : ℕ) (hp : Prime p) (a : ℕ) : a ^ (p - 1) % p = 1 :=
  by
    sorry

repo: RSA-cryptosystems


text:
import Mathlib.Tactic.Rename

example (a : Nat) (b : Int) : Int × Nat := by
  rename' a => c, b => d
  exact (d, c)

example (a : Nat) (b : Int) : Int × Nat := by
  rename' a => b, b => a
  exact (a, b)


text:
import Aesop.Search.Main
import Aesop
import Lean
import LeanCodePrompts.Utils
open Aesop Lean Meta Elab Parser.Tactic

initialize tacticSuggestions : IO.Ref (Array Syntax.Tactic)
        ← IO.mkRef #[]

initialize rewriteSuggestions : IO.Ref (Array Syntax.Term)
        ← IO.mkRef #[]

initialize subgoalSuggestions : IO.Ref (Array Syntax.Term)
        ← IO.mkRef #[]

theorem mpFrom (α  : Prop) {β : Prop} : α  → (α  → β) → β  :=
  fun a f => f a

example : 1 = 1 := by
  apply mpFrom (2 = 2)
  · rfl
  · simp only [Nat.succ]

def getTacticSuggestions: IO (Array Syntax.Tactic) :=
  tacticSuggestions.get

def rwTacticSuggestions : MetaM (Array Syntax.Tactic) := do
  let rws ← rewriteSuggestions.get
  let rwTacs ← rws.mapM fun rw => do
    let rw ← `(tactic|rw [$rw:term])
    return rw
  let rwTacFlips ← rws.mapM fun rw => do
    let rw ← `(tactic|rw [← $rw:term])
    return rw
  return rwTacs ++ rwTacFlips

def rwAtTacticSuggestions : MetaM (Array Syntax.Tactic) := do
  let rws ← rewriteSuggestions.get
  let mut tacs := #[]
  let lctx ←  getLCtx
  let fvarIdents := lctx.getFVarIds.map (mkIdent ·.name)
  for r in rws do
    for f in fvarIdents do
      let tac ← `(tactic|rw [$r:term] at $f:ident)
      tacs := tacs.push tac
      let tac ← `(tactic|rw [← $r:term] at $f:ident)
      tacs := tacs.push tac
  return tacs

def subgoalTacticSuggestions : MetaM (Array Syntax.Tactic) := do
  let subgoals ← subgoalSuggestions.get
  let mp := mkIdent ``mpFrom
  subgoals.mapM <| fun α => do
    let fx ← `($mp $α:term)
    `(tactic|apply $fx:term)

def clearSuggestions : IO Unit := do
  tacticSuggestions.set #[]
  rewriteSuggestions.set #[]
  subgoalSuggestions.set #[]

def addTacticSuggestions (suggestions: Array Syntax.Tactic) : IO Unit := do
  let old ← tacticSuggestions.get
  tacticSuggestions.set (old ++ suggestions)

def addTacticSuggestion (suggestion: Syntax.Tactic) : IO Unit := do
  let old ← tacticSuggestions.get
  tacticSuggestions.set (old.push suggestion)

def addRwSuggestions (suggestions: Array Syntax.Term) : IO Unit := do
  let old ← rewriteSuggestions.get
  rewriteSuggestions.set (old ++ suggestions)

def addRwSuggestion (suggestion: Syntax.Term) : IO Unit := do
  let old ← rewriteSuggestions.get
  rewriteSuggestions.set (old.push suggestion)

def addSubgoalSuggestions (suggestions: Array Syntax.Term) : IO Unit := do
  let old ← subgoalSuggestions.get
  subgoalSuggestions.set (old ++ suggestions)

def addSubgoalSuggestion (suggestion: Syntax.Term) : IO Unit := do
  let old ← subgoalSuggestions.get
  subgoalSuggestions.set (old.push suggestion)

def addConstRewrite (decl: Name)(flip: Bool) : MetaM Unit := do
  let stx : Syntax.Term := mkIdent decl
  if flip  then
    addTacticSuggestion <| ← `(tactic|rw [← $stx])
  else
    addTacticSuggestions #[← `(tactic|rw [$stx:term])]

/-- Rule set member for `apply` for a global constant -/
def applyConstRuleMember (decl: Name)(p: Float) : MetaM RuleSetMember := do
  let type := (← getConstInfo decl).type
  let indexingMode ←  IndexingMode.targetMatchingConclusion type
  let name : RuleName := {
    name := decl
    builder := BuilderName.apply
    phase := PhaseName.«unsafe»
    scope := ScopeName.global
  }
  return RuleSetMember.unsafeRule {
    name:= name
    indexingMode := indexingMode
    usesBranchState := false
    extra:= ⟨⟨p⟩⟩
    tac := .applyConst decl}

/-- Rule set members for `simp` for a global constant proof -/
partial def simpConstRuleMember (decl: Name) : MetaM <| Array RuleSetMember := do
  let cinfo ← getConstInfo decl
  let val := cinfo.value!
  if ¬(← isProof val) then
    let head := RuleSetMember.unfoldRule {
      decl := decl
      unfoldThm? := ← getUnfoldEqnFor? decl
    }
    if let some eqns ← getEqnsFor? decl then
      let r ← eqns.mapM simpConstRuleMember
      let r := r.foldl (fun c r => c ++ r) #[]
      return r.push head
    else
      return #[head]
  else
    let entries ←  mkSimpTheorems (.decl decl) cinfo.levelParams.toArray val
    let name : RuleName := {
      name := decl
      builder := BuilderName.simp
      phase := PhaseName.norm
      scope := ScopeName.global
    }
    return #[RuleSetMember.normSimpRule {
      name:= name
      entries := entries.map .thm
      }]

def tacticExpr (goal : MVarId) (tac : Syntax.Tactic) :
    MetaM (Array MVarId × RuleTacScriptBuilder) :=
  goal.withContext do
  let goalState ← runTactic goal tac
      {errToSorry := false, implicitLambda := false} {}
  let goals := goalState.1.toArray
  let scriptBuilder :=
    ScriptBuilder.ofTactic goals.size (pure tac)
  return (goals, scriptBuilder)

def applyTacticsAux (tacs : Array Syntax.Tactic) : RuleTac := fun input => do
  let initialState ← saveState
  let appsTacs ← tacs.filterMapM fun (tac) => do
    try
      let (goals, scriptBuilder) ← tacticExpr input.goal tac
      let postState ← saveState
      return some ({ postState, goals, scriptBuilder }, tac)
    catch _ =>
      return none
    finally
      restoreState initialState
  let (apps, tacs) := appsTacs.unzip
  if apps.isEmpty then
    throwError "failed to apply any of the tactics"
  trace[leanaide.proof.info] "applied custom tactics {tacs}"
  return { applications := apps, postBranchState? := none }

def customTactics : RuleTac := fun input => do
  let tacs ← getTacticSuggestions
  logInfo m!"customTactics: {tacs}"
  applyTacticsAux tacs input

def customRuleMember (p: Float) : MetaM RuleSetMember := do
  let name : RuleName := {
    name := `customTactics
    builder := BuilderName.tactic
    phase := PhaseName.«unsafe»
    scope := ScopeName.global
  }
  return RuleSetMember.unsafeRule {
    name:= name
    indexingMode := IndexingMode.unindexed
    usesBranchState := false
    extra:= ⟨⟨p⟩⟩
    tac := .ruleTac ``customTactics}

def getRuleSet (p: Float) (apps simps rws : Array Name) : MetaM RuleSet := do
  clearSuggestions
  for n in rws do
    addConstRewrite n false
    addConstRewrite n true
  let appRules ← apps.mapM (applyConstRuleMember · p)
  let simpRules ← simps.mapM simpConstRuleMember
  let simpRules := simpRules.foldl (fun c r => c ++ r) #[]
  let defaultRules ←
      Frontend.getDefaultRuleSet (includeGlobalSimpTheorems := true)
  let allRules : RuleSet :=
    ((appRules ++ simpRules).push (← customRuleMember p)).foldl
    (fun c r => c.add r) defaultRules
  return allRules

def Lean.MessageData.format? (msg: MessageData) : Option Format :=
  match msg with
  | .ofFormat f => some f
  | _ => none

def Lean.MessageData.ppformat? (msg: MessageData) : Option PPFormat :=
  match msg with
  | .ofPPFormat f => some f
  | _ => none

-- to extract tactics later
def Lean.MessageData.split (msg: MessageData) : Array MessageData :=
  match msg with
  | .compose l₁ l₂ => l₁.split ++ l₂.split
  | .nest n l => #[m!"nest {n}"] ++ l.split
  | .withContext _ l => #[m!"ctx"] ++ l.split
  | .withNamingContext _ l => #[m!"nmgctx"] ++ l.split
  | .ofFormat _ => #["format", msg]
  | .ofPPFormat _ => #["ppformat", msg]
  | _ => #[msg]

def runAesop (p: Float) (apps simps rws : Array Name) : MVarId → MetaM (List MVarId) := fun goal => goal.withContext do
  let allRules ← getRuleSet p apps simps rws
  let (goals, _) ← Aesop.search goal allRules {traceScript := true}
  let msgLog ← Core.getMessageLog
  let msgs := msgLog.toList
  logInfo m!"Messages: {msgs.map (·.data.split)}"
  return goals.toList

example : α → α := by
  aesop

-- For introducing local definitions
/- Convert the given goal `Ctx |- target` into `Ctx |- let name : type := val; target`. It assumes `val` has type `type` -/
#check MVarId.define -- Lean.MVarId.define (mvarId : MVarId) (name : Name) (type val : Expr) : MetaM MVarId

#check MessageData.instAppendMessageData

author: siddhartha-gadgil

repo: LeanAide