Several enhancements requested by Cedric

[nikswamy]

-- Better projector syntax for datatypes and dependent records

-- Type inference for type arguments type t i = | MkT : x:nat{x=i} -> t i

-- Proving strong elimination/pattern matching at the level of types

-- Syntactic support for Let

-- Allowing F* to infer the pre-condition of pure/ghost functions locally, overriding the default Tot effect

-- Allowing type ascriptions on patterns

-- as_t : (unit -> Lemma a) -> GTot a

[catalin-hritcu]

-- Allowing type ascriptions on patterns

This one seems the same as #183

as_t : (unit -> Lemma a) -> GTot a

This one has a big chance of leading to unsoundness because of impredicative polymorphism (see examples/paradoxes/berardi.fst).

[s-zanella]

Isn't magic more dangerous? as_t can be defined with some magic:

val as_t : (unit -> Lemma 'a) -> GTot 'a
let as_t _ = magic ()

[catalin-hritcu]

Isn't magic more dangerous?

Magic is directly assuming false. So if the choice is between these two then sure, go for as_t, although we haven't yet figured out how to soundly mix the SMT and the outer logics.

For Berardi's paradox we use the following more convenient variant of as_t:

assume val get_proof: a:Type -> Ghost a (requires a) (ensures (fun _ -> True))

The standard library (classical.fst) already contains the converse:

assume val give_proof: #a:Type -> a -> Lemma (ensures a)

None of these axioms has any formal backing at the moment, on the contrary I'm working on counterexamples for them, so use at your own risk.

[s-zanella]

Thanks for the clarification. Indeed, get_proof is more convenient. Just to make sure, checked they can be defined from each other:

let get_proof (a:Type) = as_t (fun _ -> ())
let as_t f = f (); get_proof _

[s-zanella]

I just pushed a minimalistic version of Berardi's paradox, assuming only excluded middle in Type and cfalse elimination (no magic, proof irrelevance or get_proof).

[catalin-hritcu]

Nice! Excluded middle in Type is probably provable from excluded middle in the SMT solver (excluded_middle' lemma in classical.fst) + get_proof + Nik's recent "constructivization" of the SMT logical constants (https://github.com/FStarLang/FStar/commit/21fca9504b764954e2c0596d1343f744ca8c5ded#diff-d238d59ddc70ce7755080a376f14dceaR30). Otherwise, we should be able to replay the Berardi proof for these "constructivazed" SMT constants, instead of cor, cnot, etc ... right?

cfalse elimination is a standard lemma we can't prove only because F* still doesn't support syntax for empty types and empty pattern matches (#70) ... a silly limitation that affects constructive proofs in general.

[fournet]

Some follow-up on yesterday's discussion with Nikhil and Santiago:

• a general theme was my wish to (1) reduce the need to duplicate code between specs and implementations; and (2) keep the two syntaxes close, in case that's needed anyway.
• I ran into some Ghost problems when writing "stateful" lemmas for HyperHeap. Lemma returns a concrete Tot unit, hence can't be applied to ghost arguments returned e.g. by as_ref. Not sure whether/where that should be fixed.
• I did not manage to use local type annotations in "let" to save the need for an explicit "val"; this is a pain when the explicit type is verbose and I just need a trivial precondition. I guess I can define a type alias for that.

[beurdouche]

a general theme was my wish to (1) reduce the need to duplicate code between specs and implementations

I am not sure what you mean exactly by that ? Interfaces & Implem ? Can you give and example ? ;)

[catalin-hritcu]

I'm also have troubles following this.

I ran into some Ghost problems when writing "stateful" lemmas for HyperHeap. Lemma returns a concrete Tot unit, hence can't be applied to ghost arguments returned e.g. by as_ref. Not sure whether/where that should be fixed.

What are you trying to do? Tot is a sub-effect of Ghost, so Tot unit can be converted by sub-computation to Ghost unit. You can't convert the other way around, but what is the point anway in converting units? You can always create a new unit, like this (). Also, I don't see where as_ref fits in all this? Would your problem be better with get_proof?

[catalin-hritcu]

Nevermind I'm starting to get it. The problem is that one can't get out of Ghost even if one ignores the result of the computation. For instance bar below can't be typed at the given type:

assume val foo: unit -> Ghost unit (requires True) (ensures (fun _ -> True))
val bar : unit -> Tot unit
let bar() = foo(); ()

because simply calling foo makes the whole computation in bar be considered ghost. This seems silly, so how about making Ghost unit and Tot unit equivalent by sub-computation (and maybe similarly for all inductives with only one inhabitant)?

Edit: just realized that unit is not an inductive, so whatever, only for unit Edit: this seems now filed as #455

[s-zanella]

As Catalin suspected, a constructive excluded middle lemma can be proved from get_proof and the constructivization of logical connectives (after fixing #358). So, assuming get_proof would be unsound (proof)

open FStar.Constructive

assume val get_proof : p:Type -> Tot p (requires p) (ensures (fun _ -> True))

val excluded_middle : p:Type -> Tot (b:bool{(b = true) <==> p})
let excluded_middle (p:Type) = 
  let t = get_proof (p \/ (~p)) in
  match t with
  | Left  _ -> true
  | Right r -> Classical.give_proof r; false
(* Doesn't work without (Classical.give_proof r); why? *)

val cem : p:Type -> Tot (cor p (cnot p))
let cem (p:Type) = 
  if excluded_middle p then
    IntroL (get_proof _)
  else
    IntroR (get_proof _)

[nikswamy]

@s-zanella @catalin-hritcu : great job drilling into this!

Backing up to the original request: The point was to have a way to use the properties proven by a lemma in another function's specification, both to ensure the spec is well-formed and to carry the properties proven by the lemma in the spec.

For example, Cedric wanted to write something analogous to this:

type Good : int -> Type
val lemma: x:int{Good x} -> Lemma (x > 0)
val foo: x:int{Good x} -> Tot (y:int{lemma x /\ y=1/x})

As written, the refinement on y in the last line is not well-formed, since lemma x : unit and you can't use /\ with it.

The initial rough proposal was to go with something like get_proof (lemma x) /\ y=1/x ... but that compromises soundness, as you've observed.

But, get_proof is seriously overkill anyway. How about something like:

type Lem (#a:Type)  (_:(unit -> Lemma a)) = a

And now we can write:

y:int{Lem (fun () -> lemma x) /\ y=1/x}

We could provide concrete syntax for this ... avoiding the need to thunk the lemma application.

Update:

Besides, get_proof(lemma x) /\ y=1/x doesn't even solve the problem we were setting out to solve anyway. /\ can only be applied to a type (or to a bool, via the b2t promotion), and get_proof (lemma x) is neither.

So, this part of the proposal (as_t etc.) was barking up entirely the wrong tree.

[nikswamy]

Coming back to excluded middle and get_proof: I guess all of this is pointing perhaps to the need to separate out something like Prop from Type in F*? @catalin-hritcu: you had suggested something like this a while back, although at the time the motivation was somewhat different, IIRC. Can you say a bit about whether excluded_middle and get_proof can coexist provided some Prop-like restriction?

[s-zanella]

type Lem (#a:Type)  (_:(unit -> Lemma a)) = a
val foo: x:int{Good x} -> Tot (y:int{Lem (fun () -> lemma x) /\ y=1/x})

This would solve the problem of having to copy/paste a complex formula a, but is it any different than just writing a? I mean, would Z3 pick up lemma to prove a or would one need to apply lemma explicitly in the definition of foo?

BTW, this doesn't work at the moment because F* can't infer the implicit parameter of Lem

type Good : int -> Type
assume val lemma : x:int{Good x} -> Lemma (requires True) (ensures (x > 0)) 
type Lem (#a:Type) (p:(unit -> Lemma a)) = a
val foo : x:int{Good x} -> Tot (y:int{Lem (fun () -> lemma x) /\ y=1/x})

Results in Unconstrained unification variables U11029 in type signature (x:x:int{(Good x)} -> Tot y:int{((Lem #(U11029 x y) ((fun _8_9073:unit -> ((match _8_9073 with () -> (lemma x)):unit)):(unit -> Lemma (unit)))) /\ (y = (1 / x)))})

[nikswamy]

I think the original requirement from our discussion the other day was mainly to provide some syntactic convenience to save the user from having to copy-paste large formulas just to establish the well-formedness of some specs. That's a pretty modest goal.

Unfortunately, type inference for this style is still a bit brittle : ( Here's a variation that works.

module Lem
type Good : int -> Type
//needed to add an extra unit argument, rather than thunking the lemma in-place : (
assume val lemma: x:int{Good x} -> unit -> Lemma (x > 0)

//Needed the equality constraint, =f ... that's expected
type Lem (#a:Type) (=f:(unit -> Lemma a)) = a

//Style 1: The use of Lem (lemma x) in the spec serves both 
//         establish the well-formedness of the (y=1/x)
//         as well as to propagate the lemma's post-condition
//         in the refinement of y. Checking the well-formedness
//         of the refinement does not require re-proving the lemma
val foo: x:int{Good x} -> Tot (y:int{Lem (lemma x) /\ y=1/x})
let foo x = 
  lemma x ();  
  1 / x

val as_tot : #a:Type -> =f:(unit -> Lemma a) -> Tot (x:unit{a})
let as_tot f = f ()
type Let (#a:Type) (=x:a) (=body:(a -> Type)) = body x

//Style 2: The use of Let (as_tot (lemma x)) in the spec serves only
//         to establish the well-formedness of the (y=1/x)
//         Checking the well-formedness of the refinement does 
//         not require re-proving the lemma
val bar : x:int{Good x} -> Tot (y:int{Let (as_tot (lemma x)) (fun _ -> y==1/x)})
let bar x =
  lemma x ();
  1/x

[nikswamy]

This is really at the core of the discussion that led to --universes. It's not clear to me now what, if anything, is the particular deliverable associated with this issue, beyond --universes.

At the least, it would be great for someone to revisit Berardi, Russell etc. and try to replay them with --universes. Should we just track that with #360 and close this issue?

[catalin-hritcu]

Ok, let's track that in #360