text:
import tactic.suggest
import tactic.simps

/-
In this project I will work on formalizing Donald Knuth's lovely classic Surreal Numbers.

My strategy for the formalization will be to define the initial rules as axioms, without proving
that they are consistent with Lean's axiomatic foundations. This is not how Lean is supposed to be
used, it is generally frowned upon to use axioms since it can be quite easy to introduce
contradictions and invalidate the whole theory. It is "unsafe", but I have my reasons for it.

I've already spent many hours getting an understanding of mathlib's definition of surreal numbers,
on attempting (and failing) to find a simpler alternative definition, and to prove the initial rules
on mathlib's surreals.

All of this has been proven to be surprisingly hard, too damn hard for my introductory understanding
of Lean. Mathlib's proof library on surreal is itself very limited, and proving multiplication
is an ongoing effort and it sounds like it's becoming into a huge project. Surreals just seem
to clash with Lean's fundamental design, and people way more experienced that me are already
struggling with it. Indeed, I keep seeing indirect comments implying Conway's theory of games (with
surreals within) is perhaps still not formally linked to set theory and wider maths, not sure.

I tried using mathlib's definition to prove the initial rules, so that then I could build on it
without going into implementation details. But mathlib doesn't even have a simple operation to get
the left and right sets for a surreal, so I cannot even express the first rule cleanly to prove it.

Discussion with the community about it:
https://leanprover-community.github.io/archive/stream/113489-new-members/topic/defining.20surreal.20numbers.html

Turns out someone else was also trying to do the exact same thing:
https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/Surreal.20numbers.html

This was always intended to be a nice chill introductory learning experience, I don't really care
about being too formal, which is also in the spirit of Knuth's book. Every time I try to tie surreals to existing Lean constructs it instead becomes a nightmare of fighting against extremely
advanced and obscure Lean features. I'll just prove all of this as an isolated island, and we can
leave it for later to think about proving that it is consistent with the fundamental axioms, in
other words, that surreal numbers indeed "exist".
-/

/-
These are the two rules that define surreal numbers in the book:

> **Rule 1**: Every number corresponds to two sets of previously created numbers, such that no member of the left is greater than or equal to any member of the right set.

> **Rule 2**: One number is less than or equal to another number if and only if no member of the first number's left set is greater than or equal to the second number, and no member of the second number's right set is less than or equal to the first number.

First we define an empty type to represent surreals.

You may think that it would make more sense to create a struct with two sets. Go ahead, try. As it
can be seen in the discussion I linked to above, this is black-hole. Lean can't handle this type
of recursive struct, and even if you define it as an inductive type, it apparently contradicts
Cantor's Theorem (which I still don't fully understand, but fair enough).

https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/Surreal.20numbers.html#214704929

The fact that it violates Cantor may bite me in the ass down the line, perhaps my axioms are
not sound. But, honestly, I don't really care, this is supposed to be some light fun to learn Lean.
-/

constant surreal: Type

namespace surreal

/-
Similarly, we define two empty functions to represent the operations for extracting the two sets
that constitute a surreal number. They are both the same, the distinction between the two sets
is merely symbolic and will only take on meaning through their usage in the axioms below.
-/

constant left: surreal → set surreal
constant right: surreal → set surreal

/-
We will need a ≥ and ≤ operation to define the initial axioms. ≥ comes for free if we define ≤ with Lean's standard type class `has_le`.

Again, we define it as an empty function, just saying that such a function exists.

Indeed, one of the core challenges of defining surreals in Lean seems to be the requirement for
having to define the type simultaneously with its ordering. This is hard, and can only be done by
bootstrapping the type with a lower-level more general type with defined ordering, but that is still
quite a challenge.
-/

constant le: surreal → surreal → Prop
noncomputable instance : has_le surreal := ⟨le⟩

/-
> **Rule 1**: Every number corresponds to two sets of previously created numbers, such that no member of the left is greater than or equal to any member of the right set.
-/

def valid (L R: set surreal): Prop :=
  ¬∃ l ∈ L, ∃ r ∈ R, l ≥ r
axiom rule_1 (x: surreal): valid x.left x.right

/-
> **Rule 2**: One number is less than or equal to another number if and only if no member of the first number's left set is greater than or equal to the second number, and no member of the second
number's right set is less than or equal to the first number.
-/

axiom rule_2 (x y: surreal):
  x ≤ y ↔
    (¬∃ xl ∈ x.left, xl ≥ y) ∧
    (¬∃ yr ∈ y.right, yr ≤ x)

/-
> And the first number was created from the void left set and the void right set. Conway called this
number "zero", and said that it shall be a sign to separate positive numbers from negative numbers.

This is the first number we define, so I'd like to note a subtle design decision regarding how they are represented.

If you look carefully, there's nothing forcing us to prove that `zero` is `valid` (as in `rule_1`). In fact, we already claim it is `valid` when we say its type is `surreal`.

Again, all my attempts to include a proof for `valid` as part of the `surreal` type have failed
after several hours-long sessions of unpleasant head-wall-hitting. A structure, an inductive type, a type class... It all looks like it should be easy a-priori, but the recursive nature of the type makes everything really hard. You can't easily define a type that requires a proof that all its subelements of the same type fullfil a certain criteria, because, well, the type is not defined yet so you can't really talk about it.

And, from a different perspective, you cannot really prove that a surreal is valid, because we have
no concept of a non-valid surreal. What about its internal surreals? Would those be valid or not?
It just becomes a mess. Surreals are valid by definition, its an axiom.

When we name a specific surreal number, like `zero` here, and we describe the contets of its two
sets, we do it to our own risk. Lean allows us to define non-valid surreals, and it will think they
are valid, which will introduce a contradiction and break things. It is fairly obvious for `zero`
to see that it is valid, but we need to be careful moving forward.

As a compromise, I've isolated `valid` above (from `rule_1`) and I will prove it for every
specific surreal number I define. Again, Lean doesn't enforce this, but it is a handy convention
to avoid intorducing footguns.
-/

constant zero: surreal
axiom zero.has_left: zero.left = ∅
axiom zero.has_right: zero.right = ∅
lemma zero.is_valid: valid zero.left zero.right :=
begin
  rw [valid, zero.has_left, zero.has_right],
  rw not_bex,
  intros l hl,
  rw not_bex,
  intros r hr,
  intro hge,
  exact hl,
end

/-
> On the next day, two more numbers were created, one with zero as its left set and one with zero as
its right set. And Conway called the former number "one", and the latter he called "minus one".
-/

constant one: surreal
axiom one.has_left: one.left = {zero}
axiom one.has_right: one.right = ∅
lemma one.is_valid: valid one.left one.right :=
begin
  rw [valid, one.has_left, one.has_right],
  rw not_bex, intros l hl,
  rw not_bex, intros r hr,
  intro hge,
  exact hr,
end

constant minus_one: surreal
axiom minus_one.has_left: minus_one.left = ∅
axiom minus_one.has_right: minus_one.right = {zero}
lemma minus_one.is_valid: valid minus_one.left minus_one.right :=
begin
  rw [valid, minus_one.has_left, minus_one.has_right],
  rw not_bex, intros l hl,
  rw not_bex, intros r hr,
  intro hge,
  exact hl,
end

/-
> Conway proved that zero was less than or equal to zero
> And he proved that minus one is less than but not equal to zero and zero is less than but not equal to one.

Proofs for these are discussed in `chapter_3`, so let's wait until then.
-/

end surreal

author: oersted

repo: lean-surreal-numbers


text:
/-
Homeowork 11
Sina Hazratpour
Introduction to Proof
MATH 301, Johns Hopkins University, Fall 2022
-/

import ..prooflab
import lectures.lec10_surj_inj_fact
import lectures.lec14_inductive_naturals
import homework.hw10

open PROOFS
open PROOFS.STR

/-
Note that the code below is not wrapped by the namespace `mat`, so if you want to use a definition or lemma/theorem named `xyz` from lec14 you need to append `mat` to its name and use it as `mat.xyz`.
-/

/-! ## Question 1 (20 pts) :
Prove the following results using `cases` or `induction`.
-/

lemma mat.zero_of_add_eq_zero (m n : mat) :
  m + n = 0  → (m = 0) ∧ (n = 0) :=
begin
 sorry,
end

lemma mat.zero_of_mul_eq_zero (m n : mat) :
  m * n = 0  → (m = 0) ∨ (n = 0) :=
begin
  sorry,
end

/-! ## Question 2 (20 pts) :
Prove the following distributivity result and then use them to prove lemma `mat.two_mul` (a proof of `mat.two_mul` which does not use distributivity lemmas is also accepted).
-/

lemma mat.mul_add_distrib (k m n : mat) :
  k * (m + n) = k * m + k * n :=
begin
  sorry,
end
#check nat.left_distrib

lemma mat.add_mul_distrib (m n s : mat) :
  (m + n) * s = m  * s + n * s :=
begin
  sorry,
end

lemma mat.two_mul (m : mat) :
  2 * m = m + m :=
begin
  sorry,
end

/-! ## Question 3 (20 pts) :
In this exercise you will prove that for any natural number `n`,
`2 * (1 + ... + n) = n * (n + 1)`
which is allegedly proved by Gauss in the 18th century when he was a primary school student. https://nrich.maths.org/2478
-/

#check mat.sum_up_to --defined in the lecture

/- To prove this statement we need to prove an additional lemma to the repository of lemmas proved about `mat` in lecture 14.  -/

theorem sum_up_to_closed_formula :
  ∀ n : mat, 2 * (mat.sum_up_to n) = n * (n + 1) :=
begin
  sorry,
end

/-! ## Question 4 (20 pts)-/

variables {X Y : Type}

def has_retract (f : X → Y) : Prop :=
∃ r : Y → X, r ∘ f = id

lemma retract_inj {f : X → Y} :
  has_retract f → is_injective f :=
begin
  sorry,
end

/-
Use the lemma `has_retract` above to prove that the function `mat.succ` is injective.
-/

#check mat.succ

lemma inj_succ :
  is_injective mat.succ :=
begin
 sorry,
end

/-! ## Question 5 (20 pts)
Give a different proof that `mat.succ` is injective by filling in `sorry` placeholder below.
-/

@[simp]
def diagonal : mat → mat → Prop
| (mat.succ m) (mat.succ n) := (m = n)
| _     _     := true

lemma succ_inj (m n : mat) (h₁ : mat.succ m = mat.succ n) :
  m = n :=
begin
  have h₂ : (mat.succ m = mat.succ n) → diagonal (mat.succ m) (mat.succ n), sorry,
  have h₃ : diagonal (mat.succ m) (mat.succ n), sorry,
  have h₄ : m = n, by sorry,
  sorry,
end

/-! ## Question 6 (20 pts)
Equip `mat` with the structure of a preorder by completing the following instance where the `≤` relation is defined as in below:
-/

def mat.le (m n : mat) : Prop := ∃ k, m + k = n

--#check mat.le

lemma add_cancel {k m n : mat} :
  (k + m = k + n) → m = n :=
begin
  intro h,
  -- want to prove m = n,
  induction k with d ihd,
  {
    sorry,
  },
  {
    sorry,
  },

end

/-
Prove that ≤ relation
-/
lemma mat.le_antisymm (m n : mat) :
  (mat.le m n) → (mat.le n m) → m = n :=
begin
  intros h₁ h₂,
  obtain ⟨k, hk⟩ := h₁,
  obtain ⟨l, hl⟩ := h₂,
  sorry,
end

/-! ## Question 7 (20 pts)
Equip `mat` with the structure of a preorder by completing the following instance where the `≤` relation is defined as in below:
-/

instance additive_preorder_mat : preorder mat :=
{
  le := mat.le,
  lt := sorry,
  le_refl := sorry,
  le_trans := sorry,
  lt_iff_le_not_le := sorry,
}

#reduce additive_preorder_mat.le

/-! ## Question 8 (20 pts)
We define __exponentiation__ for the type `mat`. Then you should prove that all powers of a positive number are positive.
-/

def mat.power : mat → mat → mat
| m 0        := 1
| m (n + 1)  := (mat.power m n) * m

example :
  mat.power 4 3 = 64 :=
begin
  refl,
end

postfix ` ^^ `:15  := mat.power

example : 0 ^^ 31 = 0 :=
begin
  refl,
end

@[simp]
lemma power_succ {a n : mat} :
  a ^^  n.succ = (a ^^ n)  * a :=
begin
  refl,
end

-- Use induction on natural numbers to prove the following theorem. You may need to prove an extra lemma before that which states that the multiplication of two positive numbers  `a b : mat` is again positive (`a` is positive here means that `0 < a` which is inherited from the type class `preorder` and the fact that we gave an instance of preorder structure for type `mat`. ).
theorem pos_of_power_of_pos (a : mat) :
  ∀ n : mat, (0 < a) → (0 < (a^^n)) :=
begin
  sorry,
end

author: sinhp

repo: ProofLab

save_path: github-repos/lean/sinhp-ProofLab


text:
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import order.antichain
import order.upper_lower.basic

/-!
# Minimal/maximal elements of a set

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

This file defines minimal and maximal of a set with respect to an arbitrary relation.

## Main declarations

* `maximals r s`: Maximal elements of `s` with respect to `r`.
* `minimals r s`: Minimal elements of `s` with respect to `r`.

## TODO

Do we need a `finset` version?
-/

open function set

variables {α : Type*} (r r₁ r₂ : α → α → Prop) (s t : set α) (a b : α)

/-- Turns a set into an antichain by keeping only the "maximal" elements. -/
def maximals : set α := {a ∈ s | ∀ ⦃b⦄, b ∈ s → r a b → r b a}

/-- Turns a set into an antichain by keeping only the "minimal" elements. -/
def minimals : set α := {a ∈ s | ∀ ⦃b⦄, b ∈ s → r b a → r a b}

lemma maximals_subset : maximals r s ⊆ s := sep_subset _ _
lemma minimals_subset : minimals r s ⊆ s := sep_subset _ _

@[simp] lemma maximals_empty : maximals r ∅ = ∅ := sep_empty _
@[simp] lemma minimals_empty : minimals r ∅ = ∅ := sep_empty _

@[simp] lemma maximals_singleton : maximals r {a} = {a} :=
(maximals_subset _ _).antisymm $ singleton_subset_iff.2 $
  ⟨rfl, by { rintro b (rfl : b = a), exact id }⟩

@[simp] lemma minimals_singleton : minimals r {a} = {a} := maximals_singleton _ _

lemma maximals_swap : maximals (swap r) s = minimals r s := rfl
lemma minimals_swap : minimals (swap r) s = maximals r s := rfl

section is_antisymm
variables {r s t a b} [is_antisymm α r]

lemma eq_of_mem_maximals (ha : a ∈ maximals r s) (hb : b ∈ s) (h : r a b) : a = b :=
antisymm h $ ha.2 hb h

lemma eq_of_mem_minimals (ha : a ∈ minimals r s) (hb : b ∈ s) (h : r b a) : a = b :=
antisymm (ha.2 hb h) h

variables (r s)

lemma maximals_antichain : is_antichain r (maximals r s) :=
λ a ha b hb hab h, hab $ eq_of_mem_maximals ha hb.1 h

lemma minimals_antichain : is_antichain r (minimals r s) :=
by { haveI := is_antisymm.swap r, exact (maximals_antichain _ _).swap }

end is_antisymm

lemma maximals_eq_minimals [is_symm α r] : maximals r s = minimals r s :=
by { congr, ext a b, exact comm }

