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

José A. Alonso

2019-10-12 sáb 19:05