I'm wondering what would be the preferred way to handle the following situation I often come to in proofs, using ssr tactics. Here is an example goal:

```
t1, t2: PCUICAst.term
IHt1: AstUtils.strip_casts (trans t1) = trans t1
IHt2: AstUtils.strip_casts (trans t2) = trans t2
wfargs: wf (mkApp (trans t1) (trans t2)) ->
exists (f : term) (args : list term),
mkApp (trans t1) (trans t2) = tApp f args /\ isApp f = false
--------------------------------------------------------
AstUtils.strip_casts (mkApp (trans t1) (trans t2)) =
mkApp (trans t1) (trans t2)
```

I have this `wfargs`

hypothesis that I produce using `have wfargs := lemma`

and I'd like to get the side condition `wf (mkApp ...) ..`

solved. Usually I would use a `forward wfargs`

tactic that would give me the side condition to prove in one goal and the simplified hypothesis in the next. I'm wondering how I could do it more economically (especially so that I can even avoid naming the interemediate result and directly destruct the existential there).

`case: wfargs => [| f args pf]`

? or `case: wfargs; first (* proof of the premise *).`

?

Or maybe `have [| f args pf] := lemma`

?

`[|`

is great, thanks!

The only way to turn an unresolved _ into a goal is via case. Here you are "lucky" that your conclusion is already a "box" you can case. Sometimes we do use `Wrap`

to get a box out the hat. In some cases you can also use `abstract:`

, see the second example of https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#generating-let-in-context-entries-with-have

Yes, the `case/(_ _ …)/Wrap =>`

pattern can be really nice at times, although I have forgotten how the individual parts of the pattern combine to give the behavior you describe :worried:

If I'm not mistaken `have [|...] := Wrap (lemma _ premise2).`

where `lemma`

has 2 premises. `lemma _ premise2`

will have type `premise1 -> something`

while `Wrap (lemma _ premise2)`

should have type `premise1 -> wrap something`

and that you can case.

The unresolved `_`

is abstracted over the whole term by have, before running the intro patter which does the case.

Yes, if you use `Wrap`

with `have`

while constructing the product using a bunch of `_`

s, it's "easy" to see what's happening. What's slightly more obscure is the `move/(_ _ _)/X`

for applying the view `X`

underneath of a number of products in the top assumption.

```
Coq < Require Import ssreflect.
Coq < Axiom f : nat -> nat.
Coq < Record wrap A := Wrap { a : A }.
Coq < Lemma test: True.
test < move/(_ _)/Wrap: f.
1 subgoal
============================
(nat -> wrap nat) -> True
```

So `/(_ args)`

is a way to pass arguments to the top of the stack. While `/Wrap`

is the way to pass the top of the stack to `Wrap`

. Here `args`

is `_`

, and the top of the stack is `f : nat -> nat`

.

When two or more views are one after the other (no intermediate intro pattern, not even the dummy `-`

one), the step abstracting unresolved `_`

is performed at the very end.

So you are really building the term `Wrap(top _)`

and then `fun x => Wrap(top x)`

and then you case the term which has type `nat -> wrap nat`

.

A bit esoteric... :crazy:

Yes, I wasn't fully aware of the "delayed abstraction" of unresolved `_`

when chaining views. But, yes, that does in deed make sense. Thank you for explaining it (again). :+1:

Last updated: Jan 29 2023 at 18:03 UTC