coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Doubt about In
- Date: Mon, 22 Feb 2016 17:53:21 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arthur.aa AT gmail.com; spf=Pass smtp.mailfrom=arthur.aa AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f181.google.com
- Ironport-phdr: 9a23:Wuv9hBEqeTzEn3cdxevp/Z1GYnF86YWxBRYc798ds5kLTJ75o8WwAkXT6L1XgUPTWs2DsrQf27WQ7vyrADRbqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0psGYOl0TzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB0wMjhpVGUDs/hzkU5v2+if3/sN43zObOIWiRKooWSm4qa5iYBDtgSYDcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==
If you really need the stronger variant, I'm afraid you need decidability in one way or another.
For instance, you mentioned your stronger version of In, which would give the result for free. The problem with that variant is that it does not allow you to prove "contains x l -> contains x (y :: l)" for types without decidable equality, and this property is crucial for showing many results involving In. You may be able to prove instances of this principle for some concrete values of "x" and "y", but in the general case there's nothing we can do about it.
Em seg, 22 de fev de 2016 às 12:45, Saulo Araujo <saulo2 AT gmail.com> escreveu:
Thanks a lot Artur!Unfortunately I need to use this theorem with a dependent type in which the tactic decide equality is not being able to do its job. I was able to manually prove that the equality of this type is decidable. However, since this proof ended being a little big, I was wondering if by giving a stronger definition of In, I could refraim from having to prove decidability.SauloOn Mon, Feb 22, 2016 at 2:32 PM, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:Hi Saulo,In order to prove this theorem, you need to assume that E has decidable equality:Require Import Coq.Lists.List.Import ListNotations.Theorem strong_in_inv:forall E (l: list E) e f,(forall x y : E, x = y \/ x <> y) ->In f (e :: l) -> e = f \/ (e <> f /\ In f l).Proof.intros R l e f eq_dec.simpl.destruct (eq_dec e f) as [H | H].- intros _. left. trivial.- intros [? | H']; try congruence.now right; split; trivial.Qed.Em seg, 22 de fev de 2016 às 12:27, Saulo Araujo <saulo2 AT gmail.com> escreveu:Hi,I am in the middle of a proof in which I need the following theorem:Theorem strong_in_inv:forall E (l: list E) e f,In f (e :: l) -> e = f \/ (e <> f /\ In f l).Unfortunately, I was not able to complete the proof below:Proof.intros.simpl in H.destruct H.{left.apply H.}{right.split.{(* I am stuck here! *)}{apply H.}}Qed.
- [Coq-Club] Doubt about In, Saulo Araujo, 02/22/2016
- Re: [Coq-Club] Doubt about In, Arthur Azevedo de Amorim, 02/22/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/22/2016
- Re: [Coq-Club] Doubt about In, Arthur Azevedo de Amorim, 02/22/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/22/2016
- Re: [Coq-Club] Doubt about In, Emilio Jesús Gallego Arias, 02/22/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/22/2016
- Re: [Coq-Club] Doubt about In, Emilio Jesús Gallego Arias, 02/22/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/23/2016
- Re: [Coq-Club] Doubt about In, Dominique Larchey-Wendling, 02/24/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/24/2016
- Re: [Coq-Club] Doubt about In (and refine), Jean-Francois Monin, 02/25/2016
- Re: [Coq-Club] Doubt about In (and refine), Saulo Araujo, 02/25/2016
- Re: [Coq-Club] Doubt about In (and refine), Jean-Francois Monin, 02/25/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/22/2016
- Re: [Coq-Club] Doubt about In, Emilio Jesús Gallego Arias, 02/22/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/22/2016
- Re: [Coq-Club] Doubt about In, Arthur Azevedo de Amorim, 02/22/2016
- Re: [Coq-Club] Doubt about In, Saulo Araujo, 02/22/2016
- Re: [Coq-Club] Doubt about In, Arthur Azevedo de Amorim, 02/22/2016
Archive powered by MHonArc 2.6.18.