Tácticas básicas de Lean
Índice
Notas sobre las tácticas básicas de Lean basadas en Basic guide to tactics de Kevin Buzzard para el proyecto Xena.
1 Reglas
| Conectiva | Introducción | Eliminación |
|---|---|---|
| → | intro | aplicación |
| ∧ | split | cases |
| ∨ | left y right | cases |
| ↔ | split | cases |
| ¬ | intro | aplicación |
| ∀ | intro | applicación |
| ∃ | existsi | cases |
2 Tácticas
2.1 La táctica cases
example (P Q : Prop) (H : P ∧ Q) : P := begin /- P Q : Prop, H : P ∧ Q ⊢ P -/ cases H with HP HQ, /- P Q : Prop, HP : P, HQ : Q ⊢ P -/ exact HP end
example (P Q : Prop) (H : P ∨ Q) : true := begin /- P Q : Prop, H : P ∨ Q ⊢ true -/ cases H with HP HQ, { /- P Q : Prop, H : P ∨ Q ⊢ true -/ trivial}, { /- P Q : Prop, HQ : Q ⊢ true -/ trivial}, end
example (P Q : Prop) (H : P ↔ Q) : P → Q := begin /- P Q : Prop, HQ : Q ⊢ true -/ cases H with HPQ HQP, /- P Q : Prop, HPQ : P → Q, HQP : Q → P ⊢ P → Q -/ exact HPQ end
example (X : Type) (P Q : X → Prop) (H : ∃ x : X, P x ∧ Q x) : ∃ x : X, P x := begin /- X : Type, P Q : X → Prop, H : ∃ (x : X), P x ∧ Q x ⊢ ∃ (x : X), P x -/ cases H with x Hx, /- X : Type, P Q : X → Prop, x : X, Hx : P x ∧ Q x ⊢ ∃ (x : X), P x -/ cases Hx with HPx HQx, /- X : Type, P Q : X → Prop, x : X, HPx : P x, HQx : Q x ⊢ ∃ (x : X), P x -/ existsi x, /- X : Type, P Q : X → Prop, x : X, HPx : P x, HQx : Q x ⊢ P x -/ assumption end
2.2 La táctica apply
example (P Q : Prop) (HPQ : P → Q) : ¬ Q → ¬ P := begin /- P Q : Prop, HPQ : P → Q ⊢ ¬Q → ¬P -/ intro HnQ, /- P Q : Prop, HPQ : P → Q, HnQ : ¬Q ⊢ ¬P -/ intro HP, /- P Q : Prop, HPQ : P → Q, HnQ : ¬Q, HP : P ⊢ false -/ apply HnQ, /- P Q : Prop, HPQ : P → Q, HnQ : ¬Q, HP : P ⊢ Q -/ apply HPQ, /- P Q : Prop, HPQ : P → Q, HnQ : ¬Q, HP : P ⊢ P -/ assumption end
2.3 La táctica exact
example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q := begin exact (HPQ HP) end -- 2ª demostración example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q := HPQ HP
2.4 La táctica have
example (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R) : R := begin /- P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R ⊢ R -/ have HQ : Q, /- P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R ⊢ Q P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R, HQ : Q ⊢ R -/ apply HPQ, /- 2 goals P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R ⊢ Q P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R, HQ : Q ⊢ R -/ exact HP, /- P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R, HQ : Q ⊢ R -/ apply HQR, /- P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R, HQ : Q ⊢ Q -/ exact HQ end -- 2ª demostración example (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R) : R := begin /- P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R ⊢ R -/ have HQ : Q := HPQ HP, /- P Q R : Prop, HP : P, HPQ : P → Q, HQR : Q → R, HQ : Q ⊢ R -/ exact (HQR HQ), end
example (X : Type) (P Q : X → Prop) (a : X) (HP : ∀ x : X, P x) (HQ : ∀ x : X, Q x): P a ∧ Q a := begin /- X : Type, P Q : X → Prop, a : X, HP : ∀ (x : X), P x, HQ : ∀ (x : X), Q x ⊢ P a ∧ Q a -/ have HPa : P a := HP a, /- X : Type, P Q : X → Prop, a : X, HP : ∀ (x : X), P x, HQ : ∀ (x : X), Q x, HPa : P a ⊢ P a ∧ Q a -/ have HQa : Q a := HQ a, /- X : Type, P Q : X → Prop, a : X, HP : ∀ (x : X), P x, HQ : ∀ (x : X), Q x, HPa : P a, HQa : Q a ⊢ P a ∧ Q a -/ split, { /- X : Type, P Q : X → Prop, a : X, HP : ∀ (x : X), P x, HQ : ∀ (x : X), Q x, HPa : P a, HQa : Q a ⊢ P a -/ exact HPa}, { /- X : Type, P Q : X → Prop, a : X, HP : ∀ (x : X), P x, HQ : ∀ (x : X), Q x, HPa : P a, HQa : Q a ⊢ Q a -/ exact HQa}, end
2.5 La táctica intro
example (P Q : Prop) (HQ : Q) : P → Q := begin /- P Q : Prop HQ : Q ⊢ P → Q -/ intro HP, /- P Q : Prop, HQ : Q, HP : P ⊢ Q -/ exact HQ end
example (X : Type) (P Q : X → Prop) (HPQ : ∀ x, P x → Q x) (HP : ∀ x, P x) : ∀ x, Q x := begin intro, /- X : Type, P Q : X → Prop, HPQ : ∀ (x : X), P x → Q x, HP : ∀ (x : X), P x, x : X ⊢ Q x -/ have h1 : P x := HP x, /- X : Type, P Q : X → Prop, HPQ : ∀ (x : X), P x → Q x, HP : ∀ (x : X), P x, x : X, h1 : P x ⊢ Q x -/ have h2 : P x → Q x := HPQ x, /- X : Type, P Q : X → Prop, HPQ : ∀ (x : X), P x → Q x, HP : ∀ (x : X), P x, x : X, h1 : P x, h2 : P x → Q x ⊢ Q x -/ apply h2, /- X : Type, P Q : X → Prop, HPQ : ∀ (x : X), P x → Q x, HP : ∀ (x : X), P x, x : X, h1 : P x, h2 : P x → Q x ⊢ P x -/ exact h1 end -- 2ª demostración example (X : Type) (P Q : X → Prop) (HPQ : ∀ x, P x → Q x) (HP : ∀ x, P x) : ∀ x, Q x := begin intro, /- X : Type, P Q : X → Prop, HPQ : ∀ (x : X), P x → Q x, HP : ∀ (x : X), P x, x : X ⊢ Q x -/ apply HPQ x, /- X : Type, P Q : X → Prop, HPQ : ∀ (x : X), P x → Q x, HP : ∀ (x : X), P x, x : X ⊢ P x -/ apply HP x end -- 2ª demostración example (X : Type) (P Q : X → Prop) (HPQ : ∀ x, P x → Q x) (HP : ∀ x, P x) : ∀ x, Q x := begin intro, /- X : Type, P Q : X → Prop, HPQ : ∀ (x : X), P x → Q x, HP : ∀ (x : X), P x, x : X ⊢ Q x -/ apply (HPQ x) (HP x) end
example (X : Type) (a : X) (P : X → Prop) (H : ∀ x, P x) : P a := begin /- X : Type, a : X, P : X → Prop, H : ∀ (x : X), P x ⊢ P a -/ exact (H a), end
example (P Q : Prop) : ¬ P → ¬ (P ∧ Q) := begin /- P Q : Prop ⊢ ¬P → ¬(P ∧ Q) -/ intro HnP, /- P Q : Prop HnP : ¬P ⊢ ¬(P ∧ Q) -/ intro HPQ, /- P Q : Prop, HnP : ¬P, HPQ : P ∧ Q ⊢ false -/ apply HnP, /- P Q : Prop, HnP : ¬P, HPQ : P ∧ Q ⊢ P -/ cases HPQ with HP HQ, /- P Q : Prop, HnP : ¬P, HP : P, HQ : Q ⊢ P -/ exact HP, end
2.6 Las tácticas left y right
example (P Q : Prop) (HP : P) : P ∨ Q := begin /- P Q : Prop, HP : P ⊢ P ∨ Q -/ left, /- P Q : Prop, HP : P ⊢ P -/ exact HP, end example (P Q : Prop) (HQ : Q) : P ∨ Q := begin /- P Q : Prop, HQ : Q ⊢ P ∨ Q -/ right, /- P Q : Prop, HQ : Q ⊢ Q -/ exact HQ, end
2.7 La táctica split
example (P Q : Prop) (HP : P) (HQ : Q) : P ∧ Q := begin /- P Q : Prop, HP : P, HQ : Q ⊢ P ∧ Q -/ split, { /- P Q : Prop, HP : P, HQ : Q ⊢ P -/ exact HP }, { /- P Q : Prop, HP : P, HQ : Q ⊢ Q -/ exact HQ } end
example (P Q : Prop) (HPQ : P → Q) (HQP : Q → P) : P ↔ Q := begin /- P Q : Prop, HPQ : P → Q, HQP : Q → P ⊢ P ↔ Q -/ split, { /- P Q : Prop, HPQ : P → Q, HQP : Q → P ⊢ P → Q -/ exact HPQ }, { /- P Q : Prop, HPQ : P → Q, HQP : Q → P ⊢ Q → P -/ exact HQP } end
2.8 La táctica existsi
example : ∃ n : ℕ, 2 + 2 = n := begin -- ⊢ ∃ (n : ℕ), 2 + 2 = n existsi 4, -- ⊢ 2 + 2 = 4 refl end
import tactic.interactive import data.real.basic example : ∃ n : ℝ, n + 3 = 3 + 7 := begin -- ⊢ ∃ (n : ℝ), n + 3 = 3 + 7 use 7, -- ⊢ 7 + 3 = 3 + 7 apply add_comm, end