Removing eta equivalence from F* #2294
Conversation
…olution in Rel to not abstract in the flex rigid case if not necessary
…ions; killed an annotation in dependent map
…SelEffect which are admitted so far
…ns and refinements
| @@ -149,7 +149,8 @@ let lem_on_comp #a #b #c (f:b -> c) (g:a -> b) | |||
| = () | |||
|
|
|||
| /// We also rely on eta being a provable equality | |||
| let eta (f:'a -> 'b) : Lemma (f == (fun x -> f x)) = () | |||
| /// AR: 05/11, eta is no longer provable, so admitting it | |||
| let eta (f:'a -> 'b) : Lemma (f == (fun x -> f x)) = admit () | |||
There was a problem hiding this comment.
This file is just a sketch with many assumes in it already.
It's not worth fixing the proofs here to not use eta.
| Lemma (ensures (fun (x:a) -> f x) == (fun (x:a) -> g x)) = | ||
| assert ((fun (x:a) -> f x) == (fun (x:a) -> g x)) | ||
| by (l_to_r [quote (q_as_lem x)]; | ||
| trefl()) |
There was a problem hiding this comment.
Here's a hand-rolled use of functional extensionality. We didn't need to use the on_domain stuff on restricted functions from FStar.FunctionalExtensionality
| // returns Some t' | ||
| // if (fun xs -> body) is an eta-expansion of t' | ||
| // else returns None | ||
| let is_an_eta_expansion env vars body = |
There was a problem hiding this comment.
no more eta reduction in SMT encoding
| @@ -218,6 +218,26 @@ and on_subterms | |||
| : tac<(term * ctrl_flag)> | |||
| = let recurse env tm = ctrl_fold_env g0 d controller rewriter env tm in | |||
| let rr = recurse env in (* recurse on current env *) | |||
| let rec descend_binders orig accum_binders accum_flag env bs t rebuild = | |||
There was a problem hiding this comment.
Part of the change in this PR is to enhance the CtrlRewrite (the underlying code for the pointwise tactic and variants like l_to_r) to actually descend in the binders of an lambda, a refinement type etc.
Note, while this is an improvement, it is still incomplete ... there are other parts of the syntax of terms that this does not descend into.
As a separate PR, I will provide a more complete implementation of this function
|
|
||
| So, introduce needless eta expansions here would lead to unification | ||
| failures elsewhere | ||
| *) |
There was a problem hiding this comment.
One key change: Do not introduce needless etas
| let is_abs t = match t.n with | ||
| | Tm_abs _ -> true | ||
| | _ -> false in | ||
| let maybe_eta t = |
There was a problem hiding this comment.
Another key change---don't bake in eta equivalence
| let congruence_fun #a (#b:a -> Type) (f g:(x:a -> b x)) : | ||
| Lemma (requires (forall x. f x == g x)) | ||
| (ensures (fun (x:a) -> f x) == (fun (x:a) -> g x)) = admit() | ||
| (ensures (fun (x:a) -> f x) == (fun (x:a) -> g x)) = congruence_fun' f g () |
There was a problem hiding this comment.
where congruence was previously assumed, it can now be proven
|
|
||
| private | ||
| let __forall_inst #t (#pred : t -> Type0) (h : (forall x. pred x)) (x : t) : squash (pred x) = () | ||
|
|
||
| assume | ||
| val eta (#a:_) (#b:a -> Type) (f: (x:a -> b x)) (_:unit) : Lemma (f == (fun x -> f x)) |
There was a problem hiding this comment.
but we need eta as an axiom to prove fun_ext for arbitrary f, g as shown below
| FStar.Squash.return_squash Refl | ||
| // (* To begin with, eta is provable *) | ||
| // let eta_is_eq #a (#b:a -> Type) (f: (x:a -> b x)) : (f == (fun (x:a) -> f x)) = | ||
| // FStar.Squash.return_squash Refl |
There was a problem hiding this comment.
nope, not anymore
| (sq_feq : squash (feq f g)) | ||
| : Lemma (ensures on_domain a f == on_domain a g) | ||
| = admit() | ||
| // let open FStar.Tactics in |
There was a problem hiding this comment.
These are actually provable with tactics.
But, using tactics in funext leads to circularities in bootstrapping the compiler.
A separate PR will fix those bootstrapping problems and remove these admits
Joint work with @aseemr
From CHANGES.md:
Since 2686888, F* no longer
supports eta equivalence. Dominique Unruh observed that the
primitive
pointwisetactic (which treats provable equality as acongruence) allows proving functional extensionality, which is
unsound in conjunction with subtyping in F* (see below for more
discussion of that). It turns out that a crucial step in that
unsoundness proof is the use of eta equivalence (See Bug1966a.fst
for a proof of that, with thanks due there also to Catalin Hritcu,
who writes about it here).
To fix this, we removed eta equivalence. One rough intuition for
why eta reduction is incompatible with subtyping is that it can
change the type of a function, widening its domain, e.g., for
f:int -> int, reducing(fun (x:nat) -> f x)tofchanges itstype. Restricting eta reductions to only those that are type
preserving turns out to not feasible in the presence of
abstraction and subtyping.
With the removal of eta, functional extensionality is now a
theorem in F* at least for eta-expanded functions, no longer an axiom,
which is an improvement. The
removal of eta equivalence introduced regressions in some proofs
that were implicitly relying on it. See, for example,
Changes in support of an F* fix removing eta equivalence hacl-star/hacl-star#442