variables {r r₁ r₂ s t a}

lemma set.subsingleton.maximals_eq (h : s.subsingleton) : maximals r s = s :=
h.induction_on (minimals_empty _) (maximals_singleton _)

lemma set.subsingleton.minimals_eq (h : s.subsingleton) : minimals r s = s := h.maximals_eq

lemma maximals_mono [is_antisymm α r₂] (h : ∀ a b, r₁ a b → r₂ a b) :
  maximals r₂ s ⊆ maximals r₁ s :=
λ a ha, ⟨ha.1, λ b hb hab,
  by { have := eq_of_mem_maximals ha hb (h _ _ hab), subst this, exact hab }⟩

lemma minimals_mono [is_antisymm α r₂] (h : ∀ a b, r₁ a b → r₂ a b) :
  minimals r₂ s ⊆ minimals r₁ s :=
λ a ha, ⟨ha.1, λ b hb hab,
  by { have := eq_of_mem_minimals ha hb (h _ _ hab), subst this, exact hab }⟩

lemma maximals_union : maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t :=
begin
  intros a ha,
  obtain h | h := ha.1,
  { exact or.inl ⟨h, λ b hb, ha.2 $ or.inl hb⟩ },
  { exact or.inr ⟨h, λ b hb, ha.2 $ or.inr hb⟩ }
end

lemma minimals_union : minimals r (s ∪ t) ⊆ minimals r s ∪ minimals r t := maximals_union

lemma maximals_inter_subset : maximals r s ∩ t ⊆ maximals r (s ∩ t) :=
λ a ha, ⟨⟨ha.1.1, ha.2⟩, λ b hb, ha.1.2 hb.1⟩

lemma minimals_inter_subset : minimals r s ∩ t ⊆ minimals r (s ∩ t) := maximals_inter_subset

lemma inter_maximals_subset : s ∩ maximals r t ⊆ maximals r (s ∩ t) :=
λ a ha, ⟨⟨ha.1, ha.2.1⟩, λ b hb, ha.2.2 hb.2⟩

lemma inter_minimals_subset : s ∩ minimals r t ⊆ minimals r (s ∩ t) := inter_maximals_subset

lemma _root_.is_antichain.maximals_eq (h : is_antichain r s) : maximals r s = s :=
(maximals_subset _ _).antisymm $ λ a ha, ⟨ha, λ b hb hab,
  by { have := h.eq ha hb hab, subst this, exact hab }⟩

lemma _root_.is_antichain.minimals_eq (h : is_antichain r s) : minimals r s = s :=
(minimals_subset _ _).antisymm $ λ a ha, ⟨ha, λ b hb hab,
  by { have := h.eq hb ha hab, subst this, exact hab }⟩

@[simp] lemma maximals_idem : maximals r (maximals r s) = maximals r s :=
(maximals_subset _ _).antisymm $ λ a ha, ⟨ha, λ b hb, ha.2 hb.1⟩

@[simp] lemma minimals_idem : minimals r (minimals r s) = minimals r s := maximals_idem

/-- If `maximals r s` is included in but *shadows* the antichain `t`, then it is actually
equal to `t`. -/
lemma is_antichain.max_maximals (ht : is_antichain r t) (h : maximals r s ⊆ t)
  (hs : ∀ ⦃a⦄, a ∈ t → ∃ b ∈ maximals r s, r b a) :
  maximals r s = t :=
begin
  refine h.antisymm (λ a ha, _),
  obtain ⟨b, hb, hr⟩ := hs ha,
  rwa of_not_not (λ hab, ht (h hb) ha (ne.symm hab) hr),
end

/-- If `minimals r s` is included in but *shadows* the antichain `t`, then it is actually
equal to `t`. -/
lemma is_antichain.max_minimals (ht : is_antichain r t) (h : minimals r s ⊆ t)
  (hs : ∀ ⦃a⦄, a ∈ t → ∃ b ∈ minimals r s, r a b) :
  minimals r s = t :=
begin
  refine h.antisymm (λ a ha, _),
  obtain ⟨b, hb, hr⟩ := hs ha,
  rwa of_not_not (λ hab, ht ha (h hb) hab hr),
end

variables [partial_order α]

lemma is_least.mem_minimals (h : is_least s a) : a ∈ minimals (≤) s := ⟨h.1, λ b hb _, h.2 hb⟩
lemma is_greatest.mem_maximals (h : is_greatest s a) : a ∈ maximals (≤) s := ⟨h.1, λ b hb _, h.2 hb⟩

lemma is_least.minimals_eq (h : is_least s a) : minimals (≤) s = {a} :=
eq_singleton_iff_unique_mem.2 ⟨h.mem_minimals, λ b hb, eq_of_mem_minimals hb h.1 $ h.2 hb.1⟩

lemma is_greatest.maximals_eq (h : is_greatest s a) : maximals (≤) s = {a} :=
eq_singleton_iff_unique_mem.2 ⟨h.mem_maximals, λ b hb, eq_of_mem_maximals hb h.1 $ h.2 hb.1⟩

lemma is_antichain.minimals_upper_closure (hs : is_antichain (≤) s) :
  minimals (≤) (upper_closure s : set α) = s :=
hs.max_minimals (λ a ⟨⟨b, hb, hba⟩, h⟩, by rwa eq_of_mem_minimals ‹a ∈ _› (subset_upper_closure hb)
  hba) $ λ a ha, ⟨a, ⟨subset_upper_closure ha, λ b ⟨c, hc, hcb⟩ hba,
    by rwa hs.eq' ha hc (hcb.trans hba)⟩, le_rfl⟩

lemma is_antichain.maximals_lower_closure (hs : is_antichain (≤) s) :
  maximals (≤) (lower_closure s : set α) = s :=
hs.to_dual.minimals_upper_closure

author: leanprover-community

repo: mathlib


text:
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.tactic init.function

namespace tactic

open expr tactic decidable environment

private meta def contra_p_not_p : list expr → list expr → tactic unit
| []         Hs := failed
| (H1 :: Rs) Hs :=
  do t ← (extract_opt_auto_param <$> infer_type H1) >>= whnf,
     (do a   ← match_not t,
         H2  ← find_same_type a Hs,
         tgt ← target,
         pr  ← mk_app `absurd [tgt, H2, H1],
         exact pr)
     <|> contra_p_not_p Rs Hs

private meta def contra_false : list expr → tactic unit
| []        := failed
| (H :: Hs) :=
  do t ← extract_opt_auto_param <$> infer_type H,
     if is_false t
     then do tgt ← target,
             pr  ← mk_app `false.rec [tgt, H],
             exact pr
     else contra_false Hs

private meta def contra_not_a_refl_rel_a : list expr → tactic unit
| []        := failed
| (H :: Hs) :=
  do t ← (extract_opt_auto_param <$> infer_type H) >>= head_beta,
     (do (lhs, rhs) ← match_ne t,
         unify lhs rhs,
         tgt ← target,
         refl_pr ← mk_app `eq.refl [lhs],
         mk_app `absurd [tgt, refl_pr, H] >>= exact)
     <|>
     (do p ← match_not t,
         (refl_lemma, lhs, rhs) ← match_refl_app p,
         unify lhs rhs,
         tgt ← target,
         refl_pr ← mk_app refl_lemma [lhs],
         mk_app `absurd [tgt, refl_pr, H] >>= exact)
     <|>
     contra_not_a_refl_rel_a Hs

private meta def contra_constructor_eq : list expr → tactic unit
| []        := failed
| (H :: Hs) :=
  do t ← (extract_opt_auto_param <$> infer_type H) >>= whnf,
     match t with
     | `((%%lhs_0 : %%α) = %%rhs_0) :=
       do env ← get_env,
          lhs ← whnf lhs_0,
          rhs ← whnf rhs_0,
          if is_constructor_app env lhs ∧
             is_constructor_app env rhs ∧
             const_name (get_app_fn lhs) ≠ const_name (get_app_fn rhs)
          then do tgt    ← target,
                  I_name ← return $ name.get_prefix (const_name (get_app_fn lhs)),
                  pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, H],
                  exact pr
          else contra_constructor_eq Hs
     | _ := contra_constructor_eq Hs
     end

meta def contradiction : tactic unit :=
do try intro1,
   ctx ← local_context,
   (contra_false ctx <|>
    contra_not_a_refl_rel_a ctx <|>
    contra_p_not_p ctx ctx <|>
    contra_constructor_eq ctx <|>
    fail "contradiction tactic failed")

meta def exfalso : tactic unit :=
do fail_if_no_goals,
   assert `Hfalse (expr.const `false []),
   swap, contradiction

end tactic

author: subfish-zhou


text:
/- Tactic : have

## Summary

`have h : P,` will create a new goal of creating a term of type `P`,
and will add `h : P` to the hypotheses for the goal you were working on.

## Details

If you want to name a term of some type (because you want it
in your local context for some reason), and if you have the
formula for the term, you can use `have` to give the term a name.

## Example (`have q := ...` or `have q : Q := ...`)

If the local context contains
```
f : P → Q
p : P
```

then the tactic `have q := f(p),` will add `q` to our local context,
leaving it like this:

```
f : P → Q
p : P
q : Q
```

If you think about it, you don't ever really need `q`, because whenever you
think you need it you coudl just use `f(p)` instead. But it's good that
we can introduce convenient notation like this.

## Example (`have q : Q,`)

A variant of this tactic can be used where you just declare the
type of the term you want to have, finish the tactic statement with
a comma and no `:=`, and then Lean just adds it as a new goal.
The number of goals goes up by one if you use `have` like this.

For example if the local context is
```
P Q R : Prop/Type,
f : P → Q,
g : Q → R,
p : P
⊢ R
```

then after `have q : Q,`, there will be the new goal
```
f : P → Q,
g : Q → R,
p : P,
⊢ Q
```

and your original goal will have `q : Q` added to the list
of hypotheses.
-/

/-
# Function world.

## Level 3: the `have` tactic.

Say you have a whole bunch of sets and functions between them,
and your goal is to build a certain element of a certain set.
If it helps, you can build intermediate elements of other sets
along the way, using the `have` command. `have` is the Lean analogue
of saying "let's define an element $q\in Q$ by..." in the middle of a calculation.
It is often not logically necessary, but on the other hand
it is very convenient, for example it can save on notation, or
it can break proofs or calculations up into smaller steps.

In the level below, we have an element of $P$ and we want an element
of $U$; during the proof we will make several intermediate elements
of some of the other sets involved. The diagram of sets and
functions looks like this pictorially:

![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/function_diag.jpg)

and so it's clear how to make the element of $U$ from the element of $P.$
Indeed, we could solve this level in one move by typing

`exact l(j(h(p))),`

But let us instead stroll more lazily through the level.
We can start by using the `have` tactic to make an element of $Q$:

`have q := h(p),`

and then we note that $j(q)$ is an element of $T$

`have t : T := j(q),`

(notice how on this occasion we explicitly told Lean what set we thought $t$ was in, with
that `: T` thing before the `:=`) and we could even define $u$ to be $l(t)$:

`have u : U := l(t),`

and then finish the level with

`exact u,`

.
-/

/- Definition
Given an element of $P$ we can define an element of $U$.
-/
example (P Q R S T U: Type)
(p : P)
(h : P → Q)
(i : Q → R)
(j : Q → T)
(k : S → T)
(l : T → U)
: U :=
begin
  have q := h(p),
  have t : T := j(q),
  have u : U := l(t),
  exact u,

end

/-
If you solved the level using `have`, then click on the last line of your proof
(you do know you can move your cursor around with the arrow keys
and explore your proof, right?) and note that the local context at that point
is in something like the following mess:

```
P Q R S T U : Type,
p : P,
h : P → Q,
i : Q → R,
j : Q → T,
k : S → T,
l : T → U,
q : Q,
t : T,
u : U
⊢ U
```

It was already bad enough to start with, and we added three more
terms to it. In level 4 we will learn about the `apply` tactic
which solves the level using another technique, without leaving
so much junk behind.
-/

author: ImperialCollegeLondon


text:
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.data.nat.basic
import Mathlib.Lean3Lib.init.data.nat.div
import Mathlib.Lean3Lib.init.meta.default
import Mathlib.Lean3Lib.init.algebra.functions

universes u

namespace Mathlib

namespace nat

protected theorem add_comm (n : ℕ) (m : ℕ) : n + m = m + n := sorry

protected theorem add_assoc (n : ℕ) (m : ℕ) (k : ℕ) : n + m + k = n + (m + k) := sorry

protected theorem add_left_comm (n : ℕ) (m : ℕ) (k : ℕ) : n + (m + k) = m + (n + k) :=
  left_comm Nat.add nat.add_comm nat.add_assoc

protected theorem add_left_cancel {n : ℕ} {m : ℕ} {k : ℕ} : n + m = n + k → m = k := sorry

protected theorem add_right_cancel {n : ℕ} {m : ℕ} {k : ℕ} (h : n + m = k + m) : n = k :=
  (fun (this : m + n = m + k) => nat.add_left_cancel this)
    (eq.mp (Eq._oldrec (Eq.refl (m + n = k + m)) (nat.add_comm k m))
      (eq.mp (Eq._oldrec (Eq.refl (n + m = k + m)) (nat.add_comm n m)) h))

theorem succ_ne_zero (n : ℕ) : Nat.succ n ≠ 0 :=
  fun (h : Nat.succ n = 0) => nat.no_confusion h

theorem succ_ne_self (n : ℕ) : Nat.succ n ≠ n := sorry

protected theorem one_ne_zero : 1 ≠ 0 :=
  fun (h : 1 = 0) => nat.no_confusion h

protected theorem zero_ne_one : 0 ≠ 1 :=
  fun (h : 0 = 1) => nat.no_confusion h

theorem eq_zero_of_add_eq_zero_right {n : ℕ} {m : ℕ} : n + m = 0 → n = 0 := sorry

theorem eq_zero_of_add_eq_zero_left {n : ℕ} {m : ℕ} (h : n + m = 0) : m = 0 :=
  eq_zero_of_add_eq_zero_right (nat.add_comm n m ▸ h)

@[simp] theorem pred_zero : Nat.pred 0 = 0 :=
  rfl

@[simp] theorem pred_succ (n : ℕ) : Nat.pred (Nat.succ n) = n :=
  rfl

protected theorem mul_zero (n : ℕ) : n * 0 = 0 :=
  rfl

theorem mul_succ (n : ℕ) (m : ℕ) : n * Nat.succ m = n * m + n :=
  rfl

protected theorem zero_mul (n : ℕ) : 0 * n = 0 := sorry

theorem succ_mul (n : ℕ) (m : ℕ) : Nat.succ n * m = n * m + m := sorry

protected theorem right_distrib (n : ℕ) (m : ℕ) (k : ℕ) : (n + m) * k = n * k + m * k := sorry

protected theorem left_distrib (n : ℕ) (m : ℕ) (k : ℕ) : n * (m + k) = n * m + n * k := sorry

protected theorem mul_comm (n : ℕ) (m : ℕ) : n * m = m * n := sorry

protected theorem mul_assoc (n : ℕ) (m : ℕ) (k : ℕ) : n * m * k = n * (m * k) := sorry

protected theorem mul_one (n : ℕ) : n * 1 = n :=
  nat.zero_add

protected theorem one_mul (n : ℕ) : 1 * n = n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (1 * n = n)) (nat.mul_comm 1 n)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n * 1 = n)) (nat.mul_one n))) (Eq.refl n))

/- properties of inequality -/

