michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/standard/logic/connectives/if): add 'if-then-else' congruence theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-03 21:41:01 -07:00
parent 63d478c63f
commit ae2e0fd3dc
2 changed files with 25 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/standard/logic/classes/decidable.lean
View file

@ -74,4 +74,12 @@ rec_on Ha
(assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
(assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna))
theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
rec_on Ha
(assume Ha : a, inl (iff_elim_left H Ha))
(assume Hna : ¬a, inr (iff_elim_left (iff_flip_sign H) Hna))
theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
decidable_iff_equiv Ha (eq_to_iff H)
end

19
library/standard/logic/connectives/if.lean
View file

@ -5,8 +5,7 @@
----------------------------------------------------------------------------------------------------
import logic.classes.decidable tools.tactic
using decidable tactic
using decidable tactic eq_proofs
definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
rec_on H (assume Hc, t) (assume Hnc, e)
@ -36,3 +35,19 @@ if_pos trivial t e
theorem if_false {A : Type} (t e : A) : (if false then t else e) = e :=
if_neg not_false_trivial t e
theorem if_congr_aux {c₁ c₂ : Prop} {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₂) :=
have H1 : ∀ (H : decidable c₁), (@ite c₁ H₁ A t₁ e₁) = (@ite c₁ H A t₁ e₁), from
take H : decidable c₁,
have Hd : H₁ = H, from irrelevant H₁ H,
Hd ▸ refl (@ite c₁ H₁ A t₁ e₁),
have H2 : (@ite c₁ H₁ A t₁ e₁) = (@ite c₂ H₂ A t₁ e₁), from
(Hc ▸ H1) H₂,
Ht ▸ He ▸ H2
theorem if_congr {c₁ c₂ : Prop} {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_eq_equiv H₁ Hc) A t₂ e₂) :=
have H2 [fact] : decidable c₂, from (decidable_eq_equiv H₁ Hc),
if_congr_aux Hc Ht He