import macros import tactic -- "Dependent" if-then-else (dep_if c t e) -- The then-branch t gets a proof for c, and the else-branch e gets a proof for ¬ c -- We also prove that -- 1) given H : c, (dep_if c t e) = t H -- 2) given H : ¬ c, (dep_if c t e) = e H -- We define the "dependent" if-then-else using Hilbert's choice operator ε. -- Note that ε is only applicable to non-empty types. Thus, we first -- prove the following auxiliary theorem. theorem inhabited_resolve {A : TypeU} {c : Bool} (t : c → A) (e : ¬ c → A) : inhabited A := or_elim (em c) (λ Hc, inhabited_range (inhabited_intro t) Hc) (λ Hnc, inhabited_range (inhabited_intro e) Hnc) -- The actual definition definition dep_if {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) : A := ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : c) : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = t H := let s1 : (∀ Hc : c, r = t Hc) ↔ r = t H := iff_intro (assume Hl : (∀ Hc : c, r = t Hc), Hl H) (assume Hr : r = t H, λ Hc : c, subst Hr (proof_irrel H Hc)), s2 : (∀ Hnc : ¬ c, r = e Hnc) ↔ true := eqt_intro (λ Hnc : ¬ c, absurd_elim (r = e Hnc) H Hnc) in by simp -- Given H : c, (dep_if c t e) = t H theorem dep_if_elim_then {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : c) : dep_if c t e = t H := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = t H) := funext (λ r, then_simp A c r t e H) in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) ... = ε (inhabited_resolve t e) (λ r, r = t H) : { s1 } ... = t H : eps_singleton (inhabited_resolve t e) (t H) theorem dep_if_true {A : TypeU} (t : true → A) (e : ¬ true → A) : dep_if true t e = t trivial := dep_if_elim_then true t e trivial theorem else_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : ¬ c) : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H := let s1 : (∀ Hc : c, r = t Hc) ↔ true := eqt_intro (λ Hc : c, absurd_elim (r = t Hc) Hc H), s2 : (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H := iff_intro (assume Hl : (∀ Hnc : ¬ c, r = e Hnc), Hl H) (assume Hr : r = e H, λ Hnc : ¬ c, subst Hr (proof_irrel H Hnc)) in by simp -- Given H : ¬ c, (dep_if c t e) = e H theorem dep_if_elim_else {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : ¬ c) : dep_if c t e = e H := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = e H) := funext (λ r, else_simp A c r t e H) in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) ... = ε (inhabited_resolve t e) (λ r, r = e H) : { s1 } ... = e H : eps_singleton (inhabited_resolve t e) (e H) theorem dep_if_false {A : TypeU} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial := dep_if_elim_else false t e not_false_trivial import cast theorem dep_if_congr {A : TypeM} (c1 c2 : Bool) (t1 : c1 → A) (t2 : c2 → A) (e1 : ¬ c1 → A) (e2 : ¬ c2 → A) (Hc : c1 = c2) (Ht : t1 = cast (by simp) t2) (He : e1 = cast (by simp) e2) : dep_if c1 t1 e1 = dep_if c2 t2 e2 := by simp scope -- Here is an example where dep_if is useful -- Suppose we have a (div s t H) where H is a proof for t ≠ 0 variable div (s : Nat) (t : Nat) (H : t ≠ 0) : Nat -- Now, we want to define a function that -- returns 0 if x = 0 -- and div 10 x _ otherwise -- We can't use the standard if-the-else, because we don't have a way to synthesize the proof for x ≠ 0 check λ x, dep_if (x = 0) (λ H, 0) (λ H : ¬ x = 0, div 10 x H) pop_scope -- If the dependent then/else branches do not use the proofs Hc : c and Hn : ¬ c, then we -- can reduce the dependent-if to a regular if theorem dep_if_if {A : TypeU} (c : Bool) (t e : A) : dep_if c (λ Hc, t) (λ Hn, e) = if c then t else e := or_elim (em c) (assume Hc : c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hc, t) Hc : dep_if_elim_then _ _ _ Hc ... = if c then t else e : by simp) (assume Hn : ¬ c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hn, e) Hn : dep_if_elim_else _ _ _ Hn ... = if c then t else e : by simp)