search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Use Jacques-Henri Jourdan's `physEq` #101

Open nomeata opened 6 years ago

nomeata commented 6 years ago

After the ICFP talk, “Robbert” pointed out that Jacques-Henri Jourdan's PhD thesis in Section 9.1 describes a problem with out encoding of ptrEq, and how to fix it. We could try to modify our translation of reallyUnsafePtrEquality# accordingly – at least in a best-effort way.

antalsz commented 6 years ago

This is very neat! After a quick look, it seems like the biggest issue with this would be introducing the proof obligation in the translation step, rather than the verification step.

robbertkrebbers commented 6 years ago

I wonder if the following trick would be sound:

Axiom ptr_eq : forall {A B} (x y : A)
  (eq : x = y -> unit -> B) (neq : unit -> B), B.

Using this trick, the translation does not introduce a proof obligation.

Maybe @jhjourdan would know.

robbertkrebbers commented 6 years ago

Ah, no, it would not. By doing:

ptr_eq x y (fun _ _ => true) (fun _ => false)

We end up with the same problem we had before.