coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] goal selectors; tactic expressions
- Date: Fri, 25 Jan 2019 13:32:12 +0000
- Accept-language: en-CA, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BY2-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:i+CIhRxkCpgyh0bXCy+O+j09IxM/srCxBDY+r6Qd2+kSIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMx+jq1UvB2uqgdlzILIfI2YLuZycr/fcN4cWGFPXtxRVytEAo6ka4UAFfEBPeFer4LgvlcBrhu+BQ6qBOPg1zRGm3/20rM80+QuCA3NwQ4uH88Tu3nTotX6KacSUOGuzKXW0TnPcu9a1Cz96IjPbhAhpOuDXbN0ccbL1UYvEAbFg0yWpIf4PD2VzvwAvmeH4+Z6Ue+jlXQrpxxrrjWhx8ogkofJiZwWx1zY8Ch0xYc4KNmkREJnZNOoDZtdui6GOIZzRs4tWH9ntSMgxbAGpJK0YS4Hw4k9yRHFcfyIaY2I7wrjVOmPJTd4g2podqqjihi17USs1/TwW9S231pUtyZFlcLDuW4X2xzU98iHVuBy/kC82TaJyg/f8PlEIVozlarHNZEu3qIwlpsUsUTFBCP2n1j2jLOSdkUj/eio6P7rbanhpp+ZL4N0iwf+PboymsGnDuk0LhICUmyF9eimybHv50P0TbRSgv0ziKbZsZTaJcoBpq6+Bg9Yyogj5Au/Dzany9QUg2ULIE9ZdB+cj4jpPE3OIPXiAve+h1Sgiitkx/fDPrH5GJXCMmDDkKv9fbZ680NT1A0zzclG651IDrEBPen8V1TqtN3YCx85Kxa7z/zmCNV7zIMeWHiADrWXMKPI4he04bdlKO6VIYQRpTzVKv4/5veog2Vz0QsWerDs1p8KYli5GO5nKgOXeyy/rM0GFDIotxE5SqSvul2FVzEbXHa/Wa15rhEmQNaoAYfRXdr12eSp3CCnG5RXYiZNDVXaQiSgTJmNR/pZMHHaGcRmiDFRDeHwGb9k7gmnsUrB85QiK+PV/iMCspe6j4p14PHWnBA2szdzCpbEij3ffyRPhmoNAgQO8uVnu0UkkQWD1rR9iv1cU9dU4qERC1poBdvn1+V/TuvKdEfBc9OOFAn0ZPyDWWh0ZONrhtgEbgB6BsmoiQ3F02yyGbgJmreXBZsytKXBw3z2IMU7wHHDhvAs
Are you in an assert or something? all: won't catch a goal that is not visible in the current scope.
Thanks,
Jason Hu
Jason Hu
On Jan 25, 2019 08:19, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:
Hi Gaëtan,
all: repeat solve_eqs
doesn't succeed, I don't know exactly what all : repeat solve_eqs does
(previous emails addressed this question and the answer I was given)
though in this case it's consistent with applying
1: repeat solve_eqs (which leaves one subgoal, so subgoal 2: is the
original subgoal 2)
then applying 2 : repeat solve_eqs.
or maybe just
1: solve_eqs. then 2: solve_eqs. (ie without "repeat", I can't tell)
It doesn't go back to try 1 : solve_eqs again.
eg see the following, where the
second application of the tactic
all : repeat solve_eqs
makes progress beyond the results of the first application of it.
2 focused subgoals
(shelved: 5)
V : Set
Φ2, Ψ1, Ψ2, Γ1 : list (PropF V)
Q : PropF V
sel1, l, l1 : list (PropF V)
============================
((Γ1 ++ Q :: sel1) ++ l ++ Φ2, Ψ1 ++ l1 ++ Ψ2) =
(?Γ1 ++ ?Q :: ?Γ2 ++ ?Γ3, ?Δ)
subgoal 2 is:
G ++ (?Γ1 ++ ?Γ2 ++ ?Q :: ?Γ3, ?Δ, d0) :: H6 =
G ++ ((Γ1 ++ sel1) ++ l ++ Q :: Φ2, Ψ1 ++ l1 ++ Ψ2, d0) :: H6
gen_moveL < all : repeat solve_eqs.
1 subgoal
V : Set
Φ2, sel1, l : list (PropF V)
============================
sel1 ++ l ++ Φ2 = (sel1 ++ l) ++ Φ2
gen_moveL < all : repeat solve_eqs.
This subproof is complete, but there are some unfocused goals.
Try unfocusing with "}".
Cheers,
Jeremy
On 01/25/2019 08:53 PM, Gaëtan Gilbert wrote:
> Note that repeat runs the inner tactic focused on each goal separately
> so "repeat (all: solve_eqs)" would (if the syntax allowed it) be the
> same as "repeat (only 1: solve_eqs)" which is also the same as "repeat
> solve_eqs", and "repeat (only 2: solve_eqs)" is the same as "repeat
> fail" ie idtac.
>
> I feel like "all: repeat solve_eqs" should work given what you describe,
> can you explain how it fails?
>
> Gaëtan Gilbert
>
> On 25/01/2019 06:54, Jeremy Dawson wrote:
>>
>> Hi Cyprian,
>>
>> What I wanted is what I would express as
>> repeat (all : solve_eqs)
>> but it seems as though that form is forbidden.
>>
>> The various things I tried as indicated in my earlier email were simply
>> looking for alternatives that work.
>>
>> Detailed background to what I want: solve_eqs doesn't seem to enlarge
>> the number of goals in the cases where I want to use it, and sometimes
>> solves a goal, sometimes only after solve_eqs has instantiated an evar
>> in another goal, sometimes only after being repeatedly called on the
>> same goal (where each time it simplifies the goal)
>>
>> Cheers,
>>
>> Jeremy
>>
>>
>> On 01/25/2019 10:00 AM, Cyprien Mangin wrote:
>>> What you probably meant is something like "all : repeat solve_eqs"
all: repeat solve_eqs
doesn't succeed, I don't know exactly what all : repeat solve_eqs does
(previous emails addressed this question and the answer I was given)
though in this case it's consistent with applying
1: repeat solve_eqs (which leaves one subgoal, so subgoal 2: is the
original subgoal 2)
then applying 2 : repeat solve_eqs.
or maybe just
1: solve_eqs. then 2: solve_eqs. (ie without "repeat", I can't tell)
It doesn't go back to try 1 : solve_eqs again.
eg see the following, where the
second application of the tactic
all : repeat solve_eqs
makes progress beyond the results of the first application of it.
2 focused subgoals
(shelved: 5)
V : Set
Φ2, Ψ1, Ψ2, Γ1 : list (PropF V)
Q : PropF V
sel1, l, l1 : list (PropF V)
============================
((Γ1 ++ Q :: sel1) ++ l ++ Φ2, Ψ1 ++ l1 ++ Ψ2) =
(?Γ1 ++ ?Q :: ?Γ2 ++ ?Γ3, ?Δ)
subgoal 2 is:
G ++ (?Γ1 ++ ?Γ2 ++ ?Q :: ?Γ3, ?Δ, d0) :: H6 =
G ++ ((Γ1 ++ sel1) ++ l ++ Q :: Φ2, Ψ1 ++ l1 ++ Ψ2, d0) :: H6
gen_moveL < all : repeat solve_eqs.
1 subgoal
V : Set
Φ2, sel1, l : list (PropF V)
============================
sel1 ++ l ++ Φ2 = (sel1 ++ l) ++ Φ2
gen_moveL < all : repeat solve_eqs.
This subproof is complete, but there are some unfocused goals.
Try unfocusing with "}".
Cheers,
Jeremy
On 01/25/2019 08:53 PM, Gaëtan Gilbert wrote:
> Note that repeat runs the inner tactic focused on each goal separately
> so "repeat (all: solve_eqs)" would (if the syntax allowed it) be the
> same as "repeat (only 1: solve_eqs)" which is also the same as "repeat
> solve_eqs", and "repeat (only 2: solve_eqs)" is the same as "repeat
> fail" ie idtac.
>
> I feel like "all: repeat solve_eqs" should work given what you describe,
> can you explain how it fails?
>
> Gaëtan Gilbert
>
> On 25/01/2019 06:54, Jeremy Dawson wrote:
>>
>> Hi Cyprian,
>>
>> What I wanted is what I would express as
>> repeat (all : solve_eqs)
>> but it seems as though that form is forbidden.
>>
>> The various things I tried as indicated in my earlier email were simply
>> looking for alternatives that work.
>>
>> Detailed background to what I want: solve_eqs doesn't seem to enlarge
>> the number of goals in the cases where I want to use it, and sometimes
>> solves a goal, sometimes only after solve_eqs has instantiated an evar
>> in another goal, sometimes only after being repeatedly called on the
>> same goal (where each time it simplifies the goal)
>>
>> Cheers,
>>
>> Jeremy
>>
>>
>> On 01/25/2019 10:00 AM, Cyprien Mangin wrote:
>>> What you probably meant is something like "all : repeat solve_eqs"
- [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Laurent Thery, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, David Holland, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Cyprien Mangin, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Théo Zimmermann, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Cyprien Mangin, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Laurent Thery, 01/24/2019
Archive powered by MHonArc 2.6.18.