trouble unfolding dite

Stream: new members

[Daniel Fabian]

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]

dif_neg

[Kevin Buzzard]

rw dif_neg hnxx'.symm,

[Daniel Fabian]

fantastic, thanks

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

I'm addicted

[Mario Carneiro]

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

[Mario Carneiro]

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

[Daniel Fabian]

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.

[Daniel Fabian]

(deleted)

[Mario Carneiro]

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 _ _⟩

[Daniel Fabian]

ah, very nice

[Daniel Fabian]

thanks, learnt something again