# Interacción con Lean

## 2 Secciones

```section
variables x y : ℕ

def double := x + x

#check double y
#check double (2 * x)

theorem t1 : double (x + y) = double x + double y :=
by simp [double]

#check t1 y
#check t1 (2 * x)

theorem t2 : double (x * y) = double x * y :=
end
```
```section
variables (x y z : ℕ)
variables (h₁ : x = y) (h₂ : y = z)

include h₁ h₂
theorem foo : x = z :=
begin
rw [h₁, h₂]
end
omit h₁ h₂

theorem bar : x = z :=
eq.trans h₁ h₂

theorem baz : x = x := rfl

#check @foo
#check @bar
#check @baz
end
```
```section
variables (x y z : ℕ)
variables (h₁ : x = y) (h₂ : y = z)

section
variables {x y z}
include h₁ h₂
theorem foo : x = z :=
begin
rw [h₁, h₂]
end
end

theorem bar : x = z :=
eq.trans h₁ h₂

variable {x}
theorem baz : x = x := rfl

#check @foo
#check @bar
#check @baz
end
```
```section
parameters {α : Type} (r : α → α → Type)
parameter  transr : ∀ {x y z}, r x y → r y z → r x z

variables {a b c d e : α}

theorem t1 (h₁ : r a b) (h₂ : r b c) (h₃ : r c d) :
r a d :=
transr (transr h₁ h₂) h₃

theorem t2 (h₁ : r a b) (h₂ : r b c) (h₃ : r c d) (h₄ : r d e) :
r a e :=
transr h₁ (t1 h₂ h₃ h₄)

#check t1
#check t2
end

#check t1
#check t2
```

## 3 Espacios de nombres

```namespace foo
def bar : ℕ := 1
end foo

open foo

#check bar
#check foo.bar
```
```#check add_sub_cancel
```
```namespace foo
protected def bar : ℕ := 1
end foo

open foo

#check bar -- error
#check foo.bar
```

## 4 Atributos

```variable {α : Type*}

def is_prefix (l₁ : list α) (l₂ : list α) : Prop :=
∃ t, l₁ ++ t = l₂

infix ` <+: `:50 := is_prefix

attribute [simp]
theorem list.is_prefix_refl (l : list α) : l <+: l :=
⟨[], by simp⟩

example : [1, 2, 3] <+: [1, 2, 3] := by simp
```
```variable {α : Type*}

def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂

infix ` <+: `:50 := is_prefix

@[simp]
theorem list.is_prefix_refl (l : list α) : l <+: l :=
⟨[], by simp⟩

example : [1, 2, 3] <+: [1, 2, 3] := by simp
```
```variable {α : Type*}

def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂

infix ` <+: `:50 := is_prefix

-- BEGIN
theorem list.is_prefix_refl (l : list α) : l <+: l :=
⟨[], by simp⟩

attribute [simp] list.is_prefix_refl

example : [1, 2, 3] <+: [1, 2, 3] := by simp
```
```variable {α : Type*}

def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂

infix ` <+: `:50 := is_prefix

section
local attribute [simp]
theorem list.is_prefix_refl (l : list α) : l <+: l :=
⟨[], by simp⟩

example : [1, 2, 3] <+: [1, 2, 3] := by simp
end

-- error:
-- example : [1, 2, 3] <+: [1, 2, 3] := by simp
```
```variable {α : Type*}

def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂

instance list_has_le : has_le (list α) := ⟨is_prefix⟩

theorem list.is_prefix_refl (l : list α) : l ≤ l :=
⟨[], by simp⟩
```
```variable {α : Type*}

def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂

def list_has_le : has_le (list α) := ⟨is_prefix⟩

section
local attribute [instance] list_has_le

theorem foo (l : list α) : l ≤ l := ⟨[], by simp⟩
end

-- error:
-- theorem bar (l : list α) : l ≤ l := ⟨[], by simp⟩
```
```variable {α : Type*}

def is_prefix (l₁ : list α) (l₂ : list α) : Prop := ∃ t, l₁ ++ t = l₂

infix ` <+: `:50 := is_prefix

@[simp, refl]
theorem list.is_prefix_refl (l : list α) : l <+: l :=
⟨[], by simp⟩

example : [1, 2, 3] <+: [1, 2, 3] := by reflexivity
```

