lean2/library/init/logic.lean

634 lines
22 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.
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-/
prelude
import init.datatypes init.reserved_notation
/- implication -/
definition implies (a b : Prop) := a → b
lemma implies.trans [trans] {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
assume hp, h₂ (h₁ hp)
definition trivial := true.intro
definition not (a : Prop) := a → false
prefix `¬` := not
theorem absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
false.rec b (H2 H1)
/- not -/
theorem not_false : ¬false :=
assume H : false, H
definition non_contradictory (a : Prop) : Prop := ¬¬a
theorem non_contradictory_intro {a : Prop} (Ha : a) : ¬¬a :=
assume Hna : ¬a, absurd Ha Hna
/- eq -/
notation a = b := eq a b
theorem rfl {A : Type} {a : A} : a = a := eq.refl a
-- proof irrelevance is built in
theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=
rfl
-- Remark: we provide the universe levels explicitly to make sure `eq.drec` has the same type of `eq.rec` in the HoTT library
protected theorem eq.drec.{l₁ l₂} {A : Type.{l₂}} {a : A} {C : Π (x : A), a = x → Type.{l₁}} (h₁ : C a (eq.refl a)) {b : A} (h₂ : a = b) : C b h₂ :=
eq.rec (λh₂ : a = a, show C a h₂, from h₁) h₂ h₂
namespace eq
variables {A : Type}
variables {a b c a': A}
protected theorem drec_on {a : A} {C : Π (x : A), a = x → Type} {b : A} (h₂ : a = b) (h₁ : C a (refl a)) : C b h₂ :=
eq.drec h₁ h₂
theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b :=
eq.rec H₂ H₁
theorem trans (H₁ : a = b) (H₂ : b = c) : a = c :=
subst H₂ H₁
theorem symm (H : a = b) : b = a :=
eq.rec (refl a) H
namespace ops
notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
notation H1 ⬝ H2 := trans H1 H2
notation H1 ▸ H2 := subst H1 H2
end ops
end eq
theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
eq.subst H₁ (eq.subst H₂ rfl)
section
variables {A : Type} {a b c: A}
open eq.ops
theorem trans_rel_left (R : A → A → Prop) (H₁ : R a b) (H₂ : b = c) : R a c :=
H₂ ▸ H₁
theorem trans_rel_right (R : A → A → Prop) (H₁ : a = b) (H₂ : R b c) : R a c :=
H₁⁻¹ ▸ H₂
end
section
variable {p : Prop}
open eq.ops
theorem of_eq_true (H : p = true) : p :=
H⁻¹ ▸ trivial
theorem not_of_eq_false (H : p = false) : ¬p :=
assume Hp, H ▸ Hp
end
attribute eq.subst [subst]
attribute eq.refl [refl]
attribute eq.trans [trans]
attribute eq.symm [symm]
/- ne -/
definition ne {A : Type} (a b : A) := ¬(a = b)
notation a ≠ b := ne a b
namespace ne
open eq.ops
variable {A : Type}
variables {a b : A}
theorem intro : (a = b → false) → a ≠ b :=
assume H, H
theorem elim : a ≠ b → a = b → false :=
assume H₁ H₂, H₁ H₂
theorem irrefl : a ≠ a → false :=
assume H, H rfl
theorem symm : a ≠ b → b ≠ a :=
assume (H : a ≠ b) (H₁ : b = a), H (H₁⁻¹)
end ne
section
variables {A : Type} {a : A}
theorem false.of_ne : a ≠ a → false :=
assume H, H rfl
end
infixl `==`:50 := heq
namespace heq
universe variable u
variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
theorem to_eq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
λ Ht, eq.refl (eq.rec_on Ht a),
heq.rec_on H H₁ (eq.refl A)
theorem elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b :=
eq.rec_on (to_eq H₁) H₂
theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
heq.rec_on H₁ H₂
theorem symm (H : a == b) : b == a :=
heq.rec_on H (refl a)
theorem of_eq (H : a = a') : a == a' :=
eq.subst H (refl a)
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
subst H₂ H₁
theorem of_heq_of_eq (H₁ : a == b) (H₂ : b = b') : a == b' :=
trans H₁ (of_eq H₂)
theorem of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b :=
trans (of_eq H₁) H₂
end heq
theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p :=
eq.drec_on H !heq.refl
theorem of_heq_true {a : Prop} (H : a == true) : a :=
of_eq_true (heq.to_eq H)
attribute heq.refl [refl]
attribute heq.trans [trans]
attribute heq.of_heq_of_eq [trans]
attribute heq.of_eq_of_heq [trans]
attribute heq.symm [symm]
/- and -/
notation a /\ b := and a b
notation a ∧ b := and a b
variables {a b c d : Prop}
theorem and.elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
and.rec H₂ H₁
/- or -/
notation a `\/` b := or a b
notation a b := or a b
namespace or
theorem elim (H₁ : a b) (H₂ : a → c) (H₃ : b → c) : c :=
or.rec H₂ H₃ H₁
end or
theorem non_contradictory_em (a : Prop) : ¬¬(a ¬a) :=
assume not_em : ¬(a ¬a),
have neg_a : ¬a, from
assume pos_a : a, absurd (or.inl pos_a) not_em,
absurd (or.inr neg_a) not_em
/- iff -/
definition iff (a b : Prop) := (a → b) ∧ (b → a)
notation a <-> b := iff a b
notation a ↔ b := iff a b
namespace iff
theorem intro (H₁ : a → b) (H₂ : b → a) : a ↔ b :=
and.intro H₁ H₂
theorem elim (H₁ : (a → b) → (b → a) → c) (H₂ : a ↔ b) : c :=
and.rec H₁ H₂
theorem elim_left (H : a ↔ b) : a → b :=
elim (assume H₁ H₂, H₁) H
definition mp := @elim_left
theorem elim_right (H : a ↔ b) : b → a :=
elim (assume H₁ H₂, H₂) H
definition mp' := @elim_right
theorem refl (a : Prop) : a ↔ a :=
intro (assume H, H) (assume H, H)
theorem rfl {a : Prop} : a ↔ a :=
refl a
theorem 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 :=
intro
(assume Hb, elim_right H Hb)
(assume Ha, elim_left H Ha)
open eq.ops
theorem of_eq {a b : Prop} (H : a = b) : a ↔ b :=
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
end iff
theorem not_iff_not_of_iff (H₁ : a ↔ b) : ¬a ↔ ¬b :=
iff.intro
(assume (Hna : ¬ a) (Hb : b), absurd (iff.elim_right H₁ Hb) Hna)
(assume (Hnb : ¬ b) (Ha : a), absurd (iff.elim_left H₁ Ha) Hnb)
theorem of_iff_true (H : a ↔ true) : a :=
iff.mp (iff.symm H) trivial
theorem not_of_iff_false (H : a ↔ false) : ¬a :=
assume Ha : a, iff.mp H Ha
theorem iff_true_intro (H : a) : a ↔ true :=
iff.intro
(λ Hl, trivial)
(λ Hr, H)
theorem iff_false_intro (H : ¬a) : a ↔ false :=
iff.intro
(λ Hl, absurd Hl H)
(λ Hr, false.rec _ Hr)
theorem not_non_contradictory_iff_absurd (a : Prop) : ¬¬¬a ↔ ¬a :=
iff.intro
(assume Hl : ¬¬¬a,
assume Ha : a, absurd (non_contradictory_intro Ha) Hl)
(assume Hr : ¬a,
assume Hnna : ¬¬a, absurd Hr Hnna)
attribute iff.refl [refl]
attribute iff.symm [symm]
attribute iff.trans [trans]
inductive Exists {A : Type} (P : A → Prop) : Prop :=
intro : ∀ (a : A), P a → Exists P
definition exists.intro := @Exists.intro
notation `exists` binders `,` r:(scoped P, Exists P) := r
notation `∃` binders `,` r:(scoped P, Exists P) := r
theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
Exists.rec H2 H1
/- decidable -/
inductive decidable [class] (p : Prop) : Type :=
| inl : p → decidable p
| inr : ¬p → decidable p
definition decidable_true [instance] : decidable true :=
decidable.inl trivial
definition decidable_false [instance] : decidable false :=
decidable.inr not_false
namespace decidable
variables {p q : Prop}
definition rec_on_true [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3)
: decidable.rec_on H H1 H2 :=
decidable.rec_on H (λh, H4) (λh, !false.rec (h H3))
definition rec_on_false [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3)
: decidable.rec_on H H1 H2 :=
decidable.rec_on H (λh, false.rec _ (H3 h)) (λh, H4)
definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q :=
decidable.rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
theorem em (p : Prop) [H : decidable p] : p ¬p :=
by_cases (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
by_cases
(assume H1 : p, H1)
(assume H1 : ¬p, false.rec _ (H H1))
end decidable
section
variables {p q : Prop}
open decidable
definition decidable_of_decidable_of_iff (Hp : decidable p) (H : p ↔ q) : decidable q :=
decidable.rec_on Hp
(assume Hp : p, inl (iff.elim_left H Hp))
(assume Hnp : ¬p, inr (iff.elim_left (not_iff_not_of_iff H) Hnp))
definition decidable_of_decidable_of_eq (Hp : decidable p) (H : p = q) : decidable q :=
decidable_of_decidable_of_iff Hp (iff.of_eq H)
end
section
variables {p q : Prop}
open decidable (rec_on inl inr)
definition decidable_and [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∧ q) :=
rec_on Hp
(assume Hp : p, rec_on Hq
(assume Hq : q, inl (and.intro Hp Hq))
(assume Hnq : ¬q, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hq Hnq))))
(assume Hnp : ¬p, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hp Hnp)))
definition decidable_or [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p q) :=
rec_on Hp
(assume Hp : p, inl (or.inl Hp))
(assume Hnp : ¬p, rec_on Hq
(assume Hq : q, inl (or.inr Hq))
(assume Hnq : ¬q, inr (assume H : p q, or.elim H (assume Hp, absurd Hp Hnp) (assume Hq, absurd Hq Hnq))))
definition decidable_not [instance] [Hp : decidable p] : decidable (¬p) :=
rec_on Hp
(assume Hp, inr (λ Hnp, absurd Hp Hnp))
(assume Hnp, inl Hnp)
definition decidable_implies [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p → q) :=
rec_on Hp
(assume Hp : p, rec_on Hq
(assume Hq : q, inl (assume H, Hq))
(assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq)))
(assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp))
definition decidable_iff [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ↔ q) :=
show decidable ((p → q) ∧ (q → p)), from _
end
definition decidable_pred [reducible] {A : Type} (R : A → Prop) := Π (a : A), decidable (R a)
definition decidable_rel [reducible] {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b)
definition decidable_eq [reducible] (A : Type) := decidable_rel (@eq A)
definition decidable_ne [instance] {A : Type} [H : decidable_eq A] : Π (a b : A), decidable (a ≠ b) :=
show Π x y : A, decidable (x = y → false), from _
namespace bool
theorem ff_ne_tt : ff = tt → false
| [none]
end bool
open bool
definition is_dec_eq {A : Type} (p : A → A → bool) : Prop := ∀ ⦃x y : A⦄, p x y = tt → x = y
definition is_dec_refl {A : Type} (p : A → A → bool) : Prop := ∀x, p x x = tt
open decidable
protected definition bool.has_decidable_eq [instance] : ∀a b : bool, decidable (a = b)
| ff ff := inl rfl
| ff tt := inr ff_ne_tt
| tt ff := inr (ne.symm ff_ne_tt)
| tt tt := inl rfl
definition decidable_eq_of_bool_pred {A : Type} {p : A → A → bool} (H₁ : is_dec_eq p) (H₂ : is_dec_refl p) : decidable_eq A :=
take x y : A, by_cases
(assume Hp : p x y = tt, inl (H₁ Hp))
(assume Hn : ¬ p x y = tt, inr (assume Hxy : x = y, absurd (H₂ y) (eq.rec_on Hxy Hn)))
theorem decidable_eq_inl_refl {A : Type} [H : decidable_eq A] (a : A) : H a a = inl (eq.refl a) :=
match H a a with
| inl e := rfl
| inr n := absurd rfl n
end
open eq.ops
theorem decidable_eq_inr_neg {A : Type} [H : decidable_eq A] {a b : A} : Π n : a ≠ b, H a b = inr n :=
assume n,
match H a b with
| inl e := absurd e n
| inr n₁ := proof_irrel n n₁ ▸ rfl
end
/- inhabited -/
inductive inhabited [class] (A : Type) : Type :=
mk : A → inhabited A
protected definition inhabited.value {A : Type} (h : inhabited A) : A :=
inhabited.rec (λa, a) h
protected definition inhabited.destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
inhabited.rec H2 H1
definition default (A : Type) [H : inhabited A] : A :=
inhabited.rec (λa, a) H
definition arbitrary [irreducible] (A : Type) [H : inhabited A] : A :=
inhabited.rec (λa, a) H
definition Prop.is_inhabited [instance] : inhabited Prop :=
inhabited.mk true
definition inhabited_fun [instance] (A : Type) {B : Type} [H : inhabited B] : inhabited (A → B) :=
inhabited.rec_on H (λb, inhabited.mk (λa, b))
definition inhabited_Pi [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] :
inhabited (Πx, B x) :=
inhabited.mk (λa, inhabited.rec_on (H a) (λb, b))
protected definition bool.is_inhabited [instance] : inhabited bool :=
inhabited.mk ff
inductive nonempty [class] (A : Type) : Prop :=
intro : A → nonempty A
protected definition nonempty.elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
nonempty.rec H2 H1
theorem nonempty_of_inhabited [instance] {A : Type} [H : inhabited A] : nonempty A :=
nonempty.intro (default A)
/- subsingleton -/
inductive subsingleton [class] (A : Type) : Prop :=
intro : (∀ a b : A, a = b) → subsingleton A
protected definition subsingleton.elim {A : Type} [H : subsingleton A] : ∀(a b : A), a = b :=
subsingleton.rec (fun p, p) H
definition subsingleton_prop [instance] (p : Prop) : subsingleton p :=
subsingleton.intro (λa b, !proof_irrel)
definition subsingleton_decidable [instance] (p : Prop) : subsingleton (decidable p) :=
subsingleton.intro (λ d₁,
match d₁ with
| inl t₁ := (λ d₂,
match d₂ with
| inl t₂ := eq.rec_on (proof_irrel t₁ t₂) rfl
| inr f₂ := absurd t₁ f₂
end)
| inr f₁ := (λ d₂,
match d₂ with
| inl t₂ := absurd t₂ f₁
| inr f₂ := eq.rec_on (proof_irrel f₁ f₂) rfl
end)
end)
protected theorem rec_subsingleton {p : Prop} [H : decidable p]
{H1 : p → Type} {H2 : ¬p → Type}
[H3 : Π(h : p), subsingleton (H1 h)] [H4 : Π(h : ¬p), subsingleton (H2 h)]
: subsingleton (decidable.rec_on H H1 H2) :=
decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"
/- if-then-else -/
definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
decidable.rec_on H (λ Hc, t) (λ Hnc, e)
theorem if_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t :=
decidable.rec
(λ Hc : c, eq.refl (@ite c (decidable.inl Hc) A t e))
(λ Hnc : ¬c, absurd Hc Hnc)
H
theorem if_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e :=
decidable.rec
(λ Hc : c, absurd Hc Hnc)
(λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t e))
H
theorem if_t_t (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t :=
decidable.rec
(λ Hc : c, eq.refl (@ite c (decidable.inl Hc) A t t))
(λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t t))
H
theorem implies_of_if_pos {c t e : Prop} [H : decidable c] (h : if c then t else e) : c → t :=
assume Hc, eq.rec_on (if_pos Hc) h
theorem implies_of_if_neg {c t e : Prop} [H : decidable c] (h : if c then t else e) : ¬c → e :=
assume Hnc, eq.rec_on (if_neg Hnc) h
theorem if_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x y u v : A}
(h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
(if b then x else y) = (if c then u else v) :=
decidable.rec_on dec_b
(λ hp : b, calc
(if b then x else y)
= x : if_pos hp
... = u : h_t (iff.mp h_c hp)
... = (if c then u else v) : if_pos (iff.mp h_c hp))
(λ hn : ¬b, calc
(if b then x else y)
= y : if_neg hn
... = v : h_e (iff.mp (not_iff_not_of_iff h_c) hn)
... = (if c then u else v) : if_neg (iff.mp (not_iff_not_of_iff h_c) hn))
theorem if_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x y u v : A}
(h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
(if b then x else y) = (if c then u else v) :=
@if_ctx_congr A b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e)
theorem if_ctx_rw_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A}
(h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
(if b then x else y) = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
@if_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e
theorem if_rw_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A}
(h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
(if b then x else y) = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
@if_ctx_rw_congr A b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
theorem if_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
(h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) :
if b then x else y ↔ if c then u else v :=
decidable.rec_on dec_b
(λ hp : b, calc
(if b then x else y)
↔ x : iff.of_eq (if_pos hp)
... ↔ u : h_t (iff.mp h_c hp)
... ↔ (if c then u else v) : iff.of_eq (if_pos (iff.mp h_c hp)))
(λ hn : ¬b, calc
(if b then x else y)
↔ y : iff.of_eq (if_neg hn)
... ↔ v : h_e (iff.mp (not_iff_not_of_iff h_c) hn)
... ↔ (if c then u else v) : iff.of_eq (if_neg (iff.mp (not_iff_not_of_iff h_c) hn)))
theorem if_rw_congr_prop {b c x y u v : Prop} [dec_b : decidable b]
(h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) :
if b then x else y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) :=
@if_congr_prop b c x y u v dec_b (decidable_of_decidable_of_iff dec_b h_c) h_c h_t h_e
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
-- to the branches
definition dite (c : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
decidable.rec_on H (λ Hc, t Hc) (λ Hnc, e Hnc)
theorem dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = t Hc :=
decidable.rec
(λ Hc : c, eq.refl (@dite c (decidable.inl Hc) A t e))
(λ Hnc : ¬c, absurd Hc Hnc)
H
theorem dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = e Hnc :=
decidable.rec
(λ Hc : c, absurd Hc Hnc)
(λ Hnc : ¬c, eq.refl (@dite c (decidable.inr Hnc) A t e))
H
theorem dif_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A}
(h_c : b ↔ c)
(h_t : ∀ (h : c), x (iff.mp' h_c h) = u h)
(h_e : ∀ (h : ¬c), y (iff.mp' (not_iff_not_of_iff h_c) h) = v h) :
(@dite b dec_b A x y) = (@dite c dec_c A u v) :=
decidable.rec_on dec_b
(λ hp : b, calc
(if h : b then x h else y h)
= x hp : dif_pos hp
... = x (iff.mp' h_c (iff.mp h_c hp)) : proof_irrel
... = u (iff.mp h_c hp) : h_t
... = (if h : c then u h else v h) : dif_pos (iff.mp h_c hp))
(λ hn : ¬b,
let h_nc : ¬b ↔ ¬c := not_iff_not_of_iff h_c in
calc
(if h : b then x h else y h)
= y hn : dif_neg hn
... = y (iff.mp' h_nc (iff.mp h_nc hn)) : proof_irrel
... = v (iff.mp h_nc hn) : h_e
... = (if h : c then u h else v h) : dif_neg (iff.mp h_nc hn))
theorem dif_ctx_rw_congr {A : Type} {b c : Prop} [dec_b : decidable b]
{x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A}
(h_c : b ↔ c)
(h_t : ∀ (h : c), x (iff.mp' h_c h) = u h)
(h_e : ∀ (h : ¬c), y (iff.mp' (not_iff_not_of_iff h_c) h) = v h) :
(@dite b dec_b A x y) = (@dite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
@dif_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e
-- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
theorem dite_ite_eq (c : Prop) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
rfl
definition is_true (c : Prop) [H : decidable c] : Prop :=
if c then true else false
definition is_false (c : Prop) [H : decidable c] : Prop :=
if c then false else true
theorem of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c :=
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, !false.rec (if_neg Hnc ▸ H₂))
notation `dec_trivial` := of_is_true trivial
theorem not_of_not_is_true {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_true c) : ¬ c :=
decidable.rec_on H₁ (λ Hc, absurd true.intro (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
theorem not_of_is_false {c : Prop} [H₁ : decidable c] (H₂ : is_false c) : ¬ c :=
decidable.rec_on H₁ (λ Hc, !false.rec (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c :=
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, absurd true.intro (if_neg Hnc ▸ H₂))