protected theorem le_of_eq {n : ℕ} {m : ℕ} (p : n = m) : n ≤ m :=
  p ▸ less_than_or_equal.refl

theorem le_succ_of_le {n : ℕ} {m : ℕ} (h : n ≤ m) : n ≤ Nat.succ m :=
  nat.le_trans h (le_succ m)

theorem le_of_succ_le {n : ℕ} {m : ℕ} (h : Nat.succ n ≤ m) : n ≤ m :=
  nat.le_trans (le_succ n) h

protected theorem le_of_lt {n : ℕ} {m : ℕ} (h : n < m) : n ≤ m :=
  le_of_succ_le h

def lt.step {n : ℕ} {m : ℕ} : n < m → n < Nat.succ m :=
  less_than_or_equal.step

theorem eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 :=
  nat.cases_on n (Or.inl rfl) fun (n : ℕ) => Or.inr (succ_pos n)

protected theorem pos_of_ne_zero {n : ℕ} : n ≠ 0 → n > 0 :=
  or.resolve_left (eq_zero_or_pos n)

protected theorem lt_trans {n : ℕ} {m : ℕ} {k : ℕ} (h₁ : n < m) : m < k → n < k :=
  nat.le_trans (less_than_or_equal.step h₁)

protected theorem lt_of_le_of_lt {n : ℕ} {m : ℕ} {k : ℕ} (h₁ : n ≤ m) : m < k → n < k :=
  nat.le_trans (succ_le_succ h₁)

def lt.base (n : ℕ) : n < Nat.succ n :=
  nat.le_refl (Nat.succ n)

theorem lt_succ_self (n : ℕ) : n < Nat.succ n :=
  lt.base n

protected theorem le_antisymm {n : ℕ} {m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m :=
  less_than_or_equal.cases_on h₁ (fun (a : n ≤ n) => rfl)
    fun (a : ℕ) (b : less_than_or_equal n a) (c : Nat.succ a ≤ n) => absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n)

protected theorem lt_or_ge (a : ℕ) (b : ℕ) : a < b ∨ a ≥ b := sorry

protected theorem le_total {m : ℕ} {n : ℕ} : m ≤ n ∨ n ≤ m :=
  or.imp_left nat.le_of_lt (nat.lt_or_ge m n)

protected theorem lt_of_le_and_ne {m : ℕ} {n : ℕ} (h1 : m ≤ n) : m ≠ n → m < n :=
  or.resolve_right (or.swap (nat.eq_or_lt_of_le h1))

protected theorem lt_iff_le_not_le {m : ℕ} {n : ℕ} : m < n ↔ m ≤ n ∧ ¬n ≤ m := sorry

protected instance linear_order : linear_order ℕ :=
  linear_order.mk less_than_or_equal nat.lt nat.le_refl nat.le_trans nat.le_antisymm nat.le_total nat.decidable_le
    nat.decidable_eq nat.decidable_lt

theorem eq_zero_of_le_zero {n : ℕ} (h : n ≤ 0) : n = 0 :=
  le_antisymm h (zero_le n)

theorem succ_lt_succ {a : ℕ} {b : ℕ} : a < b → Nat.succ a < Nat.succ b :=
  succ_le_succ

theorem lt_of_succ_lt {a : ℕ} {b : ℕ} : Nat.succ a < b → a < b :=
  le_of_succ_le

theorem lt_of_succ_lt_succ {a : ℕ} {b : ℕ} : Nat.succ a < Nat.succ b → a < b :=
  le_of_succ_le_succ

theorem pred_lt_pred {n : ℕ} {m : ℕ} : n ≠ 0 → n < m → Nat.pred n < Nat.pred m := sorry

theorem lt_of_succ_le {a : ℕ} {b : ℕ} (h : Nat.succ a ≤ b) : a < b :=
  h

theorem succ_le_of_lt {a : ℕ} {b : ℕ} (h : a < b) : Nat.succ a ≤ b :=
  h

theorem le_add_right (n : ℕ) (k : ℕ) : n ≤ n + k := sorry

theorem le_add_left (n : ℕ) (m : ℕ) : n ≤ m + n :=
  nat.add_comm n m ▸ le_add_right n m

theorem le.dest {n : ℕ} {m : ℕ} : n ≤ m → ∃ (k : ℕ), n + k = m := sorry

theorem le.intro {n : ℕ} {m : ℕ} {k : ℕ} (h : n + k = m) : n ≤ m :=
  h ▸ le_add_right n k

protected theorem add_le_add_left {n : ℕ} {m : ℕ} (h : n ≤ m) (k : ℕ) : k + n ≤ k + m := sorry

protected theorem add_le_add_right {n : ℕ} {m : ℕ} (h : n ≤ m) (k : ℕ) : n + k ≤ m + k :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n + k ≤ m + k)) (nat.add_comm n k)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (k + n ≤ m + k)) (nat.add_comm m k))) (nat.add_le_add_left h k))

protected theorem le_of_add_le_add_left {k : ℕ} {n : ℕ} {m : ℕ} (h : k + n ≤ k + m) : n ≤ m := sorry

protected theorem le_of_add_le_add_right {k : ℕ} {n : ℕ} {m : ℕ} : n + k ≤ m + k → n ≤ m :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n + k ≤ m + k → n ≤ m)) (nat.add_comm n k)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (k + n ≤ m + k → n ≤ m)) (nat.add_comm m k))) nat.le_of_add_le_add_left)

protected theorem add_le_add_iff_le_right (k : ℕ) (n : ℕ) (m : ℕ) : n + k ≤ m + k ↔ n ≤ m :=
  { mp := nat.le_of_add_le_add_right, mpr := fun (h : n ≤ m) => nat.add_le_add_right h k }

protected theorem lt_of_add_lt_add_left {k : ℕ} {n : ℕ} {m : ℕ} (h : k + n < k + m) : n < m :=
  let h' : k + n ≤ k + m := nat.le_of_lt h;
  nat.lt_of_le_and_ne (nat.le_of_add_le_add_left h')
    fun (heq : n = m) => nat.lt_irrefl (k + m) (eq.mp (Eq._oldrec (Eq.refl (k + n < k + m)) heq) h)

protected theorem lt_of_add_lt_add_right {a : ℕ} {b : ℕ} {c : ℕ} (h : a + b < c + b) : a < c := sorry

protected theorem add_lt_add_left {n : ℕ} {m : ℕ} (h : n < m) (k : ℕ) : k + n < k + m :=
  lt_of_succ_le (add_succ k n ▸ nat.add_le_add_left (succ_le_of_lt h) k)

protected theorem add_lt_add_right {n : ℕ} {m : ℕ} (h : n < m) (k : ℕ) : n + k < m + k :=
  nat.add_comm k m ▸ nat.add_comm k n ▸ nat.add_lt_add_left h k

protected theorem lt_add_of_pos_right {n : ℕ} {k : ℕ} (h : k > 0) : n < n + k :=
  nat.add_lt_add_left h n

protected theorem lt_add_of_pos_left {n : ℕ} {k : ℕ} (h : k > 0) : n < k + n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n < k + n)) (nat.add_comm k n))) (nat.lt_add_of_pos_right h)

protected theorem add_lt_add {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h₁ : a < b) (h₂ : c < d) : a + c < b + d :=
  lt_trans (nat.add_lt_add_right h₁ c) (nat.add_lt_add_left h₂ b)

protected theorem add_le_add {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
  le_trans (nat.add_le_add_right h₁ c) (nat.add_le_add_left h₂ b)

protected theorem zero_lt_one : 0 < 1 :=
  zero_lt_succ 0

theorem mul_le_mul_left {n : ℕ} {m : ℕ} (k : ℕ) (h : n ≤ m) : k * n ≤ k * m := sorry

theorem mul_le_mul_right {n : ℕ} {m : ℕ} (k : ℕ) (h : n ≤ m) : n * k ≤ m * k :=
  nat.mul_comm k m ▸ nat.mul_comm k n ▸ mul_le_mul_left k h

protected theorem mul_lt_mul_of_pos_left {n : ℕ} {m : ℕ} {k : ℕ} (h : n < m) (hk : k > 0) : k * n < k * m :=
  nat.lt_of_lt_of_le (nat.lt_add_of_pos_right hk) (mul_succ k n ▸ mul_le_mul_left k (succ_le_of_lt h))

protected theorem mul_lt_mul_of_pos_right {n : ℕ} {m : ℕ} {k : ℕ} (h : n < m) (hk : k > 0) : n * k < m * k :=
  nat.mul_comm k m ▸ nat.mul_comm k n ▸ nat.mul_lt_mul_of_pos_left h hk

protected theorem le_of_mul_le_mul_left {a : ℕ} {b : ℕ} {c : ℕ} (h : c * a ≤ c * b) (hc : c > 0) : a ≤ b :=
  iff.mp decidable.not_lt
    fun (h1 : b < a) => (fun (h2 : c * b < c * a) => not_le_of_gt h2 h) (nat.mul_lt_mul_of_pos_left h1 hc)

theorem le_of_lt_succ {m : ℕ} {n : ℕ} : m < Nat.succ n → m ≤ n :=
  le_of_succ_le_succ

theorem eq_of_mul_eq_mul_left {m : ℕ} {k : ℕ} {n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
  le_antisymm (nat.le_of_mul_le_mul_left (le_of_eq H) Hn) (nat.le_of_mul_le_mul_left (le_of_eq (Eq.symm H)) Hn)

/- sub properties -/

@[simp] protected theorem zero_sub (a : ℕ) : 0 - a = 0 := sorry

theorem sub_lt_succ (a : ℕ) (b : ℕ) : a - b < Nat.succ a :=
  lt_succ_of_le (sub_le a b)

protected theorem sub_le_sub_right {n : ℕ} {m : ℕ} (h : n ≤ m) (k : ℕ) : n - k ≤ m - k := sorry

/- bit0/bit1 properties -/

protected theorem bit1_eq_succ_bit0 (n : ℕ) : bit1 n = Nat.succ (bit0 n) :=
  rfl

protected theorem bit1_succ_eq (n : ℕ) : bit1 (Nat.succ n) = Nat.succ (Nat.succ (bit1 n)) :=
  Eq.trans (nat.bit1_eq_succ_bit0 (Nat.succ n)) (congr_arg Nat.succ (nat.bit0_succ_eq n))

protected theorem bit1_ne_one {n : ℕ} : n ≠ 0 → bit1 n ≠ 1 := sorry

protected theorem bit0_ne_one (n : ℕ) : bit0 n ≠ 1 := sorry

protected theorem add_self_ne_one (n : ℕ) : n + n ≠ 1 := sorry

protected theorem bit1_ne_bit0 (n : ℕ) (m : ℕ) : bit1 n ≠ bit0 m := sorry

protected theorem bit0_ne_bit1 (n : ℕ) (m : ℕ) : bit0 n ≠ bit1 m :=
  ne.symm (nat.bit1_ne_bit0 m n)

protected theorem bit0_inj {n : ℕ} {m : ℕ} : bit0 n = bit0 m → n = m := sorry

protected theorem bit1_inj {n : ℕ} {m : ℕ} : bit1 n = bit1 m → n = m := sorry

protected theorem bit0_ne {n : ℕ} {m : ℕ} : n ≠ m → bit0 n ≠ bit0 m :=
  fun (h₁ : n ≠ m) (h₂ : bit0 n = bit0 m) => absurd (nat.bit0_inj h₂) h₁

protected theorem bit1_ne {n : ℕ} {m : ℕ} : n ≠ m → bit1 n ≠ bit1 m :=
  fun (h₁ : n ≠ m) (h₂ : bit1 n = bit1 m) => absurd (nat.bit1_inj h₂) h₁

protected theorem zero_ne_bit0 {n : ℕ} : n ≠ 0 → 0 ≠ bit0 n :=
  fun (h : n ≠ 0) => ne.symm (nat.bit0_ne_zero h)

protected theorem zero_ne_bit1 (n : ℕ) : 0 ≠ bit1 n :=
  ne.symm (nat.bit1_ne_zero n)

protected theorem one_ne_bit0 (n : ℕ) : 1 ≠ bit0 n :=
  ne.symm (nat.bit0_ne_one n)

protected theorem one_ne_bit1 {n : ℕ} : n ≠ 0 → 1 ≠ bit1 n :=
  fun (h : n ≠ 0) => ne.symm (nat.bit1_ne_one h)

protected theorem one_lt_bit1 {n : ℕ} : n ≠ 0 → 1 < bit1 n := sorry

protected theorem one_lt_bit0 {n : ℕ} : n ≠ 0 → 1 < bit0 n := sorry

protected theorem bit0_lt {n : ℕ} {m : ℕ} (h : n < m) : bit0 n < bit0 m :=
  nat.add_lt_add h h

protected theorem bit1_lt {n : ℕ} {m : ℕ} (h : n < m) : bit1 n < bit1 m :=
  succ_lt_succ (nat.add_lt_add h h)

protected theorem bit0_lt_bit1 {n : ℕ} {m : ℕ} (h : n ≤ m) : bit0 n < bit1 m :=
  lt_succ_of_le (nat.add_le_add h h)

protected theorem bit1_lt_bit0 {n : ℕ} {m : ℕ} : n < m → bit1 n < bit0 m := sorry

protected theorem one_le_bit1 (n : ℕ) : 1 ≤ bit1 n :=
  (fun (this : 1 ≤ Nat.succ (bit0 n)) => this) (succ_le_succ (zero_le (bit0 n)))

protected theorem one_le_bit0 (n : ℕ) : n ≠ 0 → 1 ≤ bit0 n := sorry

/- subtraction -/

@[simp] protected theorem sub_zero (n : ℕ) : n - 0 = n :=
  rfl

theorem sub_succ (n : ℕ) (m : ℕ) : n - Nat.succ m = Nat.pred (n - m) :=
  rfl

theorem succ_sub_succ (n : ℕ) (m : ℕ) : Nat.succ n - Nat.succ m = n - m :=
  succ_sub_succ_eq_sub n m

protected theorem sub_self (n : ℕ) : n - n = 0 := sorry

/- TODO(Leo): remove the following ematch annotations as soon as we have
   arithmetic theory in the smt_stactic -/

protected theorem add_sub_add_right (n : ℕ) (k : ℕ) (m : ℕ) : n + k - (m + k) = n - m := sorry

protected theorem add_sub_add_left (k : ℕ) (n : ℕ) (m : ℕ) : k + n - (k + m) = n - m :=
  eq.mpr (id (Eq._oldrec (Eq.refl (k + n - (k + m) = n - m)) (nat.add_comm k n)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n + k - (k + m) = n - m)) (nat.add_comm k m)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (n + k - (m + k) = n - m)) (nat.add_sub_add_right n k m))) (Eq.refl (n - m))))

protected theorem add_sub_cancel (n : ℕ) (m : ℕ) : n + m - m = n :=
  (fun (this : n + m - (0 + m) = n) => eq.mp (Eq._oldrec (Eq.refl (n + m - (0 + m) = n)) (nat.zero_add m)) this)
    (eq.mpr (id (Eq._oldrec (Eq.refl (n + m - (0 + m) = n)) (nat.add_sub_add_right n m 0)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (n - 0 = n)) (nat.sub_zero n))) (Eq.refl n)))

protected theorem add_sub_cancel_left (n : ℕ) (m : ℕ) : n + m - n = m :=
  (fun (this : n + m - (n + 0) = m) => this)
    (eq.mpr (id (Eq._oldrec (Eq.refl (n + m - (n + 0) = m)) (nat.add_sub_add_left n m 0)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (m - 0 = m)) (nat.sub_zero m))) (Eq.refl m)))