## 5 Argumentos implícitos

```-- BEGIN
namespace hidden
variables {α : Type} (r : α → α → Prop)

definition reflexive  : Prop := ∀ (a : α), r a a
definition symmetric  : Prop := ∀ {a b : α}, r a b → r b a
definition transitive : Prop := ∀ {a b c : α}, r a b → r b c → r a c
definition euclidean  : Prop := ∀ {a b c : α}, r a b → r a c → r b c

variable {r}

theorem th1 (reflr : reflexive r) (euclr : euclidean r) :
symmetric r :=
assume a b : α,
assume : r a b,
show r b a, from euclr this (reflr _)

theorem th2 (symmr : symmetric r) (euclr : euclidean r) :
transitive r :=
assume (a b c : α),
assume (rab : r a b) (rbc : r b c),
euclr (symmr rab) rbc

-- error:
/-
theorem th3 (reflr : reflexive r) (euclr : euclidean r) :
transitive r :=
th2 (th1 reflr euclr) euclr
-/

theorem th3 (reflr : reflexive r) (euclr : euclidean r) :
transitive r :=
@th2 _ _ (@th1 _ _ reflr @euclr) @euclr
end hidden
```
```namespace hidden

variables {α : Type} (r : α → α → Prop)

definition reflexive  : Prop := ∀ (a : α), r a a
definition symmetric  : Prop := ∀ ⦃a b : α⦄, r a b → r b a
definition transitive : Prop := ∀ ⦃a b c : α⦄, r a b → r b c → r a c
definition euclidean  : Prop := ∀ ⦃a b c : α⦄, r a b → r a c → r b c

variable {r}

theorem th1 (reflr : reflexive r) (euclr : euclidean r) :
symmetric r :=
assume a b : α, assume : r a b,
show r b a, from euclr this (reflr _)

theorem th2 (symmr : symmetric r) (euclr : euclidean r) :
transitive r :=
assume (a b c : α), assume (rab : r a b) (rbc : r b c),
euclr (symmr rab) rbc

theorem th3 (reflr : reflexive r) (euclr : euclidean r) :
transitive r :=
th2 (th1 reflr euclr) euclr

end hidden
```

## 6 Notaciones

```notation `[` a `**` b `]` := a * b + 1

def mul_square (a b : ℕ) := a * a * b * b

infix `<*>`:50 := mul_square

#reduce [2 ** 3]
#reduce 2 <*> 3
```
```local notation `[` a `**` b `]` := a * b + 1
local infix `<*>`:50 := λ a b : ℕ, a * a * b * b
```
```notation [parsing_only] `[` a `**` b `]` := a * b + 1

variables a b : ℕ
#check [a ** b]
```
```namespace int

def dvd (m n : ℤ) : Prop := ∃ k, n = m * k
instance : has_dvd int := ⟨int.dvd⟩

@[simp]
theorem dvd_zero (n : ℤ) : n ∣ 0 :=
⟨0, by simp⟩

theorem dvd_intro {m n : ℤ} (k : ℤ) (h : n = m * k) : m ∣ n :=
⟨k, h⟩

end int

open int

section mod_m
parameter (m : ℤ)
variables (a b c : ℤ)

definition mod_equiv := (m ∣ b - a)

local infix ≡ := mod_equiv

theorem mod_refl : a ≡ a :=
show m ∣ a - a, by simp

theorem mod_symm (h : a ≡ b) : b ≡ a :=
by cases h with c hc; apply dvd_intro (-c); simp [eq.symm hc]

theorem mod_trans (h₁ : a ≡ b) (h₂ : b ≡ c) : a ≡ c :=
begin
cases h₁ with d hd, cases h₂ with e he,
apply dvd_intro (d + e),
simp [mul_add, eq.symm hd, eq.symm he]
end
end mod_m

#check (mod_refl : ∀ (m a : ℤ), mod_equiv m a a)

#check (mod_symm : ∀ (m a b : ℤ), mod_equiv m a b →
mod_equiv m b a)

#check (mod_trans :  ∀ (m a b c : ℤ), mod_equiv m a b →
mod_equiv m b c → mod_equiv m a c)
```

