coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Lemma regarding fold_left
- Date: Thu, 4 Aug 2016 09:00:20 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
- Ironport-phdr: 9a23:9oiIlhIJpYrLdTbcM9mcpTZWNBhigK39O0sv0rFitYgULPnxwZ3uMQTl6Ol3ixeRBMOAuqoC27Cd6/yocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+kQsiC1Y/vi6ibwN76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtM0rzyMF8fkm7otLVbjwV6U+V71RSjo8eShh78ry8BLHUAGn530GU2xQnAAeUCbf6xSvFKz2vyTmrO1lnGG/PMb2RL0wE3z26qZgSBbljGEcMDM27HvQkuRxir5WpFSqoBkpkN2cW52cKPcrJvCVRtgdX2cUBss=
Dear Tiwari,
I would think this is not true in general. Imagine an f which returns false for the first element of a list and true for all other elements of the list regardless of the accumulator bool. Then the result of fold_left would be true, but (f true <firstelem>) would be false.
Best regards,
Michael
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr]
On Behalf Of mukesh tiwari
Hello everyone, I am trying to state a property related to fold_left.
fold_left f (h1 :: (h2 :: t)) true = true -> fold_left f (h2 :: t) (f true h1) = true -> fold_left f t (f (f true h1) h2) Induction on l is not any helpful because I am stuck with true = true in context, and destruct (f true b) is also not any helpful because of false = true in goal. Any idea how to solve this lemma ? Best regards, Mukesh Tiwari Intel Deutschland GmbH |
- [Coq-Club] Lemma regarding fold_left, mukesh tiwari, 08/04/2016
- RE: [Coq-Club] Lemma regarding fold_left, Soegtrop, Michael, 08/04/2016
- Re: [Coq-Club] Lemma regarding fold_left, Gaetan Gilbert, 08/04/2016
- Re: [Coq-Club] Lemma regarding fold_left, mukesh tiwari, 08/04/2016
Archive powered by MHonArc 2.6.18.