protected theorem sub_sub (n : ℕ) (m : ℕ) (k : ℕ) : n - m - k = n - (m + k) := sorry

theorem le_of_le_of_sub_le_sub_right {n : ℕ} {m : ℕ} {k : ℕ} (h₀ : k ≤ m) (h₁ : n - k ≤ m - k) : n ≤ m := sorry

protected theorem sub_le_sub_right_iff (n : ℕ) (m : ℕ) (k : ℕ) (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m :=
  { mp := le_of_le_of_sub_le_sub_right h, mpr := fun (h : n ≤ m) => nat.sub_le_sub_right h k }

theorem sub_self_add (n : ℕ) (m : ℕ) : n - (n + m) = 0 :=
  (fun (this : n + 0 - (n + m) = 0) => this)
    (eq.mpr (id (Eq._oldrec (Eq.refl (n + 0 - (n + m) = 0)) (nat.add_sub_add_left n 0 m)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (0 - m = 0)) (nat.zero_sub m))) (Eq.refl 0)))

theorem add_le_to_le_sub (x : ℕ) {y : ℕ} {k : ℕ} (h : k ≤ y) : x + k ≤ y ↔ x ≤ y - k := sorry

theorem sub_lt_of_pos_le (a : ℕ) (b : ℕ) (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b :=
  sub_lt (lt_of_lt_of_le h₀ h₁) h₀

theorem sub_one (n : ℕ) : n - 1 = Nat.pred n :=
  rfl

theorem succ_sub_one (n : ℕ) : Nat.succ n - 1 = n :=
  rfl

theorem succ_pred_eq_of_pos {n : ℕ} : n > 0 → Nat.succ (Nat.pred n) = n := sorry

theorem sub_eq_zero_of_le {n : ℕ} {m : ℕ} (h : n ≤ m) : n - m = 0 := sorry

protected theorem le_of_sub_eq_zero {n : ℕ} {m : ℕ} : n - m = 0 → n ≤ m := sorry

protected theorem sub_eq_zero_iff_le {n : ℕ} {m : ℕ} : n - m = 0 ↔ n ≤ m :=
  { mp := nat.le_of_sub_eq_zero, mpr := sub_eq_zero_of_le }

theorem add_sub_of_le {n : ℕ} {m : ℕ} (h : n ≤ m) : n + (m - n) = m := sorry

protected theorem sub_add_cancel {n : ℕ} {m : ℕ} (h : n ≥ m) : n - m + m = n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n - m + m = n)) (nat.add_comm (n - m) m)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (m + (n - m) = n)) (add_sub_of_le h))) (Eq.refl n))

protected theorem add_sub_assoc {m : ℕ} {k : ℕ} (h : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) := sorry

protected theorem sub_eq_iff_eq_add {a : ℕ} {b : ℕ} {c : ℕ} (ab : b ≤ a) : a - b = c ↔ a = c + b := sorry

protected theorem lt_of_sub_eq_succ {m : ℕ} {n : ℕ} {l : ℕ} (H : m - n = Nat.succ l) : n < m := sorry

@[simp] theorem zero_min (a : ℕ) : min 0 a = 0 :=
  min_eq_left (zero_le a)

@[simp] theorem min_zero (a : ℕ) : min a 0 = 0 :=
  min_eq_right (zero_le a)

-- Distribute succ over min

theorem min_succ_succ (x : ℕ) (y : ℕ) : min (Nat.succ x) (Nat.succ y) = Nat.succ (min x y) := sorry

theorem sub_eq_sub_min (n : ℕ) (m : ℕ) : n - m = n - min n m := sorry

@[simp] theorem sub_add_min_cancel (n : ℕ) (m : ℕ) : n - m + min n m = n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n - m + min n m = n)) (sub_eq_sub_min n m)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n - min n m + min n m = n)) (nat.sub_add_cancel (min_le_left n m)))) (Eq.refl n))

/- TODO(Leo): sub + inequalities -/

protected def strong_rec_on {p : ℕ → Sort u} (n : ℕ) (h : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n) : p n :=
  (fun (this : (n m : ℕ) → m < n → p m) => this (Nat.succ n) n (lt_succ_self n))
    fun (n : ℕ) =>
      Nat.rec (fun (m : ℕ) (h₁ : m < 0) => absurd h₁ (not_lt_zero m))
        (fun (n : ℕ) (ih : (m : ℕ) → m < n → p m) (m : ℕ) (h₁ : m < Nat.succ n) =>
          or.by_cases sorry (fun (ᾰ : m < n) => ih m ᾰ)
            fun (ᾰ : m = n) => Eq._oldrec (fun (h₁ : n < Nat.succ n) => h n ih) (Eq.symm ᾰ) h₁)
        n

protected theorem strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) : p n :=
  nat.strong_rec_on n h

protected theorem case_strong_induction_on {p : ℕ → Prop} (a : ℕ) (hz : p 0) (hi : ∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p (Nat.succ n)) : p a := sorry

/- mod -/

theorem mod_def (x : ℕ) (y : ℕ) : x % y = ite (0 < y ∧ y ≤ x) ((x - y) % y) x := sorry

@[simp] theorem mod_zero (a : ℕ) : a % 0 = a := sorry

theorem mod_eq_of_lt {a : ℕ} {b : ℕ} (h : a < b) : a % b = a := sorry

@[simp] theorem zero_mod (b : ℕ) : 0 % b = 0 := sorry

theorem mod_eq_sub_mod {a : ℕ} {b : ℕ} (h : a ≥ b) : a % b = (a - b) % b := sorry

theorem mod_lt (x : ℕ) {y : ℕ} (h : y > 0) : x % y < y := sorry

@[simp] theorem mod_self (n : ℕ) : n % n = 0 :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n % n = 0)) (mod_eq_sub_mod (le_refl n))))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((n - n) % n = 0)) (nat.sub_self n)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (0 % n = 0)) (zero_mod n))) (Eq.refl 0)))

@[simp] theorem mod_one (n : ℕ) : n % 1 = 0 :=
  (fun (this : n % 1 < 1) => eq_zero_of_le_zero (le_of_lt_succ this)) (mod_lt n (succ_pos 0))

theorem mod_two_eq_zero_or_one (n : ℕ) : n % bit0 1 = 0 ∨ n % bit0 1 = 1 := sorry

/- div & mod -/

theorem div_def (x : ℕ) (y : ℕ) : x / y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0 := sorry

theorem mod_add_div (m : ℕ) (k : ℕ) : m % k + k * (m / k) = m := sorry

/- div -/

@[simp] protected theorem div_one (n : ℕ) : n / 1 = n := sorry

@[simp] protected theorem div_zero (n : ℕ) : n / 0 = 0 := sorry

@[simp] protected theorem zero_div (b : ℕ) : 0 / b = 0 :=
  Eq.trans (div_def 0 b) (if_neg (And._oldrec not_le_of_gt))

protected theorem div_le_of_le_mul {m : ℕ} {n : ℕ} {k : ℕ} : m ≤ k * n → m / k ≤ n := sorry

protected theorem div_le_self (m : ℕ) (n : ℕ) : m / n ≤ m := sorry

theorem div_eq_sub_div {a : ℕ} {b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a / b = (a - b) / b + 1 := sorry

theorem div_eq_of_lt {a : ℕ} {b : ℕ} (h₀ : a < b) : a / b = 0 := sorry

-- this is a Galois connection

--   f x ≤ y ↔ x ≤ g y

-- with

--   f x = x * k

--   g y = y / k

theorem le_div_iff_mul_le (x : ℕ) (y : ℕ) {k : ℕ} (Hk : k > 0) : x ≤ y / k ↔ x * k ≤ y := sorry

theorem div_lt_iff_lt_mul (x : ℕ) (y : ℕ) {k : ℕ} (Hk : k > 0) : x / k < y ↔ x < y * k := sorry

def iterate {α : Sort u} (op : α → α) : ℕ → α → α :=
  sorry

/- successor and predecessor -/

theorem add_one_ne_zero (n : ℕ) : n + 1 ≠ 0 :=
  succ_ne_zero n

theorem eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ∨ n = Nat.succ (Nat.pred n) := sorry

theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : ∃ (k : ℕ), n = Nat.succ k :=
  Exists.intro (Nat.pred n) (or.resolve_left (eq_zero_or_eq_succ_pred n) H)

theorem discriminate {B : Sort u} {n : ℕ} (H1 : n = 0 → B) (H2 : (m : ℕ) → n = Nat.succ m → B) : B :=
  (fun (_x : ℕ) (h : n = _x) =>
      Nat.rec (fun (h : n = 0) => H1 h) (fun (n_1 : ℕ) (ih : n = n_1 → B) (h : n = Nat.succ n_1) => H2 n_1 h) _x h)
    n rfl

theorem one_succ_zero : 1 = Nat.succ 0 :=
  rfl

theorem two_step_induction {P : ℕ → Sort u} (H1 : P 0) (H2 : P 1) (H3 : (n : ℕ) → P n → P (Nat.succ n) → P (Nat.succ (Nat.succ n))) (a : ℕ) : P a := sorry

theorem sub_induction {P : ℕ → ℕ → Sort u} (H1 : (m : ℕ) → P 0 m) (H2 : (n : ℕ) → P (Nat.succ n) 0) (H3 : (n m : ℕ) → P n m → P (Nat.succ n) (Nat.succ m)) (n : ℕ) (m : ℕ) : P n m := sorry

/- addition -/

theorem succ_add_eq_succ_add (n : ℕ) (m : ℕ) : Nat.succ n + m = n + Nat.succ m := sorry

-- theorem one_add (n : ℕ) : 1 + n = succ n := by simp [add_comm]

protected theorem add_right_comm (n : ℕ) (m : ℕ) (k : ℕ) : n + m + k = n + k + m :=
  right_comm Nat.add nat.add_comm nat.add_assoc

theorem eq_zero_of_add_eq_zero {n : ℕ} {m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 :=
  { left := eq_zero_of_add_eq_zero_right H, right := eq_zero_of_add_eq_zero_left H }

theorem eq_zero_of_mul_eq_zero {n : ℕ} {m : ℕ} : n * m = 0 → n = 0 ∨ m = 0 := sorry

/- properties of inequality -/

theorem le_succ_of_pred_le {n : ℕ} {m : ℕ} : Nat.pred n ≤ m → n ≤ Nat.succ m :=
  nat.cases_on n less_than_or_equal.step fun (a : ℕ) => succ_le_succ

theorem le_lt_antisymm {n : ℕ} {m : ℕ} (h₁ : n ≤ m) (h₂ : m < n) : False :=
  nat.lt_irrefl n (nat.lt_of_le_of_lt h₁ h₂)

theorem lt_le_antisymm {n : ℕ} {m : ℕ} (h₁ : n < m) (h₂ : m ≤ n) : False :=
  le_lt_antisymm h₂ h₁

protected theorem lt_asymm {n : ℕ} {m : ℕ} (h₁ : n < m) : ¬m < n :=
  le_lt_antisymm (nat.le_of_lt h₁)

protected def lt_ge_by_cases {a : ℕ} {b : ℕ} {C : Sort u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C :=
  decidable.by_cases h₁ fun (h : ¬a < b) => h₂ sorry

protected def lt_by_cases {a : ℕ} {b : ℕ} {C : Sort u} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) : C :=
  nat.lt_ge_by_cases h₁ fun (h₁ : a ≥ b) => nat.lt_ge_by_cases h₃ fun (h : b ≥ a) => h₂ (nat.le_antisymm h h₁)

protected theorem lt_trichotomy (a : ℕ) (b : ℕ) : a < b ∨ a = b ∨ b < a :=
  nat.lt_by_cases (fun (h : a < b) => Or.inl h) (fun (h : a = b) => Or.inr (Or.inl h))
    fun (h : b < a) => Or.inr (Or.inr h)

protected theorem eq_or_lt_of_not_lt {a : ℕ} {b : ℕ} (hnlt : ¬a < b) : a = b ∨ b < a :=
  or.resolve_left (nat.lt_trichotomy a b) hnlt

theorem lt_succ_of_lt {a : ℕ} {b : ℕ} (h : a < b) : a < Nat.succ b :=
  le_succ_of_le h

def one_pos : 0 < 1 :=
  nat.zero_lt_one

/- subtraction -/

protected theorem sub_le_sub_left {n : ℕ} {m : ℕ} (k : ℕ) (h : n ≤ m) : k - m ≤ k - n :=
  less_than_or_equal.drec (le_refl (k - n))
    (fun {h_b : ℕ} (h_ᾰ : less_than_or_equal n h_b) (h_ih : k - h_b ≤ k - n) => le_trans (pred_le (Nat.sub k h_b)) h_ih) h

theorem succ_sub_sub_succ (n : ℕ) (m : ℕ) (k : ℕ) : Nat.succ n - m - Nat.succ k = n - m - k := sorry

protected theorem sub.right_comm (m : ℕ) (n : ℕ) (k : ℕ) : m - n - k = m - k - n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m - n - k = m - k - n)) (nat.sub_sub m n k)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (m - (n + k) = m - k - n)) (nat.sub_sub m k n)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (m - (n + k) = m - (k + n))) (nat.add_comm n k))) (Eq.refl (m - (k + n)))))

theorem mul_pred_left (n : ℕ) (m : ℕ) : Nat.pred n * m = n * m - m := sorry

theorem mul_pred_right (n : ℕ) (m : ℕ) : n * Nat.pred m = n * m - n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n * Nat.pred m = n * m - n)) (nat.mul_comm n (Nat.pred m))))
    (eq.mpr (id (Eq._oldrec (Eq.refl (Nat.pred m * n = n * m - n)) (mul_pred_left m n)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (m * n - n = n * m - n)) (nat.mul_comm m n))) (Eq.refl (n * m - n))))

protected theorem mul_sub_right_distrib (n : ℕ) (m : ℕ) (k : ℕ) : (n - m) * k = n * k - m * k := sorry

protected theorem mul_sub_left_distrib (n : ℕ) (m : ℕ) (k : ℕ) : n * (m - k) = n * m - n * k := sorry

protected theorem mul_self_sub_mul_self_eq (a : ℕ) (b : ℕ) : a * a - b * b = (a + b) * (a - b) := sorry

theorem succ_mul_succ_eq (a : ℕ) (b : ℕ) : Nat.succ a * Nat.succ b = a * b + a + b + 1 := sorry

theorem succ_sub {m : ℕ} {n : ℕ} (h : m ≥ n) : Nat.succ m - n = Nat.succ (m - n) := sorry

protected theorem sub_pos_of_lt {m : ℕ} {n : ℕ} (h : m < n) : n - m > 0 :=
  (fun (this : 0 + m < n - m + m) => nat.lt_of_add_lt_add_right this)
    (eq.mpr (id (Eq._oldrec (Eq.refl (0 + m < n - m + m)) (nat.zero_add m)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (m < n - m + m)) (nat.sub_add_cancel (le_of_lt h)))) h))

protected theorem sub_sub_self {n : ℕ} {m : ℕ} (h : m ≤ n) : n - (n - m) = m :=
  iff.mpr (nat.sub_eq_iff_eq_add (sub_le n m)) (Eq.symm (add_sub_of_le h))

