Hybrid of `csimp` and `implemented_by`

Stream: Is there code for X?

[cmlsharp]

Is there an idiom for expressing "here's a proof that this efficient implementation is equivalent to this reference implementation, given this (necessarily unsafe) assumption that I promise is true"? The purpose is to "factor out" the unsafety into just a single assumption while still proving equivalence as much as is possible

I find myself writing this rather verbosely as

-- giving this a name because its common across several "unsafe" implementations
-- necessarily unprovable
def myAssumption : Prop := ...
unsafe def unsafeAssumeAssumption : myAssumption := lcProof

private def myFunEfficient (h : myAssumption) (input: a) := ...
private unsafe def myFunUnsafe (input: a) := myFunEfficient (unsafeAssumeAssumption)

-- public reference impl
@[implemented_by myFunUnsafe]
def myFun (input : a) := ...

-- keep myself honest
theorem myFunEfficient_eq_myFun (h : myAssumption) : myFun = myFunEfficient h := ...

I suppose I could cut down on the boilerplate with metaprogramming (something like @[csimp_unsafe_assume myAssumption] but I was wondering if there was an existing idiom for this.

[Jakub Nowak]

Is there even some example in core/batteries/mathlib where we have some kind of proof about the implementation referred to by implemented_by?

[cmlsharp]

I don’t know! I’m not sure how general this pattern is but I’ve been writing implementations of Array.scanl/scanr/scanlM/scanrM (planning on PRing batteries) and the correctness of the efficient versions solely rely on the (unprovable but true) assumption that arr.size < USize.size. It seems desirable to prove that the two versions are equivalent modulo this detail.

The fact that Array.foldl/foldr/et al don’t do this (and instead merely use implemented_by) led to a bug I reported recently.

[Jakub Nowak]

Now that we fixed these two bugs, surely, there are no more bugs. :grinning_face_with_smiling_eyes:

[Jakub Nowak]

You could make an unsafe csimp maybe? But I guess, the point is to have a proof not be unsafe, to ensure it's an honest proof.

[Jakub Nowak]

Though, you could always cheat with native_decide anyway, so maybe it's okay if you just read that there's only one use of unsafe lcProof? Something like this:

-- giving this a name because its common across several "unsafe" implementations
-- necessarily unprovable
def myAssumption : Prop := ...
unsafe def unsafeAssumeAssumption : myAssumption := lcProof

private def myFunEfficient (h : myAssumption) (input: a) := ...
private unsafe def myFunUnsafe (input: a) := myFunEfficient unsafeAssumeAssumption

-- public reference impl
def myFun (input : a) := ...

-- keep myself honest
theorem myFun_eq_myFunEfficient (h : myAssumption) : myFun = myFunEfficient h := ...

@[csimp]
unsafe def myFun_eq_myFunUnsafe : @myFun = @myFunUnsafe :=
  myFun_eq_myFunEfficient unsafeAssumeAssumption

[Jakub Nowak]

My reasoning for using csimp over implemented_by is that it better communicates your intention that there is a proof (almost) that the implementation is safe.

[Jakub Nowak]

Oh, nvm, this doesn't work. "'unsafe' theorems are not allowed". But def works.

[Jakub Nowak]

Btw, where you able to make a proof? I've looked a bit at how hard arr.foldlM = arr.foldlMUnsafe would be though I gave up quickly.

[cmlsharp]

I was able to for an earlier version of scanl/scanr (haven’t tried the monadic versions). I’ve since changed the implementation a bit and the proof broke, but I don’t think that’s fundamental.

The main thing I’ve noticed is that USize is really annoying to work with in proofs (at least partially due to a lack of @[simp]/grind lemmas

[cmlsharp]

Jakub Nowak said:

Oh, nvm, this doesn't work. "'unsafe' theorems are not allowed". But def works.

Oh interesting! I didnt realize csimp worked with defs but I guess that makes sense

[cmlsharp]

Jakub Nowak said:

Btw, where you able to make a proof? I've looked a bit at how hard arr.foldlM = arr.foldlMUnsafe would be though I gave up quickly.

By the way, if interested I got the proof working for Array.scanlM (Array.scanrM is tougher because it diverges a bit more from the reference impl).

Proof here