Proving int =!= (int -> Dv int)

[mtzguido]

let _ = assert (int =!= (int -> int))
let _ = assert (int =!= (int -> Dv int))

The second assertion here fails, probably due to SMT encoding for effectful arrows. But it seems like this could be made to work easily, int is not a function (effectul or otherwise).

@andricicezar

[andricicezar]

A proof of concept of the inversion lemma I would like to prove, but I cannot because of this issue.

module Inversion

type typ =
| TUnit   : typ
| TInt    : typ
| TArr    : typ -> typ -> typ
| TSum    : typ -> typ -> typ

let rec elab_typ (t:typ) : Type0 = 
  match t with
  | TUnit -> unit
  | TInt -> int
  | TArr t1 t2 -> (elab_typ t1 -> Dv (elab_typ t2))
  | TSum t1 t2 -> either (elab_typ t1) (elab_typ t2)

let rec inversion (a:typ) (b:typ) :
  Lemma
    (requires (elab_typ a == elab_typ b))
    (ensures (a == b)) =
    match a, b with
    | TUnit, TUnit -> ()
    | TInt, TInt -> ()
    | TSum t1 t2, TSum t1' t2' -> begin
      assume (elab_typ t1 == elab_typ t1');
      inversion t1 t1';
      assume (elab_typ t2 == elab_typ t2');
      inversion t2 t2'
    end
    | TArr x y, TArr x' y' ->
      assume (elab_typ x == elab_typ x');
      inversion x x';
      assume (elab_typ y == elab_typ y');
      inversion y y'
    | _, _ -> admit () (* other cases are impossible because of the pre-condition*)

[andricicezar]

For what I need, it seems that the situation is even more complicated because the following also don't hold:

assert (forall a b c d. either a b == either c d ==> a == c /\ b == d);
assert (forall a b c d. (a * b) == (c * d) ==> a == c /\ b == d);
assert (forall a b. ref a == ref b ==> a == b);

For my specific case, they should hold. I am curious if there are cases when these don't hold.