Error with rw tactic

Stream: new members

[Joshua E Cook]

Can someone help me understand why this gives an error at rw [h₀],? The error states rewrite tactic failed, motive is not type correct

/- Iverson bracket -/
structure Iverson :=
(z: ℤ)
(p: Prop)
(decidable: decidable p)
(invariant: z = ite p 1 0)

/--
[¬P] = 1 - [P]
-/
lemma not_is_one_minus (i j: Iverson)
: (i.p = ¬j.p) → (i.z = 1 - j.z) :=
begin
  intro h₀,
  rw [i.invariant, j.invariant],
  rw [h₀],
end

[Mario Carneiro]

The ite in your Iverson definition contains a reference to the decidable field, as in z = @ite p decidable 1 0. After the rewrites, i.z becomes @ite i.p i.decidable 1 0, and then you try to rewrite with h0 to get @ite (not j.p) i.decidable 1 0. But this doesn't work because i.decidable is a proof that i.p is decidable, not that not j.p is

[Mario Carneiro]

One way you can fix this is to instead rewrite with rw [show ite i.p 1 0 = ite (not j.p) 1 0, by congr; exact h0]

[Joshua E Cook]

thanks! but after I replace that rewrite, I get a new error, failed to synthesize type class instance

[Mario Carneiro]

which one?

[Mario Carneiro]

the line after that is the important one

[Mario Carneiro]

actually it's probably j.p; you need to mark Iverson.decidable as an instance using attribute [instance] Iverson.decidable

[Joshua E Cook]

this lemma:

lemma not_is_one_minus (i j: Iverson)
: (i.p = ¬j.p) → (i.z = 1 - j.z) :=
begin
  intro h₀,
  rw [i.invariant, j.invariant],
  rw [show ite i.p 1 0 = ite ¬j.p 1 0, by congr; exact h0],
end

gives this error:

failed to synthesize type class instance for
i j : Iverson,
h₀ : i.p = ¬j.p
⊢ decidable i.p
state:
i j : Iverson,
h₀ : i.p = ¬j.p
⊢ ite i.p 1 0 = 1 - ite j.p 1 0

[Mario Carneiro]

the important bit is ⊢ decidable i.p, it doesn't know how to prove this because i.decidable isn't an instance

[Joshua E Cook]

after adding attribute [instance] Iverson.decidable I get a new error at

  rw [show (ite i.p 1 0) = (ite (¬j.p) 1 0), by congr; exact h₀],

which says

rewrite tactic failed, did not find instance of the pattern in the target expression
  ite i.p 1 0
state:
i j : Iverson,
h₀ : i.p = ¬j.p
⊢ ite i.p 1 0 = 1 - ite j.p 1 0

[Scott Morrison]

#mwe?

[Joshua E Cook]

@Scott Morrison what I have with Mario's feedback is this, plus I had vscode paste the error back into the place where it was raised. I'm not sure how to make this more minimal, but what I want to achieve is to form a proof of some properties of "Iverson brackets" <https://en.wikipedia.org/wiki/Iverson_bracket#Properties> starting with [¬P] = 1 - [P]

/- Iverson bracket -/
structure Iverson :=
(z: ℤ)
(p: Prop)
(decidable: decidable p)
(invariant: z = ite p 1 0)

attribute [instance] Iverson.decidable

/--
[¬P] = 1 - [P]
-/
lemma not_is_one_minus (i j: Iverson)
: (i.p = ¬j.p) → (i.z = 1 - j.z) :=
begin
  intro h₀,
  rw [i.invariant, j.invariant],
  /-
  rewrite tactic failed, did not find instance of the pattern in the target expression
    ite i.p 1 0
  state:
  i j : Iverson,
  h₀ : i.p = ¬j.p
  ⊢ ite i.p 1 0 = 1 - ite j.p 1 0
  -/
  rw [show (ite i.p 1 0) = (ite (¬j.p) 1 0), by congr; exact h₀],
  sorry,
end

[Joshua E Cook]

I've managed to do something like the above with bool as the type of the dependent variable, but I'm having a hard time doing this with Prop and decidable

[Scott Morrison]

Thanks. (Just didn't want to have to read the thread above to patch Mario's suggestion into your code myself. :-)

[Scott Morrison]

If you add set_option pp.all true above the lemma you'll see immediately the problem.