coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] how to rewrite, needed to match goal
- Date: Wed, 30 Dec 2020 12:36:46 +1100
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=LeLSthJ7a+i4BKHslX4gX2DPzrTKLlrr7vrrcKTeb58=; b=n761SFImak2cs4IGzQQekbQ1AEJmO5oW7SVUuT6nHdEpojeYvWddXFMLd1CcY8yyGpkzF6Vr0CQBsgrFlhgbIWDPcDOVWq4NQpCSNcs1UF7K4kpJB7maOIMysJguT6tbalRj93o2dDqaqKcodXxNhuY7xKeB2vNp3Dj30SeQP6lSkcMAP8MI+jpljx6rD+PbnnZ2vMFNqEOoV9osCOZpPKFSW6dSlDAd/VeivPhgcot0o8hpTF4YGGTgdQFNWNLgHFBgv6SW613kbXdBiT6CmqPnwuAdHkd0gbTS4np7pn+Kovyz8t/pW9XvlAANOrJ226esPcapAd1Vz4S+1hnDBw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=cfd5jzhwQIH5NCKFNSZyu6Xr0+xnIXOwV4teCc0WUerqL2tecZJgOsGvNVGsB6fFNDPJpPBRMRdalOkTFMCpNGe37GGkGcBf4oyAVo0SdDrY67dZ7J5fP/zAr9Bdqh2P+mEsX2EM5dhFBHZPK2tvMEDBCbzNkEP1EqfXnsZm5IYA0CbTclKSZEiDJ7i8EKOzkmBRP+j8jh/cX/S06z5fxIRkX0BNVzR2v0cKz504C64QItQpG3EiYPlV4wWetEBjACGo2j/+WtvPVmqccGpatQMJxGcfilqu/sOjGeG209Vu10EhlIRzy3v+EWJBoKetpxzxEWIkfygtWbdadHNPUg==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY4-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:g8BRXBXuZJfN7yfs+Gjzy4HRo9bV8LGtZVwlr6E/grcLSJyIuqrYbB2Dt8tkgFKBZ4jH8fUM07OQ7/m/HzZau93a6jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrwjdrNcajZV8Jqo+xBbFvGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJi3YDUboGbOvlwcKzTf9wVWWVPXsdeWCFaHoOxbJECA/YdMetWrYTwoUYFoxukBQmrAePi0jtGiWHs3aIk1uQgERzN0gI6ENMAq3TUq9P1P7oVXO6x0qbI1yvMb/ZW2Dvn5obHaB4goeqLXbJ2asfe008vFx7fglqOtIPlIimZ2f4Qs2WC6edrSO2ghXI9pQ5rvjiv2tkjipPPho8NxF7I6Tl1zokpKNC7VEN2fd6qHIZOuy2EKYd6X94vTW92tSg6ybALp4O3cScFxpkoyBPSZP2Kf5aH7x/hWuicITF1j29mdrKnnxu//lSsxvfhWsWo0ltGtDdJnsXOu3wXyhDf9NaLRuNy80qlwzqDygLe5+VeLUwoj6bXNp0sz7gtnZQJq0vDBDX5mEDuga+WaEok/u+o5vz7b7rou5GQK5J4hhjjPKsslcGzGOM4PRMQUGSB/uS8yaHj8lb+QLVXiP05j7PVsIjAJcQcuq62HRNa0poi6xa4CTeqytMYnWQbLFJBfxKHiIvpN0vSL/D/CPezm1WskDF1yPDaJrDsDYnBImLenLv9f7tx8VNQxBYxwNxF+p5YFK8NLOr2WkDrtdzYChE5Mxazw+biENhz0p0RWXiRDa+cMKLeq1GG6fghIumXY48Vvi3wJOIj5/7zl3M2h0ISfbSz0ZQNdXC0Bu5mLFmBYXrwntcBFn8HsRY5TOzzkVGNTTpTZ2upUK8n/TE6CIemDZ/ZSYy3gbyB2j27HpxMaWxcBFCMCySgS4LRUPAVLSmWP8VJkzoeVLHnRZVy+wupsVrYxqBqK/uc1iQHrpXlnIxX6vfekAB02TVrFMOb+2iLUid5kn5OTiJgj/M3mlB01lrWifswuPdfD9EGv6oYADd/DobVyqlBM/63XwvAetmTT1P/GIevByx3Q94shdYTMR8kR4eSyyvb1i/vOIc70qSRDcVuoKvawj78K9s7wmuUjPB83WljedNGMCidvoA69wXXANKWwWykrP7zMJ8tgGvK/mrFyneStkZFVgI2Sb/CQX0UekrRq5L++1/GSLitT78gN1kYxA==
Further to this, I have noticed that I can get
Show.
============================
no_rpt_same seq_ord
(derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
l0 d1)
Check no_rpt_same seq_ord
(derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
l0 d1).
(yes this is exactly cutting and pasting the output of Show)
and this gives a type error.
The term "d1" has type "dersrec LJArules emptyT lpst"
while it is expected to have type
"dersrec LJArules emptyT
[(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]"
(cannot unify "lpst" and
"[(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]").
I don't understand how this can be possible. Wouldn't you expect Coq to refuse to have a goal containing a type error? What would be happening here?
Thanks
Jeremy
On 29/12/20 12:10 am, Jeremy Dawson wrote:
Thanks Clement, this has been very helpful indeed, and has enabled me to solve this sort of problem several times.
But in some cases I still seem to be stuck.
For example (just showing the last two hypotheses), I have
H : [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)] = lpst
n : no_rpt_same seq_ord
(derI
(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
?l0 d1)
============================
no_rpt_same seq_ord
(derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
l0 d1)
exact n. fails with the error message
The term "n" has type
"no_rpt_same seq_ord
(derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
?l0 d1)" while it is expected to have type
"no_rpt_same seq_ord
(derI (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p)
l0 d1)"
(cannot unify "[(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0],
Var p0);
(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]" [note - the above few lines are part of the type of l0]
and
"lpst").
I'm presuming this is because the existential ?l0 is expected to have type involving lpst. Is there a way of getting Coq to show the type of an existential?
subst lpst. here gives a really long error message,
> subst lpst.
> ^^^^^^^^^^
Error: Ltac call to "subst (ne_var_list)" failed.
Abstracting over the term "lpst" leads to a term
fun lpst0 : list (list (PropF V) * PropF V) =>
forall
[snip]
which is ill-typed.
Reason is: Illegal application:
The term "derI" of type
[snip]
cannot be applied to the terms
[snip]
The 7th term has type "dersrec LJArules emptyT lpst0"
which should be coercible to
"dersrec LJArules emptyT
[(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]".
So if I'm right in thinking that the type of ?l0 is something containing lpst, how to I change that to the corresponding term on the rhs of H?
Thanks for any help
Jeremy
On 17/12/20 5:05 pm, Clément Pit-Claudel wrote:
This is the short version of your problem, I think:
Require Coq.Vectors.Vector.
Goal forall n (v: Vector.t nat (S (n + 0))),
@Vector.hd (n + 0) v = 0 -> True.
Proof.
intros.
Fail rewrite plus_n_O in v.
(* Error: Cannot change v, it is used in hypothesis H. *)
remember (n + 0) as n0 eqn:Heq in *.
rewrite <- plus_n_O in Heq.
subst.
The first rewrite fails because H would be ill-typed if it succeeded: you'd have (v: S n) and (H: @Vector.hd (n + 0) v); the latter is ill-typed because (n + 0) and n are not unifiable.
So what you need to do is rewrite in both hypotheses at once, so that there's no ill-typed intermediate stage. You can do this with [remember] and [subst] as I did above (and as you observed) or with revert:
Require Coq.Vectors.Vector.
Goal forall n (v: Vector.t nat (S (n + 0))),
Vector.hd v = 0 -> True.
Proof.
intros.
Fail rewrite plus_n_O in v.
(* Error: Cannot change v, it is used in hypothesis H. *)
revert v H.
rewrite <- plus_n_O.
intros.
The key is that you can't rewrite an hypothesis' type if that leads other hypotheses to being ill-typed.
Clément.
On 12/16/20 11:42 PM, Jeremy Dawson wrote:
curiouser and curiouser -
in investigating how I got to this situation I found that
Coq would substitute (using subst.) the following equality in l and d1
Γ0 = Γ1 ++ []
So doing rewrite app_nil_r before substituting solves my problem in this particular case.
But in general - (1) why can you do subst but not rewrite in d1
(2) in general, how do you handle this problem
Jeremy
On 17/12/20 2:43 pm, Jeremy Dawson wrote:
Hi,
I have the following goal (only key parts included)
l : LJArules (map (apfst (fmlsext (Γ1 ++ []) Γ2)) ps1)
(fmlsext Γ1 Γ2 [Imp (Var p) B], Var p)
d1 : dersrec LJArules prems (map (apfst (fmlsext (Γ1 ++ []) Γ2)) ps1)
apd : allDT (no_rpt_same seq_ord (prems:=prems))
(derI (fmlsext Γ1 Γ2 [Imp (Var p) B], Var p) l d1)
============================
allDT (no_rpt_same seq_ord (prems:=prems))
(derI (fmlsext Γ1 Γ2 [Imp (Var p) B], Var p) ?l ?d1)
Now the goal doesn't match apd because the types are wrong,
?l and ?d1 have types which would match those of l and d1 if
l and d1 had (Γ1 ++ []) rewritten to Γ1
But rewrite app_nil_r in d1. rewrite app_nil_r in l.
fails because
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
d1 is used in hypothesis apd.
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
l is used in hypothesis apd.
How can I handle this situation?
Thanks
Jeremy
- [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/28/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
Archive powered by MHonArc 2.6.19+.