protected theorem sub_add_comm {n : ℕ} {m : ℕ} {k : ℕ} (h : k ≤ n) : n + m - k = n - k + m :=
  iff.mpr (nat.sub_eq_iff_eq_add (nat.le_trans h (le_add_right n m)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n + m = n - k + m + k)) (nat.add_right_comm (n - k) m k)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (n + m = n - k + k + m)) (nat.sub_add_cancel h))) (Eq.refl (n + m))))

theorem sub_one_sub_lt {n : ℕ} {i : ℕ} (h : i < n) : n - 1 - i < n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n - 1 - i < n)) (nat.sub_sub n 1 i)))
    (sub_lt (lt_of_lt_of_le (zero_lt_succ i) h)
      (eq.mpr (id (Eq._oldrec (Eq.refl (0 < 1 + i)) (nat.add_comm 1 i))) (zero_lt_succ i)))

theorem pred_inj {a : ℕ} {b : ℕ} : a > 0 → b > 0 → Nat.pred a = Nat.pred b → a = b := sorry

/- find -/

protected def find_x {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) : Subtype fun (n : ℕ) => p n ∧ ∀ (m : ℕ), m < n → ¬p m :=
  well_founded.fix (wf_lbp H)
    (fun (m : ℕ)
      (IH :
      (y : ℕ) →
        lbp y m → (fun (k : ℕ) => (∀ (n : ℕ), n < k → ¬p n) → Subtype fun (n : ℕ) => p n ∧ ∀ (m : ℕ), m < n → ¬p m) y)
      (al : ∀ (n : ℕ), n < m → ¬p n) =>
      dite (p m) (fun (pm : p m) => { val := m, property := sorry })
        fun (pm : ¬p m) => (fun (this : ∀ (n : ℕ), n ≤ m → ¬p n) => IH (m + 1) sorry sorry) sorry)
    0 sorry

protected def find {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) : ℕ :=
  subtype.val (nat.find_x H)

protected theorem find_spec {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) : p (nat.find H) :=
  and.left (subtype.property (nat.find_x H))

protected theorem find_min {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) {m : ℕ} : m < nat.find H → ¬p m :=
  and.right (subtype.property (nat.find_x H))

protected theorem find_min' {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) {m : ℕ} (h : p m) : nat.find H ≤ m :=
  decidable.le_of_not_lt fun (l : m < nat.find H) => nat.find_min H l h

/- mod -/

theorem mod_le (x : ℕ) (y : ℕ) : x % y ≤ x := sorry

@[simp] theorem add_mod_right (x : ℕ) (z : ℕ) : (x + z) % z = x % z :=
  eq.mpr (id (Eq._oldrec (Eq.refl ((x + z) % z = x % z)) (mod_eq_sub_mod (le_add_left z x))))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((x + z - z) % z = x % z)) (nat.add_sub_cancel x z))) (Eq.refl (x % z)))

@[simp] theorem add_mod_left (x : ℕ) (z : ℕ) : (x + z) % x = z % x :=
  eq.mpr (id (Eq._oldrec (Eq.refl ((x + z) % x = z % x)) (nat.add_comm x z)))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((z + x) % x = z % x)) (add_mod_right z x))) (Eq.refl (z % x)))

@[simp] theorem add_mul_mod_self_left (x : ℕ) (y : ℕ) (z : ℕ) : (x + y * z) % y = x % y := sorry

@[simp] theorem add_mul_mod_self_right (x : ℕ) (y : ℕ) (z : ℕ) : (x + y * z) % z = x % z :=
  eq.mpr (id (Eq._oldrec (Eq.refl ((x + y * z) % z = x % z)) (nat.mul_comm y z)))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((x + z * y) % z = x % z)) (add_mul_mod_self_left x z y))) (Eq.refl (x % z)))

@[simp] theorem mul_mod_right (m : ℕ) (n : ℕ) : m * n % m = 0 :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m * n % m = 0)) (Eq.symm (nat.zero_add (m * n)))))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((0 + m * n) % m = 0)) (add_mul_mod_self_left 0 m n)))
      (eq.mpr (id (Eq._oldrec (Eq.refl (0 % m = 0)) (zero_mod m))) (Eq.refl 0)))

@[simp] theorem mul_mod_left (m : ℕ) (n : ℕ) : m * n % n = 0 :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m * n % n = 0)) (nat.mul_comm m n)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n * m % n = 0)) (mul_mod_right n m))) (Eq.refl 0))

theorem mul_mod_mul_left (z : ℕ) (x : ℕ) (y : ℕ) : z * x % (z * y) = z * (x % y) := sorry

theorem mul_mod_mul_right (z : ℕ) (x : ℕ) (y : ℕ) : x * z % (y * z) = x % y * z := sorry

theorem cond_to_bool_mod_two (x : ℕ) [d : Decidable (x % bit0 1 = 1)] : cond (to_bool (x % bit0 1 = 1)) 1 0 = x % bit0 1 := sorry

theorem sub_mul_mod (x : ℕ) (k : ℕ) (n : ℕ) (h₁ : n * k ≤ x) : (x - n * k) % n = x % n := sorry

/- div -/

theorem sub_mul_div (x : ℕ) (n : ℕ) (p : ℕ) (h₁ : n * p ≤ x) : (x - n * p) / n = x / n - p := sorry

theorem div_mul_le_self (m : ℕ) (n : ℕ) : m / n * n ≤ m := sorry

@[simp] theorem add_div_right (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) / z = Nat.succ (x / z) :=
  eq.mpr (id (Eq._oldrec (Eq.refl ((x + z) / z = Nat.succ (x / z))) (div_eq_sub_div H (le_add_left z x))))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((x + z - z) / z + 1 = Nat.succ (x / z))) (nat.add_sub_cancel x z)))
      (Eq.refl (x / z + 1)))

@[simp] theorem add_div_left (x : ℕ) {z : ℕ} (H : z > 0) : (z + x) / z = Nat.succ (x / z) :=
  eq.mpr (id (Eq._oldrec (Eq.refl ((z + x) / z = Nat.succ (x / z))) (nat.add_comm z x)))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((x + z) / z = Nat.succ (x / z))) (add_div_right x H))) (Eq.refl (Nat.succ (x / z))))

@[simp] theorem mul_div_right (n : ℕ) {m : ℕ} (H : m > 0) : m * n / m = n := sorry

@[simp] theorem mul_div_left (m : ℕ) {n : ℕ} (H : n > 0) : m * n / n = m :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m * n / n = m)) (nat.mul_comm m n)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n * m / n = m)) (mul_div_right m H))) (Eq.refl m))

protected theorem div_self {n : ℕ} (H : n > 0) : n / n = 1 :=
  let t : (0 + n) / n = Nat.succ (0 / n) := add_div_right 0 H;
  eq.mp (Eq._oldrec (Eq.refl (n / n = Nat.succ (0 / n))) (nat.zero_div n))
    (eq.mp (Eq._oldrec (Eq.refl ((0 + n) / n = Nat.succ (0 / n))) (nat.zero_add n)) t)

theorem add_mul_div_left (x : ℕ) (z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) / y = x / y + z := sorry

theorem add_mul_div_right (x : ℕ) (y : ℕ) {z : ℕ} (H : z > 0) : (x + y * z) / z = x / z + y :=
  eq.mpr (id (Eq._oldrec (Eq.refl ((x + y * z) / z = x / z + y)) (nat.mul_comm y z)))
    (eq.mpr (id (Eq._oldrec (Eq.refl ((x + z * y) / z = x / z + y)) (add_mul_div_left x y H))) (Eq.refl (x / z + y)))

protected theorem mul_div_cancel (m : ℕ) {n : ℕ} (H : n > 0) : m * n / n = m := sorry

protected theorem mul_div_cancel_left (m : ℕ) {n : ℕ} (H : n > 0) : n * m / n = m :=
  eq.mpr (id (Eq._oldrec (Eq.refl (n * m / n = m)) (nat.mul_comm n m)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (m * n / n = m)) (nat.mul_div_cancel m H))) (Eq.refl m))

protected theorem div_eq_of_eq_mul_left {m : ℕ} {n : ℕ} {k : ℕ} (H1 : n > 0) (H2 : m = k * n) : m / n = k :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m / n = k)) H2))
    (eq.mpr (id (Eq._oldrec (Eq.refl (k * n / n = k)) (nat.mul_div_cancel k H1))) (Eq.refl k))

protected theorem div_eq_of_eq_mul_right {m : ℕ} {n : ℕ} {k : ℕ} (H1 : n > 0) (H2 : m = n * k) : m / n = k :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m / n = k)) H2))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n * k / n = k)) (nat.mul_div_cancel_left k H1))) (Eq.refl k))

protected theorem div_eq_of_lt_le {m : ℕ} {n : ℕ} {k : ℕ} (lo : k * n ≤ m) (hi : m < Nat.succ k * n) : m / n = k := sorry

theorem mul_sub_div (x : ℕ) (n : ℕ) (p : ℕ) (h₁ : x < n * p) : (n * p - Nat.succ x) / n = p - Nat.succ (x / n) := sorry

protected theorem mul_pos {a : ℕ} {b : ℕ} (ha : a > 0) (hb : b > 0) : a * b > 0 :=
  (fun (h : 0 * b < a * b) => eq.mp (Eq._oldrec (Eq.refl (0 * b < a * b)) (nat.zero_mul b)) h)
    (nat.mul_lt_mul_of_pos_right ha hb)

protected theorem div_div_eq_div_mul (m : ℕ) (n : ℕ) (k : ℕ) : m / n / k = m / (n * k) := sorry

protected theorem mul_div_mul {m : ℕ} (n : ℕ) (k : ℕ) (H : m > 0) : m * n / (m * k) = n / k :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m * n / (m * k) = n / k)) (Eq.symm (nat.div_div_eq_div_mul (m * n) m k))))
    (eq.mpr (id (Eq._oldrec (Eq.refl (m * n / m / k = n / k)) (nat.mul_div_cancel_left n H))) (Eq.refl (n / k)))

/- dvd -/

@[simp] protected theorem dvd_mul_right (a : ℕ) (b : ℕ) : a ∣ a * b :=
  Exists.intro b rfl

protected theorem dvd_trans {a : ℕ} {b : ℕ} {c : ℕ} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := sorry

