Incompatibilities between functional extensionality, subtyping, and untyped equality

[kyoDralliam]

aseem >>> Our SMT encoding of functional extensionality is currently unsound and allows for a proof of False. Here is an example:

module Test

open FStar.FunctionalExtensionality

#set-options "--max_fuel 0 --max_ifuel 0"

let g (f:int -> int) :nat -> int = f

let lemma_g_is_injective (f1 f2:int -> int) :Lemma (requires (feq #nat #int (g f1) (g f2))) (ensures (feq #int #int f1 f2)) = ()

The lemma_g_is_injective is clearly wrong: it says any two int -> int functions that are extensionally equal on nat arguments, are extensionally equal for int arguments.When we encode functional extensionality to Z3, we say forall (x:a). f1 x == f2 x ==> f1 == f2. In F* == has a type argument, and so, equality is only at that type. But when we encode == to Z3, we encode it into native equality and that loses the type information. As a result, we can read back that equality at some other type, as in the example above.Just to complete the proof of False, continuing the example above:

let f1 :int -> int = fun x -> if x >= 0 then 0 else 1
let f2 :int -> int = fun x -> if x >= 0 then 0 else 2

let bad () :squash False = lemma_g_is_injective f1 f2; assert (f1 (-1) == f2 (-1))

We can discuss it in the F* meeting on Monday.

guido >>> Ouch, this looks nasty

nik >>> ugh

nik >>> this reminds me of the same problem with dropping the type arguments when encoding heterogeneous equality

nik >>> g isn't really necessary, it seems. This works too

nik >>>
let lemma_g_is_injective (f1 f2:int -> int)
:Lemma (requires (feq #nat #int f1 f2))
(ensures (feq #int #int f1 f2)) = ()

guido >>> This is not an encoding issue, afaict, but about reconciling that axiom with subtyping

guido >>> a could be very well be empty (x:int{False}) (edited)

aseem >>> I thought it's an encoding issue since in F* the == has type, which is lost in the smt encoding

guido >>> Yes, but we can eliminate it anyway, no?

aseem >>> Not sure, typing should prevent such cases just in F*

nik >>> I agree, it's not an encoding issue, but a problem with the formulation of the axiom itself

nik >>> I'm considering this alternative: (edited)

nik >>>
assume Extensionality :
forall (a:Type) (b:Type) (f: efun a b) (g: efun a b).
{:pattern feq #a #b f g} feq #a #b f g <==> (fun (x:a) -> f x) == (fun (x:a) -> g x)

nik >>> explicitly restricting the domain of f and g to a

nik >>> but it's rather brittle and somewhat odd to rely on an eta-expansion to restrict the domain in this way

nik >>> this particular trick doesn't work though, because the SMT encoding actively attempts to remove redundant eta-expansions

aseem >>> If we just deep embed eq2 then the axiom fine as it is?

aseem >>> So why is is not an encoding issue?

aseem >>> (I tried that version too!)

aseem >>> in its current form the axiom has eq2 #(a -> b) f g which seems fine to me

nik >>> but eq2 is very primitive ... we encode it everywhere to Z3 =. Changing this to a deep encoding would mess up almost everything, i think

aseem >>> I was thinking for function types (edited)

aseem >>> Essentially I am saying feq is the notion of equality for functions

aseem >>> But that's breaking too, I agree

nik >>> How about something like:

nik >>>
let eta #a (#b:a -> Type) (f:(x:a -> b x)) (x:a) = f x

assume Extensionality :
forall (a:Type) (b:Type) (f: efun a b) (g: efun a b).
{:pattern feq #a #b f g} feq #a #b f g <==> (eta #a f == eta #a g)

nik >>> This time the SMT encoding doesn't eliminate the eta-expansion

nik >>> and this is no longer provable

nik >>>
let lemma_g_is_injective (f1 f2:int -> int)
:Lemma (requires (feq #nat #int f1 f2))
(ensures (feq #int #int f1 f2)) = ()

nik >>> which is good

nik >>> but sadly, neither is

nik >>>
let test (f: (int -> int)) = assert (f == eta f)

nik >>> But, we can prove eta f == eta (eta f)

nik >>> actually, this doesn't really help .. since we can kind of trick the SMT encoding into eliminating the eta anyway

nik >>>
let extensionality (a:Type) (b:Type) (f: efun a b) (g: efun a b)
: Lemma (ensures (feq #a #b f g <==> (eta #a #(fun _ -> b) f == eta #a #(fun _ -> b) g)))
[SMTPat (feq #a #b f g)]
= admit()

let lemma_g_is_injective (f1 f2:int -> int)
:Lemma (requires (feq #nat #int f1 f2))
(ensures (f1 == f2)) =
extensionality nat int f1 f2;
assert (eta #nat #(fun _ -> int) f1 == eta #nat #(fun _ -> int) f2);
assert (eta #nat #(fun _ -> int) f1 == (f1 <: nat -> int))
by (norm [delta_only [%eta]]); assert (eta #nat #(fun _ -> int) f2 == (f2 <: nat -> int)) by (norm [delta_only [%eta]])

nik >>> hmm, this one is nasty

aseem >>> With function subtyping around, saying eq2 #(a -> b) f g translates to Z3_equal f g seems fishy (edited)

nik >>> agreed

nik >>> alternatives?

aseem >>> We could try to remove this axiom, keep feq as the notion of function equality, and see how much of the code breaks, I guess F* CI would have some cases, may not be as many in mitls and hacl*?

nik >>> it's used quite a lot in many places ...

aseem >>> Yeah ...

nik >>> will have to think more, but so far, I suspect we need some way (like eta above) to restrict the domain of a function in a robust way, i.e., in some way that the SMT encoding doesn't drop it

aseem >>> Yeah, I will also think about it today

aseem >>> How about this:

aseem >>>
assume Extensionality : forall (a:Type) (b:Type) (f: efun a b) (g: efun a b). feq #a #b f g <==> (forall (f1 f2:a -> b) (x:a). (f1 x == f x /\ f2 x == g x) ==> f1 == f2)

(edited)

nik >>> what prevents instantiating f1, f2 with f, g?

nik >>> I was thinking of something like this:

nik >>>
type efun (a:Type) (b:a -> Type) = x:a -> Tot (b x)

type feq #a #b (f:efun a b) (g:efun a b) =
(forall x.{:pattern (f x) / (g x)} f x == g x)

abstract
let restrict #a (#b:a -> Type) (f:(x:a -> b x)) (x:a) = f x

open FStar.Tactics
let extensionality #a #b (f: efun a b) (g: efun a b)
: Lemma (ensures (feq f g <==> restrict f == restrict g))
[SMTPat (feq f g)]
= admit()

let restrict_properties #a #b (f:efun a b)
: Lemma (ensures (feq f (restrict f)))
[SMTPat (restrict f)]
= ()

nik >>> so that you can prove

nik >>>
let test #a #b (f:efun a b) =
assert (restrict f == restrict (restrict f))

(edited)

nik >>> but not

nik >>>
assert (f == restrict f)

nik >>> This will still break stuff, since we'll have to start reasoning about this idempotent restrict thing ...

aseem >>> So we won't be able to prove:

let f1 (x:int) = 2
let f2 (x:int) = 2
assert (f1 == f2)

nik >>> but, at least we can have real == on restricted functions

aseem >>> we can prove restrict f1 == restrict f2

nik >>> yes

nik >>> maybe we could try to figure out some way to support that if you have restrict #t f and if there are there are no types t' such that t <: t' and t' is larger than t, then restrict #t f == f.

nik >>> but that sounds fragile

nik >>> anyway, this restrict thing is the only thing I got right now ...

nik >>> how did you come across this @aseem? it's nasty ... i'm surprised it's been under the radar for so long

aseem >>> Came up in some proof with buffers, where it worked when it shouldn't have :(

nik >>> alright, turning in for the night. talk to you at the meeting

aseem >>> Talk to aseem Yesterday at 10:25 PM
Our SMT encoding of functional extensionality is currently unsound and allows for a proof of False. Here is an example:

module Test

open FStar.FunctionalExtensionality

#set-options "--max_fuel 0 --max_ifuel 0"

let g (f:int -> int) :nat -> int = f

let lemma_g_is_injective (f1 f2:int -> int) :Lemma (requires (feq #nat #int (g f1) (g f2))) (ensures (feq #int #int f1 f2)) = ()

The lemma_g_is_injective is clearly wrong: it says any two int -> int functions that are extensionally equal on nat arguments, are extensionally equal for int arguments.When we encode functional extensionality to Z3, we say forall (x:a). f1 x == f2 x ==> f1 == f2. In F* == has a type argument, and so, equality is only at that type. But when we encode == to Z3, we encode it into native equality and that loses the type information. As a result, we can read back that equality at some other type, as in the example above.Just to complete the proof of False, continuing the example above:

let f1 :int -> int = fun x -> if x >= 0 then 0 else 1
let f2 :int -> int = fun x -> if x >= 0 then 0 else 2

let bad () :squash False = lemma_g_is_injective f1 f2; assert (f1 (-1) == f2 (-1))

We can discuss it in the F* meeting on Monday.

guido >>> Ouch, this looks nasty

nik >>> ugh

nik >>> this reminds me of the same problem with dropping the type arguments when encoding heterogeneous equality

nik >>> g isn't really necessary, it seems. This works too

nik >>>
let lemma_g_is_injective (f1 f2:int -> int)
:Lemma (requires (feq #nat #int f1 f2))
(ensures (feq #int #int f1 f2)) = ()

guido >>> This is not an encoding issue, afaict, but about reconciling that axiom with subtyping

guido >>> a could be very well be empty (x:int{False}) (edited)

aseem >>> I thought it's an encoding issue since in F* the == has type, which is lost in the smt encoding

guido >>> Yes, but we can eliminate it anyway, no?

aseem >>> Not sure, typing should prevent such cases just in F*

nik >>> I agree, it's not an encoding issue, but a problem with the formulation of the axiom itself

nik >>> I'm considering this alternative: (edited)

nik >>>
assume Extensionality :
forall (a:Type) (b:Type) (f: efun a b) (g: efun a b).
{:pattern feq #a #b f g} feq #a #b f g <==> (fun (x:a) -> f x) == (fun (x:a) -> g x)

nik >>> explicitly restricting the domain of f and g to a

nik >>> but it's rather brittle and somewhat odd to rely on an eta-expansion to restrict the domain in this way

nik >>> this particular trick doesn't work though, because the SMT encoding actively attempts to remove redundant eta-expansions

aseem >>> If we just deep embed eq2 then the axiom fine as it is?

aseem >>> So why is is not an encoding issue?

aseem >>> (I tried that version too!)

aseem >>> in its current form the axiom has eq2 #(a -> b) f g which seems fine to me

nik >>> but eq2 is very primitive ... we encode it everywhere to Z3 =. Changing this to a deep encoding would mess up almost everything, i think

aseem >>> I was thinking for function types (edited)

aseem >>> Essentially I am saying feq is the notion of equality for functions

aseem >>> But that's breaking too, I agree

nik >>> How about something like:

nik >>>
let eta #a (#b:a -> Type) (f:(x:a -> b x)) (x:a) = f x

assume Extensionality :
forall (a:Type) (b:Type) (f: efun a b) (g: efun a b).
{:pattern feq #a #b f g} feq #a #b f g <==> (eta #a f == eta #a g)

nik >>> This time the SMT encoding doesn't eliminate the eta-expansion

nik >>> and this is no longer provable

nik >>>
let lemma_g_is_injective (f1 f2:int -> int)
:Lemma (requires (feq #nat #int f1 f2))
(ensures (feq #int #int f1 f2)) = ()

nik >>> which is good

nik >>> but sadly, neither is

nik >>>
let test (f: (int -> int)) = assert (f == eta f)

nik >>> But, we can prove eta f == eta (eta f)

nik >>> actually, this doesn't really help .. since we can kind of trick the SMT encoding into eliminating the eta anyway

nik >>>
let extensionality (a:Type) (b:Type) (f: efun a b) (g: efun a b)
: Lemma (ensures (feq #a #b f g <==> (eta #a #(fun _ -> b) f == eta #a #(fun _ -> b) g)))
[SMTPat (feq #a #b f g)]
= admit()

let lemma_g_is_injective (f1 f2:int -> int)
:Lemma (requires (feq #nat #int f1 f2))
(ensures (f1 == f2)) =
extensionality nat int f1 f2;
assert (eta #nat #(fun _ -> int) f1 == eta #nat #(fun _ -> int) f2);
assert (eta #nat #(fun _ -> int) f1 == (f1 <: nat -> int))
by (norm [delta_only [%eta]]); assert (eta #nat #(fun _ -> int) f2 == (f2 <: nat -> int)) by (norm [delta_only [%eta]])

nik >>> hmm, this one is nasty

aseem >>> With function subtyping around, saying eq2 #(a -> b) f g translates to Z3_equal f g seems fishy (edited)

nik >>> agreed

nik >>> alternatives?

aseem >>> We could try to remove this axiom, keep feq as the notion of function equality, and see how much of the code breaks, I guess F* CI would have some cases, may not be as many in mitls and hacl*?

nik >>> it's used quite a lot in many places ...

aseem >>> Yeah ...

nik >>> will have to think more, but so far, I suspect we need some way (like eta above) to restrict the domain of a function in a robust way, i.e., in some way that the SMT encoding doesn't drop it

aseem >>> Yeah, I will also think about it today

aseem >>> How about this:

aseem >>>
assume Extensionality : forall (a:Type) (b:Type) (f: efun a b) (g: efun a b). feq #a #b f g <==> (forall (f1 f2:a -> b) (x:a). (f1 x == f x /\ f2 x == g x) ==> f1 == f2)

(edited)

nik >>> what prevents instantiating f1, f2 with f, g?

nik >>> I was thinking of something like this:

nik >>>
type efun (a:Type) (b:a -> Type) = x:a -> Tot (b x)

type feq #a #b (f:efun a b) (g:efun a b) =
(forall x.{:pattern (f x) / (g x)} f x == g x)

abstract
let restrict #a (#b:a -> Type) (f:(x:a -> b x)) (x:a) = f x

open FStar.Tactics
let extensionality #a #b (f: efun a b) (g: efun a b)
: Lemma (ensures (feq f g <==> restrict f == restrict g))
[SMTPat (feq f g)]
= admit()

let restrict_properties #a #b (f:efun a b)
: Lemma (ensures (feq f (restrict f)))
[SMTPat (restrict f)]
= ()

nik >>> so that you can prove

nik >>>
let test #a #b (f:efun a b) =
assert (restrict f == restrict (restrict f))

(edited)

nik >>> but not

nik >>>
assert (f == restrict f)

nik >>> This will still break stuff, since we'll have to start reasoning about this idempotent restrict thing ...

aseem >>> So we won't be able to prove:

let f1 (x:int) = 2
let f2 (x:int) = 2
assert (f1 == f2)

nik >>> but, at least we can have real == on restricted functions

aseem >>> we can prove restrict f1 == restrict f2

nik >>> yes

nik >>> maybe we could try to figure out some way to support that if you have restrict #t f and if there are there are no types t' such that t <: t' and t' is larger than t, then restrict #t f == f.

nik >>> but that sounds fragile

nik >>> anyway, this restrict thing is the only thing I got right now ...

nik >>> how did you come across this @aseem? it's nasty ... i'm surprised it's been under the radar for so long

aseem >>> Came up in some proof with buffers, where it worked when it shouldn't have :(

nik >>> alright, turning in for the night. talk to you at the meeting

aseem >>> Talk to you in the morning!

aseem >>> I can try to assess the impact of this change (edited)

nik >>> that would be useful

aseem >>> More bad news(?):

module Test

#set-options "--max_fuel 0 --max_ifuel 0"
let g (f:int -> int) :nat -> int = f

let foo (f1 f2:int -> int) =
assume (g f1 == g f2);
assert (f1 == f2)

This does not rely on the functional extensionality axiom but rather on F* encoding of g as: forall f. g f = f, where = is the native Z3 equality.So: (a) Is our eta-optimization in the smt encoding sound? (b) Suppose we remove (or restrict) the functional extensionality axiom, then may be g f1 == g f2 won't be provable, so it's fine then?

aseem >>> If we wanted to handle this, we can eta expand function encoding (and not do the optimization)you in the morning!

aseem >>> I can try to assess the impact of this change (edited)

nik >>> that would be useful

aseem >>> More bad news(?):

module Test

#set-options "--max_fuel 0 --max_ifuel 0"
let g (f:int -> int) :nat -> int = f

let foo (f1 f2:int -> int) =
assume (g f1 == g f2);
assert (f1 == f2)

This does not rely on the functional extensionality axiom but rather on F* encoding of g as: forall f. g f = f, where = is the native Z3 equality.So: (a) Is our eta-optimization in the smt encoding sound? (b) Suppose we remove (or restrict) the functional extensionality axiom, then may be g f1 == g f2 won't be provable, so it's fine then?

aseem >>> If we wanted to handle this, we can eta expand function encoding (and not do the optimization)

[nikswamy]

@aseemr @tahina-pro @catalin-hritcu @victor-dumitrescu and I discussed this at length today.

There are a few different perspectives. This first note is about typed vs. untyped equality.

• One view is that encoding typed equality in F* to untyped equality in SMT is wrong

This is indeed tricky, but encoding F* equality to SMT equality is essential to making the SMT encoding work in practice at all. Trying to encode some custom notion of equality in SMT is a massive change and unlikely to work.

We prefer to take as a hard constraing that == in F* is encoded to = in SMT.

That said, even without the SMT solver in the loop, using tactics alone it is possible to exploit equality on functions with subtyping to derive false. For example, taking a variant of one of Aseem's examples:

let bad (f1:int -> int) (f2:int -> int) = 
  assert (eq2 #(nat -> int) f1 f2 ==> f1 (-1) == f2 (-1))
      by (let h = implies_intro () in rewrite h; trefl())

This is provable without SMT and makes use of that nat -> int equality to rewrite f1:int -> int to f2:int -> int. So, this appears to be a problem without SMT anyway.

[nikswamy]

Another view is that the treatment of functional extensionality in the presence of subtyping is the culprit.

From this perspective, we propose the following revision of the FStar.FunctionalExtensionality library.

1. Make feq dependent. It is currently only available for non-dependent functions, which appears to be an oversight. I.e., we should define

let feq #a (#b:(a -> Type)) (f g : (x:a -> Tot (b x))) = forall (x:a). f x == g x

2. Introduce a new construct to restrict the domain of a function f, implemented just as an eta-expansion of f.

abstract
val on_domain a #(b : a -> Type) (f:(x:a -> b x)) : x:a -> b x
let on_domain #a #b f = fun x -> f x

3. on_domain is idempotent:

val on_domain_idem (#a:_) (#b:_) (f:(x:a -> b x)) 
   : Lemma (on_domain a (on_domain a f) == on_domain a f)

4. on_domain respects feq

val on_domain_feq (#a:_) (#b:_) (f:(x:a -> b x)) 
   : Lemma (feq #a f (on_domain a f))

5. Revise the functional extensionality axiom so that it is only equates functions on their suitable restricted domains.

val extensionality (#a:Type) (#b:(a -> Type)) (f g : (x:a -> b x)) 
    : Lemma (ensures (feq #a f g <==> on_domain a f == on_domain a g))
                  [SMTPat (feq #a f g)]

Essentially, with this revision, we support functional extensionality only on functions whose domain is suitably restricted.

The intended usage is that in contexts that rely on extensionality, we would work with explicitly restricted functions.

Note, the crucial bit is to not be able to prove that on_domain a f == f

[nikswamy]

We considered and rejected a proposal to allow proving:

val on_domain_eta a b f : on_domain a (fun (x:a) -> f x) == (fun (x:a) -> f x)

Equivalently, one may see this as revealing that the on_domain a f is just an eta-expansion of f and concluding via the idempotence of on_domain a.

But, this is doomed. Since one can prove that eta expansions respects provable equality. i.e.,

let eta_is_eq #a (#b:a -> Type) (f: (x:a -> b x)) : (f == (fun (x:a) -> f x)) =
  FStar.Squash.return_squash Refl

Which would, in conjunction with on_domain_eta allow proving that on_domain a f == f which defeats the purpose.

[nikswamy]

Overall, in comparison with other proofs of false discovered in F*, this one is particularly pernicious since it's not the result of an implementation bug. Rather, it's a problem in the formulation of a familiar axiom that interacts poorly with the presence of subtyping in the core of the system.

Our current plan is to revise the FunctionalExtensionality library as outlined in the 5-step plan above and to evaluate the impact in our existing codebases.

[nikswamy]

@aseemr also rightly points out that the same problem also applies to FStar.PredicateExtensionality.

module Test

open FStar.PredicateExtensionality

let p1 (x:int) :prop = (x >= 0 ==> True) /\ (x < 0 ==> True)
let p2 (x:int) :prop = (x >= 0 ==> True) /\ (x < 0 ==> False)

let foo () :squash False =
  assert (peq #nat p1 p2);
  predicateExtensionality nat p1 p2;
  assert (p1 (-1) <==> p2 (-1))

We should apply that same on_domain fix there.

[nikswamy]

More troubles: Looking into predicate extensionality, and then into propositional extensionality on which it is based, I see that the propositional extensionality axiom is inconsistent with the recently revised definition of prop.

i.e., we now have

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

i.e., the type of sub-singletons.

However, we do not identify all sub-singletons. For example, the following two types are not equal

type t1 = T1
type t2 = T2

Both of these types are prop but they are not equal.

However, with the extensionality axiom, if we do have t1 <==> t2 and the axiom then tells us that p1 == p2, which is a contradiction.

This is already demonstrated in examples/paradoxes/PropositionalExtensionalityInconsistent.fst but somehow I missed this when changing the definition of prop while working on #1533

I see three courses of action:

1. We just remove FStar.PropositionalExtensionality and FStar.PredicateExtensionality

2. We find some other definition of prop so that it doesn't cover all sub-singletons in Type0. Note, the previous definition prop as a:Type0{forall (x:a). x === ()} is also not workable, since this use of heterogeneous equality rules out the use of refinements of unit as prop. See An inconsistency from heterogeneous equality #1533

3. Take this refined notion of propositional extensionality:

module FStar.PropositionalExtensionality

let compatible_at (p1 p2:prop) (p3:prop) =
    (forall (x:p1). has_type x p3) /\
    (forall (y:p2). has_type y p3)

let compatible (p1 p2:prop) = exists (p3:prop). compatible_at p1 p2 p3

assume val axiom :
    unit
  -> Lemma (forall (p1:prop) (p2:prop {compatible p1 p2}).{:pattern (compatible p1 p2)}
                (p1 <==> p2) <==> (p1 == p2))

let apply (p1 p2:prop)
  : Lemma (requires (compatible p1 p2))
          (ensures  ((p1 <==> p2) <==> (p1 == p2)))
  = axiom ()

And

module FStar.PredicateExtensionality
module F = FStar.FunctionalExtensionality
module P = FStar.PropositionalExtensionality

let predicate (a:Type) = a -> Tot prop

let peq (#a:Type) (p1:predicate a) (p2:predicate a) =
  forall x. (p1 x <==> p2 x) /\ P.compatible (p1 x) (p2 x)

let predicateExtensionality (a:Type) (p1 p2:predicate a)
  : Lemma (requires (peq #a p1 p2))
  	  (ensures (F.on_domain a p1==F.on_domain a p2))
  = P.axiom();
    assert (F.feq p1 p2)

[kyoDralliam]

About propositional extensionality and prop : a candidate for your second option would be the quotient of a:Type{forall (x y:a). x == y} by the relation <==>, no ? But I don't think this insight will give anything more than a potential guideline since we would probably need to assume prop and related functions (at least as long as we don't have quotients).

On the topic of functional extensionality, I have seen it presented sometimes as the combination of congruence under lambda (or weak functional extensionality)
Γ,x : A ⊢ f = g : B ⇒ Γ ⊢ λx:A. f = λx:A. g : (x:A) → B
with η :
Γ ⊢ f = λx:A. f x : (x:A) → B
If I understand correctly the specification of on_domain it seems that we are keeping the weak functional extensionality but dropping η, no ?

(As a side remark, I think we rely crucially on η to prove that the wp-monads satisfy monadic-laws but that's at the meta-theoretical level)

[catalin-hritcu]

The propositional extensionality issue is serious too. F* uses any miss-application of the current axiom to immediately prove false:

type t1 = | C1
type t2 = | C2
let f () : Lemma (requires (t1 == t2)) (ensures False) = ()
let g () : Lemma (t1 <==> t2) = ()
let done () : Lemma (ensures False) = apply t1 t2

What I'm not yet sure is how exactly is t1 <==> t2 proved in the g lemma? The logical encoding must be pretty smart about singletons!? Is this also provable without SMT? This is definitely very simple to prove in Coq, where <==> is the same as <->. Kenji has a non-SMT proof in F* and it's simple too, but he was wondering about the proof of f and whether it's so obvious that t1 == t2 should imply False.

[kyoDralliam]

Here is a derivation of g (named equiv12 below) which shouldn't use the smt I think :

module Test

#set-options "--no_smt"

type t1 = | C1
type t2 = | C2

let f12 (x : t1) : GTot t2 = match x with | C1 -> C2
let f21 (x : t2) : GTot t1 = match x with | C2 -> C1

let impl12 : (t1 ==> t2) = FStar.Squash.return_squash f12
let impl21 : (t2 ==> t1) = FStar.Squash.return_squash f21

(* I don't understand why F* does not accept the inlined version... *)
let biimpl : (l_and (t1 ==> t2) (t2 ==> t1)) = FStar.Squash.return_squash (And impl12 impl21)
let equiv12 : (t1 <==> t2) = biimpl

The g part does not seem to depend on any exotic feature of F* and should be derivable in most standard type theory having something corresponding to squash.

The f part does use 2 ingredients specific to F* :

let coerce #a #b (h: a == b) (x :a) : b = x

let f0 (h: t2 == t1) : False = match coerce h C2 with

The first one is equality reflection as shown in coerce. It allows in particular to derive h : t₂ == t₁ ⊢ C₂ : t₁. This is also the case in ETT (but not in ITT where the reduction would be stuck on evaluating h).

The second one is its specific pattern matching. I have trouble to express exactly how pattern-matching is specified, any help would be welcome. My understanding is that this pattern-matching is deemed exhaustive since the only constructor C1 of t1 cannot be matched by the scrutinee.

This feature does not seem derivable in more standard type theories (A draft result of Bauer & Winterhalter that I hint to in #1204 shows actually that its negation is consistent with ETT).

If I remember correctly the intuitive argument for such a pattern matching relies on canonicity, i.e. that the head of the canonical inhabitants of an inductive in an empty context should be among the list of its constructors. Should that also hold in our context containing the equality t1 == t2 ?

[nikswamy]

Another possibility for the definition of prop that is more restrictive is the following:

let subtype_of (p1 p2:Type) = forall (x:p1). has_type x p2
let prop = a:Type0{a `subtype_of` unit}

This is closer in spirit to the previous a:Type{forall (x:a). x === ()}, without going into the problems of heteregeneous equality.

It's also much less disruptive than the other solutions proposed so far, in that it allows us to have propositional and predicate extensionality defined more naturally, as one would expect.

And it's compatible with our predominant use of squashed types (unit refinements) as propositions.

On the downside, it requires making use of an internalized has_type relation.

[kyoDralliam]

@nikswamy Is it written anywhere what's making === such troubles ? I saw some inconsistency issue, but which features make it inconsistent exactly ? (deriving a == b from x:a, y:b |- x === y ?)

I like the spirit of this latest proposal for prop, but (let me be devil's advocate here) what's the argument to explain that it is sound to assume propositional extensionality ? (I don't think we can actually define it, can we ?)

Here is my try at it :
I guess one argument should be that if a `subtype_of` unit holds then any canonical term t of type a should be () (and not just == but actually syntactically the same) in the empty context.

And if in a context G we have a canonical C provably different from () we should be able to prove that the context is actually inconsistent...

[nikswamy]

=== is not really that useful in F*. eq3 #a #b x y can really just be seen as eq2 #Type a b /\ eq2 #a x y. Since /\ is biased left to right, the eq2 #Type a b is seen as a hypothesis when checking the well-typedness of eq2 #a x y, where y:b is implicitly converted to a.

So, if we were to define prop as a:Type0{forall (x:a). eq3 #a #unit x ()} then this is effectively the same as a:Type0{forall (x:a). a == unit /\ x == ()}, which is not very useful: i.e., prop becomes equal to unit.

[catalin-hritcu]

My main worry with internalizing has_type is that it's inherently an under-approximation of the inductive typing rules, and if we use it negatively we could get inconsistency. My guess is that the SMT encoding has to be super careful not to misuse this, by for instance always having good triggers. But if we make it a primitive of the language then my worry is that we can no longer prevent misuse. Unless it's only used to define prop, which is anyway a bit special?

[nikswamy]

has_type is indeed an under-approximation of typing, but it's interpretation is also intentionally left open, i.e., it is not fully specified. Can you say more about the sort of negative usage you are worried about?

[nikswamy]

About this comment from Kenji:

On the topic of functional extensionality, I have seen it presented sometimes as the combination of congruence under lambda (or weak functional extensionality)
Γ,x : A ⊢ f = g : B ⇒ Γ ⊢ λx:A. f = λx:A. g : (x:A) → B
with η :
Γ ⊢ f = λx:A. f x : (x:A) → B
If I understand correctly the specification of on_domain it seems that we are keeping the weak functional extensionality but dropping η, no ?

[Later update: the following claim about eta is no longer true, since it was unsound]

Just to be explicit, η equivalence is still provable in F*.

let eta_is_eq #a (#b:a -> Type) (f: (x:a -> b x)) : (f == (fun (x:a) -> f x)) =
  FStar.Squash.return_squash Refl

The on_domain a f construction is internally given as an eta, but that's irrelevant, I think. We could just give it internally as the identity.

The way I see restricted_t a b is that this is a new type former, a subtype of x:a -> b x, with the interpretation that a is the maximal domain of the function. And it is only these functions whose maximal domain is well-identified that we can safely provide the extensionality axiom. on_domain a #b f introduces this new type.

See examples/micro-benchmarks/Test.FunctionalExtensionality.fst (in the feq_sn branch) for some more discussion and examples.

[aseemr]

This is fixed in master based on the plan above.

See also examples/micro-benchmarks/Test.FunctionalExtensionality.fst for more.

Closing the issue, we can still use it for discussions.

[catalin-hritcu]

So far I haven't been able to find anything terrible when has_type is used unrestricted, but I'll keep searching :)

[mtzguido]

Catching up only now.. sorry for not being around during the heroic effort! I am also pretty convinced this is fixed now, and very well so.

For PropositionalExtensionality, I feel an anternative would be stating (p1 <==> p2) ==> (squash p1 == squash p2), quite similarly to on_domain. In that case I don't think we need to depend on the definition of prop.

(In any case, I think we cannot have the "singletons" definition of prop if we want an elimination from squash to prop. I have a small argument written down if anyone is interested. Essentially, I think we could turn a proof that there is a number satisfying p to an actual number satisying p, purely, which does not make sense to me.)

[nikswamy]

That's an interesting variant of prop extensionality. But is squash (squash p) == squash p?

[mtzguido]

Yes, by the same axiom, since p <==> squash p (which holds for any definition of prop.. right? I may be mixing things up).