Structure substitution

Stream: general

[Alice Laroche]

Is there a way to go from this context :

prop: Point → Prop
⊢ prop {x := 0, y := 0}

to this one :

prop: Point → Prop
p: Point := {x := 0, y := 0}
⊢ prop p

[Yakov Pechersky]

let p : Point := {x := 0, y := 0}

[Alice Laroche]

Naaah, It's giving me the object in the context but it doesn't replace it in the goal.

[Eric Rodriguez]

you can use change ... or set ... with hp, rw ←hp at * to force it to behave

[Eric Rodriguez]

and worst case they are defeq so you can mostly just pretend that it's fine

[Floris van Doorn]

import tactic.interactive

example {α} (p : α → Prop) (x : α) : p x :=
begin
  set y := x,
  /- State
    α : Sort ?,
    p : α → Prop,
    x : α,
    y : α := x
    ⊢ p y
  -/
end

[Floris van Doorn]

@Yakov Pechersky was off by 1 letter :)

[Yakov Pechersky]

is there a reason we still have let as opposed to set? because let is in core?

[Eric Rodriguez]

set can sometimes still not overwrite though, and let is slightly different with binders iirc

[Floris van Doorn]

let seems also useful, if you don't want to change the other hypotheses or the goal. But in cases where they behave differently, you usually want to use set.

[Alice Laroche]

Huuuu,
For strange reason, it's not working in my actual proof, but it work with a not-sso-working mwe

[Floris van Doorn]

Ideas:

• Does Eric's suggestion with rw ←hp at * help?
• Double check that the value of p and the term in the goal are precisely the same, including in implicit arguments etc. (Maybe you can click through them in widgets?).

[Alice Laroche]

"MWE"

example (prop : Point → Prop) : prop (create_point 0 0) :=
begin
  let p : Point := create_point 0 0,
  change create_point 0 0 with p,
  /- State
     prop: Point → Prop
     p: Point := create_point 0 0
     ⊢ prop p
  -/
end

Actual proof :

theorem rename_accept (fsa : FSA S L) (old new : S) (h₁ : new ∉ fsa.states) (w : word L) : accept fsa w → accept (rename_state fsa old new h₁) w :=
begin
  intro h₂,
  let fsa' : FSA S L := rename_state fsa old new h₁,
  change rename_state fsa old new h₁ with fsa',
  /- State
     ...
     fsa': FSA S L := fsa.rename_state old new h₁
     ⊢ (fsa.rename_state old new h₁).accept w
  -/
end

[Floris van Doorn]

did you try set?
If you replace the let by set fsa' : FSA S L := rename_state fsa old new h₁ with hp
does rw ←hp or simp_rw ←hp do anything?

[Floris van Doorn]

Does change fsa'.accept w work after your let?

[Alice Laroche]

Well it's work but i don't understand why change doesn't work in the same way

[Alice Laroche]

(set + rw hp)

[Alice Laroche]

And change fsa'.accept w work too
Very strange

[Alice Laroche]

In the same topic, is there a way to rewrite the definition of a structure ?
like go from p: Point := {x := 0, y := 1 + 1} to p: Point := {x := 0, y := 2} for example

[Yaël Dillies]

You can prove the equality between those two using ext, and then use that to rw. Maybe there's a shortcut, though. Like, in that particular instance, your two points are defeq.

[Eric Wieser]

Can you give a #mwe?

[Alice Laroche]

Yaël Dillies
If i do :

example : true :=
begin
  let p : Point := { x := 0, y := 1 + 1 },
  have h : {Point . x := 0, y := 1 + 1} = {Point . x := 0, y := 2} := rfl,
  rw h at p,
end

I obtain

/- State
rewrite tactic failed, did not find instance of the pattern in the target expression
  {x := 0, y := 1 + 1}
state:
p : Point := {x := 0, y := 1 + 1},
h : {x := 0, y := 1 + 1} = {x := 0, y := 2}
-/
⊢ true

[Yakov Pechersky]

p is not a hypothesis at which you can rewrite. Use "set p :=... with hp"

[Alice Laroche]

Hmmm, of course it's work but it doesn't help me to do what i hoped to do
I have

