From 2f9005827c26ee38f6803d33d6184cd032e11e6a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Jun 2015 13:14:38 -0700 Subject: [PATCH] feat(library/init/logic): 'if-then-else' and 'dependent-if-then-else' congruence theorems We will use these theorems to test the new simplifier. --- library/init/logic.lean | 44 ++++++++++++++++++++++++++++++++++ library/logic/connectives.lean | 21 ---------------- 2 files changed, 44 insertions(+), 21 deletions(-) diff --git a/library/init/logic.lean b/library/init/logic.lean index 280d48b3d6..022ec30702 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -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 diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 7676272aab..67706523a8 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -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