Zulip Chat Archive

Stream: new members

Topic: trouble unfolding dite


view this post on Zulip 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 xxx' \ne x.

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 21:42):

dif_neg

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 21:43):

rw dif_neg hnxx'.symm,

view this post on Zulip Daniel Fabian (Jun 10 2020 at 21:44):

fantastic, thanks

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (Jun 10 2020 at 21:47):

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

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 21:47):

I'm addicted

view this post on Zulip Mario Carneiro (Jun 10 2020 at 21:51):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 21:52):

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

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (Jun 10 2020 at 21:54):

(deleted)

view this post on Zulip 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 _ _⟩

view this post on Zulip Daniel Fabian (Jun 10 2020 at 21:59):

ah, very nice

view this post on Zulip Daniel Fabian (Jun 10 2020 at 22:00):

thanks, learnt something again


Last updated: May 15 2021 at 23:13 UTC