lean2/library/hott/logic.lean
Leonardo de Moura a450ad5a95 feat(frontends/lean/inductive_cmd): improve notation for declaring 'empty' inductive datatypes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 11:24:01 -07:00

250 lines
7.3 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
abbreviation id {A : Type} (a : A) := a
abbreviation compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
infixl `∘`:60 := compose
inductive path {A : Type} (a : A) : A → Type :=
| refl : path a a
infix `=`:50 := path
definition transport {A : Type} {a b : A} {P : A → Type} (H1 : a = b) (H2 : P a) : P b
:= path_rec H2 H1
namespace logic
notation p `*(`:75 u `)` := transport p u
end
using logic
definition symm {A : Type} {a b : A} (p : a = b) : b = a
:= p*(refl a)
definition trans {A : Type} {a b c : A} (p1 : a = b) (p2 : b = c) : a = c
:= p2*(p1)
calc_subst transport
calc_refl refl
calc_trans trans
namespace logic
postfix `⁻¹`:100 := symm
infixr `⬝`:75 := trans
end
using logic
theorem trans_refl_right {A : Type} {x y : A} (p : x = y) : p = p ⬝ (refl y)
:= refl p
theorem trans_refl_left {A : Type} {x y : A} (p : x = y) : p = (refl x) ⬝ p
:= path_rec (trans_refl_right (refl x)) p
theorem refl_symm {A : Type} (x : A) : (refl x)⁻¹ = (refl x)
:= refl (refl x)
theorem refl_trans {A : Type} (x : A) : (refl x) ⬝ (refl x) = (refl x)
:= refl (refl x)
theorem trans_symm {A : Type} {x y : A} (p : x = y) : p ⬝ p⁻¹ = refl x
:= have q : (refl x) ⬝ (refl x)⁻¹ = refl x, from
((refl_symm x)⁻¹)*(refl_trans x),
path_rec q p
theorem symm_trans {A : Type} {x y : A} (p : x = y) : p⁻¹ ⬝ p = refl y
:= have q : (refl x)⁻¹ ⬝ (refl x) = refl x, from
((refl_symm x)⁻¹)*(refl_trans x),
path_rec q p
theorem symm_symm {A : Type} {x y : A} (p : x = y) : (p⁻¹)⁻¹ = p
:= have q : ((refl x)⁻¹)⁻¹ = refl x, from
refl (refl x),
path_rec q p
theorem trans_assoc {A : Type} {x y z w : A} (p : x = y) (q : y = z) (r : z = w) : p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r
:= have e1 : (p ⬝ q) ⬝ (refl z) = p ⬝ q, from
(trans_refl_right (p ⬝ q))⁻¹,
have e2 : q ⬝ (refl z) = q, from
(trans_refl_right q)⁻¹,
have e3 : p ⬝ (q ⬝ (refl z)) = p ⬝ q, from
e2*(refl (p ⬝ (q ⬝ (refl z)))),
path_rec (e3 ⬝ e1⁻¹) r
definition ap {A : Type} {B : Type} (f : A → B) {a b : A} (p : a = b) : f a = f b
:= p*(refl (f a))
theorem ap_refl {A : Type} {B : Type} (f : A → B) (a : A) : ap f (refl a) = refl (f a)
:= refl (refl (f a))
section
parameters {A : Type} {B : Type} {C : Type}
parameters (f : A → B) (g : B → C)
parameters (x y z : A) (p : x = y) (q : y = z)
theorem ap_trans_dist : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q)
:= have e1 : ap f (p ⬝ refl y) = (ap f p) ⬝ (ap f (refl y)), from refl _,
path_rec e1 q
theorem ap_inv_dist : ap f (p⁻¹) = (ap f p)⁻¹
:= have e1 : ap f ((refl x)⁻¹) = (ap f (refl x))⁻¹, from refl _,
path_rec e1 p
theorem ap_compose : ap g (ap f p) = ap (g∘f) p
:= have e1 : ap g (ap f (refl x)) = ap (g∘f) (refl x), from refl _,
path_rec e1 p
theorem ap_id : ap id p = p
:= have e1 : ap id (refl x) = (refl x), from refl (refl x),
path_rec e1 p
end
section
parameters {A : Type} {B : A → Type} (f : Π x, B x)
definition D [private] (x y : A) (p : x = y) := p*(f x) = f y
definition d [private] (x : A) : D x x (refl x)
:= refl (f x)
theorem apd {a b : A} (p : a = b) : p*(f a) = f b
:= path_rec (d a) p
end
abbreviation homotopy {A : Type} {P : A → Type} (f g : Π x, P x)
:= Π x, f x = g x
namespace logic
infix ``:50 := homotopy
end
using logic
notation `assume` binders `,` r:(scoped f, f) := r
notation `take` binders `,` r:(scoped f, f) := r
section
parameters {A : Type} {B : Type}
theorem hom_refl (f : A → B) : f f
:= take x, refl (f x)
theorem hom_symm {f g : A → B} : f g → g f
:= assume h, take x, (h x)⁻¹
theorem hom_trans {f g h : A → B} : f g → g h → f h
:= assume h1 h2, take x, (h1 x) ⬝ (h2 x)
theorem hom_fun {f g : A → B} {x y : A} (H : f g) (p : x = y) : (H x) ⬝ (ap g p) = (ap f p) ⬝ (H y)
:= have e1 : (H x) ⬝ (refl (g x)) = (refl (f x)) ⬝ (H x), from
calc (H x) ⬝ (refl (g x)) = H x : (trans_refl_right (H x))⁻¹
... = (refl (f x)) ⬝ (H x) : trans_refl_left (H x),
have e2 : (H x) ⬝ (ap g (refl x)) = (ap f (refl x)) ⬝ (H x), from
calc (H x) ⬝ (ap g (refl x)) = (H x) ⬝ (refl (g x)) : {ap_refl g x}
... = (refl (f x)) ⬝ (H x) : e1
... = (ap f (refl x)) ⬝ (H x) : {symm (ap_refl f x)},
path_rec e2 p
end
definition loop_space (A : Type) (a : A) := a = a
notation `Ω` `(` A `,` a `)` := loop_space A a
definition loop2d_space (A : Type) (a : A) := (refl a) = (refl a)
notation `Ω²` `(` A `,` a `)` := loop2d_space A a
inductive empty : Type
theorem empty_elim (c : Type) (H : empty) : c
:= empty_rec (λ e, c) H
definition not (A : Type) := A → empty
prefix `¬`:40 := not
theorem not_intro {a : Type} (H : a → empty) : ¬ a
:= H
theorem not_elim {a : Type} (H1 : ¬ a) (H2 : a) : empty
:= H1 H2
theorem absurd {a : Type} (H1 : a) (H2 : ¬ a) : empty
:= H2 H1
theorem mt {a b : Type} (H1 : a → b) (H2 : ¬ b) : ¬ a
:= assume Ha : a, absurd (H1 Ha) H2
theorem contrapos {a b : Type} (H : a → b) : ¬ b → ¬ a
:= assume Hnb : ¬ b, mt H Hnb
theorem absurd_elim {a : Type} (b : Type) (H1 : a) (H2 : ¬ a) : b
:= empty_elim b (absurd H1 H2)
inductive unit : Type :=
| star : unit
notation `⋆`:max := star
theorem absurd_not_unit (H : ¬ unit) : empty
:= absurd star H
theorem not_empty_trivial : ¬ empty
:= assume H : empty, H
theorem upun (x : unit) : x = ⋆
:= unit_rec (refl ⋆) x
inductive product (A : Type) (B : Type) : Type :=
| pair : A → B → product A B
infixr `×`:30 := product
infixr `∧`:30 := product
notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t
definition pr1 {A : Type} {B : Type} (p : A × B) : A
:= product_rec (λ a b, a) p
definition pr2 {A : Type} {B : Type} (p : A × B) : B
:= product_rec (λ a b, b) p
theorem uppt {A : Type} {B : Type} (p : A × B) : (pr1 p, pr2 p) = p
:= product_rec (λ x y, refl (x, y)) p
inductive sum (A : Type) (B : Type) : Type :=
| inl : A → sum A B
| inr : B → sum A B
namespace logic
infixr `+`:25 := sum
end
using logic
infixr ``:25 := sum
theorem sum_elim {a : Type} {b : Type} {c : Type} (H1 : a + b) (H2 : a → c) (H3 : b → c) : c
:= sum_rec H2 H3 H1
theorem resolve_right {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ a) : b
:= sum_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb)
theorem resolve_left {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ b) : a
:= sum_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
theorem sum_flip {a : Type} {b : Type} (H : a + b) : b + a
:= sum_elim H (assume Ha, inr b Ha) (assume Hb, inl a Hb)
inductive bool : Type :=
| true : bool
| false : bool
theorem bool_cases (p : bool) : p = true p = false
:= bool_rec (inl _ (refl true)) (inr _ (refl false)) p
inductive Sigma {A : Type} (B : A → Type) : Type :=
| sigma_intro : Π a, B a → Sigma B
notation `Σ` binders `,` r:(scoped P, Sigma P) := r
definition dpr1 {A : Type} {B : A → Type} (p : Σ x, B x) : A
:= Sigma_rec (λ a b, a) p
definition dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p)
:= Sigma_rec (λ a b, b) p