Problems with Subtype equality

Stream: new members

[Jakub Nowak]

Is there some other way to prove that beside using exact? I feel like simp should be handling that, but it isn't and I couldn't even get it to work:

def Bar' := Nat

structure Foo' where
  bar : Bar'
  n : Nat

def func' : Nat → Bar' := id

def Foo'.WF (foo : Foo') : Prop := func' foo.n = foo.bar
def Bar'.WF (bar : Bar') : Prop := True

def Foo := { foo : Foo' // foo.WF }
def Bar := { bar : Bar' // bar.WF }

def func (n : Nat) : Bar := ⟨func' n, by trivial⟩

def Foo.mk (bar : Bar) (n : Nat) (wf : func n = bar) : Foo := ⟨Foo'.mk bar.val n, by
    simp_all [Foo'.WF, func]
    --simp [Subtype.ext_iff]
    --rw [Subtype.ext_iff]
    --simp [Subtype.ext_iff.mp]
    --rw [Subtype.ext_iff.mp]
    exact Subtype.ext_iff.mp wf
  ⟩

And my actual problem, how can I rewrite ⟨func' x, True.intro⟩ = bar to func' x = bar.val in this code?

def Bar' := Nat

structure Foo' where
  bar : Bar'
  n? : Option Nat

def func' : Nat → Bar' := id

def Foo'.WF (foo : Foo') : Prop := foo.n?.elim True (func' · = foo.bar)
def Bar'.WF (bar : Bar') : Prop := True

def Foo := { foo : Foo' // foo.WF }
def Bar := { bar : Bar' // bar.WF }

def func (n : Nat) : Bar := ⟨func' n, by trivial⟩

def Foo.mk (bar : Bar) (n? : Option Nat) (wf : n?.elim True (func · = bar)) : Foo := ⟨Foo'.mk bar.val n?, by
    simp_all [Foo'.WF, func, Foo, Bar]
    --conv at wf in _ = _ => apply Subtype.ext_iff.mp
  ⟩

[Jakub Nowak]

Well, giving it some though, maybe it's not actually a good idea to always rewrite subtype equality with simp.

[Kenny Lau]

every time you make a new definition, you need to provide the standard set of lemmas to interact with the new definition. this is called the "API".

[Jakub Nowak]

That's what I'm trying to do.

[Jakub Nowak]

Should I prove something about Bar first?

[Kenny Lau]

Jakub Nowak said:

That's what I'm trying to do.

yes, and when you're proving the API results, you shouldn't expect simp to work, because simp relies on the API

[Jakub Nowak]

Thanks! That works:

def Bar' := Nat

structure Foo' where
  bar : Bar'
  n? : Option Nat

def func' : Nat → Bar' := id

def Foo'.WF (foo : Foo') : Prop := foo.n?.elim True (func' · = foo.bar)
def Bar'.WF (bar : Bar') : Prop := True

def Foo := { foo : Foo' // foo.WF }
def Bar := { bar : Bar' // bar.WF }

theorem Bar.ext (bar bar' : Bar) : bar.val = bar'.val → bar = bar' := Subtype.ext
theorem Bar.ext_iff (bar bar' : Bar) : bar = bar' ↔ bar.val = bar'.val := Subtype.ext_iff

def func (n : Nat) : Bar := ⟨func' n, by trivial⟩

def Foo.mk (bar : Bar) (n? : Option Nat) (wf : n?.elim True (func · = bar)) : Foo := ⟨Foo'.mk bar.val n?, by
    simp_all [Foo'.WF, func, Bar.ext_iff]
  ⟩

Is there some checklist of what properties should I prove when making an API?

[Kenny Lau]

you'll find out as you prove more things :slight_smile: