Interpret ** on both sides of @==> to allow inferring implicit arguments to stick lemmas

[tahina-pro]

I am trying to use the "stick" (or magic wand-like view shift), with lemmas such as:

steel/share/steel/examples/pulse/dice/cbor/CDDL.Pulse.fst

Lines 275 to 297 in 092c02c

	assume
	val stick_consume_l
	(_: unit)
	(#p #q #r: vprop)
	: stt_ghost unit emp_inames
	(p ** ((p ** q) @==> r))
	(fun _ -> q @==> r)
	assume
	val stick_consume_r
	(_: unit)
	(#q #p #r: vprop)
	: stt_ghost unit emp_inames
	(p ** ((q ** p) @==> r))
	(fun _ -> q @==> r)
	assume
	val stick_trans
	(_: unit)
	(#p #q #r: vprop)
	: stt_ghost unit emp_inames
	((p @==> q) ** (q @==> r))
	(fun _ -> p @==> r)

While I can use stick_trans with Pulse successfully inferring implicit arguments, this is not the case for stick_consume_l or stick_consume_r, where I need to specify the two parts of the left-hand-side. From what I understood of @nikswamy 's interpretation, this may be because ** becomes an ordinary F* term as opposed to a Pulse Tm_star AST construct.

Making it easier to use such lemmas would be a first step towards further automation of reasoning about @==> (e.g. an automatic tautology checker)

[nikswamy]

I have a fix to at least the main symptom reported in this issue. However, keep in mind that the Pulse unifier is, by design, very simple, e.g., it does not backtrack.

So, see 80a3d28 for a test case which shows what you can expect to work and not.

That said, there is one aspect of it that I had been trying to get to work, which I think ought to work eventually, but is hard to do in the current way the prover is structured. Consider this example:

ghost
fn test_elim_3 (p q r:vprop)
requires ((p ** q) @==> r) ** p ** q
ensures r
{
    elim _ _;
}

Say the invocation of elim is really elim ?1 ?2, to give names to those uvars.
The prover is called with the following goals : ?1 @==> ?2 and ?1.
The unifier correctly solves the first goal, setting ?1 := p ** q and ?2 := r.
Now it recurses trying to check that the second goal ?1 := p ** q is properly solved.
But this goal is not an atomic vprop and the matcher is currently designed to solve things one atomic vprop at a time, trying to match it against atomic vprops from the context. So, this fails.
@aseemr : would be nice to talk through this; seems to require some non-trivial restructuring of the matcher and its invariants ... but perhaps you know of an easier way.