protected theorem eq_zero_of_zero_dvd {a : ℕ} (h : 0 ∣ a) : a = 0 :=
  exists.elim h fun (c : ℕ) (H' : a = 0 * c) => Eq.trans H' (nat.zero_mul c)

protected theorem dvd_add {a : ℕ} {b : ℕ} {c : ℕ} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c := sorry

protected theorem dvd_add_iff_right {k : ℕ} {m : ℕ} {n : ℕ} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n := sorry

protected theorem dvd_add_iff_left {k : ℕ} {m : ℕ} {n : ℕ} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n :=
  eq.mpr (id (Eq._oldrec (Eq.refl (k ∣ m ↔ k ∣ m + n)) (nat.add_comm m n))) (nat.dvd_add_iff_right h)

theorem dvd_sub {k : ℕ} {m : ℕ} {n : ℕ} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
  iff.mpr (nat.dvd_add_iff_left h₂) (eq.mpr (id (Eq._oldrec (Eq.refl (k ∣ m - n + n)) (nat.sub_add_cancel H))) h₁)

theorem dvd_mod_iff {k : ℕ} {m : ℕ} {n : ℕ} (h : k ∣ n) : k ∣ m % n ↔ k ∣ m :=
  let t : k ∣ m % n ↔ k ∣ m % n + n * (m / n) := nat.dvd_add_iff_left (nat.dvd_trans h (nat.dvd_mul_right n (m / n)));
  eq.mp (Eq._oldrec (Eq.refl (k ∣ m % n ↔ k ∣ m % n + n * (m / n))) (mod_add_div m n)) t

theorem le_of_dvd {m : ℕ} {n : ℕ} (h : n > 0) : m ∣ n → m ≤ n := sorry

theorem dvd_antisymm {m : ℕ} {n : ℕ} : m ∣ n → n ∣ m → m = n := sorry

theorem pos_of_dvd_of_pos {m : ℕ} {n : ℕ} (H1 : m ∣ n) (H2 : n > 0) : m > 0 := sorry

theorem eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 :=
  le_antisymm (le_of_dvd (of_as_true trivial) H) (pos_of_dvd_of_pos H (of_as_true trivial))

theorem dvd_of_mod_eq_zero {m : ℕ} {n : ℕ} (H : n % m = 0) : m ∣ n :=
  Exists.intro (n / m)
    (eq.mp (Eq._oldrec (Eq.refl (n = 0 + m * (n / m))) (nat.zero_add (m * (n / m))))
      (eq.mp (Eq._oldrec (Eq.refl (n = n % m + m * (n / m))) H) (Eq.symm (mod_add_div n m))))

theorem mod_eq_zero_of_dvd {m : ℕ} {n : ℕ} (H : m ∣ n) : n % m = 0 := sorry

theorem dvd_iff_mod_eq_zero (m : ℕ) (n : ℕ) : m ∣ n ↔ n % m = 0 :=
  { mp := mod_eq_zero_of_dvd, mpr := dvd_of_mod_eq_zero }

protected instance decidable_dvd : DecidableRel has_dvd.dvd :=
  fun (m n : ℕ) => decidable_of_decidable_of_iff (nat.decidable_eq (n % m) 0) sorry

protected theorem mul_div_cancel' {m : ℕ} {n : ℕ} (H : n ∣ m) : n * (m / n) = m :=
  let t : m % n + n * (m / n) = m := mod_add_div m n;
  eq.mp (Eq._oldrec (Eq.refl (0 + n * (m / n) = m)) (nat.zero_add (n * (m / n))))
    (eq.mp (Eq._oldrec (Eq.refl (m % n + n * (m / n) = m)) (mod_eq_zero_of_dvd H)) t)

protected theorem div_mul_cancel {m : ℕ} {n : ℕ} (H : n ∣ m) : m / n * n = m :=
  eq.mpr (id (Eq._oldrec (Eq.refl (m / n * n = m)) (nat.mul_comm (m / n) n)))
    (eq.mpr (id (Eq._oldrec (Eq.refl (n * (m / n) = m)) (nat.mul_div_cancel' H))) (Eq.refl m))

protected theorem mul_div_assoc (m : ℕ) {n : ℕ} {k : ℕ} (H : k ∣ n) : m * n / k = m * (n / k) := sorry

theorem dvd_of_mul_dvd_mul_left {m : ℕ} {n : ℕ} {k : ℕ} (kpos : k > 0) (H : k * m ∣ k * n) : m ∣ n := sorry

theorem dvd_of_mul_dvd_mul_right {m : ℕ} {n : ℕ} {k : ℕ} (kpos : k > 0) (H : m * k ∣ n * k) : m ∣ n :=
  dvd_of_mul_dvd_mul_left kpos
    (eq.mp (Eq._oldrec (Eq.refl (k * m ∣ n * k)) (nat.mul_comm n k))
      (eq.mp (Eq._oldrec (Eq.refl (m * k ∣ n * k)) (nat.mul_comm m k)) H))

/- --- -/

protected theorem mul_le_mul_of_nonneg_left {a : ℕ} {b : ℕ} {c : ℕ} (h₁ : a ≤ b) : c * a ≤ c * b := sorry

protected theorem mul_le_mul_of_nonneg_right {a : ℕ} {b : ℕ} {c : ℕ} (h₁ : a ≤ b) : a * c ≤ b * c := sorry

protected theorem mul_lt_mul {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) : a * b < c * d :=
  lt_of_lt_of_le (nat.mul_lt_mul_of_pos_right hac pos_b) (nat.mul_le_mul_of_nonneg_left hbd)

protected theorem mul_lt_mul' {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h1 : a ≤ c) (h2 : b < d) (h3 : 0 < c) : a * b < c * d :=
  lt_of_le_of_lt (nat.mul_le_mul_of_nonneg_right h1) (nat.mul_lt_mul_of_pos_left h2 h3)

-- TODO: there are four variations, depending on which variables we assume to be nonneg

protected theorem mul_le_mul {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) : a * b ≤ c * d :=
  le_trans (nat.mul_le_mul_of_nonneg_right hac) (nat.mul_le_mul_of_nonneg_left hbd)

theorem div_lt_self {n : ℕ} {m : ℕ} : n > 0 → m > 1 → n / m < n := sorry

author: AurelienSaue


text:
-- El_conjunto_de_las_clases_de_equivalencia_es_una_particion.lean
-- El conjunto de las clases de equivalencia es una partición.
-- José A. Alonso Jiménez
-- Sevilla, 24 de agosto de 2021
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Demostrar que si R es una relación de equivalencia en X, entonces las
-- clases de equivalencia de R es una partición de X.
-- ---------------------------------------------------------------------

import tactic

variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

def particion (A : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ A, x ∈ B ∧ ∀ C ∈ A, x ∈ C → B = C)) ∧ ∅ ∉ A

lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz

-- 1ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        apply le_antisymm,
        { exact aux h hx, },
        { exact aux h (h.2.1 hx), }}}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

-- 2ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

-- 3ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use [clase R y,
         ⟨by use y,
          ⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

author: jaalonso

repo: Calculemus

save_path: github-repos/lean/jaalonso-Calculemus


text:
/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau
-/
import data.fin.vec_notation
import logic.equiv.basic
import tactic.norm_num

/-!
# Equivalences for `fin n`
-/

universes u

variables {m n : ℕ}

/-- Equivalence between `fin 0` and `empty`. -/
def fin_zero_equiv : fin 0 ≃ empty :=
equiv.equiv_empty _

/-- Equivalence between `fin 0` and `pempty`. -/
def fin_zero_equiv' : fin 0 ≃ pempty.{u} :=
equiv.equiv_pempty _

/-- Equivalence between `fin 1` and `unit`. -/
def fin_one_equiv : fin 1 ≃ unit :=
equiv_punit_of_unique

/-- Equivalence between `fin 2` and `bool`. -/
def fin_two_equiv : fin 2 ≃ bool :=
⟨@fin.cases 1 (λ_, bool) ff (λ_, tt),
  λb, cond b 1 0,
  begin
    refine fin.cases _ _, by norm_num,
    refine fin.cases _ _, by norm_num,
    exact λi, fin_zero_elim i
  end,
  begin
    rintro ⟨_|_⟩,
    { refl },
    { rw ← fin.succ_zero_eq_one, refl }
  end⟩

/-- `Π i : fin 2, α i` is equivalent to `α 0 × α 1`. See also `fin_two_arrow_equiv` for a
non-dependent version and `prod_equiv_pi_fin_two` for a version with inputs `α β : Type u`. -/
@[simps {fully_applied := ff}] def pi_fin_two_equiv (α : fin 2 → Type u) : (Π i, α i) ≃ α 0 × α 1 :=
{ to_fun := λ f, (f 0, f 1),
  inv_fun := λ p, fin.cons p.1 $ fin.cons p.2 fin_zero_elim,
  left_inv := λ f, funext $ fin.forall_fin_two.2 ⟨rfl, rfl⟩,
  right_inv := λ ⟨x, y⟩, rfl }

lemma fin.preimage_apply_01_prod {α : fin 2 → Type u} (s : set (α 0)) (t : set (α 1)) :
  (λ f : Π i, α i, (f 0, f 1)) ⁻¹' (s ×ˢ t) =
    set.pi set.univ (fin.cons s $ fin.cons t fin.elim0) :=
begin
  ext f,
  have : (fin.cons s (fin.cons t fin.elim0) : Π i, set (α i)) 1 = t := rfl,
  simp [fin.forall_fin_two, this]
end

lemma fin.preimage_apply_01_prod' {α : Type u} (s t : set α) :
  (λ f : fin 2 → α, (f 0, f 1)) ⁻¹' (s ×ˢ t) = set.pi set.univ ![s, t] :=
fin.preimage_apply_01_prod s t

/-- A product space `α × β` is equivalent to the space `Π i : fin 2, γ i`, where
`γ = fin.cons α (fin.cons β fin_zero_elim)`. See also `pi_fin_two_equiv` and
`fin_two_arrow_equiv`. -/
@[simps {fully_applied := ff }] def prod_equiv_pi_fin_two (α β : Type u) :
  α × β ≃ Π i : fin 2, ![α, β] i :=
(pi_fin_two_equiv (fin.cons α (fin.cons β fin_zero_elim))).symm

/-- The space of functions `fin 2 → α` is equivalent to `α × α`. See also `pi_fin_two_equiv` and
`prod_equiv_pi_fin_two`. -/
@[simps { fully_applied := ff }] def fin_two_arrow_equiv (α : Type*) : (fin 2 → α) ≃ α × α :=
{ inv_fun := λ x, ![x.1, x.2],
  .. pi_fin_two_equiv (λ _, α) }

/-- `Π i : fin 2, α i` is order equivalent to `α 0 × α 1`. See also `order_iso.fin_two_arrow_equiv`
for a non-dependent version. -/
def order_iso.pi_fin_two_iso (α : fin 2 → Type u) [Π i, preorder (α i)] :
  (Π i, α i) ≃o α 0 × α 1 :=
{ to_equiv := pi_fin_two_equiv α,
  map_rel_iff' := λ f g, iff.symm fin.forall_fin_two }

/-- The space of functions `fin 2 → α` is order equivalent to `α × α`. See also
`order_iso.pi_fin_two_iso`. -/
def order_iso.fin_two_arrow_iso (α : Type*) [preorder α] : (fin 2 → α) ≃o α × α :=
{ to_equiv := fin_two_arrow_equiv α, .. order_iso.pi_fin_two_iso (λ _, α) }

/-- The 'identity' equivalence between `fin n` and `fin m` when `n = m`. -/
def fin_congr {n m : ℕ} (h : n = m) : fin n ≃ fin m :=
(fin.cast h).to_equiv

@[simp] lemma fin_congr_apply_mk {n m : ℕ} (h : n = m) (k : ℕ) (w : k < n) :
  fin_congr h ⟨k, w⟩ = ⟨k, by { subst h, exact w }⟩ :=
rfl

@[simp] lemma fin_congr_symm {n m : ℕ} (h : n = m) :
  (fin_congr h).symm = fin_congr h.symm := rfl

@[simp] lemma fin_congr_apply_coe {n m : ℕ} (h : n = m) (k : fin n) :
  (fin_congr h k : ℕ) = k :=
by { cases k, refl, }

lemma fin_congr_symm_apply_coe {n m : ℕ} (h : n = m) (k : fin m) :
  ((fin_congr h).symm k : ℕ) = k :=
by { cases k, refl, }

/-- An equivalence that removes `i` and maps it to `none`.
This is a version of `fin.pred_above` that produces `option (fin n)` instead of
mapping both `i.cast_succ` and `i.succ` to `i`. -/
def fin_succ_equiv' {n : ℕ} (i : fin (n + 1)) :
  fin (n + 1) ≃ option (fin n) :=
{ to_fun := i.insert_nth none some,
  inv_fun := λ x, x.cases_on' i (fin.succ_above i),
  left_inv := λ x, fin.succ_above_cases i (by simp) (λ j, by simp) x,
  right_inv := λ x, by cases x; dsimp; simp }

@[simp] lemma fin_succ_equiv'_at {n : ℕ} (i : fin (n + 1)) :
  (fin_succ_equiv' i) i = none := by simp [fin_succ_equiv']

@[simp] lemma fin_succ_equiv'_succ_above {n : ℕ} (i : fin (n + 1)) (j : fin n) :
  fin_succ_equiv' i (i.succ_above j) = some j :=
@fin.insert_nth_apply_succ_above n (λ _, option (fin n)) i _ _ _

lemma fin_succ_equiv'_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
  (fin_succ_equiv' i) m.cast_succ = some m :=
by rw [← fin.succ_above_below _ _ h, fin_succ_equiv'_succ_above]

lemma fin_succ_equiv'_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
  (fin_succ_equiv' i) m.succ = some m :=
by rw [← fin.succ_above_above _ _ h, fin_succ_equiv'_succ_above]

@[simp] lemma fin_succ_equiv'_symm_none {n : ℕ} (i : fin (n + 1)) :
  (fin_succ_equiv' i).symm none = i := rfl

@[simp] lemma fin_succ_equiv'_symm_some {n : ℕ} (i : fin (n + 1)) (j : fin n) :
  (fin_succ_equiv' i).symm (some j) = i.succ_above j :=
rfl

lemma fin_succ_equiv'_symm_some_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
  (fin_succ_equiv' i).symm (some m) = m.cast_succ :=
fin.succ_above_below i m h

lemma fin_succ_equiv'_symm_some_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
  (fin_succ_equiv' i).symm (some m) = m.succ :=
fin.succ_above_above i m h

lemma fin_succ_equiv'_symm_coe_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
  (fin_succ_equiv' i).symm m = m.cast_succ :=
fin_succ_equiv'_symm_some_below h

lemma fin_succ_equiv'_symm_coe_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
  (fin_succ_equiv' i).symm m = m.succ :=
fin_succ_equiv'_symm_some_above h

/-- Equivalence between `fin (n + 1)` and `option (fin n)`.
This is a version of `fin.pred` that produces `option (fin n)` instead of
requiring a proof that the input is not `0`. -/
def fin_succ_equiv (n : ℕ) : fin (n + 1) ≃ option (fin n) :=
fin_succ_equiv' 0

@[simp] lemma fin_succ_equiv_zero {n : ℕ} :
  (fin_succ_equiv n) 0 = none :=
by cases n; refl

@[simp] lemma fin_succ_equiv_succ {n : ℕ} (m : fin n):
  (fin_succ_equiv n) m.succ = some m :=
fin_succ_equiv'_above (fin.zero_le _)

@[simp] lemma fin_succ_equiv_symm_none {n : ℕ} :
  (fin_succ_equiv n).symm none = 0 :=
fin_succ_equiv'_symm_none _

@[simp] lemma fin_succ_equiv_symm_some {n : ℕ} (m : fin n) :
  (fin_succ_equiv n).symm (some m) = m.succ :=
congr_fun fin.succ_above_zero m

@[simp] lemma fin_succ_equiv_symm_coe {n : ℕ} (m : fin n) :
  (fin_succ_equiv n).symm m = m.succ :=
fin_succ_equiv_symm_some m

/-- The equiv version of `fin.pred_above_zero`. -/
lemma fin_succ_equiv'_zero {n : ℕ} :
  fin_succ_equiv' (0 : fin (n + 1)) = fin_succ_equiv n := rfl

/-- `equiv` between `fin (n + 1)` and `option (fin n)` sending `fin.last n` to `none` -/
def fin_succ_equiv_last {n : ℕ} : fin (n + 1) ≃ option (fin n) :=
fin_succ_equiv' (fin.last n)

@[simp] lemma fin_succ_equiv_last_cast_succ {n : ℕ} (i : fin n) :
  fin_succ_equiv_last i.cast_succ = some i :=
fin_succ_equiv'_below i.2

@[simp] lemma fin_succ_equiv_last_last {n : ℕ} :
  fin_succ_equiv_last (fin.last n) = none :=
by simp [fin_succ_equiv_last]

@[simp] lemma fin_succ_equiv_last_symm_some {n : ℕ} (i : fin n) :
  fin_succ_equiv_last.symm (some i) = i.cast_succ :=
fin_succ_equiv'_symm_some_below i.2

@[simp] lemma fin_succ_equiv_last_symm_coe {n : ℕ} (i : fin n) :
  fin_succ_equiv_last.symm ↑i = i.cast_succ :=
fin_succ_equiv'_symm_some_below i.2

@[simp] lemma fin_succ_equiv_last_symm_none {n : ℕ}  :
  fin_succ_equiv_last.symm none = fin.last n :=
fin_succ_equiv'_symm_none _

/-- Equivalence between `fin m ⊕ fin n` and `fin (m + n)` -/
def fin_sum_fin_equiv : fin m ⊕ fin n ≃ fin (m + n) :=
{ to_fun := sum.elim (fin.cast_add n) (fin.nat_add m),
  inv_fun := λ i, @fin.add_cases m n (λ _, fin m ⊕ fin n) sum.inl sum.inr i,
  left_inv := λ x, by { cases x with y y; dsimp; simp },
  right_inv := λ x, by refine fin.add_cases (λ i, _) (λ i, _) x; simp }

@[simp] lemma fin_sum_fin_equiv_apply_left (i : fin m) :
  (fin_sum_fin_equiv (sum.inl i) : fin (m + n)) = fin.cast_add n i := rfl

@[simp] lemma fin_sum_fin_equiv_apply_right (i : fin n) :
  (fin_sum_fin_equiv (sum.inr i) : fin (m + n)) = fin.nat_add m i := rfl

@[simp] lemma fin_sum_fin_equiv_symm_apply_cast_add (x : fin m) :
  fin_sum_fin_equiv.symm (fin.cast_add n x) = sum.inl x :=
fin_sum_fin_equiv.symm_apply_apply (sum.inl x)

@[simp] lemma fin_sum_fin_equiv_symm_apply_nat_add (x : fin n) :
  fin_sum_fin_equiv.symm (fin.nat_add m x) = sum.inr x :=
fin_sum_fin_equiv.symm_apply_apply (sum.inr x)

/-- The equivalence between `fin (m + n)` and `fin (n + m)` which rotates by `n`. -/
def fin_add_flip : fin (m + n) ≃ fin (n + m) :=
(fin_sum_fin_equiv.symm.trans (equiv.sum_comm _ _)).trans fin_sum_fin_equiv

@[simp] lemma fin_add_flip_apply_cast_add (k : fin m) (n : ℕ) :
  fin_add_flip (fin.cast_add n k) = fin.nat_add n k :=
by simp [fin_add_flip]

@[simp] lemma fin_add_flip_apply_nat_add (k : fin n) (m : ℕ) :
  fin_add_flip (fin.nat_add m k) = fin.cast_add m k :=
by simp [fin_add_flip]

@[simp] lemma fin_add_flip_apply_mk_left {k : ℕ} (h : k < m)
  (hk : k < m + n := nat.lt_add_right k m n h)
  (hnk : n + k < n + m := add_lt_add_left h n) :
  fin_add_flip (⟨k, hk⟩ : fin (m + n)) = ⟨n + k, hnk⟩ :=
by convert fin_add_flip_apply_cast_add ⟨k, h⟩ n

@[simp] lemma fin_add_flip_apply_mk_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
  fin_add_flip (⟨k, h₂⟩ : fin (m + n)) = ⟨k - m, tsub_le_self.trans_lt $ add_comm m n ▸ h₂⟩ :=
begin
  convert fin_add_flip_apply_nat_add ⟨k - m, (tsub_lt_iff_right h₁).2 _⟩ m,
  { simp [add_tsub_cancel_of_le h₁] },
  { rwa add_comm }
end

/-- Rotate `fin n` one step to the right. -/
def fin_rotate : Π n, equiv.perm (fin n)
| 0 := equiv.refl _
| (n+1) := fin_add_flip.trans (fin_congr (add_comm _ _))

lemma fin_rotate_of_lt {k : ℕ} (h : k < n) :
  fin_rotate (n+1) ⟨k, lt_of_lt_of_le h (nat.le_succ _)⟩ = ⟨k + 1, nat.succ_lt_succ h⟩ :=
begin
  dsimp [fin_rotate],
  simp [h, add_comm],
end

lemma fin_rotate_last' : fin_rotate (n+1) ⟨n, lt_add_one _⟩ = ⟨0, nat.zero_lt_succ _⟩ :=
begin
  dsimp [fin_rotate],
  rw fin_add_flip_apply_mk_right,
  simp,
end

lemma fin_rotate_last : fin_rotate (n+1) (fin.last _) = 0 :=
fin_rotate_last'

lemma fin.snoc_eq_cons_rotate {α : Type*} (v : fin n → α) (a : α) :
  @fin.snoc _ (λ _, α) v a = (λ i, @fin.cons _ (λ _, α) a v (fin_rotate _ i)) :=
begin
  ext ⟨i, h⟩,
  by_cases h' : i < n,
  { rw [fin_rotate_of_lt h', fin.snoc, fin.cons, dif_pos h'],
    refl, },
  { have h'' : n = i,
    { simp only [not_lt] at h', exact (nat.eq_of_le_of_lt_succ h' h).symm, },
    subst h'',
    rw [fin_rotate_last', fin.snoc, fin.cons, dif_neg (lt_irrefl _)],
    refl, }
end

@[simp] lemma fin_rotate_zero : fin_rotate 0 = equiv.refl _ := rfl

@[simp] lemma fin_rotate_one : fin_rotate 1 = equiv.refl _ :=
subsingleton.elim _ _

@[simp] lemma fin_rotate_succ_apply {n : ℕ} (i : fin n.succ) :
  fin_rotate n.succ i = i + 1 :=
begin
  cases n,
  { simp },
  rcases i.le_last.eq_or_lt with rfl|h,
  { simp [fin_rotate_last] },
  { cases i,
    simp only [fin.lt_iff_coe_lt_coe, fin.coe_last, fin.coe_mk] at h,
    simp [fin_rotate_of_lt h, fin.eq_iff_veq, fin.add_def, nat.mod_eq_of_lt (nat.succ_lt_succ h)] },
end

@[simp] lemma fin_rotate_apply_zero {n : ℕ} : fin_rotate n.succ 0 = 1 :=
by rw [fin_rotate_succ_apply, zero_add]

lemma coe_fin_rotate_of_ne_last {n : ℕ} {i : fin n.succ} (h : i ≠ fin.last n) :
  (fin_rotate n.succ i : ℕ) = i + 1 :=
begin
  rw fin_rotate_succ_apply,
  have : (i : ℕ) < n := lt_of_le_of_ne (nat.succ_le_succ_iff.mp i.2) (fin.coe_injective.ne h),
  exact fin.coe_add_one_of_lt this
end

lemma coe_fin_rotate {n : ℕ} (i : fin n.succ) :
  (fin_rotate n.succ i : ℕ) = if i = fin.last n then 0 else i + 1 :=
by rw [fin_rotate_succ_apply, fin.coe_add_one i]

/-- Equivalence between `fin m × fin n` and `fin (m * n)` -/
@[simps]
def fin_prod_fin_equiv : fin m × fin n ≃ fin (m * n) :=
{ to_fun := λ x, ⟨x.2 + n * x.1,
    calc x.2.1 + n * x.1.1 + 1
        = x.1.1 * n + x.2.1 + 1 : by ac_refl
    ... ≤ x.1.1 * n + n : nat.add_le_add_left x.2.2 _
    ... = (x.1.1 + 1) * n : eq.symm $ nat.succ_mul _ _
    ... ≤ m * n : nat.mul_le_mul_right _ x.1.2⟩,
  inv_fun := λ x, (x.div_nat, x.mod_nat),
  left_inv := λ ⟨x, y⟩,
    have H : 0 < n, from nat.pos_of_ne_zero $ λ H, nat.not_lt_zero y.1 $ H ▸ y.2,
    prod.ext
      (fin.eq_of_veq $ calc
              (y.1 + n * x.1) / n
            = y.1 / n + x.1 : nat.add_mul_div_left _ _ H
        ... = 0 + x.1 : by rw nat.div_eq_of_lt y.2
        ... = x.1 : nat.zero_add x.1)
      (fin.eq_of_veq $ calc
              (y.1 + n * x.1) % n
            = y.1 % n : nat.add_mul_mod_self_left _ _ _
        ... = y.1 : nat.mod_eq_of_lt y.2),
  right_inv := λ x, fin.eq_of_veq $ nat.mod_add_div _ _ }

/-- Promote a `fin n` into a larger `fin m`, as a subtype where the underlying
values are retained. This is the `order_iso` version of `fin.cast_le`. -/
@[simps apply symm_apply]
def fin.cast_le_order_iso {n m : ℕ} (h : n ≤ m) : fin n ≃o {i : fin m // (i : ℕ) < n} :=
{ to_fun := λ i, ⟨fin.cast_le h i, by simpa using i.is_lt⟩,
  inv_fun := λ i, ⟨i, i.prop⟩,
  left_inv := λ _, by simp,
  right_inv := λ _, by simp,
  map_rel_iff' := λ _ _, by simp }

/-- `fin 0` is a subsingleton. -/
instance subsingleton_fin_zero : subsingleton (fin 0) :=
fin_zero_equiv.subsingleton

/-- `fin 1` is a subsingleton. -/
instance subsingleton_fin_one : subsingleton (fin 1) :=
fin_one_equiv.subsingleton

author: saisurbehera

repo: mathProof


text:
import logic.basic

/-
  **Implementation of Dynamic Epistemic Logic**
-/

variable σ : ℕ

/-
  Inductive types for actions and formulas and notations
-/

inductive action : Type
| skip : fin σ → action
| seq : action → action → action

notation `PDL∅` := action.skip
notation act1 `;` act2 := action.seq act1 act2

inductive const : Type
| const : fin σ -> const
| encr : const -> const -> const
| tupl : const -> const -> const

inductive agent : Type
| agent : fin σ -> agent

inductive form : Type
| atom : fin σ → form
| const : const σ → form
| bot : form
| impl : form → form → form
| k : form → form
| b : form → form
| pdl : form → action σ → form

prefix `#` := form.atom
notation `c` := form.const
notation `⊥` := form.bot
infix `⊃` := form.impl
notation `¬`:40 p := form.impl p (form.bot)
notation p `&` q := ¬(p ⊃ ¬q)
notation p `or` q := ¬(¬p & ¬q)
notation `K□`:80 p := form.k p
notation `K◇`:80 := λ p, ¬(K□ (¬ p))
notation `B□`:80 p := form.b p
notation `B◇`:80 := λ p, ¬(B□ (¬ p))
notation `PDL□`:80 := form.pdl
-- notation `PDL◇`:80 p (act) := λ p, ¬ (PDL□ (¬p) (act))

variables { p q : fin σ }
variables { act1 act2 : fin σ }
#check PDL□ (#p) (PDL∅ act1)

/-
  Context definition
-/

@[reducible]
def ctx (σ : nat) : Type := set (form σ)

notation `·` := {}
notation Γ ` ∪ ` p := set.insert p Γ

#check · ∪ (#p)

/-
  Proof system
-/

open form
open action

inductive Proof : ctx σ → form σ → Prop
-- Propositional logic
| ax { Γ } { p } (h : p ∈ Γ) : Proof Γ p
| pl1 { Γ } { p q } : Proof Γ (p ⊃ (q ⊃ p))
| pl2 { Γ } { p q r } : Proof Γ ((p ⊃ (q ⊃ r)) ⊃ ((p ⊃ q) ⊃ (p ⊃ r)))
| pl3 { Γ } { p q } : Proof Γ (((¬p) ⊃ ¬q) ⊃ (((¬p) ⊃ q) ⊃ p))
-- Constant axioms
| c₁ { Γ } { t k : const σ } : Proof Γ $ ((c t) ⊃ (c k)) ⊃ c (const.encr t k)
| c₂ { Γ } { t k : const σ } : Proof Γ $ ((c $ const.encr t k) ⊃ (c k)) ⊃ c t
| c₃ { Γ } { m₁ m₂ : const σ } : Proof Γ $ (c m₁ ⊃ c m₂) ⊃ c (m₁.tupl m₂)
-- (h₁ :  Proof Γ $ const t) (h₂ : Proof Γ $ const k) : Proof Γ $ const $ const.encr t k
-- S5
| kk { Γ } { p q } : Proof Γ ((K□(p ⊃ q)) ⊃ (K□p ⊃ K□q))
| t { Γ } { p } : Proof Γ (K□p ⊃ p)
| s4 { Γ } { p } : Proof Γ (K□p ⊃ K□K□p)
| s5 { Γ } { p } : Proof Γ (¬(K□p) ⊃ K□(¬K□p))
-- KD
| bk { Γ } { p q } : Proof Γ (B□(p ⊃ q) ⊃ (B□p ⊃ B□q))
| dox { Γ } { p } : Proof Γ (B□p ⊃ B◇p)
| kb { Γ } { p } : Proof Γ (K□p ⊃ B□p)
-- PDL
| pdlk { Γ } { p q } (α : action σ) : Proof Γ (PDL□(p ⊃ q) α ⊃ (PDL□p α ⊃ PDL□q α))
-- Deductive rules
| mp { Γ } { p q } (hpq : Proof Γ (p ⊃ q)) (hp : Proof Γ p) : Proof Γ q
| knec { Γ } { p } (h : Proof · p) : Proof Γ (K□p)
| bnec { Γ } { p } (h : Proof · p) : Proof Γ (B□p)
| gen { Γ } { p } (α : action σ) (h : Proof · p) : Proof Γ (PDL□p α)

notation Γ `-` σ ` ⊢κ ` p := Proof σ Γ p
notation Γ `-` σ ` ⊬κ ` p := Proof σ Γ p → false

/-
  Some lemmas
-/

open Proof

variable { S : ctx σ }
#check  S-σ ⊢κ (#p)

lemma idd {σ : ℕ} { p : form σ } { Γ : ctx σ } : Γ-σ ⊢κ (p ⊃ p) := mp (mp (@pl2 σ Γ p (p ⊃ p) p) pl1) pl1

lemma cut {σ : ℕ} {Γ : ctx σ} {p q r : form σ} :
  (Γ-σ ⊢κ p ⊃ q) → (Γ-σ ⊢κ q ⊃ r) → (Γ-σ ⊢κ p ⊃ r) :=
λ hpq hqr, mp (mp pl2 (mp pl1 hqr)) hpq

lemma dne { σ : ℕ } {p : form σ} {Γ : ctx σ} :
  Γ-σ ⊢κ (¬¬p) ⊃ p :=
have h : Γ-σ ⊢κ (¬¬p) ⊃ ((¬p) ⊃ (¬p)) := mp pl1 idd,
mp (mp pl2 (cut pl1 pl3)) h

/-
  Deduction theorem
-/

theorem deduction { σ : ℕ } { Γ : ctx σ } { p q : form σ } { α : action σ } : ((Γ ∪ p)-σ ⊢κ q) → (Γ-σ ⊢κ p ⊃ q) :=
begin
  generalize eq : (Γ ∪ p) = Γ',
  intro h,
  induction h; subst eq,
  {
    repeat {cases h_h},
    exact idd,
    {
      exact mp pl1 (ax h_h)
    }
  },
  { exact mp pl1 pl1 },
  { exact mp pl1 pl2 },
  { exact mp pl1 pl3 },
  { exact mp pl1 c₁ },
  { exact mp pl1 c₂ },
  { exact mp pl1 c₃ },
  { exact mp pl1 kk },
  { exact mp pl1 t },
  { exact mp pl1 s4 },
  { exact mp pl1 s5 },
  { exact mp pl1 bk },
  { exact mp pl1 dox },
  { exact mp pl1 kb },
  { exact mp pl1 (pdlk h_α) },
  { apply mp,
    { exact (mp pl2 (h_ih_hpq rfl)) },
    { exact h_ih_hp rfl }
  },
  { exact mp pl1 (knec h_h) },
  { exact mp pl1 (bnec h_h) },
  { exact mp pl1 (gen h_α h_h) }
end

/-
  Basic Semantics
-/

open form classical

@[reducible]
def world (σ : ℕ) := ctx σ

/-
  Models
-/

structure model :=
  (worlds : set (world σ))
  (kaccess : world σ → world σ → bool)
  (baccess : world σ → world σ → bool)
  (pdlaccess : world σ → world σ → bool)
  (val : fin σ → world σ → bool)
  (valc : const σ -> world σ -> bool)
  -- R_K S5 relation
  (refl : ∀ w ∈ worlds, kaccess w w = tt)
  (symm : ∀ w ∈ worlds, ∀ v ∈ worlds, kaccess w v = tt → kaccess v w = tt)
  (trans : ∀ w ∈ worlds, ∀ v ∈ worlds, ∀ u ∈ worlds, kaccess w v = tt → kaccess v u = tt → kaccess w u = tt)
  -- R_B is a serial relation
  (serial : ∀ w ∈ worlds, ∃ v ∈ worlds, baccess w v = tt)
  (RKB : ∀ w ∈ worlds, ∀ v ∈ worlds, kaccess w v = tt → baccess w v = tt)

local attribute [instance] prop_decidable

noncomputable def forces_form { σ : ℕ } (M : model σ) : form σ → world σ → bool
| (#p) := λ w, M.val p w
| (c p) := λ w, M.valc p w
| (⊥) := λ w, ff
| (p ⊃ q) := λ w, (bnot (forces_form p w)) || (forces_form q w)
| (K□ p) := λ w, if (∀ v ∈ M.worlds, w ∈ M.worlds → M.kaccess w v = tt → forces_form p v = tt) then tt else ff
| (B□ p) := λ w, if (∀ v ∈ M.worlds, w ∈ M.worlds → M.baccess w v = tt → forces_form p v = tt) then tt else ff
| (PDL□ p (α : action σ)) := λ w, if (∀ v ∈ M.worlds, w ∈ M.worlds → M.pdlaccess w v = tt → forces_form p v = tt) then tt else ff

notation w `⊩` `⦃` M `⦄ ` p := forces_form M p w

axiom c₁_is_true { σ : ℕ } (M : model σ) (w : world σ) (t k : const σ) : (w⊩⦃M⦄ c t⊃c k⊃c (t.encr k)) = tt
axiom c₂_is_true { σ : ℕ } (M : model σ) (w : world σ) (t k : const σ) : (w⊩⦃M⦄ c (t.encr k) ⊃ c k ⊃ c t) = tt
axiom c₃_is_true { σ : ℕ } (M : model σ) (w : world σ) (m₁ m₂ : const σ) : (w⊩⦃M⦄ c m₁ ⊃ c m₂ ⊃ c (m₁.tupl m₂)) = tt

noncomputable def forces_ctx { σ : ℕ } (M : model σ) (Γ : ctx σ) : world σ → bool :=
  λ w, if (∀ p, p ∈ Γ → forces_form M p w = tt) then tt else ff

notation w `⊩` `⦃` M `⦄ ` p := forces_ctx M p w

inductive sem_csq { σ : ℕ } (Γ : ctx σ) (p : form σ) : Prop
| is_true (m : ∀ (M : model σ) (w ∈ M.worlds), ((w ⊩ ⦃M⦄ Γ) = tt) → (w ⊩ ⦃M⦄ p) = tt) : sem_csq

notation Γ `-` σ ` ⊨κ ` p := @sem_csq σ Γ p

/-
  Some lemmas
-/

lemma ctx_tt_iff_mem_tt { σ : ℕ } {Γ : ctx σ} {M : model σ} {w : world σ} :
  (w ⊩⦃M⦄ Γ) = tt ↔ (∀ p, p ∈ Γ → (w ⊩⦃M⦄ p) = tt) := sorry
-- begin
--   unfold forces_ctx,
--   induction (classical.prop_decidable _),
--   { apply iff.intro,
--     simp, intro,
--     simp, assumption },
--   { simp }
-- end

lemma ctx_tt_to_mem_tt { σ : ℕ } {Γ : ctx σ} {M : model σ } {w : world σ} {p : form σ} :
  (w ⊩⦃M⦄ Γ) = tt → p ∈ Γ → (w ⊩⦃M⦄ p) = tt :=
by intro; apply ctx_tt_iff_mem_tt.1; assumption

axiom impl_iff_implies_v2 :
  ∀ (σ : ℕ) {M : model σ} {w : world σ} {p q : form σ},
    (λ (x_1 : world σ) (x_2 : model σ) (x_3 : form σ), x_1⊩⦃x_2⦄ x_3) w M (p⊃q) = tt ↔
      ↥((λ (x_1 : world σ) (x_2 : model σ) (x_3 : form σ), x_1⊩⦃x_2⦄ x_3) w M p) →
      ↥((λ (x_1 : world σ) (x_2 : model σ) (x_3 : form σ), x_1⊩⦃x_2⦄ x_3) w M q)

lemma impl_iff_implies {M : model σ } {w : world σ} {p q : form σ} :
  (w ⊩⦃M⦄ p ⊃ q) = tt ↔ ((w ⊩⦃M⦄ p) → (w ⊩⦃M⦄ q)) :=
by unfold forces_form; induction (forces_form M p w); repeat {induction (forces_form M q w), simp, simp}

lemma impl_tt_iff_ff_or_tt { σ : ℕ } {M : model σ } {w : world σ} {p q : form σ} :
  (w ⊩⦃M⦄ p ⊃ q) = tt ↔ ¬(w ⊩⦃M⦄ p) ∨ (w ⊩⦃M⦄ q) = tt :=
by unfold forces_form; induction (forces_form M p w); repeat {induction (forces_form M q w), simp, simp}

lemma ff_or_tt_and_tt_implies_tt_right { σ : ℕ } {M : model σ} {w : world σ} {p q : form σ} :
  (¬(w ⊩⦃M⦄ p) ∨ (w ⊩⦃M⦄ q) = tt) → (w ⊩⦃M⦄ p) = tt → (w ⊩⦃M⦄ q) = tt := sorry
-- by simp; induction (forces_form M p w); repeat {induction (forces_form M q w), simp, simp}

lemma bot_is_insatisf { σ : ℕ }{w : world σ} :
  ¬ ∃ (M : model σ ), (w ⊩⦃M⦄ ⊥) = tt :=
by intro h; cases h; exact (bool.no_confusion h_h)

lemma is_true_pl1 { σ : ℕ }{M : model σ } {w : world σ} {p q : form σ} :
  (w ⊩⦃M⦄ p ⊃ (q ⊃ p)) = tt :=
begin
  apply impl_iff_implies.2,
  intro, apply impl_iff_implies.2,
  intro, assumption
end

lemma is_true_pl2 { σ : ℕ } {M : model σ } {w : world σ} {p q r : form σ} :
  (w ⊩⦃M⦄ (p ⊃ (q ⊃ r)) ⊃ ((p ⊃ q) ⊃ (p ⊃ r))) = tt :=
begin
  apply impl_iff_implies.2,
  intro h₁, apply impl_iff_implies.2,
  intro h₂, apply impl_iff_implies.2,
  intro h₃, apply impl_iff_implies.1 ((impl_iff_implies.1 h₁) h₃),
  apply impl_iff_implies.1 h₂, assumption
end

lemma is_true_pl3 { σ : ℕ } { M : model σ } {w : world σ} {p q : form σ} :
  (w ⊩⦃M⦄ ((¬p) ⊃ ¬q) ⊃ (((¬p) ⊃ q) ⊃ p)) = tt :=
begin
  unfold forces_form,
  induction (forces_form M p w),
  repeat { induction (forces_form M q w), repeat {simp} },
end

lemma nec_impl_to_nec_to_nec { σ : ℕ } {M : model σ } {w : world σ} {p q : form σ} :
  (w ⊩⦃M⦄ K□ (p ⊃ q)) = tt → (w ⊩⦃M⦄ K□p) = tt → (w ⊩⦃M⦄ K□q) = tt := sorry
-- begin
--   unfold forces_form, simp at *, intros hlpq hlp v wmem vmem rwv,
--   apply ff_or_tt_and_tt_implies_tt_right,
--     rw or.comm, simp, apply hlpq, repeat {assumption},
--     apply hlp, repeat {assumption},
-- end

lemma knec_impl_to_knec_impl_knec { σ : ℕ } {M : model σ } {w : world σ} {p q : form σ} :
  (w ⊩⦃M⦄ K□(p ⊃ q)) = tt → (¬(w ⊩⦃M⦄ K□p) ∨ (w ⊩⦃M⦄ K□q) = tt) := sorry

lemma bnec_impl_to_bnec_impl_bnec  { σ : ℕ } {M : model σ } {w : world σ} {p q : form σ} :
  (w ⊩⦃M⦄ B□(p ⊃ q)) = tt → (¬(w ⊩⦃M⦄ B□p) ∨ (w ⊩⦃M⦄ B□q) = tt) := sorry

lemma gen_impl_to_gen_impl_gen  { σ : ℕ } {M : model σ } {w : world σ} { α : action σ } {p q : form σ} :
  (w ⊩⦃M⦄ PDL□(p ⊃ q) α) = tt → (¬(w ⊩⦃M⦄ PDL□ p α) ∨ (w ⊩⦃M⦄ PDL□ q α) = tt) := sorry

lemma is_true_kk { σ : ℕ } {M : model σ} {w : world σ} {p q : form σ} :
  (w⊩⦃M⦄ (K□p⊃q)⊃K□p⊃K□q) = tt :=
impl_iff_implies_v2 (λ h, impl_tt_iff_ff_or_tt.2 (knec_impl_to_knec_impl_knec h))

axiom is_true_dox { σ : ℕ } { M : model σ } { w : world σ } { p q : form σ } :
  (w⊩⦃M⦄ B□p⊃¬B□¬p) = tt

axiom is_true_kb {σ : ℕ} {M : model σ } {w : world σ} {p q : form σ} :
  (w⊩⦃M⦄ B□(p⊃q)⊃(B□p⊃B□q)) = tt

axiom is_true_kpdl {σ : ℕ} {M : model σ } {w : world σ} {α : action σ} {p q : form σ} :
  (w ⊩⦃M⦄ (PDL□(p ⊃ q) α) ⊃ ((PDL□ p α) ⊃ PDL□ q α)) = tt

lemma nec_to_tt {σ : ℕ} {M : model σ } {w : world σ} {wm : w ∈ M.worlds} {p : form σ} :
  (w ⊩⦃M⦄ K□p) = tt → (w ⊩⦃M⦄ p) = tt :=
begin
  unfold forces_form, simp at *,
  intro f, apply f, repeat {assumption},
  apply M.refl, assumption
end

axiom K_implies_B {σ: ℕ}
(M: model σ) (w: world σ) (wm: w ∈ M.worlds)
(p: form σ) (f₁: world σ) (f₂: f₁ ∈ M.worlds)
(f₃: w ∈ M.worlds) (f₄: M.kaccess w f₁ = tt) : (f₁⊩⦃M⦄ p) = ff ∨ ∀ (v : world σ), v ∈ M.worlds → f₁ ∈ M.worlds → M.baccess f₁ v = tt → (v⊩⦃M⦄ p) = tt

lemma is_true_kd { σ : ℕ } { M : model σ } { w : world σ } { wm : w ∈ M.worlds } { p : form σ } :
  (w⊩⦃M⦄ K□p⊃B□p) = tt :=
begin
  unfold forces_form,
  simp at *,
  intros f₁ f₂ f₃ f₄,
  exact K_implies_B M w wm p f₁ f₂ f₃ f₄
end

axiom is_true_t {σ : ℕ} {M : model σ} {w : world σ} {w ∈ M.worlds} {p : form σ} :
  (w⊩⦃M⦄ K□p⊃p) = tt

lemma nec_to_nec_of_nec {σ : ℕ} {M : model σ} {w : world σ} {p : form σ} :
  (w ⊩⦃M⦄ K□p) = tt → (w ⊩⦃M⦄ K□K□p) = tt :=
begin
  unfold forces_form, simp at *,
  intros f v wmem vmem rwv u vmem' umem rvu,
  apply f, repeat {assumption},
  refine M.trans _ _ _ _ _ _ rwv rvu,
  repeat {assumption}
end

axiom neg_nec_to_neg_of_neg_nec_helper {σ : ℕ}
(M: model σ) (w: world σ) (p: form σ)
(f: ¬∀ (v : world σ), v ∈ M.worlds → w ∈ M.worlds → M.kaccess w v = tt → (v⊩⦃M⦄ p) = tt)
(v: world σ) (vmem: v ∈ M.worlds) (wmem: w ∈ M.worlds)
(rwv: M.kaccess w v = tt) (u: ∀ (v_1 : world σ), v_1 ∈ M.worlds → v ∈ M.worlds → M.kaccess v v_1 = tt → (v_1⊩⦃M⦄ p) = tt)
: ∀ (v : world σ), v ∈ M.worlds → w ∈ M.worlds → M.kaccess w v = tt → (v⊩⦃M⦄ p) = tt

lemma neg_nec_to_neg_of_neg_nec { σ : ℕ } { M : model σ } { w : world σ } { p : form σ } :
  (w ⊩ ⦃M⦄ ¬K□p) = tt → (w ⊩ ⦃M⦄ K□(¬K□p)) = tt :=
begin
  unfold forces_form, simp at *,
  intros f v vmem wmem rwv u,
  apply f,
  repeat {assumption},
  apply neg_nec_to_neg_of_neg_nec_helper M w p f v vmem wmem rwv,
  sorry
end

axiom is_true_s4 {σ : ℕ} {M : model σ} {w : world σ} {p : form σ} :
  (w⊩⦃M⦄ K□p⊃K□K□p) = tt

axiom is_true_s5 {σ : ℕ} {M : model σ} {w : world σ} {p : form σ} :
  (w ⊩⦃M⦄ ¬(K□p) ⊃ K□(¬K□p)) = tt

lemma empty_ctx_tt {σ : ℕ } {M : model σ } {w : world σ} :
  (w ⊩⦃M⦄ ·) = tt := by sorry

/-
  Soundness
-/

theorem soundness { σ : ℕ } { Γ : ctx σ } { p : form σ } : (Γ-σ ⊢κ p) → (Γ-σ ⊨κ p) :=
begin
  intro h,
  induction h,
  {
    apply sem_csq.is_true,
    intros,
    apply ctx_tt_to_mem_tt,
    repeat { assumption }
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_pl1
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_pl2
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_pl3
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    exact c₁_is_true M w h_t h_k
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    exact c₂_is_true M w h_t h_k
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    exact c₃_is_true M w h_m₁ h_m₂
  },
  { apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_kk
  },
  { apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_t,
    repeat {assumption}
  },
  { apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_s4
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_s5
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_kb
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_dox,
    repeat { assumption }
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_kd,
    repeat { assumption }
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    apply is_true_kpdl
  },
  { apply sem_csq.is_true,
    induction h_ih_hpq,
    induction h_ih_hp,
    intros M w wmem ctt,
    revert h_ih_hpq,
    unfold forces_form, simp,
    intro hpq,
    cases (hpq M w wmem ctt),
    { assumption },
    { exfalso,
      apply tt_eq_ff_eq_false,
      rw eq.symm (h_ih_hp M w wmem ctt),
      assumption
    }
  },
  {
    apply sem_csq.is_true,
    intros M w wmem ctt,
    unfold forces_form, simp,
    induction h_ih,
    intros v vmem wmem rwv,
    apply h_ih, assumption,
    apply empty_ctx_tt
  },
  { apply sem_csq.is_true,
    intros M w wmem ctt,
    unfold forces_form, simp,
    induction h_ih,
    intros v vmem wmem rwv,
    apply h_ih, assumption,
    apply empty_ctx_tt
  },
  { apply sem_csq.is_true,
    intros M w wmem ctt,
    unfold forces_form, simp,
    induction h_ih,
    intros v vmem wmem rwv,
    apply h_ih, assumption,
    apply empty_ctx_tt
  }
end

/-
  Completeness
-/

open nat set classical

local attribute [instance, priority 0] prop_decidable

def is_consist { σ : ℕ } (Γ : ctx σ) := Γ-σ ⊬κ ⊥

def is_max (Γ : ctx σ) := is_consist Γ ∧ ∀ p, p ∈ Γ ∨ (¬p) ∈ Γ

def insert_form (Γ : ctx σ) (p : form σ) : ctx σ :=
  if is_consist (Γ ∪ p) then Γ ∪ p else Γ ∪ ¬p

-- def insert_code (Γ : ctx σ) (n : nat) : ctx σ :=
-- match encodable.decode (form σ) n with
-- | none := Γ
-- | some p := insert_form Γ p
-- end

-- @[simp]
-- def maxn (Γ : ctx σ) : nat → ctx σ
-- | 0     := Γ
-- | (n+1) := insert_code (maxn n) n

-- @[simp]
-- def max (Γ : ctx σ) : ctx σ := ⋃ n, maxn Γ n

lemma consist_not_of_not_prf { σ : ℕ } {Γ : ctx σ} {p : form σ} :
  (Γ-σ ⊬κ  p) → is_consist (Γ ∪ ¬p) :=
λ hnp hc, hnp (mp dne (deduction hc))

axiom not_imp_not : ∀ {a b : Prop} [_inst_1 : decidable a], ¬a → ¬b ↔ b → a

theorem completeness { σ : ℕ }{ Γ : ctx σ} {p : form σ} :
  (Γ-σ ⊨κ p) → (Γ-σ ⊢κ  p) :=
begin
  apply (@not_imp_not (Γ-σ ⊢κ p) (Γ-σ ⊨κ  p) (prop_decidable _)).1,
  intros nhp hp, cases hp,
  have : is_consist (Γ ∪ ¬p) := consist_not_of_not_prf nhp,
  apply absurd,
  fapply hp,
    { exact model σ },
    { apply mem_domain c },
    { exact ctx.max (Γ ∪ ¬p) },
    { apply cons_ctx_tt_to_ctx_tt,
      apply ctx_tt_to_subctx_tt,
      apply ctx_tt_of_mem_domain (ctx.max (Γ ∪ ¬p)),
      apply mem_domain c,
      apply ctx.subset_max_self },

    { simp, apply eq_ff_of_not_eq_tt,
      apply neg_tt_iff_ff.1,
      apply and.elim_right,
      apply cons_ctx_tt_iff_and.1,
      apply ctx_tt_to_subctx_tt,
      apply ctx_tt_of_mem_domain (ctx.max (Γ ∪ ¬p)),
      apply mem_domain c,
      apply ctx.subset_max_self },
end

author: bogdanmacovei

repo: DEAL-Lean