Tácticas en Lean
Índice
En estas notas se presentan la construcción de demostraciones aplicativas con las tácticas de Lean.
1 Activación del modo de tácticas
-- 1ª demostración theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := begin /- p q : Prop, hp : p, hq : q ⊢ p ∧ q ∧ p -/ apply and.intro, /- p q : Prop, hp : p, hq : q ⊢ p p q : Prop, hp : p, hq : q ⊢ q ∧ p -/ exact hp, /- p q : Prop, hp : p, hq : q ⊢ q ∧ p -/ apply and.intro, /- p q : Prop, hp : p, hq : q ⊢ q p q : Prop, hp : p, hq : q ⊢ p -/ exact hq, /- p q : Prop, hp : p, hq : q ⊢ p -/ exact hp end -- Escritura #print test -- Da theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p := -- λ (p q : Prop) (hp : p) (hq : q), ⟨hp, ⟨hq, hp⟩⟩ -- 2ª demostración theorem test2 (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := begin /- p q : Prop, hp : p, hq : q ⊢ p ∧ q ∧ p -/ apply and.intro hp, /- p q : Prop, hp : p, hq : q ⊢ q ∧ p -/ exact and.intro hq hp end -- Escritura #print test2 -- Da theorem test2 : ∀ (p q : Prop), p → q → p ∧ q ∧ p := -- λ (p q : Prop) (hp : p) (hq : q), ⟨hp, ⟨hq, hp⟩⟩ -- 3ª demostración theorem test3 (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := begin apply and.intro hp; exact and.intro hq hp end -- Escritura #print test3 -- Da theorem test3 : ∀ (p q : Prop), p → q → p ∧ q ∧ p := -- λ (p q : Prop) (hp : p) (hq : q), ⟨hp, ⟨hq, hp⟩⟩ -- 4ª demostración theorem test4 (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by exact and.intro hp (and.intro hq hp) -- Escritura #print test4 -- Da theorem test4 : ∀ (p q : Prop), p → q → p ∧ q ∧ p := -- λ (p q : Prop) (hp : p) (hq : q), ⟨hp, ⟨hq, hp⟩⟩ -- 5ª demostración -- =============== variables {p q : Prop} (hp : p) (hq : q) include hp hq example : p ∧ q ∧ p := begin apply and.intro hp, exact and.intro hq hp end omit hp hq -- 6ª demostración -- =============== section include hp hq example : p ∧ q ∧ p := begin apply and.intro hp, exact and.intro hq hp end end -- 7ª demostración -- =============== example : p ∧ q ∧ p := let hp := hp, hq := hq in begin apply and.intro hp, exact and.intro hq hp end
2 Tácticas básicas
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, intro h, apply or.elim (and.right h), intro hq, apply or.inl, apply and.intro, exact and.left h, exact hq, intro hr, apply or.inr, apply and.intro, exact and.left h, exact hr, intro h, apply or.elim h, intro hpq, apply and.intro, exact and.left hpq, apply or.inl, exact and.right hpq, intro hpr, apply and.intro, exact and.left hpr, apply or.inr, exact and.right hpr end
example (α : Type) : α → α := begin intro a, exact a end example (α : Type) : ∀ x : α, x = x := begin intro x, exact eq.refl x end
example : ∀ a b c : ℕ, a = b → a = c → c = b := begin intros a b c h₁ h₂, exact eq.trans (eq.symm h₂) h₁ end
variables x y z w : ℕ -- 1ª demostración example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := begin apply eq.trans h₁, apply eq.trans h₂, assumption end -- 2ª demostración example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := begin apply eq.trans, assumption, apply eq.trans, assumption, assumption end
example : ∀ a b c : ℕ, a = b → a = c → c = b := begin intros, apply eq.trans, apply eq.symm, assumption, assumption end
example (y : ℕ) : (λ x : ℕ, 0) y = 0 := begin refl end example (x : ℕ) : x ≤ x := begin refl end
example : ∀ a b c : ℕ, a = b → a = c → c = b := begin intros, transitivity, symmetry, assumption, assumption end
example : ∀ a b c : ℕ, a = b → a = c → c = b := begin intros a b c h₁ h₂, transitivity a, symmetry, assumption, assumption end
example : ∀ a b c : ℕ, a = b → a = c → c = b := begin intros, apply eq.trans, apply eq.symm, repeat { assumption } end
example : ∃ a : ℕ, 5 = a := begin apply exists.intro, reflexivity end
example : ∃ a : ℕ, a = a := begin fapply exists.intro, exact 0, reflexivity end
example (x : ℕ) : x = x := begin revert x, -- goal is ⊢ ∀ (x : ℕ), x = x intro y, -- goal is y : ℕ ⊢ y = y reflexivity end example (x y : ℕ) (h : x = y) : y = x := begin revert h, -- goal is x y : ℕ ⊢ x = y → y = x intro h₁, -- goal is x y : ℕ, h₁ : x = y ⊢ y = x symmetry, assumption end example (x y : ℕ) (h : x = y) : y = x := begin revert x, -- goal is y : ℕ ⊢ ∀ (x : ℕ), x = y → y = x intros, symmetry, assumption end example (x y : ℕ) (h : x = y) : y = x := begin revert x y, -- goal is ⊢ ∀ (x y : ℕ), x = y → y = x intros, symmetry, assumption end
example : 3 = 3 := begin generalize : 3 = x, -- goal is x : ℕ ⊢ x = x, revert x, -- goal is ⊢ ∀ (x : ℕ), x = x intro y, reflexivity end
example : 2 + 3 = 5 := begin generalize : 3 = x, -- goal is x : ℕ ⊢ 2 + x = 5, sorry end
example : 2 + 3 = 5 := begin generalize h : 3 = x, -- goal is x : ℕ, h : 3 = x ⊢ 2 + x = 5, rw ←h end
3 Más tácticas
example (p q : Prop) : p ∨ q → q ∨ p := begin intro h, cases h with hp hq, right, exact hp, left, exact hq end
example (p q : Prop) : p ∧ q → q ∧ p := begin intro h, cases h with hp hq, constructor, exact hq, exact hp end
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, intro h, cases h with hp hqr, cases hqr with hq hr, left, constructor, repeat { assumption }, right, constructor, repeat { assumption }, intro h, cases h with hpq hpr, cases hpq with hp hq, constructor, exact hp, left, exact hq, cases hpr with hp hr, constructor, exact hp, right, exact hr end
example (p q : ℕ → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := begin intro h, cases h with x px, constructor, left, exact px end -- 2ª demostración example (p q : ℕ → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := begin intro h, cases h with x px, existsi x, left, exact px end
example (p q : ℕ → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := begin intro h, cases h with x hpq, cases hpq with hp hq, existsi x, split; assumption end
universes u v def swap_pair {α : Type u} {β : Type v} : α × β → β × α := begin intro p, cases p with ha hb, constructor, exact hb, exact ha end def swap_sum {α : Type u} {β : Type v} : α ⊕ β → β ⊕ α := begin intro p, cases p with ha hb, right, exact ha, left, exact hb end
open nat example (P : ℕ → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : ℕ) : P m := begin cases m with m', exact h₀, exact h₁ m' end
example (p q : Prop) : p ∧ ¬ p → q := begin intro h, cases h, contradiction end
4 Estructuración de demostraciones aplicativas
example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := begin intro h, exact have hp : p, from h.left, have hqr : q ∨ r, from h.right, show (p ∧ q) ∨ (p ∧ r), begin cases hqr with hq hr, exact or.inl ⟨hp, hq⟩, exact or.inr ⟨hp, hr⟩ end end
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, intro h, cases h.right with hq hr, exact or.inl ⟨h.left, hq⟩, exact or.inr ⟨h.left, hr⟩, intro h, cases h with hpq hpr, exact ⟨hpq.left, or.inl hpq.right⟩, exact ⟨hpr.left, or.inr hpr.right⟩ end
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, intro h, cases h.right with hq hr, show (p ∧ q) ∨ (p ∧ r), from or.inl ⟨h.left, hq⟩, show (p ∧ q) ∨ (p ∧ r), from or.inr ⟨h.left, hr⟩, intro h, cases h with hpq hpr, show p ∧ (q ∨ r), from ⟨hpq.left, or.inl hpq.right⟩, show p ∧ (q ∨ r), from ⟨hpr.left, or.inr hpr.right⟩ end -- 2ª demostración example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, intro h, cases h.right with hq hr, show (p ∧ q) ∨ (p ∧ r), { left, split, exact h.left, assumption }, show (p ∧ q) ∨ (p ∧ r), { right, split, exact h.left, assumption }, intro h, cases h with hpq hpr, show p ∧ (q ∨ r), { cases hpq, split, assumption, left, assumption }, show p ∧ (q ∨ r), { cases hpr, split, assumption, right, assumption } end
example (n : ℕ) : n + 1 = nat.succ n := begin show nat.succ n = nat.succ n, reflexivity end
example (p q : Prop) : p ∧ q → q ∧ p := begin intro h, cases h with hp hq, split, show q, from hq, show p, from hp end example (p q : Prop) : p ∧ q → q ∧ p := begin intro h, cases h with hp hq, split, show p, from hp, show q, from hq end
example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := begin intro h, cases h with hp hqr, show (p ∧ q) ∨ (p ∧ r), cases hqr with hq hr, have hpq : p ∧ q, from and.intro hp hq, left, exact hpq, have hpr : p ∧ r, from and.intro hp hr, right, exact hpr end -- 2ª demostración example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := begin intro h, cases h with hp hqr, show (p ∧ q) ∨ (p ∧ r), cases hqr with hq hr, have hpq : p ∧ q, split; assumption, left, exact hpq, have hpr : p ∧ r, split; assumption, right, exact hpr end -- 3ª demostración example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := begin intro h, cases h with hp hqr, show (p ∧ q) ∨ (p ∧ r), cases hqr with hq hr, have : p ∧ q, split; assumption, left, exact this, have : p ∧ r, split; assumption, right, exact this end -- 4ª demostración example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := begin intro h, have hp : p := h.left, have hqr : q ∨ r := h.right, show (p ∧ q) ∨ (p ∧ r), cases hqr with hq hr, exact or.inl ⟨hp, hq⟩, exact or.inr ⟨hp, hr⟩ end
example : ∃ x, x + 2 = 8 := begin let a : ℕ := 3 * 2, existsi a, reflexivity end -- 2ª demostración example : ∃ x, x + 2 = 8 := begin let a := 3 * 2, existsi a, reflexivity end
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, begin intro h, cases h.right with hq hr, begin show (p ∧ q) ∨ (p ∧ r), exact or.inl ⟨h.left, hq⟩ end, show (p ∧ q) ∨ (p ∧ r), exact or.inr ⟨h.left, hr⟩ end, intro h, cases h with hpq hpr, begin show p ∧ (q ∨ r), exact ⟨hpq.left, or.inl hpq.right⟩ end, show p ∧ (q ∨ r), exact ⟨hpr.left, or.inr hpr.right⟩ end -- 2ª demostración example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, { intro h, cases h.right with hq hr, { show (p ∧ q) ∨ (p ∧ r), exact or.inl ⟨h.left, hq⟩ }, show (p ∧ q) ∨ (p ∧ r), exact or.inr ⟨h.left, hr⟩ }, intro h, cases h with hpq hpr, { show p ∧ (q ∨ r), exact ⟨hpq.left, or.inl hpq.right⟩ }, show p ∧ (q ∨ r), exact ⟨hpr.left, or.inr hpr.right⟩ end -- 3ª demostración example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := begin apply iff.intro, { intro h, cases h.right with hq hr, { show (p ∧ q) ∨ (p ∧ r), exact or.inl ⟨h.left, hq⟩ }, { show (p ∧ q) ∨ (p ∧ r), exact or.inr ⟨h.left, hr⟩ }}, { intro h, cases h with hpq hpr, { show p ∧ (q ∨ r), exact ⟨hpq.left, or.inl hpq.right⟩ }, { show p ∧ (q ∨ r), exact ⟨hpr.left, or.inr hpr.right⟩ }} end
example (p q : Prop) : p ∧ q ↔ q ∧ p := begin apply iff.intro, { intro h, have hp : p := h.left, have hq : q := h.right, show q ∧ p, exact ⟨hq, hp⟩ }, intro h, have hp : p := h.right, have hq : q := h.left, show p ∧ q, exact ⟨hp, hq⟩ end
5 Combinadores de tácticas
example (p q : Prop) (hp : p) : p ∨ q := begin left, assumption end -- 2ª demostración example (p q : Prop) (hp : p) : p ∨ q := by { left, assumption }
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by split; assumption
example (p q : Prop) (hp : p) : p ∨ q := by { left, assumption } <|> { right, assumption} example (p q : Prop) (hq : q) : p ∨ q := by { left, assumption } <|> { right, assumption} example (p q r : Prop) (hp : p) : p ∨ q ∨ r := by repeat { {left, assumption} <|> right <|> assumption } example (p q r : Prop) (hq : q) : p ∨ q ∨ r := by repeat { {left, assumption} <|> right <|> assumption } example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by repeat { {left, assumption} <|> right <|> assumption }
meta def tac_1 : tactic unit := `[ repeat { {left, assumption} <|> right <|> assumption } ] example (p q r : Prop) (hp : p) : p ∨ q ∨ r := by tac_1 example (p q r : Prop) (hq : q) : p ∨ q ∨ r := by tac_1 example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by tac_1
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by split; try {split}; assumption
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := begin split, all_goals { try {split} }, all_goals { assumption } end
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := begin split, any_goals { split }, any_goals { assumption } end
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := begin repeat { any_goals { split }}, all_goals { assumption } end -- 2ª demostración example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by repeat { any_goals { split <|> assumption} }
6 Reescritura
variables (f : ℕ → ℕ) (k : ℕ) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := begin rw h₂, rw h₁ end
example (x y : ℕ) (p : ℕ → Prop) (q : Prop) (h : q → x = y) (h' : p y) (hq : q) : p x := by { rw (h hq), assumption }
variables (f : ℕ → ℕ) (k : ℕ) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by rw [h₂, h₁]
variables (f : ℕ → ℕ) (a b : ℕ) example (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := begin rw [←h₁, h₂] end
example (a b c : ℕ) : a + b + c = a + c + b := begin rw [add_assoc, add_comm b, ←add_assoc] end example (a b c : ℕ) : a + b + c = a + c + b := begin rw [add_assoc, add_assoc, add_comm b] end example (a b c : ℕ) : a + b + c = a + c + b := begin rw [add_assoc, add_assoc, add_comm _ b] end
variables (f : ℕ → ℕ) (a : ℕ) example (h : a + 0 = 0) : f a = f 0 := begin rw add_zero at h, rw h end -- 2ª demostración example (h : a + 0 = 0) : f a = f 0 := by { rw add_zero at h, rw h }
universe u def tuple (α : Type u) (n : ℕ) := { l : list α // list.length l = n } variables {α : Type u} {n : ℕ} example (h : n = 0) (t : tuple α n) : tuple α 0 := begin rw h at t, exact t end
universe u example {α : Type u} [ring α] (a b c : α) : a * 0 + 0 * b + c * 0 + 0 * a = 0 := begin rw [mul_zero, mul_zero, zero_mul, zero_mul], repeat { rw add_zero } end example {α : Type u} [group α] {a b : α} (h : a * b = 1) : a⁻¹ = b := begin rw ←(mul_one a⁻¹), rw ←h, rw inv_mul_cancel_left end example {α : Type u} [group α] {a b : α} (h : a * b = 1) : a⁻¹ = b := by rw [←(mul_one a⁻¹), ←h, inv_mul_cancel_left]
7 Uso del simplificador
variables (x y z : ℕ) (p : ℕ → Prop) variable (h : p (x * y)) example : (x + 0) * (0 + y * 1 + z * 0) = x * y := by simp include h example : p ((x + 0) * (0 + y * 1 + z * 0)) := by { simp, assumption }
import data.list.basic universe u variable {α : Type} open list example (xs : list ℕ) : reverse (xs ++ [1, 2, 3]) = [3, 2, 1] ++ reverse xs := by simp example (xs ys : list α) : length (reverse (xs ++ ys)) = length xs + length ys := by simp
variables (x y z : ℕ) (p : ℕ → Prop) example (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := by { simp at h, assumption }
variables (w x y z : ℕ) (p : ℕ → Prop) local attribute [simp] mul_comm mul_assoc mul_left_comm example (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by { simp at *, assumption } example (h₁ : p (1 * x + y)) (h₂ : p (x * z * 1)) : p (y + 0 + x) ∧ p (z * x) := by { simp at *, split; assumption }
variables (x y z w : ℕ) (p : ℕ → Prop) local attribute [simp] mul_comm mul_assoc mul_left_comm example : x * y + z * w * x = x * w * z + y * x := by simp example (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := begin simp, simp at h, assumption end
variables {α : Type} [comm_ring α] local attribute [simp] mul_comm mul_assoc mul_left_comm example (x y z : α) : (x - x) * y + z = z := begin simp end example (x y z w : α) : x * y + z * w * x = x * w * z + y * x := by simp
def f (m n : ℕ) : ℕ := m + n + m example {m n : ℕ} (h : n = 1) (h' : 0 = m) : (f m n) * m = m := by simp [h, h'.symm, f]
variables (f : ℕ → ℕ) (k : ℕ) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by simp [h₁, h₂] -- 2ª demostración example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by simp * example (u w x y z : ℕ) (h₁ : x = y + z) (h₂ : w = u + x) : w = z + y + u := by simp *
variables (p q r : Prop) example (hp : p) : p ∧ q ↔ q := by simp * example (hp : p) : p ∨ q := by simp * example (hp : p) (hq : q) : p ∧ (q ∨ r) := by simp *
section variables (u w x x' y y' z : ℕ) (p : ℕ → Prop) example (h₁ : x + 0 = x') (h₂ : y + 0 = y') : x + y + 0 = x' + y' := by { simp at *, simp * } example (h₁ : x = y + z) (h₂ : w = u + x) (h₃ : p (z + y + u)) : p w := by { simp at *, simp * } end
import data.list.basic open list universe u variables {α : Type} (x y z : α) (xs ys zs : list α) def mk_symm (xs : list α) := xs ++ reverse xs theorem reverse_mk_symm (xs : list α) : reverse (mk_symm xs) = mk_symm xs := by { unfold mk_symm, simp } -- 2ª demostración theorem reverse_mk_symm2 (xs : list α) : reverse (mk_symm xs) = mk_symm xs := by simp [mk_symm] -- Simplificación con el teorema demostrado example (xs ys : list ℕ) : reverse (xs ++ mk_symm ys) = mk_symm ys ++ reverse xs := by simp [reverse_mk_symm] example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (mk_symm ys ++ reverse xs) := by simp [reverse_mk_symm] at h; assumption
import data.list.basic open list universe u variables {α : Type} (x y z : α) (xs ys zs : list α) def mk_symm (xs : list α) := xs ++ reverse xs @[simp] theorem reverse_mk_symm (xs : list α) : reverse (mk_symm xs) = mk_symm xs := by simp [mk_symm] example (xs ys : list ℕ) : reverse (xs ++ mk_symm ys) = mk_symm ys ++ reverse xs := by simp example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (mk_symm ys ++ reverse xs) := by simp at h; assumption
import data.list.basic open list universe u variables {α : Type} (x y z : α) (xs ys zs : list α) def mk_symm (xs : list α) := xs ++ reverse xs attribute [simp] theorem reverse_mk_symm (xs : list α) : reverse (mk_symm xs) = mk_symm xs := by simp [mk_symm] example (xs ys : list ℕ) : reverse (xs ++ mk_symm ys) = mk_symm ys ++ reverse xs := by simp example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (mk_symm ys ++ reverse xs) := by simp at h; assumption
import data.list.basic open list universe u variables {α : Type} (x y z : α) (xs ys zs : list α) def mk_symm (xs : list α) := xs ++ reverse xs theorem reverse_mk_symm (xs : list α) : reverse (mk_symm xs) = mk_symm xs := by simp [mk_symm] attribute [simp] reverse_mk_symm example (xs ys : list ℕ) : reverse (xs ++ mk_symm ys) = mk_symm ys ++ reverse xs := by simp example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (mk_symm ys ++ reverse xs) := by simp at h; assumption
import data.list.basic open list universe u variables {α : Type} (x y z : α) (xs ys zs : list α) def mk_symm (xs : list α) := xs ++ reverse xs theorem reverse_mk_symm (xs : list α) : reverse (mk_symm xs) = mk_symm xs := by simp [mk_symm] section local attribute [simp] reverse_mk_symm example (xs ys : list ℕ) : reverse (xs ++ mk_symm ys) = mk_symm ys ++ reverse xs := by simp example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (mk_symm ys ++ reverse xs) := by simp at h; assumption end
import data.list.basic open list universe u variables {α : Type} (x y z : α) (xs ys zs : list α) def mk_symm (xs : list α) := xs ++ reverse xs theorem reverse_mk_symm (xs : list α) : reverse (mk_symm xs) = mk_symm xs := by simp [mk_symm] run_cmd mk_simp_attr `my_simps attribute [my_simps] reverse_mk_symm example (xs ys : list ℕ) : reverse (xs ++ mk_symm ys) = mk_symm ys ++ reverse xs := by simp with my_simps example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (mk_symm ys ++ reverse xs) := by simp with my_simps at h; assumption
import data.list.basic open list universe u variables {α : Type} (x y z : α) (xs ys zs : list α) def mk_symm (xs : list α) := xs ++ reverse xs theorem reverse_mk_symm (xs : list α) : reverse (mk_symm xs) = mk_symm xs := begin unfold mk_symm, simp end attribute [simp] reverse_mk_symm example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (mk_symm ys ++ reverse xs) := by { simp at h, assumption } example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (reverse (mk_symm ys) ++ reverse xs) := by { simp [-reverse_mk_symm] at h, assumption } example (xs ys : list ℕ) (p : list ℕ → Prop) (h : p (reverse (xs ++ (mk_symm ys)))) : p (reverse (mk_symm ys) ++ reverse xs) := by { simp only [reverse_append] at h, assumption }
8 Referencias
- Theorem proving in Lean por Jeremy Avigad, Leonardo de Moura y Soonho Kong.
- Cap. 5 Tactics.