Define our logical connectives in prop

[catalin-hritcu]

We can currently define a prop type in various ways, for instance:

type prop = a:Type0{ forall (x:a). x === () }

or (maybe) better:

abstract let prop (* : Type1 *)
  = a:Type0{ l_forall #a (fun x -> l_forall #a (fun y -> l_equals x y)) }

Started working on an experiment to switch our logical connectives to prop this fall on the catalin_prop branch: https://github.com/FStarLang/FStar/blob/catalin_prop/ulib/prims.fst#L127

Quickly run into lots of troubles, including the fact that making prop abstract means that going from prop to Type needs to be coercive (a p2t, something like b2t). There were more issues, but unfortunately I can no longer find my notes on this, so will need to rediscover them when returning to this.

One big advantage of this change would be that we would get much better error messages for types that make no sense logically, and that we could get rid of the logic qualifier hack.

[catalin-hritcu]

Finally found my old notes on this by Gmail search in commit messages. Hallelujah!
(they were buried in <fstar-priv>/papers/dm4free/popl17/final-version.org)

TODO (Catalin) Switching to prop instead of Type -- punted

CH: We didn't promise this but it would make the presentation much nicer.

Current plan (take 3):

• Stage 1 (final version):
  • change prims.fst to add a 3rd layer of logical operators:
    • layer 1 (c_ prefix): constructive logic
    • layer 2 (l_ prefix): squashed operators
    • layer 3 (p_ prefix): prop operators (new!)
      • defined as the l_ operators but with stronger prop types
      • operators like \/ and /\ and forall should desugar to this
  • change parsing to produce p_ operators instead of l_ ones
  • change logical encoding to treat p_ and l_ ops the same
  • remove the logical keyword and its syntactic special casing
  • [Kenji can help] make dm4free turn M t into (t -> prop) -> prop
  • make this work for examples/dm4free only
  • change the paper to use prop for the CPS
• Stage 2 (after final version)
  • push this change to all std library and examples
  • improve the SMT encoding
    • to treat squash (c_ ...) the same as l_ and p_
    • to automatically remove double squashes
  • try to reduce the number of squashes
    • c_true, c_false, and even c_and/or p1 p2 when p1 and p2 are prop
      are already in prop even without the extra squash, so we could
      consider making p_true be c_true directly and removing l_true, etc
  • some discussion about l_ not being a good name for Z3
    • could rename it to s_ maybe (for squash)?
• Pending issues:
  • making prop abstract prevents subtyping between prop and Type
    • was planning to make prop abstract and use an escape hatch
      coercion between a sub-singleton Type and prop ... but we didn't
      think about the prop to Type direction; explicitly coercing that
      way could be painful? Although, will that be so frequent once we
      make all our combinators strongly prop typed? More motivation
      for the point below then!
  • shouldn't the x:t{p} notation require p to be a prop?
    • I think we should, since this would prevent stuff like x:int{int}
    • we would still need some way to reference the primitive
      refinements, but they would only be used for defining squash
  • should try to make PURE private
  • l_forall and quantifier patterns
    • understand current cheating
    • what's the purpose of guard_free?
    • maybe create an explicit Meta_pattern node,
      and use it for the only pattern in PURE?
  • think about b2t vs b2p
    • a priori we should be able to do a lot better than b2t,
      which is super syntactic and flaky
  • should the constructive operators keep using GTot?

[catalin-hritcu]

discussed a bit with Nik about this a few days back

in the short run we can probably hack something up by making prop abstract in prims and bringing in stuff like squash to prims as well ... and after typechecking prims requiring that refinements and WPs use prop
[the immediate problem with this is the need for a coercion between prop and Type]

in the less short run we have been discussing in Paris with @kyoDralliam and @danelahman about making prop primitive in order to simplify and streamline our formalization (in particular getting rid of the separate logical entailment judgment completely, and relying on squashed arrows and inductive types for the logical part)

[catalin-hritcu]

Worked out some of this in @kyoDralliam's uEMFStar.org (which builds on @mtzguido's ufstar.org). The main change is adding a new -1 universe level and defining prop as Type -1. This allows us to build arrows using prop elements (like squash). We assume that inductives can only be defined at levels >= 0.

The rest is syntactically simple, and it basically only involves assuming a bunch of constants:

