Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Lemma regarding fold_left

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Lemma regarding fold_left


Chronological Thread 
  • 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
Sent: Thursday, August 04, 2016 10:52 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] Lemma regarding fold_left

 

Hello everyone, I am trying to state a property related to fold_left.


 Lemma fold_left_true : forall (A : Type) (f : bool -> A -> bool) (l : list A),
    fold_left f l true = true -> forall b : A, f true b = true.
 

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
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928




Archive powered by MHonArc 2.6.18.

Top of Page