Stream: math-comp users

Topic: Idiom with have?


view this post on Zulip 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).

view this post on Zulip 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 ?

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 19:02):

[| is great, thanks!

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Dec 14 2020 at 15:16):

A bit esoteric... :crazy:

view this post on Zulip 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: Jan 29 2023 at 18:03 UTC