squash : Πk. α:Type k -> prop
witness : Πk. α:Type k -> α -> squash α
elim_squash : Πk. α:Type k ->                squash α -> φ':prop -> (α   -> φ') -> φ'
elim_refine : Πk. α:Type k -> φ:(α->prop) -> x:α{φ x} -> φ':prop -> (φ x -> φ') -> φ'
proof_irrelevance : φ:prop -> w:φ -> w':φ -> eq w w'
excluded_middle : φ:prop -> φ \/ ~φ   (where \/ is the squashed sum)

... before being able to define all logical connectives in prop:

let (==) k x y = squash (eq k x y)
let coerce (φ:prop) : Type Z = x:unit{φ}
let (/\) (φ φ' : prop) : prop = squash (pair Z Z (coerce φ) (coerce φ'))
let (\/) (φ φ' : prop) : prop = squash (sum Z Z (coerce φ) (coerce φ'))
let (=>) (φ φ' : prop) : prop = squash (φ -> φ')
let forall k (α:Type k) (f: (α -> prop)) : prop = squash (x:α -> f x)
let true : prop = squash unit
let false : prop = squash empty
let not (φ : prop) : prop = φ => false

It seems simple to turn this into a bunch of axioms and definitions in prims:

assume val squash : Type -> prop
assume val witness : a:Type -> a -> squash a
assume val elim_squash : a:Type -> squash a ->                p:prop -> (a   -> p) -> p
assume val elim_refine : a:Type -> q:(a->prop) -> x:a{q x} -> p:prop -> (q x -> p) -> p

let l_eq (a:Type) (x y : a) = squash (equals x y)
let coerce (p:prop) : Type0 = x:unit{p}
let l_and (p q:prop) : prop = squash (c_and (coerce p) (coerce q))
let l_or (p q:prop) : prop = squash (c_or (coerce p) (coerce q))
let l_imp (p q:prop) : prop = squash (p -> GTot q)
let l_forall (a:Type) (p:a -> prop) : prop = squash (x:a -> p x)
let l_true : prop = squash c_True
let l_false : prop = squash c_False
let l_not (p:prop) : prop = l_imp p l_false

assume val proof_irrelevance : p:prop -> w:p -> w':p -> equals w w'
assume val excluded_middle : p:prop -> l_or p (l_not p)

Some typing rules also need to change, but it's in the expected way, for instance:

    S;G |- t : Type(u)
    S;G, x:t |- t' : prop
   -------------------------- [T-Refine]
    S;G |- x:t{t'} : Type(u)

    S;G |- e : t
    S;G, x:t |- t' : prop
    S;G |= t'[e/x]
   -------------------------- [T-RefineI]
    S;G |- e : x:t{t'}

The big advantage on the formalization side is that we can completely get rid of the whole S;G |= φ judgment. In return we need a single extra rule about reduction and subtyping:

    t ~>* t'   S;G |- t : Type(u)   S;G |- t' : Type(u)
   ----------------------------------------------------- [Sub-Red]
                  S;G |- t <:> t'

[catalin-hritcu]

We are also looking at a variant that doesn't involve a prop universe, but to me it's less intuitive:

assume val prop : Type0

assume val squash : Type -> prop
let el (p:prop) : Type0 = x:unit{p}
assume val witness : a:Type -> a -> el (squash a)
assume val elim_squash : a:Type -> el (squash a) ->
  p:prop -> (a        -> el p) -> el p
assume val elim_refine : a:Type -> q:(a->prop) -> x:a{q x} ->
  p:prop -> (el (q x) -> el p) -> el p

let l_eq (a:Type) (x y : a) : prop = squash (equals x y)
let l_and (p q:prop) : prop = squash (c_and (el p) (el q))
let l_or (p q:prop) : prop = squash (c_or (el p) (el q))
let l_imp (p q:prop) : prop = squash (el p -> GTot (el q))
let l_forall (a:Type) (p:a -> prop) : prop = squash (x:a -> el (p x))
let l_true : prop = squash c_True
let l_false : prop = squash c_False
let l_not (p:prop) : prop = l_imp p l_false

// we don't need proof irrelevance
assume val excluded_middle : p:prop -> el (l_or p (l_not p))

We also don't know if this would work without a special treatment of the el coercion (aka p2t), both in the implementation and in the theory.

[catalin-hritcu]

I started implementing a least intrusive solution on the c_prop-dev branch. Here's a list of things still to do:
https://github.com/FStarLang/FStar/blob/c_prop-dev/PropTODO.org

[aseemr]

This would also be useful to address issues like #1041.