example : ∃x, some_prop x :=
begin
  let x : Big_struct := func_which_eval_into_a_really_big_struct,
  use x,
end

But now to prove the goal i need to access to the value of the fields of the structure, but i can't because i_eval_into_a_really_big_struct is not unfolded
I can use set p :=... with hp and unfold it in hp then rewrite x in the goal , but then i have a big structure in the goal and it's messy and unreadable

[Yakov Pechersky]

Very hard to understand your issue without a mwe context. Why not just "use (func_which_eval)"?

[Alice Laroche]

Hmmm,
I guess this work ? I hope you will understand my mindset

import tactic

structure Big_struct :=
  (a : ℕ)
  (b : ℕ)
  (c : Prop)
  (d : Prop)
  (e : Prop)
  (f : Prop)
  (g : Prop)
  (h : Prop)
  (i : Prop)
  (j : Prop)
  (k : Prop)
  (l : Prop)
  (m : Prop)

@[simp] def i_eval_to_big_struct (a b : ℕ): Big_struct :=
{
  a := a,
  b := b,
  c := true,
  d := true,
  e := true,
  f := true,
  g := true,
  h := true,
  i := true,
  j := true,
  k := true,
  l := true,
  m := true,
}

-- work but ugly
example (f : Big_struct → Big_struct) : ∃x : Big_struct, x.a > (f x).b :=
begin
  use (i_eval_to_big_struct 5 2),
  /- State
     f: Big_struct → Big_struct
     ⊢ (i_eval_to_big_struct 5 2).a > (f (i_eval_to_big_struct 5 2)).b
  -/
  simp,
  /- State
     f: Big_struct → Big_struct
     ⊢ (f {a := 5, b := 2, c := true, d := true, e := true, f := true, g := true, h := true, i := true, j := true, k := true, l := true, m := true}).b < 5
  -/
end

-- what i wish i could do
example (f : Big_struct → Big_struct) : ∃x : Big_struct, x.a > (f x).b :=
begin
  some_tactics,
  /-
    f: Big_struct → Big_struct
    x: Big_struct := {a := 5, b := 2, c := true, d := true, e := true, f := true, g := true, h := true, i := true, j := true, k := true, l := true, m := true}
    ⊢ x.a > (f x).b
  -/
  simp,
  /- State
     f: Big_struct → Big_struct
     x: Big_struct := {a := 5, b := 2, c := true, d := true, e := true, f := true, g := true, h := true, i := true, j := true, k := true, l := true, m := true}
     ⊢ (f x).b < 5
  -/
end

[Floris van Doorn]

Here are two options to do roughly want you want

-- to get mostly what you want
example (f : Big_struct → Big_struct) : ∃x : Big_struct, x.a > (f x).b :=
begin
  let x := i_eval_to_big_struct 5 2,
  use x,
  /-
    f: Big_struct → Big_struct
    x: Big_struct := i_eval_to_big_struct 5 2
    ⊢ x.a > (f x).b
  -/
  revert x, dsimp [i_eval_to_big_struct, gt] {zeta := ff}, intro x,
  /- State
     f: Big_struct → Big_struct
     x: Big_struct := {a := 5, b := 2, c := true, d := true, e := true, f := true, g := true, h := true, i := true, j := true, k := true, l := true, m := true}
     ⊢ (f x).b < 5
  -/
end

-- another option
example (f : Big_struct → Big_struct) : ∃x : Big_struct, x.a > (f x).b :=
begin
  generalize hx : i_eval_to_big_struct 5 2 = x,
  use x,
  /-
    f: Big_struct → Big_struct
    x: Big_struct
    hx: i_eval_to_big_struct 5 2 = x
    ⊢ x.a > (f x).b
  -/
  conv_lhs { rw [←hx] }, simp [i_eval_to_big_struct],
  /- State
    f: Big_struct → Big_struct
    x: Big_struct
    hx: i_eval_to_big_struct 5 2 = x
    ⊢ (f x).b < 5
  -/
end

[Kyle Miller]

For others who, like me, aren't familiar with fancy options to dsimp, this is what zeta is for:

(zeta : bool               := tt) -- do zeta-reductions: `let x : a := b in c ↝ c[x/b]`.