Interacción con Lean

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 :=
  by simp [double, add_mul]
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

namespace foo
def bar : ℕ := 1
end foo

open foo

#check bar
#check foo.bar

#check add_sub_cancel
#check nat.add_sub_cancel
#check _root_.add_sub_cancel

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

open foo

#check bar -- error
#check foo.bar

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

-- 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

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)

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 : ℤ

-- 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

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

open nat

#check succ_ne_zero
#check @mul_zero
#check @mul_one
#check @sub_add_eq_add_sub
#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_lt_add_of_lt_of_le

#check @add_le_add_left
#check @add_le_add_right

#check mul_inv_self
#check neg_add_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