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

feat(library/standard/logic/connectives/if): add more general if_congr theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-04 12:00:46 -07:00
parent d8ae285f93
commit 47d49643b0
1 changed files with 21 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -36,18 +36,26 @@ 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_cond_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} (Heq : c₁ ↔ c₂) {A : Type} (t e : A)
: (if c₁ then t else e) = (if c₂ then t else e) :=
rec_on H₁
(assume Hc₁ : c₁, rec_on H₂
(assume Hc₂ : c₂, (if_pos Hc₁ t e) ⬝ (if_pos Hc₂ t e)⁻¹)
(assume Hnc₂ : ¬c₂, absurd_elim _ (iff_elim_left Heq Hc₁) Hnc₂))
(assume Hnc₁ : ¬c₁, rec_on H₂
(assume Hc₂ : c₂, absurd_elim _ (iff_elim_right Heq Hc₂) Hnc₁)
(assume Hnc₂ : ¬c₂, (if_neg Hnc₁ t e) ⬝ (if_neg Hnc₂ t e)⁻¹))
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),
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₂) :=
-- TODO(Leo): We can't write (Ht ▸ He ▸ if_cond_congr Hc t₁ e₁) because the class instance
-- mechanism is not applicable to the auxiliary metavariables created by the unifier.
-- We should fix that in the future.
have e : (@ite c₁ H₁ A t₁ e₁) = (@ite c₂ H₂ A t₁ e₁), from if_cond_congr Hc t₁ e₁,
Ht ▸ He ▸ e
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_iff_equiv H₁ Hc) A t₂ e₂) :=
have H2 [fact] : decidable c₂, from (decidable_iff_equiv H₁ Hc),
if_congr_aux Hc Ht He