Matthieu Sozeau (Dec 10 2020 at 19:23): 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
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: Jan 29 2023 at 18:03 UTC