Failed nested rewrite when eliminating from Prop to Prop

Stream: lean4

[Jakub Nowak]

Is it expected, that this doesn't work, or is it a bug?

namespace WithType

inductive Foo : Type where
| foo (x : Nat) : Foo

inductive Bar : Foo → Type where
| bar (x : Nat) (h : x = 2) : Bar (.foo x)

def Bar.h {x : Nat} (bar : Bar (.foo x)) : x = 2 :=
  match _ : bar with
  | .bar x h => h

end WithType


namespace WithProp

inductive Foo : Prop where
| foo (x : Nat) : Foo

inductive Bar : Foo → Prop where
| bar (x : Nat) (h : x = 2) : Bar (.foo x)

/--
error: Type mismatch
  h
has type
  x = 2
but is expected to have type
  x✝ = 2
-/
#guard_msgs in
def Bar.h {x : Nat} (bar : Bar (.foo x)) : x = 2 :=
  match _ : bar with
  | .bar x h => h

end WithProp

[Jakub Nowak]

It's the same with cases instead of match.

[Jakub Nowak]

It's worth noting, that in the WithType section, match generates these two equalities in context:

h✝¹ : x✝ = x
h✝ : bar ≍ Bar.bar x h

But in WithProp section, it only generates:

h✝ : bar = Bar.bar x h

[Jakub Nowak]

I also have no idea how to workaround this, and how to prove Bar.h. Is it even possible to prove?

[Jakub Nowak]

Hm, Lean generates Foo.foo.noConfusion in WithType section, but not in WithProp section.

[Eric Wieser]

Does including x in the match help?

[Jakub Nowak]

Eric Wieser said:

Does including x in the match help?

Nope.

inductive Foo : Prop where
| foo (x : Nat) : Foo

inductive Bar : Foo → Prop where
| bar (x : Nat) (h : x = 2) : Bar (.foo x)

/--
error: Type mismatch
  h
has type
  x = 2
but is expected to have type
  x' = 2
-/
#guard_msgs in
def Bar.h {x : Nat} (bar : Bar (.foo x)) : x = 2 :=
  match x, _ : bar with
  | x', .bar x h => h

[Kyle Miller]

This is expected. Foo is a proposition, so Foo.foo x = Foo.foo y does not imply x = y.

[Kyle Miller]

Every proof of Bar (.foo x) is equal to each other as well, so having match generate an equality wouldn't be useful.

[Jakub Nowak]

Kyle Miller said:

This is expected. Foo is a proposition, so Foo.foo x = Foo.foo y does not imply x = y.

I see. I've tried to prove exactly this implication. That explains why is there no Foo.foo.noConfusion.

[Aaron Liu]

oh

inductive Foo : Prop where
| foo (x : Nat) : Foo

inductive Bar : Foo → Prop where
| bar (x : Nat) (h : x = 2) : Bar (.foo x)

def Bar.h {x : Nat} (bar : Bar (.foo x)) : x = 2 := sorry

example : False := nomatch @Bar.h 1 (.bar 2 rfl)

[Aaron Liu]

I guess that explains it

[Jakub Nowak]

Yeah, that's because Foo.foo 1 = Foo.foo 2 I think.