text:
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-/
import data.list.join

/-!
# Permutations of a list

In this file we prove properties about `list.permutations`, a list of all permutations of a list. It
is defined in `data.list.defs`.

## Order of the permutations

Designed for performance, the order in which the permutations appear in `list.permutations` is
rather intricate and not very amenable to induction. That's why we also provide `list.permutations'`
as a less efficient but more straightforward way of listing permutations.

### `list.permutations`

TODO. In the meantime, you can try decrypting the docstrings.

### `list.permutations'`

The list of partitions is built by recursion. The permutations of `[]` are `[[]]`. Then, the
permutations of `a :: l` are obtained by taking all permutations of `l` in order and adding `a` in
all positions. Hence, to build `[0, 1, 2, 3].permutations'`, it does
* `[[]]`
* `[[3]]`
* `[[2, 3], [3, 2]]]`
* `[[1, 2, 3], [2, 1, 3], [2, 3, 1], [1, 3, 2], [3, 1, 2], [3, 2, 1]]`
* `[[0, 1, 2, 3], [1, 0, 2, 3], [1, 2, 0, 3], [1, 2, 3, 0],`
   `[0, 2, 1, 3], [2, 0, 1, 3], [2, 1, 0, 3], [2, 1, 3, 0],`
   `[0, 2, 3, 1], [2, 0, 3, 1], [2, 3, 0, 1], [2, 3, 1, 0],`
   `[0, 1, 3, 2], [1, 0, 3, 2], [1, 3, 0, 2], [1, 3, 2, 0],`
   `[0, 3, 1, 2], [3, 0, 1, 2], [3, 1, 0, 2], [3, 1, 2, 0],`
   `[0, 3, 2, 1], [3, 0, 2, 1], [3, 2, 0, 1], [3, 2, 1, 0]]`

## TODO

Show that `l.nodup → l.permutations.nodup`. See `data.fintype.list`.
-/

open nat

variables {α β : Type*}

namespace list

lemma permutations_aux2_fst (t : α) (ts : list α) (r : list β) : ∀ (ys : list α) (f : list α → β),
  (permutations_aux2 t ts r ys f).1 = ys ++ ts
| []      f := rfl
| (y::ys) f := match _, permutations_aux2_fst ys _ : ∀ o : list α × list β, o.1 = ys ++ ts →
      (permutations_aux2._match_1 t y f o).1 = y :: ys ++ ts with
  | ⟨_, zs⟩, rfl := rfl
  end

@[simp] lemma permutations_aux2_snd_nil (t : α) (ts : list α) (r : list β) (f : list α → β) :
  (permutations_aux2 t ts r [] f).2 = r := rfl

@[simp] lemma permutations_aux2_snd_cons (t : α) (ts : list α) (r : list β) (y : α) (ys : list α)
  (f : list α → β) :
  (permutations_aux2 t ts r (y::ys) f).2 = f (t :: y :: ys ++ ts) ::
    (permutations_aux2 t ts r ys (λx : list α, f (y::x))).2 :=
match _, permutations_aux2_fst t ts r _ _ : ∀ o : list α × list β, o.1 = ys ++ ts →
   (permutations_aux2._match_1 t y f o).2 = f (t :: y :: ys ++ ts) :: o.2 with
| ⟨_, zs⟩, rfl := rfl
end

