coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] need help with a difficult match

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] need help with a difficult match
Date: Wed, 2 Jun 2021 10:51:29 -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-qk1-f176.google.com
Ironport-hdrordr: A9a23:2qsxL6CD3/ehBX7lHemd55DYdb4zR+YMi2TDsHoBMiC9E/bo7/xG+c5w6faaskdzZJhNo6HjBEDiewKkyXcW2/h3AV7KZmCP0wuVxelZjLcKqAeQfxEWmNQtsJuIsJITNDQzNzVHZArBjzVQa+xQpuVvOZrHudvj
Ironport-phdr: A9a23:vQHUYRwjiEmGsCDXCzJtylBlVkEcU1XcAAcZ59Idhq5Udez7ptK+ZR2Zv6QyxwCUFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoVJ8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9mz2uyo5ZHeZwdFiDW/bL5yMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhikHOTAn7W/Zict+g61HrxyuvBF/34zZbZuJOPdkYq/RY9UXTndBUMZLUCxBB5uxY4UND+oGO+ZYror9qEUKrRSgGwahH+zvyjpSiX/32a02yfguEQbD3AAuAtkDt3bUrNLzNKcTUuC60q3IwivdYP5N1jf97ZLHchElof2WQb1wds/RxFApGgjYgVqetZbrMCmJ1uQRrWeb9exgWPqyh2Mnqw98rSaiytswh4TJhI8YxEzJ+CplzIs1ONG2RlJ3bNqlHZVQtCyXKZd6T98/Tm12uis31qALtJC7cSYEzpks2h3Ra+SffoSW/h7uUPydLDR4iX5/Zr6zmQi+/VK9xuD+V8S4yEhGoytZntXRs30Byhje5dSCR/Zy/0qtxSqD2gXO5u1aPUw5kK7WJII8zrMyk5cTv1jPHiH4mEjzgq+ZaFgr9vWt5uv6f7nquIKTOolpgQ/kKKsugNawAeEgPwgOQWeb/eO82aXm/ULjQbVKiuQ6krDasJzHPMgbqLO1Dg1U34o55Ba/CDCm0NscnXYZNl5KZBWHj43xN1HPJvD3E+u/jkyynDt3w/3KJL7sD5XXInTdjrvtY6xx51NexQcy1dxf4ohbCrAFIPL9QE/xs9nYAwc7MwyzxebnCdZ92Z0aWW2RHKCUK6zSsVqS6eIuJ+mAfpMauDH4K/Q9/f7hkWc5mUMBfamuxZYYdHe4Hu1/L0qFZXrsn8wOHHwRvgs+SezqkEeNXSRSZ3a0RaI85ys0BJioDYfZFciRh+mK2z7+FZlLbCgSAVeVVHzsao+sWvEWaSvULNU3wRIeUr30AY0m0xCtuQv3xpJoK+PV/msTspepnIx34OvSlhw2+DFcAMGU0mXLRGZxyDBbDwQq1bxy9BQugmyI1rJ11qQw/T174vpIVkIjNseZwbUlVZb9XQXOetrPQ1GjEI3O6d4ZQdc4wttIaEF4SYzKZvXr0C+jArtTnLuOVsRczw==

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