## Stream: new members

### Topic: trouble unfolding dite

#### Daniel Fabian (Jun 10 2020 at 21:41):

In order to construct a counter example, I want to modify a function at one point and I'm having trouble proving it.

import tactic

theorem modified
{α : Type}
{β : α → Type}
(f : Π x, β x)
(x : α) (y : β x) : ∃ f' : Π x, β x, f' x = y ∧ ∀ x' ≠ x, f' x' = f x' :=
begin
classical,
set f' : Π x, β x := λ x', dite (x = x') (λ hxx', by { rw hxx' at y, exact y }) (λ _, f x') with hf',
use f',
split,
begin
rw hf',
--refl -- doesn't work,
simp,
end,
begin
intros x' hnxx',
rw hf',
simp,
sorry
end,
end


it boils down to this:

hnxx' : x' ≠ x
⊢ dite (x = x') (λ (hxx' : x = x'), eq.mp _ y) (λ (_x : ¬x = x'), f x') = f x'


which should obviously hold. But how can we unfold dite, taking into consideration, that we've got a proof of $x' \ne x$.

#### Kevin Buzzard (Jun 10 2020 at 21:42):

dif_neg

#### Kevin Buzzard (Jun 10 2020 at 21:43):

 rw dif_neg hnxx'.symm,

#### Daniel Fabian (Jun 10 2020 at 21:44):

fantastic, thanks

#### Kevin Buzzard (Jun 10 2020 at 21:46):

In general you can deconstruct dite with split_ifs but in the situation where you know the truth value of the hypothesis dif_pos and dif_neg are easier.

#### Daniel Fabian (Jun 10 2020 at 21:47):

thanks. (and you sure are very quick to respond, lol)

#### Mario Carneiro (Jun 10 2020 at 21:51):

If you want to modify a function at one point, try function.update

#### Mario Carneiro (Jun 10 2020 at 21:52):

which in particular deals with the messy business of dependent function updates

#### Daniel Fabian (Jun 10 2020 at 21:53):

but that particular one changes the type, though, right? Because at point a', you are now of a different type. My theorem preserves the same type.

(deleted)

#### Mario Carneiro (Jun 10 2020 at 21:55):

import tactic logic.function.basic

theorem modified
{α : Type}
{β : α → Type}
(f : Π x, β x)
(x : α) (y : β x) : ∃ f' : Π x, β x, f' x = y ∧ ∀ x' ≠ x, f' x' = f x' :=
by classical; exact
⟨function.update f x y,
function.update_same _ _ _,
λ x' h, function.update_noteq h _ _⟩


ah, very nice

#### Daniel Fabian (Jun 10 2020 at 22:00):

thanks, learnt something again

Last updated: May 15 2021 at 23:13 UTC