<commit_before>definition Bool [inline] := Type.{0}

inductive false : Bool :=
-- No constructors

theorem false_elim (c : Bool) (H : false)
:= false_rec c H

inductive true : Bool :=
| trivial : true

definition not (a : Bool) := a → false
precedence `¬`:40
notation `¬` a := not a

notation `assume` binders `,` r:(scoped f, f) := r
notation `take`   binders `,` r:(scoped f, f) := r

theorem not_intro {a : Bool} (H : a → false) : ¬ a
:= H

theorem not_elim {a : Bool} (H1 : ¬ a) (H2 : a) : false
:= H1 H2

theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
:= H2 H1

theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
:= assume Ha : a, absurd (H1 Ha) H2

theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
:= assume Hnb : ¬ b, mt H Hnb

theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= false_elim b (absurd H1 H2)

inductive and (a b : Bool) : Bool :=
| and_intro : a → b → and a b

infixr `/\` 35 := and
infixr `∧`  35 := and

theorem and_elim_left {a b : Bool} (H : a ∧ b) : a
:= and_rec (λ a b, a) H

theorem and_elim_right {a b : Bool} (H : a ∧ b) : b
:= and_rec (λ a b, b) H

inductive or (a b : Bool) : Bool :=
| or_intro_left  : a → or a b
| or_intro_right : b → or a b

infixr `\/` 30 := or
infixr `∨` 30 := or

theorem or_elim (a b c : Bool) (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= or_rec H2 H3 H1

inductive eq {A : Type} (a : A) : A → Bool :=
| refl : eq a a

infix `=` 50 := eq

theorem subst {A : Type} {a b : A} {P : A → Bool} (H1 : a = b) (H2 : P a) : P b
:= eq_rec H2 H1

theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
:= subst H2 H1

theorem symm {A : Type} {a b : A} (H : a = b) : b = a
:= subst H (refl a)

theorem congr1 {A B : Type} {f g : A → B} (H : f = g) (a : A) : f a = g a
:= subst H (refl (f a))

theorem congr2 {A B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b
:= subst H (refl (f a))

definition cast {A B : Type} (H : A = B) (a : A) : B
:= eq_rec a H

-- TODO(Leo): check why unifier needs 'help' in the following theorem
theorem cast_refl.{l} {A : Type.{l}} (a : A) : @cast.{l} A A (refl A) a = a
:= refl (@cast.{l} A A (refl A) a)

definition iff (a b : Bool) := (a → b) ∧ (b → a)
infix `↔` 50 := iff

theorem iff_intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a ↔ b
:= and_intro H1 H2

theorem iff_elim {a b c : Bool} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c
:= and_rec H1 H2

theorem iff_elim_left {a b : Bool} (H : a ↔ b) : a → b
:= iff_elim (assume H1 H2, H1) H

theorem iff_elim_right {a b : Bool} (H : a ↔ b) : b → a
:= iff_elim (assume H1 H2, H2) H

inductive Exists {A : Type} (P : A → Bool) : Bool :=
| exists_intro : ∀ (a : A), P a → Exists P

notation `∃` binders `,` r:(scoped P, Exists P) := r<commit_msg>feat(library/standard): add iff_mp_right and iff_mp_left<commit_after>definition Bool [inline] := Type.{0}

inductive false : Bool :=
-- No constructors

theorem false_elim (c : Bool) (H : false)
:= false_rec c H

inductive true : Bool :=
| trivial : true

definition not (a : Bool) := a → false
precedence `¬`:40
notation `¬` a := not a

notation `assume` binders `,` r:(scoped f, f) := r
notation `take`   binders `,` r:(scoped f, f) := r

theorem not_intro {a : Bool} (H : a → false) : ¬ a
:= H

theorem not_elim {a : Bool} (H1 : ¬ a) (H2 : a) : false
:= H1 H2

theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
:= H2 H1

theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
:= assume Ha : a, absurd (H1 Ha) H2

theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
:= assume Hnb : ¬ b, mt H Hnb

theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= false_elim b (absurd H1 H2)

inductive and (a b : Bool) : Bool :=
| and_intro : a → b → and a b

infixr `/\` 35 := and
infixr `∧`  35 := and

theorem and_elim_left {a b : Bool} (H : a ∧ b) : a
:= and_rec (λ a b, a) H

theorem and_elim_right {a b : Bool} (H : a ∧ b) : b
:= and_rec (λ a b, b) H

inductive or (a b : Bool) : Bool :=
| or_intro_left  : a → or a b
| or_intro_right : b → or a b

infixr `\/` 30 := or
infixr `∨` 30 := or

theorem or_elim (a b c : Bool) (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= or_rec H2 H3 H1

inductive eq {A : Type} (a : A) : A → Bool :=
| refl : eq a a

infix `=` 50 := eq

theorem subst {A : Type} {a b : A} {P : A → Bool} (H1 : a = b) (H2 : P a) : P b
:= eq_rec H2 H1

theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
:= subst H2 H1

theorem symm {A : Type} {a b : A} (H : a = b) : b = a
:= subst H (refl a)

theorem congr1 {A B : Type} {f g : A → B} (H : f = g) (a : A) : f a = g a
:= subst H (refl (f a))

theorem congr2 {A B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b
:= subst H (refl (f a))

definition cast {A B : Type} (H : A = B) (a : A) : B
:= eq_rec a H

-- TODO(Leo): check why unifier needs 'help' in the following theorem
theorem cast_refl.{l} {A : Type.{l}} (a : A) : @cast.{l} A A (refl A) a = a
:= refl (@cast.{l} A A (refl A) a)

definition iff (a b : Bool) := (a → b) ∧ (b → a)
infix `↔` 50 := iff

theorem iff_intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a ↔ b
:= and_intro H1 H2

theorem iff_elim {a b c : Bool} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c
:= and_rec H1 H2

theorem iff_elim_left {a b : Bool} (H : a ↔ b) : a → b
:= iff_elim (assume H1 H2, H1) H

theorem iff_elim_right {a b : Bool} (H : a ↔ b) : b → a
:= iff_elim (assume H1 H2, H2) H

theorem iff_mp_left {a b : Bool} (H1 : a ↔ b) (H2 : a) : b
:= (iff_elim_left H1) H2

theorem iff_mp_right {a b : Bool} (H1 : a ↔ b) (H2 : b) : a
:= (iff_elim_right H1) H2

inductive Exists {A : Type} (P : A → Bool) : Bool :=
| exists_intro : ∀ (a : A), P a → Exists P

notation `∃` binders `,` r:(scoped P, Exists P) := r
{'fraction_non_alphanumeric': 0.1889652741054116, 'fraction_numerical': 0.022915564956812975, 'mean_word_length': 2.651222651222651, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6689894', 'n_tokens_mistral': 2830, 'n_tokens_neox': 2645, 'n_words': 1097}