Simple theorem can't be proven

[arpj-rebola]

The following fails to be shown (couldn't prove post-condition):

abstract val foo :
	a : Type ->
	Tot Type0
let foo a = 
	let _ = () in
	exists (x : a). True

val bar :
	a : Type ->
	Lemma (ensures (
		(foo a) <==> (exists (x : a). True)
	))
let bar a = ()

The part with let _ = () in is a workaround for #638 .

[cpitclaudel]

The problem is the workaround, it seems; this works:

let foo a =
	exists (x : a). True

val bar :
	a : Type ->
	Lemma (ensures (foo a  <==>  (exists (x : a). True)))
let bar a = ()

[arpj-rebola]

Thanks, this works. However, the following does not:

val foo :
	a : Type ->
	Tot Type0
let foo a = 
	exists (x : a). True

val bar :
	a : Type ->
	Lemma (ensures (
		(foo a) <==> (exists (x : a). True)
	))
let bar a = ()

So the problem seems to be provoked by the first val. In the case where I intend to use this, the situation is a bit more complex: (EDIT)

val rel_compose :
	#a : Type ->
	#b : Type ->
	#c : Type ->
	g : (b -> c -> Tot Type0) ->
	f : (a -> b -> Tot Type0) ->
	Tot (a -> c -> Tot Type0)
let rel_compose #a #b #c g f = fun x z -> exists (y : b). True

val def_rel_compose :
	#a : Type ->
	#b : Type ->
	#c : Type ->
	g : (b -> c -> Tot Type0) ->
	f : (a -> b -> Tot Type0) ->
	Lemma (ensures ( forall (x : a) (z : c).
		((rel_compose #a #b #c g f) x z) <==> (exists (y : b). True)
	))
let def_rel_compose #a #b #c g f = ()

This is not proven as it is, and eliminating the val declaration leads to inconsistent qualifier errors.

[nikswamy]

Sorry, all of this is really ugly ... we're working hard to remove the logic qualifier and make use of prop more systematically. If you're curious, you can read about this at #1048

Meanwhile, here are a few workarounds ... I hope that at least one of them is applicable in your real code.

module Bug1430

//Alternative 1:
logic    //explicitly mark it as 'logic' to trigger an optimized SMT encoding
val foo :
        a : Type ->
        Tot Type0
let foo a =
  let _ = () in //workaround the brittle syntactic "inference" of the 'logic' qualifier
  exists (x : a). True

val bar :
        a : Type ->
        Lemma (ensures (
                (foo a) <==> (exists (x : a). True)
        ))
let bar a = ()


//Alternative 2: Avoid the `val`
let foo2 (a:Type) : Type0 = exists (x:a). True

val bar2 :
        a : Type ->
        Lemma (ensures (
                (foo2 a) <==> (exists (x : a). True)
        ))
let bar2 a = ()


//Alternative 3: Avoid the val and add `logic` since the body
//               is not syntactically recognized as a logic term
logic
let rel_compose
        (#a : Type)
        (#b : Type)
        (#c : Type)
        (g : (b -> c -> Tot Type0))
        (f : (a -> b -> Tot Type0)) = fun (x:a) (z:c) -> exists (y : b). True

val def_rel_compose :
        #a : Type ->
        #b : Type ->
        #c : Type ->
        g : (b -> c -> Tot Type0) ->
        f : (a -> b -> Tot Type0) ->
        Lemma (ensures ( forall (x : a) (z : c).
                ((rel_compose #a #b #c g f) x z) <==> (exists (y : b). True)
        ))
let def_rel_compose #a #b #c g f = ()


//Alternative 4: Avoid the val and rewrite the body to make the
//               brittle syntactic inference of the 'logic' qualifier
//               work
let rel_compose2
        (#a : Type)
        (#b : Type)
        (#c : Type)
        (g : (b -> c -> Tot Type0))
        (f : (a -> b -> Tot Type0)) (x:a) (z:c) = exists (y : b). True

val def_rel_compose2 :
        #a : Type ->
        #b : Type ->
        #c : Type ->
        g : (b -> c -> Tot Type0) ->
        f : (a -> b -> Tot Type0) ->
        Lemma (ensures ( forall (x : a) (z : c).
                ((rel_compose2 #a #b #c g f) x z) <==> (exists (y : b). True)
        ))
let def_rel_compose2 #a #b #c g f = ()

[aseemr]

All these examples work in master with the new way of inferring the logic qualifier (which is now deprecated). Adding these to the regressions.