coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] need help with a difficult match

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] need help with a difficult match
Date: Thu, 3 Jun 2021 11:21:37 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f172.google.com
Ironport-hdrordr: A9a23:ZC1S6638l10SwbDZv2Q4JQqjBDskLtp133Aq2lEZdPVwSL3IqynIpoVK6faUskdDZJhOo6HUBEDtewKJyXcX2/hOAV7dZnjPhILAFugLnNaSn0y+J8SZzJ916U4KSdkpNPTASXB2kcKS2njuLz9Z+qjUzImYwdv7i11pTQ1sduVJ4gpjYzzxeCAbK2cmZetbZfjsg7si1l3QHwVvH7zLfQh+LpWz26y15eyWEG93dm1Xmnj6/EfYn8+NYlHolmZUInk/jMZvgCe13X25l+XT8ID4u1qskx6VntImwaq4u4AzXvCxtg==
Ironport-phdr: A9a23:TyOPNx23jg1Z2bn8smDOzwMyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBWOo6883RSSBM3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsiq0+2+4YPfbgFMiTayb75+MQi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZUMhfVzJPDJ6/YYQNAeoPOulXoJXyqVYVsRuzBxOhCP/1xzNUmHP727Ax3eQ7EQHB2QwtB9wCsHbTrNXzNacSUv66zK3WwjrddP5W1jL955LJchAlu/2DQbVwcc/fxUIyEA7FjFKQqYrkPzOWyOsNt3aU4PR7WOKgjm4osQBxojy1ysgwjYnJg5sYx1bZ/ip23Ig7P8e3SFJnYdG6CptQsTmXO5d5T88/Xm1lpiY3x74FtJO0YiUExpsqyRDRZvGJbYSF7BLuWfuMLDl4in9pZayyiRis/EWjxOPxUsm63lZJoydDj9LCtWgN2gTN5sSbTvZx5ESs1DaV2wzO6+xIPVo4mbfZJpI/2rI8iJsevVjeEiLzhUn7iLOZe0Ar9+Wp9+jrfrDrqoKCO4NojwzyL6sjldeiDek9LAQOUWab+eq52b3t40L0QbZHg/g0n6bCq5/XJsIWrbOjDQBPyIYs8RO/Ai+m0NsGmXkHK0pIeBedgIjoP1HCOen4Deuij1i1njdn2vLLMqP7DpXCKXjDl7jhfbJj5EJG1AUzytVf64pVCrEHPv3zRlf8uMLEAhI9KQC5wObqBM9g2o4fRW6DGLKVPaHMvVOQ4+IgOeiMZIsbuDbnLPgl4ubjjX0+mV8bfKmp3oUYaHSmEft4OEiZbn/sjc0AEWcOpAYxUOvqiFiaXT5Je3myR7485i08CI++EYjDQZmtjKWd0ye/A51ZfXtLCkuMEHftb4WLQe0AaCOUIs97kzwLT6KtS4E71ULmiAiv6bN8Keyc1TcfromrgNp8/OrVmgs17iclJ8uY2mCJCWpzmzVbaSUx2fU1o0t7y1SO1aV1q/NdHN1XofhOV01yYZzbye15BtT/VyrOe96ITBCtRdDwUmJ5dc4439JbOxU1IN6llB2WmnPyW9f9eJSEAZU19uTX2H2jfq6VLl7J0aAgix8tRc4dbQVOZ4Z6/gnXQpfVygCXzvnwM6sb2yHJ+SGIym/c5Cll

Using generalize dependent on both (g a) and (f a) works. Thanks
Jason! I also had to pose other facts about f and g into the goal first
so that their relevance wasn't generalized away.

On Wed, 2 Jun 2021 11:03:02 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> generalize (g a); generalize dependent (f a); intros; subst
>
>
> On Wed, Jun 2, 2021, 10:51 jonikelee AT gmail.com <jonikelee AT gmail.com>
> wrote:
>
> > I have something like the following:
> >
> > Parameter A : Type.
> > Parameter f : A -> option nat.
> > Parameter g : forall (a:A)(n:nat), (f a = Some n) -> bool.
> >
> > Goal forall a, match f a as o return (f a = o -> bool) with
> > | Some i => g a i
> > | None => fun _ => false
> > end eq_refl = true -> forall n, (f a = Some n) -> bool.
> > intros a m n e.
> > Fail destruct (f a).
> > Fail rewrite e in m.
> >
> > and I'm not having any luck breaking match m down - neither
> > "destruct (f a)" nor "rewrite e in m" work here. Is there some
> > other way to accomplish something similar?
> >
> > Thanks,
> > Jonathan
> >

[Coq-Club] need help with a difficult match, jonikelee AT gmail.com, 06/02/2021
- Re: [Coq-Club] need help with a difficult match, Jason Gross, 06/02/2021
  - Re: [Coq-Club] need help with a difficult match, jonikelee AT gmail.com, 06/03/2021