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

feat(library/init/logic): 'if-then-else' and 'dependent-if-then-else' congruence theorems

Browse source 
We will use these theorems to test the new simplifier.
This commit is contained in:
Leonardo de Moura 2015-06-02 13:14:38 -07:00
parent 50fe4ec6c0
commit 2f9005827c
2 changed files with 44 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
library/init/logic.lean
View file

@ -506,6 +506,27 @@ 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] {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) :=
assert dec_c : decidable c, from decidable_of_decidable_of_iff dec_b h_c,
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] {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_congr A b c dec_b x y u v h_c (λ h, h_t) (λ h, 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 :=
@ -523,6 +544,29 @@ decidable.rec
(λ 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]
{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) :=
assert dec_c : decidable c, from decidable_of_decidable_of_iff dec_b h_c,
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))
-- 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

21
library/logic/connectives.lean
View file

@ -248,25 +248,4 @@ section
definition if_false (t e : A) : (if false then t else e) = e :=
if_neg not_false
theorem if_congr_cond [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) (t e : A) :
(if c₁ then t else e) = (if c₂ then t else e) :=
decidable.rec_on H₁
(λ Hc₁ : c₁, decidable.rec_on H₂
(λ Hc₂ : c₂, if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹)
(λ Hnc₂ : ¬c₂, absurd (iff.elim_left Heq Hc₁) Hnc₂))
(λ Hnc₁ : ¬c₁, decidable.rec_on H₂
(λ Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁)
(λ Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹))
theorem if_congr_aux [H₁ : decidable c₁] [H₂ : decidable c₂] {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₂) :=
Ht ▸ He ▸ (if_congr_cond Hc t₁ e₁)
theorem if_congr [H₁ : decidable c₁] {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂)
(He : e₁ = e₂) :
(if c₁ then t₁ else e₁) = (@ite c₂ (decidable_of_decidable_of_iff H₁ Hc) A t₂ e₂) :=
assert H2 : decidable c₂, from (decidable_of_decidable_of_iff H₁ Hc),
if_congr_aux Hc Ht He
end