Enable subtyping in ctrl_rewrite (and hence, l_to_r)

[R1kM]

#2476 reported issues when using l_to_r to perform rewritings.
l_to_r is based on the primitive ctrl_rewrite, which traverses all subterms t of a given term, creates a goal of the shape t == ?u, and tries to apply lemma a rewriter lemma provided by the user. The core problem was that the goal created also sets a type for the equality based on the type of t in the environment, i.e. eq2 #(type_of t) t ?u. With @TWal and @W95Psp, we observed that this type was sometimes imprecise, for instance, it was often without guards, and led to unification errors when trying to apply the rewriter lemma.

To solve this issue, this PR does not set the type of the eq2 goal, but instead creates a new unification variable for it. The rationale is that rewritings should focus only on the terms to rewrite, assuming all equalities are well-typed, the eq2 type itself is superfluous information (which, in this case, leads to an overly restrictive behaviour). Unfortunately, because of the structure of do_rewrite, there is no rollback of the environment when a rewriting fails and uvars created when generating the eq2 goal must be solved. To do so, I'm currently querying the unifier to ensure that the type of the subterm is a subtype of the type indicated in eq2, but there might be a better way to do that.

Fixes #2476

[R1kM]

Update on this: generating a uvar for the equality in all cases is a bit too powerful.
In particular, a common usecase of ctrl_rewrite is through pointwise, where a lot of rewritings are based on unification through trefl. If we solve the goal eq2 ?u_ty t ?u through trefl, the uvar ?u_ty will remain unsolved, leading to errors down the line.
Note, this does not occur when solving this goal through an application of a lemma of the shape x == y, since the type of the equality in the lemma statement will have been inferred when typechecking the lemma itself.

The new solution proposes to generate a uvar for the equality type conditionally, based on a flag passed to ctrl_rewrite. This flag is set to false (i.e., no generalization of the equality type) for most uses (topdown_rewrite, pointwise, ...), but is set to true in the implementation of the l_to_r tactic which expects a list of lemmas about equalities.

The current implementation passes CI, and also allows the rewritings presented in #2476

[nikswamy]

A few comments about this change:
IIUC, rather than applying trefl in case all the rewriting lemmas fail, this change will instead fail silently.

1. I don't see changes anywhere to any callers of l_to_r. How come?
2. Because of the fold_left, if I write l_to_r [l1;l2;l3] wouldn't this actually try to apply

(fun () -> apply_lemma_r1 l3) `or_else`
(fun () -> apply_lemma_r1 l2) `or_else`
(fun () -> apply_lemma_r1 l1) `or_else`
(fun () -> fail_silently "SKIP")

i.e., isn't this backwards? Or rather isn't it more like "last_or_skip". Looks like that was the original behavior too ... is it intentional?

[R1kM]

Re: 1, the implementation of ctrl_rewrite hardcodes a special behaviour for a failure with Msg "SKIP", where it simply rolls back the current proofstate to before generating the equality, hence avoiding unresolved uvars when all rewritings fail. Note that the previous use of trefl had a similar "fallback" workflow, but trefl does not solve the type of the equality, which would here lead to an unresolved uvar in the default case.

Re: 2, you're indeed right, testing it with the small program below, the last lemma is indeed the one called. Another slightly annoying thing is that it stops at the first lemma it can apply instead of trying them all if rewritings can be chained. I think all our usecases so far use l_to_r with only one lemma, but it'd be good to change in the future.

assume val f : int
assume val g : int
assume val h : int

assume
val lem1 (u:unit) : Lemma (f == g)

assume
val lem2 (u:unit) : Lemma (f == h)

open FStar.Tactics

let test () =
  assert (f == h) by (l_to_r [(`lem1); (`lem2)]; dump "here")

[nikswamy]

this looks good to me, thanks

[nikswamy]

Overall, this looks pretty good.

However, it would be great to have some test cases for l_to_r that exploit the new behavior.
It could be something like the examples from #2476 fixed to work with the new flag used in l_to_r.

[nikswamy]

@R1kM : I think our last conversation about this PR was to try to find a way to avoid the use of matching on this string constant, right?

[R1kM]

@nikswamy My understanding was that, we would ideally like to avoid relying on this string, but that it might be a bit hard without refactoring ctrl_rewrite, and hence should be done in a subsequent PR since this mechanism was already part of ctrl_rewrite. Some possible ideas to do this I had:

• Raise an actual failure (instead of fail "SKIP") if none of the l_to_r lemma rewritings worked, and catch it when calling t_pointwise in the implementation of l_to_r. The problem is that this prevents deep rewritings, as l_to_r will now stop at the first subterm where rewriting is not possible.
• Rollback by default during ctrl_rewrite if no rewriting succeeded. I'm not sure this can be distinguished from a standard exception, and there are likely cases where we would want exceptions raised during ctrl_rewrite to bubble up.
• Pattern-match on a new exception (say, CtrlRewriteSkip) instead of TacticFailure "SKIP", and raise this exception at the end of l_to_r if no rewriting was performed. This might be the better solution, but 1. I'm not sure how removing the pattern-matching on TacticFailure "SKIP" would impact existing code, and 2. is it possible to expose not just functions, but exceptions from FStar.Tactics.Basic.fsti, so that they can be accessed in FStar.Tactics.Builtins?