/-- The `r` argument to `permutations_aux2` is the same as appending. -/
lemma permutations_aux2_append (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :
  (permutations_aux2 t ts nil ys f).2 ++ r = (permutations_aux2 t ts r ys f).2 :=
by induction ys generalizing f; simp *

/-- The `ts` argument to `permutations_aux2` can be folded into the `f` argument. -/
lemma permutations_aux2_comp_append {t : α} {ts ys : list α} {r : list β} (f : list α → β) :
  (permutations_aux2 t [] r ys $ λ x, f (x ++ ts)).2 = (permutations_aux2 t ts r ys f).2 :=
begin
  induction ys generalizing f,
  { simp },
  { simp [ys_ih (λ xs, f (ys_hd :: xs))] },
end

lemma map_permutations_aux2' {α β α' β'} (g : α → α') (g' : β → β')
  (t : α) (ts ys : list α) (r : list β) (f : list α → β) (f' : list α' → β')
  (H : ∀ a, g' (f a) = f' (map g a)) :
  map g' (permutations_aux2 t ts r ys f).2 =
  (permutations_aux2 (g t) (map g ts) (map g' r) (map g ys) f').2 :=
begin
  induction ys generalizing f f'; simp *,
  apply ys_ih, simp [H],
end

/-- The `f` argument to `permutations_aux2` when `r = []` can be eliminated. -/
lemma map_permutations_aux2 (t : α) (ts : list α) (ys : list α) (f : list α → β) :
  (permutations_aux2 t ts [] ys id).2.map f = (permutations_aux2 t ts [] ys f).2 :=
begin
  convert map_permutations_aux2' id _ _ _ _ _ _ _ _; simp only [map_id, id.def],
  exact (λ _, rfl)
end

/-- An expository lemma to show how all of `ts`, `r`, and `f` can be eliminated from
`permutations_aux2`.

`(permutations_aux2 t [] [] ys id).2`, which appears on the RHS, is a list whose elements are
produced by inserting `t` into every non-terminal position of `ys` in order. As an example:
```lean
#eval permutations_aux2 1 [] [] [2, 3, 4] id
-- [[1, 2, 3, 4], [2, 1, 3, 4], [2, 3, 1, 4]]
```
-/
lemma permutations_aux2_snd_eq (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :
  (permutations_aux2 t ts r ys f).2 =
    (permutations_aux2 t [] [] ys id).2.map (λ x, f (x ++ ts)) ++ r :=
by rw [← permutations_aux2_append, map_permutations_aux2, permutations_aux2_comp_append]

lemma map_map_permutations_aux2 {α α'} (g : α → α') (t : α) (ts ys : list α) :
  map (map g) (permutations_aux2 t ts [] ys id).2 =
  (permutations_aux2 (g t) (map g ts) [] (map g ys) id).2 :=
map_permutations_aux2' _ _ _ _ _ _ _ _ (λ _, rfl)

lemma map_map_permutations'_aux (f : α → β) (t : α) (ts : list α) :
  map (map f) (permutations'_aux t ts) = permutations'_aux (f t) (map f ts) :=
by induction ts with a ts ih; [refl, {simp [← ih], refl}]

lemma permutations'_aux_eq_permutations_aux2 (t : α) (ts : list α) :
  permutations'_aux t ts = (permutations_aux2 t [] [ts ++ [t]] ts id).2 :=
begin
  induction ts with a ts ih, {refl},
  simp [permutations'_aux, permutations_aux2_snd_cons, ih],
  simp only [← permutations_aux2_append] {single_pass := tt},
  simp [map_permutations_aux2],
end

lemma mem_permutations_aux2 {t : α} {ts : list α} {ys : list α} {l l' : list α} :
  l' ∈ (permutations_aux2 t ts [] ys (append l)).2 ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts :=
begin
  induction ys with y ys ih generalizing l,
  { simp {contextual := tt} },
  rw [permutations_aux2_snd_cons, show (λ (x : list α), l ++ y :: x) = append (l ++ [y]),
      by funext; simp, mem_cons_iff, ih], split,
  { rintro (e | ⟨l₁, l₂, l0, ye, _⟩),
    { subst l', exact ⟨[], y::ys, by simp⟩ },
    { substs l' ys, exact ⟨y::l₁, l₂, l0, by simp⟩ } },
  { rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩,
    { simp [ye] },
    { simp only [cons_append] at ye, rcases ye with ⟨rfl, rfl⟩,
      exact or.inr ⟨l₁, l₂, l0, by simp⟩ } }
end

lemma mem_permutations_aux2' {t : α} {ts : list α} {ys : list α} {l : list α} :
  l ∈ (permutations_aux2 t ts [] ys id).2 ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts :=
by rw [show @id (list α) = append nil, by funext; refl]; apply mem_permutations_aux2

lemma length_permutations_aux2 (t : α) (ts : list α) (ys : list α) (f : list α → β) :
  length (permutations_aux2 t ts [] ys f).2 = length ys :=
by induction ys generalizing f; simp *

lemma foldr_permutations_aux2 (t : α) (ts : list α) (r L : list (list α)) :
  foldr (λy r, (permutations_aux2 t ts r y id).2) r L =
    L.bind (λ y, (permutations_aux2 t ts [] y id).2) ++ r :=
by induction L with l L ih; [refl, {simp [ih], rw ← permutations_aux2_append}]

lemma mem_foldr_permutations_aux2 {t : α} {ts : list α} {r L : list (list α)} {l' : list α} :
  l' ∈ foldr (λy r, (permutations_aux2 t ts r y id).2) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts :=
have (∃ (a : list α), a ∈ L ∧
    ∃ (l₁ l₂ : list α), ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ (l₁ l₂ : list α), ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts),
from ⟨λ ⟨a, aL, l₁, l₂, l0, e, h⟩, ⟨l₁, l₂, l0, e ▸ aL, h⟩,
      λ ⟨l₁, l₂, l0, aL, h⟩, ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩,
by rw foldr_permutations_aux2; simp [mem_permutations_aux2', this,
  or.comm, or.left_comm, or.assoc, and.comm, and.left_comm, and.assoc]

lemma length_foldr_permutations_aux2 (t : α) (ts : list α) (r L : list (list α)) :
  length (foldr (λy r, (permutations_aux2 t ts r y id).2) r L) = sum (map length L) + length r :=
by simp [foldr_permutations_aux2, (∘), length_permutations_aux2]

lemma length_foldr_permutations_aux2' (t : α) (ts : list α) (r L : list (list α))
  (n) (H : ∀ l ∈ L, length l = n) :
  length (foldr (λy r, (permutations_aux2 t ts r y id).2) r L) = n * length L + length r :=
begin
  rw [length_foldr_permutations_aux2, (_ : sum (map length L) = n * length L)],
  induction L with l L ih, {simp},
  have sum_map : sum (map length L) = n * length L :=
    ih (λ l m, H l (mem_cons_of_mem _ m)),
  have length_l : length l = n := H _ (mem_cons_self _ _),
  simp [sum_map, length_l, mul_add, add_comm]
end

@[simp] lemma permutations_aux_nil (is : list α) : permutations_aux [] is = [] :=
by rw [permutations_aux, permutations_aux.rec]

@[simp] lemma permutations_aux_cons (t : α) (ts is : list α) :
  permutations_aux (t :: ts) is = foldr (λy r, (permutations_aux2 t ts r y id).2)
    (permutations_aux ts (t::is)) (permutations is) :=
by rw [permutations_aux, permutations_aux.rec]; refl

@[simp] lemma permutations_nil : permutations ([] : list α) = [[]] :=
by rw [permutations, permutations_aux_nil]

lemma map_permutations_aux (f : α → β) : ∀ (ts is : list α),
  map (map f) (permutations_aux ts is) = permutations_aux (map f ts) (map f is) :=
begin
  refine permutations_aux.rec (by simp) _,
  introv IH1 IH2, rw map at IH2,
  simp only [foldr_permutations_aux2, map_append, map, map_map_permutations_aux2, permutations,
    bind_map, IH1, append_assoc, permutations_aux_cons, cons_bind, ← IH2, map_bind],
end

lemma map_permutations (f : α → β) (ts : list α) :
  map (map f) (permutations ts) = permutations (map f ts) :=
by rw [permutations, permutations, map, map_permutations_aux, map]

lemma map_permutations' (f : α → β) (ts : list α) :
  map (map f) (permutations' ts) = permutations' (map f ts) :=
by induction ts with t ts ih; [refl, simp [← ih, map_bind, ← map_map_permutations'_aux, bind_map]]

lemma permutations_append (is ts : list α) :
  permutations (is ++ ts) = (permutations is).map (++ ts) ++ permutations_aux ts is.reverse :=
by simp [permutations, permutations_aux_append]

end list


text:
/-
Copyright (c) 2021 David Wärn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Wärn
-/
import topology.stone_cech
import topology.algebra.semigroup
import data.stream.init

/-!
# Hindman's theorem on finite sums

We prove Hindman's theorem on finite sums, using idempotent ultrafilters.

Given an infinite sequence `a₀, a₁, a₂, …` of positive integers, the set `FS(a₀, …)` is the set
of positive integers that can be expressed as a finite sum of `aᵢ`'s, without repetition. Hindman's
theorem asserts that whenever the positive integers are finitely colored, there exists a sequence
`a₀, a₁, a₂, …` such that `FS(a₀, …)` is monochromatic. There is also a stronger version, saying
that whenever a set of the form `FS(a₀, …)` is finitely colored, there exists a sequence
`b₀, b₁, b₂, …` such that `FS(b₀, …)` is monochromatic and contained in `FS(a₀, …)`. We prove both
these versions for a general semigroup `M` instead of `ℕ+` since it is no harder, although this
special case implies the general case.

The idea of the proof is to extend the addition `(+) : M → M → M` to addition `(+) : βM → βM → βM`
on the space `βM` of ultrafilters on `M`. One can prove that if `U` is an _idempotent_ ultrafilter,
i.e. `U + U = U`, then any `U`-large subset of `M` contains some set `FS(a₀, …)` (see
`exists_FS_of_large`). And with the help of a general topological argument one can show that any set
of the form `FS(a₀, …)` is `U`-large according to some idempotent ultrafilter `U` (see
`exists_idempotent_ultrafilter_le_FS`). This is enough to prove the theorem since in any finite
partition of a `U`-large set, one of the parts is `U`-large.

## Main results

- `FS_partition_regular`: the strong form of Hindman's theorem
- `exists_FS_of_finite_cover`: the weak form of Hindman's theorem

## Tags

Ramsey theory, ultrafilter

-/

open filter

/-- Multiplication of ultrafilters given by `∀ᶠ m in U*V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m*m')`. -/
@[to_additive "Addition of ultrafilters given by
`∀ᶠ m in U+V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m+m')`." ]
def ultrafilter.has_mul {M} [has_mul M] : has_mul (ultrafilter M) :=
{ mul := λ U V, (*) <$> U <*> V }

local attribute [instance] ultrafilter.has_mul ultrafilter.has_add

/- We could have taken this as the definition of `U * V`, but then we would have to prove that it
defines an ultrafilter. -/
@[to_additive]
lemma ultrafilter.eventually_mul {M} [has_mul M] (U V : ultrafilter M) (p : M → Prop) :
  (∀ᶠ m in ↑(U * V), p m) ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m * m') := iff.rfl

/-- Semigroup structure on `ultrafilter M` induced by a semigroup structure on `M`. -/
@[to_additive "Additive semigroup structure on `ultrafilter M` induced by an additive semigroup
structure on `M`."]
def ultrafilter.semigroup {M} [semigroup M] : semigroup (ultrafilter M) :=
{ mul_assoc := λ U V W, ultrafilter.coe_inj.mp $ filter.ext' $ λ p,
    by simp only [ultrafilter.eventually_mul, mul_assoc]
  ..ultrafilter.has_mul }

local attribute [instance] ultrafilter.semigroup ultrafilter.add_semigroup

/- We don't prove `continuous_mul_right`, because in general it is false! -/
@[to_additive]
lemma ultrafilter.continuous_mul_left {M} [semigroup M] (V : ultrafilter M) : continuous (* V) :=
topological_space.is_topological_basis.continuous ultrafilter_basis_is_basis _ $
set.forall_range_iff.mpr $ λ s, ultrafilter_is_open_basic { m : M | ∀ᶠ m' in V, m * m' ∈ s }

namespace hindman

/-- `FS a` is the set of finite sums in `a`, i.e. `m ∈ FS a` if `m` is the sum of a nonempty
subsequence of `a`. We give a direct inductive definition instead of talking about subsequences. -/
inductive FS {M} [add_semigroup M] : stream M → set M
| head (a : stream M) : FS a a.head
| tail (a : stream M) (m : M) (h : FS a.tail m) : FS a m
| cons (a : stream M) (m : M) (h : FS a.tail m) : FS a (a.head + m)

/-- `FP a` is the set of finite products in `a`, i.e. `m ∈ FP a` if `m` is the product of a nonempty
subsequence of `a`. We give a direct inductive definition instead of talking about subsequences. -/
@[to_additive FS]
inductive FP {M} [semigroup M] : stream M → set M
| head (a : stream M) : FP a a.head
| tail (a : stream M) (m : M) (h : FP a.tail m) : FP a m
| cons (a : stream M) (m : M) (h : FP a.tail m) : FP a (a.head * m)

/-- If `m` and `m'` are finite products in `M`, then so is `m * m'`, provided that `m'` is obtained
from a subsequence of `M` starting sufficiently late. -/
@[to_additive]
lemma FP.mul {M} [semigroup M] {a : stream M} {m : M} (hm : m ∈ FP a) :
  ∃ n, ∀ m' ∈ FP (a.drop n), m * m' ∈ FP a :=
begin
  induction hm with a a m hm ih a m hm ih,
  { exact ⟨1, λ m hm, FP.cons a m hm⟩, },
  { cases ih with n hn, use n+1, intros m' hm', exact FP.tail _ _ (hn _ hm'), },
  { cases ih with n hn, use n+1, intros m' hm', rw mul_assoc, exact FP.cons _ _ (hn _ hm'), },
end

@[to_additive exists_idempotent_ultrafilter_le_FS]
lemma exists_idempotent_ultrafilter_le_FP {M} [semigroup M] (a : stream M) :
  ∃ U : ultrafilter M, U * U = U ∧ ∀ᶠ m in U, m ∈ FP a :=
begin
  let S : set (ultrafilter M) := ⋂ n, { U | ∀ᶠ m in U, m ∈ FP (a.drop n) },
  obtain ⟨U, hU, U_idem⟩ := exists_idempotent_in_compact_subsemigroup _ S _ _ _,
  { refine ⟨U, U_idem, _⟩, convert set.mem_Inter.mp hU 0, },
  { exact ultrafilter.continuous_mul_left },
  { apply is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed,
    { intros n U hU,
      apply eventually.mono hU,
      rw [add_comm, ←stream.drop_drop, ←stream.tail_eq_drop],
      exact FP.tail _ },
    { intro n, exact ⟨pure _, mem_pure.mpr $ FP.head _⟩, },
    { exact (ultrafilter_is_closed_basic _).is_compact, },
    { intro n, apply ultrafilter_is_closed_basic, }, },
  { exact is_closed.is_compact (is_closed_Inter $ λ i, ultrafilter_is_closed_basic _) },
  { intros U V hU hV,
    rw set.mem_Inter at *,
    intro n,
    rw [set.mem_set_of_eq, ultrafilter.eventually_mul],
    apply eventually.mono (hU n),
    intros m hm,
    obtain ⟨n', hn⟩ := FP.mul hm,
    apply eventually.mono (hV (n' + n)),
    intros m' hm',
    apply hn,
    simpa only [stream.drop_drop] using hm', }
end

@[to_additive exists_FS_of_large]
lemma exists_FP_of_large {M} [semigroup M] (U : ultrafilter M) (U_idem : U * U = U)
  (s₀ : set M) (sU : s₀ ∈ U) : ∃ a, FP a ⊆ s₀ :=
begin
/- Informally: given a `U`-large set `s₀`, the set `s₀ ∩ { m | ∀ᶠ m' in U, m * m' ∈ s₀ }` is also
`U`-large (since `U` is idempotent). Thus in particular there is an `a₀` in this intersection. Now
let `s₁` be the intersection `s₀ ∩ { m | a₀ * m ∈ s₀ }`. By choice of `a₀`, this is again `U`-large,
so we can repeat the argument starting from `s₁`, obtaining `a₁`, `s₂`, etc. This gives the desired
infinite sequence. -/
  have exists_elem : ∀ {s : set M} (hs : s ∈ U), (s ∩ { m | ∀ᶠ m' in U, m * m' ∈ s }).nonempty :=
    λ s hs, ultrafilter.nonempty_of_mem (inter_mem hs $ by { rw ←U_idem at hs, exact hs }),
  let elem : { s // s ∈ U } → M := λ p, (exists_elem p.property).some,
  let succ : { s // s ∈ U } → { s // s ∈ U } := λ p, ⟨p.val ∩ { m | elem p * m ∈ p.val },
    inter_mem p.2 $ show _, from set.inter_subset_right _ _ (exists_elem p.2).some_mem⟩,
  use stream.corec elem succ (subtype.mk s₀ sU),
  suffices : ∀ (a : stream M) (m ∈ FP a), ∀ p, a = stream.corec elem succ p → m ∈ p.val,
  { intros m hm, exact this _ m hm ⟨s₀, sU⟩ rfl, },
  clear sU s₀,
  intros a m h,
  induction h with b b n h ih b n h ih,
  { rintros p rfl,
    rw [stream.corec_eq, stream.head_cons],
    exact set.inter_subset_left _ _ (set.nonempty.some_mem _), },
  { rintros p rfl,
    refine set.inter_subset_left _ _ (ih (succ p) _),
    rw [stream.corec_eq, stream.tail_cons], },
  { rintros p rfl,
    have := set.inter_subset_right _ _ (ih (succ p) _),
    { simpa only using this },
    rw [stream.corec_eq, stream.tail_cons], },
end

/-- The strong form of **Hindman's theorem**: in any finite cover of an FP-set, one the parts
contains an FP-set. -/
@[to_additive FS_partition_regular]
lemma FP_partition_regular {M} [semigroup M] (a : stream M) (s : set (set M)) (sfin : s.finite)
  (scov : FP a ⊆ ⋃₀ s) : ∃ (c ∈ s) (b : stream M), FP b ⊆ c :=
let ⟨U, idem, aU⟩ := exists_idempotent_ultrafilter_le_FP a in
let ⟨c, cs, hc⟩ := (ultrafilter.finite_sUnion_mem_iff sfin).mp (mem_of_superset aU scov) in
⟨c, cs, exists_FP_of_large U idem c hc⟩

/-- The weak form of **Hindman's theorem**: in any finite cover of a nonempty semigroup, one of the
parts contains an FP-set. -/
@[to_additive exists_FS_of_finite_cover]

@[to_additive FS_iter_tail_sub_FS]
lemma FP_drop_subset_FP {M} [semigroup M] (a : stream M) (n : ℕ) :
  FP (a.drop n) ⊆ FP a :=
begin
  induction n with n ih, { refl },
  rw [nat.succ_eq_one_add, ←stream.drop_drop],
  exact trans (FP.tail _) ih,
end

@[to_additive]
lemma FP.singleton {M} [semigroup M] (a : stream M) (i : ℕ) : a.nth i ∈ FP a :=
by { induction i with i ih generalizing a, { apply FP.head }, { apply FP.tail, apply ih } }

@[to_additive]
lemma FP.mul_two {M} [semigroup M] (a : stream M) (i j : ℕ) (ij : i < j) :
  a.nth i * a.nth j ∈ FP a :=
begin
  refine FP_drop_subset_FP _ i _,
  rw ←stream.head_drop,
  apply FP.cons,
  rcases le_iff_exists_add.mp (nat.succ_le_of_lt ij) with ⟨d, hd⟩,
  have := FP.singleton (a.drop i).tail d,
  rw [stream.tail_eq_drop, stream.nth_drop, stream.nth_drop] at this,
  convert this,
  rw [hd, add_comm, nat.succ_add, nat.add_succ],
end

@[to_additive]
lemma FP.finset_prod {M} [comm_monoid M] (a : stream M) (s : finset ℕ) (hs : s.nonempty) :
  s.prod (λ i, a.nth i) ∈ FP a :=
begin
  refine FP_drop_subset_FP _ (s.min' hs) _,
  induction s using finset.strong_induction with s ih,
  rw [←finset.mul_prod_erase _ _ (s.min'_mem hs), ←stream.head_drop],
  cases (s.erase (s.min' hs)).eq_empty_or_nonempty with h h,
  { rw [h, finset.prod_empty, mul_one], exact FP.head _ },
  { apply FP.cons, rw [stream.tail_eq_drop, stream.drop_drop, add_comm],
    refine set.mem_of_subset_of_mem _ (ih _ (finset.erase_ssubset $ s.min'_mem hs) h),
    have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h :=
      nat.succ_le_of_lt (finset.min'_lt_of_mem_erase_min' _ _ $ finset.min'_mem _ _),
    cases le_iff_exists_add.mp this with d hd,
    rw [hd, add_comm, ←stream.drop_drop],
    apply FP_drop_subset_FP }
end

end hindman

author: jjaassoonn


text:
import NBG.SetTheory.Defs
import NBG.SetTheory.Axioms.Extensionality

open Classical

-- 2. AxiomUniverse
axiom AxiomUniverse :
  ∃U : Class, ∀x: Class, (x∈U ↔ ∃X: Class,(x∈X))
noncomputable def U: Class :=
  choose AxiomUniverse
noncomputable def U_def:
  ∀x: Class, (x∈U ↔ ∃X: Class,(x∈X)) :=
  choose_spec AxiomUniverse

theorem UniqueU :
  isUnique (fun U => ∀x: Class, (x∈U ↔ ∃X: Class,(x∈X))) := by {
  intro U U' hU hU';
  apply (AxiomExtensionality U U').2;
  intro z;
  rw [hU, hU'];
  exact ⟨fun h => h,fun h => h⟩;
}

theorem AllSetInU {x : Class}: isSet x ↔ x∈U := by {
  apply Iff.intro;
  {exact fun ⟨y, h⟩ => (choose_spec AxiomUniverse x).2 ⟨y, h⟩;}
  {exact fun h => (choose_spec AxiomUniverse x).1 h;}
}

-- type Set
class Set (X : Class) where
  isSet : isSet X
  inU   : X ∈ U
def Set.mk₁ {X Y: Class} (h: X ∈ Y): Set X :=
  Set.mk ⟨Y, h⟩ (AllSetInU.1 ⟨Y, h⟩)
def Set.mk₂ {X: Class} (hx: X ∈ U): Set X :=
  Set.mk (AllSetInU.2 hx) hx

-- type SetType
class SetType where
  X : Class
  x : Set X
def SetType.mk₁ {X Y: Class} (h: X ∈ Y): SetType :=
  SetType.mk X (Set.mk₁ h)
def SetType.mk₂ (X: Class) (hx: X ∈ U): SetType :=
  SetType.mk X (Set.mk₂ hx)

def SetType.Eq (X Y: SetType) : Prop := X.1 ＝ Y.1
def SetType.In (X Y: SetType) : Prop := X.1 ∈ Y.1
instance : HasEq SetType where
  Eq := SetType.Eq
instance : HasIn SetType where
  In := SetType.In

theorem AllSetSubsetU (X : Class) : X⊂U :=
  fun _ hx => AllSetInU.1 ⟨X, hx⟩

repo: NBG


text:
import encode

open tree tencodable function
open_locale tree

/-- A complexity class is a set of functions closed under some
  basic operations which essentially allow constant-time modifications -/
structure complexity_class :=
(prop : (tree unit → tree unit) → Prop)
(nil : prop (λ _, nil))
(left : prop (λ x, x.left))
(right : prop (λ x, x.right))
(id : prop (λ x, x))
(pair : ∀ {f₁ f₂}, prop f₁ → prop f₂ → prop (λ x, (f₁ x) △ (f₂ x)))
(comp : ∀ {f₁ f₂}, prop f₁ → prop f₂ → prop (f₁ ∘ f₂))
(ite' : ∀ {c f g}, prop c → prop f → prop g → prop (λ x, if c x = tree.nil then f x else g x))

namespace complexity_class

variables (C : complexity_class)
  {α β γ γ₀ γ₁ γ₂ γ₃ γ₄ γ₅ γ₆ γ₇ : Type}
variables [tencodable α] [tencodable β]

def mem1 (f : α → β) : Prop :=
∃ (f' : tree unit → tree unit), C.prop f' ∧ ∀ x : α, f' (encode x) = encode (f x)

/-- Many argument function is in `C` -/
def mem [has_uncurry γ α β] (f : γ) (C : complexity_class) : Prop :=
C.mem1 ↿f

def mem_pred [has_uncurry γ α Prop] (f : γ) (C : complexity_class) : Prop :=
C.mem (λ x : α, @to_bool (↿f x) (classical.dec _))

localized "infix ` ∈ₑ `:50 := complexity_class.mem" in complexity_class
localized "infix ` ∈ₚ `:50 := complexity_class.mem_pred" in complexity_class

protected theorem prop_const : ∀ (n : tree unit), C.prop (λ _, n)
| tree.nil := C.nil
| (x △ y) := C.pair (prop_const x) (prop_const y)

protected theorem const (x : α) : (λ _ : β, x) ∈ₑ C :=
⟨_, C.prop_const (encode x), λ _, rfl⟩

protected theorem const' (x : α) : const β x ∈ₑ C := C.const x

variable {C}

@[simp] lemma mem1_iff_mem {f : α → β} : C.mem1 f ↔ f ∈ₑ C := iff.rfl

private lemma mem_iff_mem_pred_aux {f : α → Prop} :
  (λ x, @to_bool (f x) (classical.dec _)) ∈ₑ C ↔ f ∈ₚ C := iff.rfl

lemma mem_iff_mem_pred {f : α → Prop} [decidable_pred f] :
  ((λ x, to_bool (f x)) ∈ₑ C) ↔ f ∈ₚ C :=
by { convert mem_iff_mem_pred_aux, ext, congr, }

private lemma mem_iff_mem_rel_aux {f : α → β → Prop} :
  ((λ x y, @to_bool (f x y) (classical.dec _))) ∈ₑ C ↔ f ∈ₚ C := iff.rfl

lemma mem_iff_mem_rel {f : α → β → Prop} [∀ x y, decidable (f x y)] :
  ((λ x y, (f x y : bool))) ∈ₑ C ↔ f ∈ₚ C :=
by { convert mem_iff_mem_rel_aux, ext, congr, }

lemma mem₂_iff {α β γ : Type} [tencodable α] [tencodable β] [tencodable γ]
  {f : α × β → γ} {C : complexity_class} : f ∈ₑ C ↔ (λ (x : α) (y : β), f (x, y)) ∈ₑ C :=
by { dsimp only [mem, has_uncurry.uncurry, _root_.id], simp only [prod.mk.eta], }

@[simp] lemma prop_iff_mem {f : tree unit → tree unit} :
  C.prop f ↔ f ∈ₑ C :=
⟨λ pf, ⟨f, pf, λ _, rfl⟩, λ ⟨f', pf, hf⟩, by { convert pf, ext x, exact (hf x).symm, }⟩

variables [tencodable γ] [tencodable γ₀] [tencodable γ₁] [tencodable γ₂]
  [tencodable γ₃] [tencodable γ₄] [tencodable γ₅] [tencodable γ₆]

theorem mem.comp {f : α → β} {g : γ → α} :
  f ∈ₑ C → g ∈ₑ C → (λ x, f (g x)) ∈ₑ C
| ⟨f', pf', hf'⟩ ⟨g', pg', hg'⟩ :=
⟨_, C.comp pf' pg', λ x, by simp [hf', hg', has_uncurry.uncurry]⟩

theorem mem.pair {f : α → β} {g : α → γ} : f ∈ₑ C → g ∈ₑ C → (λ x, (f x, g x)) ∈ₑ C
| ⟨f', pf', hf'⟩ ⟨g', pg', hg'⟩ :=
⟨_, C.pair pf' pg', λ x, by simp [hf', hg', encode, has_uncurry.uncurry]⟩

theorem mem.fst : @prod.fst α β ∈ₑ C := ⟨_, C.left, λ _, rfl⟩
theorem mem.snd : @prod.snd α β ∈ₑ C := ⟨_, C.right, λ _, rfl⟩

protected lemma mem_pred.ite {P : α → Prop} [decidable_pred P] {f : α → β} {g : α → β} :
  P ∈ₚ C → f ∈ₑ C → g ∈ₑ C → (λ x, if P x then f x else g x) ∈ₑ C
| ⟨P', pP, hP⟩ ⟨f', pf, hf⟩ ⟨g', pg, hg⟩ :=
⟨_, C.ite' pP pf pg, λ x, by by_cases P x; simp [*, encode, has_uncurry.uncurry]⟩

/- TODO: Autogenerate these lemmas; convert following to Lean code:
var subscript = n => String.fromCharCode(8320 + n);

var template = n =>
`theorem mem.comp${subscript(n)}
  {f : ${range(n).map(m => `γ${subscript(m)}`).join(" → ") + " → α"}}
  ${range(n).map(m => `{g${subscript(m)} : β → γ${subscript(m)}}`).join(" ")}
  (hf : f ∈ₑ C) ${range(n).map(m => `(hg${subscript(m)}: g${subscript(m)} ∈ₑ C)`).join(" ")} :
  (λ x, f ${range(n).map(m => `(g${subscript(m)} x)`).join(" ")}) ∈ₑ C :=
  hf.comp $ ${range(n).map(m => `hg${subscript(m)}`).join(".pair $ ")}`

var template_pred = n =>
`theorem mem_pred.comp${subscript(n)}
  {f : ${range(n).map(m => `γ${subscript(m)}`).join(" → ") + " → Prop"}}
  ${range(n).map(m => `{g${subscript(m)} : α → γ${subscript(m)}}`).join(" ")}
  (hf : f ∈ₚ C) ${range(n).map(m => `(hg${subscript(m)}: g${subscript(m)} ∈ₑ C)`).join(" ")} :
  (λ x, f ${range(n).map(m => `(g${subscript(m)} x)`).join(" ")}) ∈ₚ C :=
  hf.comp $ ${range(n).map(m => `hg${subscript(m)}`).join(".pair $ ")}`

 -/
section comp
theorem mem.comp₂
  {f : γ₀ → γ₁ → α}
  {g₀ : β → γ₀} {g₁ : β → γ₁}
  (hf : f ∈ₑ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x)) ∈ₑ C :=
  hf.comp $ hg₀.pair $ hg₁
theorem mem.comp₃
  {f : γ₀ → γ₁ → γ₂ → α}
  {g₀ : β → γ₀} {g₁ : β → γ₁} {g₂ : β → γ₂}
  (hf : f ∈ₑ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x)) ∈ₑ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂
theorem mem.comp₄
  {f : γ₀ → γ₁ → γ₂ → γ₃ → α}
  {g₀ : β → γ₀} {g₁ : β → γ₁} {g₂ : β → γ₂} {g₃ : β → γ₃}
  (hf : f ∈ₑ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) (hg₃: g₃ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x) (g₃ x)) ∈ₑ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂.pair $ hg₃
theorem mem.comp₅
  {f : γ₀ → γ₁ → γ₂ → γ₃ → γ₄ → α}
  {g₀ : β → γ₀} {g₁ : β → γ₁} {g₂ : β → γ₂} {g₃ : β → γ₃} {g₄ : β → γ₄}
  (hf : f ∈ₑ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) (hg₃: g₃ ∈ₑ C) (hg₄: g₄ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x) (g₃ x) (g₄ x)) ∈ₑ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂.pair $ hg₃.pair $ hg₄
theorem mem.comp₆
  {f : γ₀ → γ₁ → γ₂ → γ₃ → γ₄ → γ₅ → α}
  {g₀ : β → γ₀} {g₁ : β → γ₁} {g₂ : β → γ₂} {g₃ : β → γ₃} {g₄ : β → γ₄} {g₅ : β → γ₅}
  (hf : f ∈ₑ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) (hg₃: g₃ ∈ₑ C) (hg₄: g₄ ∈ₑ C) (hg₅: g₅ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x) (g₃ x) (g₄ x) (g₅ x)) ∈ₑ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂.pair $ hg₃.pair $ hg₄.pair $ hg₅

theorem mem_pred.comp
  {f : γ₀ → Prop}
  {g₀ : α → γ₀}
  (hf : f ∈ₚ C) (hg₀: g₀ ∈ₑ C) :
  (λ x, f (g₀ x)) ∈ₚ C :=
  hf.comp $ hg₀
theorem mem_pred.comp₂
  {f : γ₀ → γ₁ → Prop}
  {g₀ : α → γ₀} {g₁ : α → γ₁}
  (hf : f ∈ₚ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x)) ∈ₚ C :=
  hf.comp $ hg₀.pair $ hg₁
theorem mem_pred.comp₃
  {f : γ₀ → γ₁ → γ₂ → Prop}
  {g₀ : α → γ₀} {g₁ : α → γ₁} {g₂ : α → γ₂}
  (hf : f ∈ₚ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x)) ∈ₚ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂
theorem mem_pred.comp₄
  {f : γ₀ → γ₁ → γ₂ → γ₃ → Prop}
  {g₀ : α → γ₀} {g₁ : α → γ₁} {g₂ : α → γ₂} {g₃ : α → γ₃}
  (hf : f ∈ₚ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) (hg₃: g₃ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x) (g₃ x)) ∈ₚ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂.pair $ hg₃
theorem mem_pred.comp₅
  {f : γ₀ → γ₁ → γ₂ → γ₃ → γ₄ → Prop}
  {g₀ : α → γ₀} {g₁ : α → γ₁} {g₂ : α → γ₂} {g₃ : α → γ₃} {g₄ : α → γ₄}
  (hf : f ∈ₚ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) (hg₃: g₃ ∈ₑ C) (hg₄: g₄ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x) (g₃ x) (g₄ x)) ∈ₚ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂.pair $ hg₃.pair $ hg₄
theorem mem_pred.comp₆
  {f : γ₀ → γ₁ → γ₂ → γ₃ → γ₄ → γ₅ → Prop}
  {g₀ : α → γ₀} {g₁ : α → γ₁} {g₂ : α → γ₂} {g₃ : α → γ₃} {g₄ : α → γ₄} {g₅ : α → γ₅}
  (hf : f ∈ₚ C) (hg₀: g₀ ∈ₑ C) (hg₁: g₁ ∈ₑ C) (hg₂: g₂ ∈ₑ C) (hg₃: g₃ ∈ₑ C) (hg₄: g₄ ∈ₑ C) (hg₅: g₅ ∈ₑ C) :
  (λ x, f (g₀ x) (g₁ x) (g₂ x) (g₃ x) (g₄ x) (g₅ x)) ∈ₚ C :=
  hf.comp $ hg₀.pair $ hg₁.pair $ hg₂.pair $ hg₃.pair $ hg₄.pair $ hg₅
end comp

theorem mem.swap_args₂ {f : α → β → γ} : f ∈ₑ C ↔ (flip f) ∈ₑ C :=
by { split; intro h; exact h.comp₂ mem.snd mem.fst, }

end complexity_class

repo: circuits


text:
/-
Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Minchao Wu
-/
import order.bounded_order

/-!
# Lexicographic order

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

This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.

## Main declarations

* `prod.lex.<pre/partial_/linear_>order`: Instances lifting the orders on `α` and `β` to `α ×ₗ β`.

## Notation

* `α ×ₗ β`: `α × β` equipped with the lexicographic order

## See also

Related files are:
* `data.finset.colex`: Colexicographic order on finite sets.
* `data.list.lex`: Lexicographic order on lists.
* `data.pi.lex`: Lexicographic order on `Πₗ i, α i`.
* `data.psigma.order`: Lexicographic order on `Σ' i, α i`.
* `data.sigma.order`: Lexicographic order on `Σ i, α i`.
-/

variables {α β γ : Type*}

namespace prod.lex

notation α ` ×ₗ `:35 β:34 := lex (prod α β)

meta instance [has_to_format α] [has_to_format β] : has_to_format (α ×ₗ β) :=
prod.has_to_format

instance decidable_eq (α β : Type*) [decidable_eq α] [decidable_eq β] : decidable_eq (α ×ₗ β) :=
prod.decidable_eq

instance inhabited (α β : Type*) [inhabited α] [inhabited β] : inhabited (α ×ₗ β) :=
prod.inhabited

/-- Dictionary / lexicographic ordering on pairs.  -/
instance has_le (α β : Type*) [has_lt α] [has_le β] : has_le (α ×ₗ β) :=
{ le := prod.lex (<) (≤) }

instance has_lt (α β : Type*) [has_lt α] [has_lt β] : has_lt (α ×ₗ β) :=
{ lt := prod.lex (<) (<) }

lemma le_iff [has_lt α] [has_le β] (a b : α × β) :
  to_lex a ≤ to_lex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 ≤ b.2 := prod.lex_def (<) (≤)

lemma lt_iff [has_lt α] [has_lt β] (a b : α × β) :
  to_lex a < to_lex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 < b.2 := prod.lex_def (<) (<)

/-- Dictionary / lexicographic preorder for pairs. -/
instance preorder (α β : Type*) [preorder α] [preorder β] : preorder (α ×ₗ β) :=
{ le_refl := refl_of $ prod.lex _ _,
  le_trans := λ _ _ _, trans_of $ prod.lex _ _,
  lt_iff_le_not_le := λ x₁ x₂, match x₁, x₂ with
  | to_lex (a₁, b₁), to_lex (a₂, b₂) := begin
      split,
      { rintro (⟨_, _, hlt⟩ | ⟨_, hlt⟩),
        { split,
          { left, assumption },
          { rintro ⟨⟩,
            { apply lt_asymm hlt, assumption },
            { apply lt_irrefl _ hlt } } },
        { split,
          { right, rw lt_iff_le_not_le at hlt, exact hlt.1 },
          { rintro ⟨⟩,
            { apply lt_irrefl a₁, assumption },
            { rw lt_iff_le_not_le at hlt, apply hlt.2, assumption } } } },
      { rintros ⟨⟨⟩, h₂r⟩,
        { left, assumption },
        { right, rw lt_iff_le_not_le, split,
          { assumption },
          { intro h, apply h₂r, right, exact h } } }
    end
  end,
  .. prod.lex.has_le α β,
  .. prod.lex.has_lt α β }

section preorder
variables [partial_order α] [preorder β]

lemma to_lex_mono : monotone (to_lex : α × β → α ×ₗ β) :=
begin
  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨ha, hb⟩,
  obtain rfl | ha : a₁ = a₂ ∨ _ := ha.eq_or_lt,
  { exact right _ hb },
  { exact left _ _ ha }
end

lemma to_lex_strict_mono : strict_mono (to_lex : α × β → α ×ₗ β) :=
begin
  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h,
  obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt,
  { exact right _ (prod.mk_lt_mk_iff_right.1 h) },
  { exact left _ _ ha }
end

end preorder

/-- Dictionary / lexicographic partial_order for pairs. -/
instance partial_order (α β : Type*) [partial_order α] [partial_order β] : partial_order (α ×ₗ β) :=
{ le_antisymm := by
  { haveI : is_strict_order α (<) := { irrefl := lt_irrefl, trans := λ _ _ _, lt_trans },
    haveI : is_antisymm β (≤) := ⟨λ _ _, le_antisymm⟩,
    exact @antisymm _ (prod.lex _ _) _, },
  .. prod.lex.preorder α β }

/-- Dictionary / lexicographic linear_order for pairs. -/
instance linear_order (α β : Type*) [linear_order α] [linear_order β] : linear_order (α ×ₗ β) :=
{ le_total := total_of (prod.lex _ _),
  decidable_le := prod.lex.decidable _ _,
  decidable_lt := prod.lex.decidable _ _,
  decidable_eq := lex.decidable_eq _ _,
  .. prod.lex.partial_order α β }

instance order_bot [partial_order α] [preorder β] [order_bot α] [order_bot β] :
  order_bot (α ×ₗ β) :=
{ bot := to_lex ⊥,
  bot_le := λ a, to_lex_mono bot_le }

instance order_top [partial_order α] [preorder β] [order_top α] [order_top β] :
  order_top (α ×ₗ β) :=
{ top := to_lex ⊤,
  le_top := λ a, to_lex_mono le_top }

instance bounded_order [partial_order α] [preorder β] [bounded_order α] [bounded_order β] :
  bounded_order (α ×ₗ β) :=
{ ..lex.order_bot, ..lex.order_top }

instance [preorder α] [preorder β] [densely_ordered α] [densely_ordered β] :
  densely_ordered (α ×ₗ β) :=
⟨begin
  rintro _ _ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩),
  { obtain ⟨c, h₁, h₂⟩ := exists_between h,
    exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩ },
  { obtain ⟨c, h₁, h₂⟩ := exists_between h,
    exact ⟨(a, c), right _ h₁, right _ h₂⟩ }
end⟩

instance no_max_order_of_left [preorder α] [preorder β] [no_max_order α] : no_max_order (α ×ₗ β) :=
⟨by { rintro ⟨a, b⟩, obtain ⟨c, h⟩ := exists_gt a, exact ⟨⟨c, b⟩, left _ _ h⟩ }⟩

instance no_min_order_of_left [preorder α] [preorder β] [no_min_order α] : no_min_order (α ×ₗ β) :=
⟨by { rintro ⟨a, b⟩, obtain ⟨c, h⟩ := exists_lt a, exact ⟨⟨c, b⟩, left _ _ h⟩ }⟩

instance no_max_order_of_right [preorder α] [preorder β] [no_max_order β] : no_max_order (α ×ₗ β) :=
⟨by { rintro ⟨a, b⟩, obtain ⟨c, h⟩ := exists_gt b, exact ⟨⟨a, c⟩, right _ h⟩ }⟩

instance no_min_order_of_right [preorder α] [preorder β] [no_min_order β] : no_min_order (α ×ₗ β) :=
⟨by { rintro ⟨a, b⟩, obtain ⟨c, h⟩ := exists_lt b, exact ⟨⟨a, c⟩, right _ h⟩ }⟩

end prod.lex

author: leanprover-community

repo: mathlib


text:
section propositional

variables P Q R : Prop

------------------------------------------------
-- Proposições de dupla negaço:
------------------------------------------------

theorem doubleneg_intro :
  P → ¬¬P  :=
begin
  intro hp,
  intro hnp,
  contradiction,
end

theorem doubleneg_elim :
  ¬¬P → P  :=
begin
  intro hp,
  by_cases h : P,
  apply h,
  contradiction,
end

theorem doubleneg_law :
  ¬¬P ↔ P  :=
begin
  split,
  intro hnnp,
  by_cases hp : P,
  apply hp,
  contradiction,
  intro hp,
  intro hnp,
  contradiction,
end

------------------------------------------------
-- Comutatividade dos ∨,∧:
------------------------------------------------

theorem disj_comm :
  (P ∨ Q) → (Q ∨ P)  :=
begin
  intro hqp,
  cases hqp with hp hq,
  right,
  apply hp,
  left,
  apply hq,
end

theorem conj_comm :
  (P ∧ Q) → (Q ∧ P)  :=
begin
  intro hpq,
  cases hpq with hp hq,
  split,
  apply hq,
  apply hp,
end

------------------------------------------------
-- Proposições de interdefinabilidade dos →,∨:
------------------------------------------------

theorem impl_as_disj_converse :
  (¬P ∨ Q) → (P → Q)  :=
begin
  intro hnpq,
  intro hp,
  cases hnpq with hnp hq,
  contradiction,
  apply hq,
end

theorem disj_as_impl :
  (P ∨ Q) → (¬P → Q)  :=
begin
  intro hpq,
  intro hnp,
  cases hpq with hp hq,
  contradiction,
  apply hq,
end

------------------------------------------------
-- Proposições de contraposição:
------------------------------------------------

theorem impl_as_contrapositive :
  (P → Q) → (¬Q → ¬P)  :=
begin
  intro hpq,
  intro hnq,
  intro hp,
  have hq : Q := hpq hp,
  contradiction,
end

theorem impl_as_contrapositive_converse :
  (¬Q → ¬P) → (P → Q)  :=
begin
  intro hnqnp,
  intro hp,
  by_cases hlq : Q,
  apply hlq,
  have hnp : ¬P := hnqnp hlq,
  contradiction,
end

theorem contrapositive_law :
  (P → Q) ↔ (¬Q → ¬P)  :=
begin
  split,
  exact impl_as_contrapositive P Q,
  exact impl_as_contrapositive_converse P Q,
end

------------------------------------------------
-- A irrefutabilidade do LEM:
------------------------------------------------

theorem lem_irrefutable :
  ¬¬(P∨¬P)  :=
begin
  intro hnpp,
  apply hnpp,
  right,
  intro hp,
  apply hnpp,
  left,
  apply hp,
end

------------------------------------------------
-- A lei de Peirce
------------------------------------------------

theorem peirce_law_weak :
  ((P → Q) → P) → ¬¬P  :=
begin
  intros hpqp hp,
  by_cases hlp : P,
  contradiction,
  apply hlp,

end

------------------------------------------------
-- Proposições de interdefinabilidade dos ∨,∧:
------------------------------------------------

theorem disj_as_negconj :
  P∨Q → ¬(¬P∧¬Q)  :=
begin
  intros hpq hnpq,
  cases hpq with hp hq,
  cases hnpq,
  contradiction,
  cases hnpq,
  contradiction,
end

theorem conj_as_negdisj :
  P∧Q → ¬(¬P∨¬Q)  :=
begin
  intros hpq hnpq,
  cases hnpq with hp hq,
  cases hpq,
  contradiction,
  cases hpq,
  contradiction,
end

------------------------------------------------
-- As leis de De Morgan para ∨,∧:
------------------------------------------------

theorem demorgan_disj :
  ¬(P∨Q) → (¬P ∧ ¬Q)  :=
begin
  intro hnpq,
  split,
  intro hp,
  apply hnpq,
  left,
  apply hp,
  intro hq,
  apply hnpq,
  right,
  apply hq,
end

theorem demorgan_disj_converse :
  (¬P ∧ ¬Q) → ¬(P∨Q)  :=
begin
  intros hnpnq hpq,
  cases hpq with hp hq,
  cases hnpnq,
    contradiction,
  cases hnpnq,
    contradiction,
end

theorem demorgan_conj :
  ¬(P∧Q) → (¬Q ∨ ¬P)  :=
begin
 intro hnpq,
  by_cases hlq: Q,
    --- lem Q
    right,
    intro hp,
    have himpl_pq : P∧Q,
      split,
      exact hp,
      exact hlq,
    apply hnpq,
    exact himpl_pq,
    left,
    exact hlq,
end

theorem demorgan_conj_converse :
  (¬Q ∨ ¬P) → ¬(P∧Q)  :=
begin
  intros hnqnp hpq,
  cases hpq,
  cases hnqnp,
    -- case ¬Q
    contradiction,
    -- Case ¬P
    contradiction,
end

theorem demorgan_conj_law :
  ¬(P∧Q) ↔ (¬Q ∨ ¬P)  :=
begin
  split,
  exact demorgan_conj P Q,
  exact demorgan_conj_converse P Q,
end

theorem demorgan_disj_law :
  ¬(P∨Q) ↔ (¬P ∧ ¬Q)  :=
begin
  split,
  exact demorgan_disj P Q,
  exact demorgan_disj_converse P Q,
end

------------------------------------------------
-- Proposições de distributividade dos ∨,∧:
------------------------------------------------

theorem distr_conj_disj :
  P∧(Q∨R) → (P∧Q)∨(P∧R)  :=
begin
  intro hp_and_qr,
  cases hp_and_qr,
  cases hp_and_qr_right with hq hr,
  left,
  split,
  assumption',
  right,
  split,
  assumption',
end

theorem distr_conj_disj_converse :
  (P∧Q)∨(P∧R) → P∧(Q∨R)  :=
begin
  intro hpq_or_pr,
  cases hpq_or_pr with hpq hpr,
  split,
  cases hpq,
  assumption,
  cases hpq,
  left,
  assumption,
  split,
  cases hpr,
  assumption,
  cases hpr,
  right,
  assumption,
end

theorem distr_disj_conj :
  P∨(Q∧R) → (P∨Q)∧(P∨R)  :=
begin
  intro hpqr,
  -- split,
  cases hpqr,
  split,
  left,
  assumption,
  left,
  assumption,
  cases hpqr,
  split,
  right,
  assumption,
  right,
  assumption,
end

theorem distr_disj_conj_converse :
  (P∨Q)∧(P∨R) → P∨(Q∧R)  :=
begin
  intro hpq_pr,
  cases hpq_pr,
  cases hpq_pr_left,
  left,
  assumption,
  cases hpq_pr_right,
  left,
  assumption,
  right,
  split,
  assumption',
end

------------------------------------------------
-- Currificação
------------------------------------------------

theorem curry_prop :
  ((P∧Q)→R) → (P→(Q→R))  :=
begin
  intros hpq_impl_r hp hq,
  apply hpq_impl_r,
  split,
  assumption',
end

theorem uncurry_prop :
  (P→(Q→R)) → ((P∧Q)→R)  :=
begin
  intros hp_q_r hpq,
  cases hpq,
  apply hp_q_r,
  assumption',
end

------------------------------------------------
-- Reflexividade da →:
------------------------------------------------

theorem impl_refl :
  P → P  :=
begin
  intro hp,
  assumption,
end

------------------------------------------------
-- Weakening and contraction:
------------------------------------------------

theorem weaken_disj_right :
  P → (P∨Q)  :=
begin
  intro hp,
  left,
  exact hp,
end

theorem weaken_disj_left :
  Q → (P∨Q)  :=
begin
  intro hq,
  right,
  exact hq,
end

theorem weaken_conj_right :
  (P∧Q) → P  :=
begin
  intro hpq,
  cases hpq,
  exact hpq_left,
end

theorem weaken_conj_left :
  (P∧Q) → Q  :=
begin
  intro hpq,
  cases hpq,
  exact hpq_right,
end

theorem conj_idempot :
  (P∧P) ↔ P :=
begin
  split,
  intro hpp,
  cases hpp,
  assumption,
  intro hp,
  split,
  assumption,
  assumption,
end

theorem disj_idempot :
  (P∨P) ↔ P  :=
begin
  split,
  intro hp_or_p,
  cases hp_or_p,
  assumption,
  assumption,
  intro hp,
  left,
  assumption,
end

end propositional

----------------------------------------------------------------

section predicate

variable U : Type
variables P Q : U -> Prop

------------------------------------------------
-- As leis de De Morgan para ∃,∀:
------------------------------------------------

theorem demorgan_exists :
  ¬(∃x, P x) → (∀x, ¬P x)  :=
begin
  intro hn_e_p,
  intros x hxp,
  apply hn_e_p,
  existsi x,
  assumption,
end

theorem demorgan_exists_converse :
  (∀x, ¬P x) → ¬(∃x, P x)  :=
begin
  intro htqx,
  intro hex,
  cases hex with x hpx,
  exact htqx x hpx,
end

theorem demorgan_forall :
  ¬(∀x, P x) → (∃x, ¬P x)  :=
begin
  intro hnptx,

end

theorem demorgan_forall_converse :
  (∃x, ¬P x) → ¬(∀x, P x)  :=
begin
  intro hexnp,
  intro htx,
  cases hexnp with hx hnp,
  -- htx x,
end

theorem demorgan_forall_law :
  ¬(∀x, P x) ↔ (∃x, ¬P x)  :=
begin
  sorry,
end

theorem demorgan_exists_law :
  ¬(∃x, P x) ↔ (∀x, ¬P x)  :=
begin
  sorry,
end

------------------------------------------------
-- Proposições de interdefinabilidade dos ∃,∀:
------------------------------------------------

theorem exists_as_neg_forall :
  (∃x, P x) → ¬(∀x, ¬P x)  :=
begin
  sorry,
end

theorem forall_as_neg_exists :
  (∀x, P x) → ¬(∃x, ¬P x)  :=
begin
  sorry,
end

theorem forall_as_neg_exists_converse :
  ¬(∃x, ¬P x) → (∀x, P x)  :=
begin
  sorry,
end

theorem exists_as_neg_forall_converse :
  ¬(∀x, ¬P x) → (∃x, P x)  :=
begin
  sorry,
end

theorem forall_as_neg_exists_law :
  (∀x, P x) ↔ ¬(∃x, ¬P x)  :=
begin
  sorry,
end

theorem exists_as_neg_forall_law :
  (∃x, P x) ↔ ¬(∀x, ¬P x)  :=
begin
  sorry,
end

------------------------------------------------
--  Proposições de distributividade de quantificadores:
------------------------------------------------

theorem exists_conj_as_conj_exists :
  (∃x, P x ∧ Q x) → (∃x, P x) ∧ (∃x, Q x)  :=
begin
  sorry,
end

theorem exists_disj_as_disj_exists :
  (∃x, P x ∨ Q x) → (∃x, P x) ∨ (∃x, Q x)  :=
begin
  sorry,
end

theorem exists_disj_as_disj_exists_converse :
  (∃x, P x) ∨ (∃x, Q x) → (∃x, P x ∨ Q x)  :=
begin
  sorry,
end

theorem forall_conj_as_conj_forall :
  (∀x, P x ∧ Q x) → (∀x, P x) ∧ (∀x, Q x)  :=
begin
  sorry,
end

theorem forall_conj_as_conj_forall_converse :
  (∀x, P x) ∧ (∀x, Q x) → (∀x, P x ∧ Q x)  :=
begin
  sorry,
end

theorem forall_disj_as_disj_forall_converse :
  (∀x, P x) ∨ (∀x, Q x) → (∀x, P x ∨ Q x)  :=
begin
  sorry,
end

/- NOT THEOREMS --------------------------------

theorem forall_disj_as_disj_forall :
  (∀x, P x ∨ Q x) → (∀x, P x) ∨ (∀x, Q x)  :=
begin
end

theorem exists_conj_as_conj_exists_converse :
  (∃x, P x) ∧ (∃x, Q x) → (∃x, P x ∧ Q x)  :=
begin
end

---------------------------------------------- -/

end predicate

author: caiorebert

repo: fmclean

save_path: github-repos/lean/caiorebert-fmclean


text:
/-
Copyright (c) 2021 Yaël Dillies, Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies, Bhavik Mehta
-/
import analysis.convex.topology
import topology.sequences

lemma interior_eq_closure_diff_frontier {X : Type _} [topological_space X] (s : set X) :
  interior s = closure s \ frontier s :=
by rw [frontier, set.diff_diff_right, set.diff_self, set.empty_union,
       set.inter_eq_self_of_subset_right interior_subset_closure]

author: mmasdeu

repo: brouwerfixedpoint