diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 5aeace60e..63ec2712a 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -13,26 +13,26 @@ prefix `¬` := not definition absurd {a : Type} {b : Type} (H₁ : a) (H₂ : ¬a) : b := empty.rec (λ e, b) (H₂ H₁) -theorem mt {a b : Type} (H₁ : a → b) (H₂ : ¬b) : ¬a := +definition mt {a b : Type} (H₁ : a → b) (H₂ : ¬b) : ¬a := assume Ha : a, absurd (H₁ Ha) H₂ -- not -- --- -theorem not_empty : ¬ empty := +definition not_empty : ¬ empty := assume H : empty, H -theorem not_not_intro {a : Type} (Ha : a) : ¬¬a := +definition not_not_intro {a : Type} (Ha : a) : ¬¬a := assume Hna : ¬a, absurd Ha Hna -theorem not_intro {a : Type} (H : a → empty) : ¬a := H +definition not_intro {a : Type} (H : a → empty) : ¬a := H -theorem not_elim {a : Type} (H₁ : ¬a) (H₂ : a) : empty := H₁ H₂ +definition not_elim {a : Type} (H₁ : ¬a) (H₂ : a) : empty := H₁ H₂ -theorem not_implies_left {a b : Type} (H : ¬(a → b)) : ¬¬a := +definition not_implies_left {a b : Type} (H : ¬(a → b)) : ¬¬a := assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H -theorem not_implies_right {a b : Type} (H : ¬(a → b)) : ¬b := +definition not_implies_right {a b : Type} (H : ¬(a → b)) : ¬b := assume Hb : b, absurd (assume Ha : a, Hb) H -- eq @@ -45,10 +45,10 @@ namespace eq variables {A : Type} variables {a b c a': A} - theorem subst {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b := + definition subst {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b := rec H₂ H₁ - theorem trans (H₁ : a = b) (H₂ : b = c) : a = c := + definition trans (H₁ : a = b) (H₂ : b = c) : a = c := subst H₂ H₁ definition symm (H : a = b) : b = a := @@ -85,16 +85,16 @@ namespace ne variable {A : Type} variables {a b : A} - theorem intro : (a = b → empty) → a ≠ b := + definition intro : (a = b → empty) → a ≠ b := assume H, H - theorem elim : a ≠ b → a = b → empty := + definition elim : a ≠ b → a = b → empty := assume H₁ H₂, H₁ H₂ - theorem irrefl : a ≠ a → empty := + definition irrefl : a ≠ a → empty := assume H, H rfl - theorem symm : a ≠ b → b ≠ a := + definition symm : a ≠ b → b ≠ a := assume (H : a ≠ b) (H₁ : b = a), H (H₁⁻¹) end ne @@ -102,13 +102,13 @@ section open eq.ops variables {A : Type} {a b c : A} - theorem false.of_ne : a ≠ a → empty := + definition false.of_ne : a ≠ a → empty := assume H, H rfl - theorem ne.of_eq_of_ne : a = b → b ≠ c → a ≠ c := + definition ne.of_eq_of_ne : a = b → b ≠ c → a ≠ c := assume H₁ H₂, H₁⁻¹ ▸ H₂ - theorem ne.of_ne_of_eq : a ≠ b → b = c → a ≠ c := + definition ne.of_ne_of_eq : a ≠ b → b = c → a ≠ c := assume H₁ H₂, H₂ ▸ H₁ end @@ -154,24 +154,24 @@ namespace iff definition rfl {a : Type} : a ↔ a := refl a - theorem trans (H₁ : a ↔ b) (H₂ : b ↔ c) : a ↔ c := + definition trans (H₁ : a ↔ b) (H₂ : b ↔ c) : a ↔ c := intro (assume Ha, elim_left H₂ (elim_left H₁ Ha)) (assume Hc, elim_right H₁ (elim_right H₂ Hc)) - theorem symm (H : a ↔ b) : b ↔ a := + definition symm (H : a ↔ b) : b ↔ a := intro (assume Hb, elim_right H Hb) (assume Ha, elim_left H Ha) - theorem true_elim (H : a ↔ unit) : a := + definition true_elim (H : a ↔ unit) : a := mp (symm H) unit.star - theorem false_elim (H : a ↔ empty) : ¬a := + definition false_elim (H : a ↔ empty) : ¬a := assume Ha : a, mp H Ha open eq.ops - theorem of_eq {a b : Type} (H : a = b) : a ↔ b := + definition of_eq {a b : Type} (H : a = b) : a ↔ b := iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) end iff @@ -219,10 +219,10 @@ namespace decidable definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q := rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp) - theorem em (p : Type) [H : decidable p] : sum p ¬p := + definition em (p : Type) [H : decidable p] : sum p ¬p := by_cases (λ Hp, sum.inl Hp) (λ Hnp, sum.inr Hnp) - theorem by_contradiction [Hp : decidable p] (H : ¬p → empty) : p := + definition by_contradiction [Hp : decidable p] (H : ¬p → empty) : p := by_cases (assume H₁ : p, H₁) (assume H₁ : ¬p, empty.rec (λ e, p) (H H₁)) @@ -306,7 +306,7 @@ if_pos unit.star definition if_empty {A : Type} (t e : A) : (if empty then t else e) = e := if_neg not_empty -theorem if_cond_congr {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A) +definition if_cond_congr {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A) : (if c₁ then t else e) = (if c₂ then t else e) := decidable.rec_on H₁ (λ Hc₁ : c₁, decidable.rec_on H₂ @@ -316,12 +316,12 @@ decidable.rec_on H₁ (λ Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁) (λ Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹)) -theorem if_congr_aux {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] {A : Type} {t₁ t₂ e₁ e₂ : A} +definition if_congr_aux {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) := Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁) -theorem if_congr {c₁ c₂ : Type} [H₁ : decidable c₁] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : +definition if_congr {c₁ c₂ : Type} [H₁ : decidable c₁] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : (if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) := have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc), if_congr_aux Hc Ht He @@ -345,5 +345,5 @@ decidable.rec H -- Remark: dite and ite are "definitionally equal" when we ignore the proofs. -theorem dite_ite_eq (c : Type) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e := +definition dite_ite_eq (c : Type) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e := rfl diff --git a/hott/init/relation.hlean b/hott/init/relation.hlean index 29935d81f..91e315482 100644 --- a/hott/init/relation.hlean +++ b/hott/init/relation.hlean @@ -29,10 +29,10 @@ definition subrelation (Q R : B → B → Type) := ∀⦃x y⦄, Q x y → R x y definition inv_image (f : A → B) : A → A → Type := λa₁ a₂, f a₁ ≺ f a₂ -theorem inv_image.trans (f : A → B) (H : transitive R) : transitive (inv_image R f) := +definition inv_image.trans (f : A → B) (H : transitive R) : transitive (inv_image R f) := λ (a₁ a₂ a₃ : A) (H₁ : inv_image R f a₁ a₂) (H₂ : inv_image R f a₂ a₃), H H₁ H₂ -theorem inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (inv_image R f) := +definition inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (inv_image R f) := λ (a : A) (H₁ : inv_image R f a a), H (f a) H₁ inductive tc {A : Type} (R : A → A → Type) : A → A → Type := diff --git a/hott/init/wf.hlean b/hott/init/wf.hlean index 6c5eaf646..53073f42a 100644 --- a/hott/init/wf.hlean +++ b/hott/init/wf.hlean @@ -29,10 +29,10 @@ namespace well_founded hypothesis [Hwf : well_founded R] - theorem recursion {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a := + definition recursion {C : A → Type} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a := acc.rec_on (Hwf a) (λ x₁ ac₁ iH, H x₁ iH) - theorem induction {C : A → Type} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a := + definition induction {C : A → Type} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a := recursion a H parameter {C : A → Type} @@ -41,7 +41,7 @@ namespace well_founded definition fix_F (x : A) (a : acc R x) : C x := acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH) - theorem fix_F_eq (x : A) (r : acc R x) : + definition fix_F_eq (x : A) (r : acc R x) : fix_F x r = F x (λ (y : A) (p : y ≺ x), fix_F y (acc.inv r p)) := acc.rec_on r (λ x H ih, rfl) @@ -75,7 +75,7 @@ namespace well_founded fix_F x (Hwf x) -- Well-founded fixpoint satisfies fixpoint equation - theorem fix_eq (x : A) : fix x = F x (λy h, fix y) := + definition fix_eq (x : A) : fix x = F x (λy h, fix y) := calc fix x = fix_F x (Hwf x) : rfl