## Stream: math-comp users

### Topic: Idiom with have?

#### Matthieu Sozeau (Dec 10 2020 at 19:23):

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).

#### Kenji Maillard (Dec 10 2020 at 21:18):

`case: wfargs => [| f args pf]` ? or `case: wfargs; first (* proof of the premise *).` ?

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

#### Matthieu Sozeau (Dec 11 2020 at 19:02):

`[|` is great, thanks!

#### Enrico Tassi (Dec 11 2020 at 19:49):

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

#### Christian Doczkal (Dec 14 2020 at 09:27):

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:

#### Enrico Tassi (Dec 14 2020 at 09:40):

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.

#### Enrico Tassi (Dec 14 2020 at 09:41):

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

#### Christian Doczkal (Dec 14 2020 at 09:53):

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.

#### Enrico Tassi (Dec 14 2020 at 15:12):

``````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
``````

#### Enrico Tassi (Dec 14 2020 at 15:14):

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`.

#### Enrico Tassi (Dec 14 2020 at 15:15):

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.

#### Enrico Tassi (Dec 14 2020 at 15:16):

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`.

#### Enrico Tassi (Dec 14 2020 at 15:16):

A bit esoteric... :crazy:

#### Christian Doczkal (Dec 14 2020 at 15:20):

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: Jul 15 2024 at 20:02 UTC