## 7 Conversiones de tipos

```variables m n : ℕ
variables i j : ℤ

#check i + m      -- i + ↑m : ℤ
#check i + m + j  -- i + ↑m + j : ℤ
#check i + m + n  -- i + ↑m + ↑n : ℤ

#check ↑m + i        -- ↑m + i : ℤ
#check ↑(m + n) + i  -- ↑(m + n) + i : ℤ
#check ↑m + ↑n + i   -- ↑m + ↑n + i : ℤ
```

## 8 Obtención de información

```-- Ejemplos con eq
-- ===============

#check eq         -- ?M_1 → ?M_1 → Prop
#check @eq        -- Π {α : Sort u_1}, α → α → Prop
#check eq.symm    -- ?M_2 = ?M_3 → ?M_3 = ?M_2
#check @eq.symm   -- ∀ {α : Sort u_1} {a b : α}, a = b → b = a

#print eq.symm
-- Da
--    @[symm]
--    theorem eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a :=
--    λ {α : Sort u} {a b : α} (h : a = b), h ▸ rfl

-- Ejemplos con and
-- ================

#check and          -- Prop → Prop → Prop
#check and.intro    -- ?M_1 → ?M_2 → ?M_1 ∧ ?M_2
#check @and.intro   -- ∀ {a b : Prop}, a → b → a ∧ b

-- Ejemplos con función definida
-- =============================

def foo {α : Type} (x : α) : α := x

#check foo               -- ?M_1 → ?M_1
#check @foo              -- Π {α : Type}, α → α
#reduce foo              -- λ (x : ?M_1), x
#reduce (foo nat.zero)   -- 0
#print foo               -- def foo : Π {α : Type}, α → α :=
-- λ {α : Type} (x : α), x
```
```#print notation
#print notation + * -
#print axioms
#print options
#print prefix nat
#print prefix nat.le
#print classes
#print instances ring
#print fields ring

#print list.append
#print definition list.append

#print +
#print notation +

#print nat
#print inductive nat

#print group
#print inductive group
```

## 9 Ajuste de opciones

```set_option pp.implicit true
set_option pp.universes true
set_option pp.notation false
set_option pp.numerals false

#check 2 + 2 = 4
#reduce (λ x, x + 2) = (λ x, x + 3)
#check (λ x, x + 1) 1
```
```set_option pp.beta true
#check (λ x, x + 1) 1
```

## 11 Uso de la librería

```open nat

#check succ_ne_zero
#check @mul_zero
#check @mul_one
#check @le_iff_lt_or_eq
```
```open nat

#check @neg_neg
#check pred_succ
```
```#check @nat.lt_of_succ_le
#check @lt_of_not_ge
#check @lt_of_le_of_ne
```
```#check @add_le_add_left
```
```#check mul_inv_self
```
```#check @prod.mk
#check @prod.fst
#check @prod.snd
#check @prod.rec
```
```#check @and.intro    -- ∀ {a b : Prop}, a → b → a ∧ b [3 times]
#check @and.elim     -- ∀ {a b c : Prop}, a ∧ b → (a → b → c) → c
#check @and.left     -- ∀ {a b : Prop}, a ∧ b → a
#check @and.right    -- ∀ {a b : Prop}, a ∧ b → b
#check @or.inl       -- ∀ {a b : Prop}, a → a ∨ b
#check @or.inr       -- ∀ {a b : Prop}, b → a ∨ b
#check @or.elim      -- ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
#check @exists.intro -- ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → Exists p
#check @exists.elim  -- ∀ {α : Sort u_1} {p : α → Prop} {b : Prop},
--   (∃ (x : α), p x) → (∀ (a : α), p a → b) → b
#check @eq.refl      -- ∀ {α : Sort u_1} (a : α), a = a
#check @eq.subst     --∀ {α : Sort u_1} {P : α → Prop} {a b : α}, a = b → P a → P b
```

## 12 Referencias

2020-06-07 dom 12:22