Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to rewrite, needed to match goal

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to rewrite, needed to match goal


Chronological Thread 
  • 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





Archive powered by MHonArc 2.6.19+.

Top of Page