<commit_before>/-
Copyright (c) 2016 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>

Theorems that require decidability hypotheses are in the namespace "decidable".
Classical versions are in the namespace "classical".

Note: in the presence of automation, this whole file may be unnecessary. On the other hand,
maybe it is useful for writing automation.
-/
import data.prod tactic.cache

/-
    miscellany

    TODO: move elsewhere
-/

section miscellany

variables {α : Type*} {β : Type*}

@[reducible] def hidden {a : α} := a

def empty.elim {C : Sort*} : empty → C.

instance : subsingleton empty := ⟨λa, a.elim⟩

instance : decidable_eq empty := λa, a.elim

@[priority 0] instance decidable_eq_of_subsingleton
  {α} [subsingleton α] : decidable_eq α
| a b := is_true (subsingleton.elim a b)

/- Add an instance to "undo" coercion transitivity into a chain of coercions, because
   most simp lemmas are stated with respect to simple coercions and will not match when
   part of a chain. -/
@[simp] theorem coe_coe {α β γ} [has_coe α β] [has_coe_t β γ]
  (a : α) : (a : γ) = (a : β) := rfl

@[simp] theorem coe_fn_coe_trans
  {α β γ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_fun γ]
  (x : α) : @coe_fn α _ x = @coe_fn β _ x := rfl

@[simp] theorem coe_fn_coe_base
  {α β} [has_coe α β] [has_coe_to_fun β]
  (x : α) : @coe_fn α _ x = @coe_fn β _ x := rfl

@[simp] theorem coe_sort_coe_trans
  {α β γ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_sort γ]
  (x : α) : @coe_sort α _ x = @coe_sort β _ x := rfl

@[simp] theorem coe_sort_coe_base
  {α β} [has_coe α β] [has_coe_to_sort β]
  (x : α) : @coe_sort α _ x = @coe_sort β _ x := rfl

/-- `pempty` is the universe-polymorphic analogue of `empty`. -/
@[derive decidable_eq]
inductive {u} pempty : Sort u

def pempty.elim {C : Sort*} : pempty → C.

instance subsingleton_pempty : subsingleton pempty := ⟨λa, a.elim⟩

lemma congr_arg_heq {α} {β : α → Sort*} (f : ∀ a, β a) : ∀ {a₁ a₂ : α}, a₁ = a₂ → f a₁ == f a₂
| a _ rfl := heq.rfl

end miscellany

/-
    propositional connectives
-/

@[simp] theorem false_ne_true : false ≠ true
| h := h.symm ▸ trivial

section propositional
variables {a b c d : Prop}

/- implies -/

theorem iff_of_eq (e : a = b) : a ↔ b := e ▸ iff.rfl

theorem iff_iff_eq : (a ↔ b) ↔ a = b := ⟨propext, iff_of_eq⟩

@[simp] theorem imp_self : (a → a) ↔ true := iff_true_intro id

theorem imp_intro {α β} (h : α) (h₂ : β) : α := h

theorem imp_false : (a → false) ↔ ¬ a := iff.rfl

theorem imp_and_distrib {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) :=
⟨λ h, ⟨λ ha, (h ha).left, λ ha, (h ha).right⟩,
 λ h ha, ⟨h.left ha, h.right ha⟩⟩

@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) :=<commit_msg>feat(logic): add plift.down_inj<commit_after>/-
Copyright (c) 2016 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>

Theorems that require decidability hypotheses are in the namespace "decidable".
Classical versions are in the namespace "classical".

Note: in the presence of automation, this whole file may be unnecessary. On the other hand,
maybe it is useful for writing automation.
-/
import data.prod tactic.cache

/-
    miscellany

    TODO: move elsewhere
-/

section miscellany

variables {α : Type*} {β : Type*}

@[reducible] def hidden {a : α} := a

def empty.elim {C : Sort*} : empty → C.

instance : subsingleton empty := ⟨λa, a.elim⟩

instance : decidable_eq empty := λa, a.elim

@[priority 0] instance decidable_eq_of_subsingleton
  {α} [subsingleton α] : decidable_eq α
| a b := is_true (subsingleton.elim a b)

/- Add an instance to "undo" coercion transitivity into a chain of coercions, because
   most simp lemmas are stated with respect to simple coercions and will not match when
   part of a chain. -/
@[simp] theorem coe_coe {α β γ} [has_coe α β] [has_coe_t β γ]
  (a : α) : (a : γ) = (a : β) := rfl

@[simp] theorem coe_fn_coe_trans
  {α β γ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_fun γ]
  (x : α) : @coe_fn α _ x = @coe_fn β _ x := rfl

@[simp] theorem coe_fn_coe_base
  {α β} [has_coe α β] [has_coe_to_fun β]
  (x : α) : @coe_fn α _ x = @coe_fn β _ x := rfl

@[simp] theorem coe_sort_coe_trans
  {α β γ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_sort γ]
  (x : α) : @coe_sort α _ x = @coe_sort β _ x := rfl

@[simp] theorem coe_sort_coe_base
  {α β} [has_coe α β] [has_coe_to_sort β]
  (x : α) : @coe_sort α _ x = @coe_sort β _ x := rfl

/-- `pempty` is the universe-polymorphic analogue of `empty`. -/
@[derive decidable_eq]
inductive {u} pempty : Sort u

def pempty.elim {C : Sort*} : pempty → C.

instance subsingleton_pempty : subsingleton pempty := ⟨λa, a.elim⟩

lemma congr_arg_heq {α} {β : α → Sort*} (f : ∀ a, β a) : ∀ {a₁ a₂ : α}, a₁ = a₂ → f a₁ == f a₂
| a _ rfl := heq.rfl

lemma plift.down_inj {α : Sort*} : ∀ (a b : plift α), a.down = b.down → a = b
| ⟨a⟩ ⟨b⟩ rfl := rfl

end miscellany

/-
    propositional connectives
-/

@[simp] theorem false_ne_true : false ≠ true
| h := h.symm ▸ trivial

section propositional
variables {a b c d : Prop}

/- implies -/

theorem iff_of_eq (e : a = b) : a ↔ b := e ▸ iff.rfl

theorem iff_iff_eq : (a ↔ b) ↔ a = b := ⟨propext, iff_of_eq⟩

@[simp] theorem imp_self : (a → a) ↔ true := iff_true_intro id

theorem imp_intro {α β} (h : α) (h₂ : β) : α := h

theorem imp_false : (a → false) ↔ ¬ a := iff.rfl

theorem imp_and_distrib {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) :=
⟨λ h, ⟨λ ha, (h ha).left, λ ha, (h ha).right⟩,
 λ h ha, ⟨h.left ha, h.right ha⟩⟩

@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) :=
{'fraction_non_alphanumeric': 0.13947274670466692, 'fraction_numerical': 0.0024937655860349127, 'mean_word_length': 3.2960979342004593, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, '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': '1264937', 'n_tokens_mistral': 2578, 'n_tokens_neox': 2373, 'n_words': 864}