Menu Close

Sucesión de antecesores y sucesores

José A. Alonso,

Definir la lista

   antecesoresYsucesores :: [[Integer]]

cuyos elementos son

   [[1],[0,2],[-1,1,1,3],[-2,2,0,0,2,0,2,2,4],...]

donde cada una de las listas se obtiene de la anterior sustituyendo cada elemento por su antecesor y su sucesor; es decir, el 1 por el 0 y el 2, el 0 por el -1 y el 1, el 2 por el 1 y el 3, etc. Por ejemplo,

   λ> take 4 antecesoresYsucesores
   [[1],[0,2],[-1,1,1,3],[-2,0,0,2,0,2,2,4]]

Comprobar con Quickcheck que la suma de los elementos de la lista n-ésima de antecesoresYsucesores es 2^n.

Nota. Limitar la búsqueda a ejemplos pequeños usando

   quickCheckWith (stdArgs {maxSize=7}) prop_suma

Soluciones

import Test.QuickCheck
 
-- 1ª solución
antecesoresYsucesores :: [[Integer]]       
antecesoresYsucesores = 
  [1] : map (concatMap (\x -> [x-1,x+1])) antecesoresYsucesores
 
-- 2ª solución
antecesoresYsucesores2 :: [[Integer]]       
antecesoresYsucesores2 = 
  iterate (concatMap (\x -> [x-1,x+1])) [1]
 
-- La propiedad es
prop_suma :: (Positive Int) -> Bool
prop_suma (Positive n) =
  sum (antecesoresYsucesores2 !! n) == 2^n
 
-- La comprobación es
--    λ> quickCheckWith (stdArgs {maxSize=7}) prop_suma
--    +++ OK, passed 100 tests.
Ejercicio
, , , , ,

6 soluciones de “Sucesión de antecesores y sucesores”

  1. Responder
    jaibengue 
    import Test.QuickCheck
 
antecesoresYsucesores :: [[Integer]]
antecesoresYsucesores = [1]:map aux antecesoresYsucesores
  where aux (x:xs) = (x-1):(x+1):aux xs
        aux _ = []
 
prop_suma :: Int -> Bool
prop_suma n = sum (antecesoresYsucesores !! ((abs n)+1)) == 2^((abs n)+1)
 
-- Y la comprobación es 
-- λ> quickCheckWith (stdArgs {maxSize=7}) prop_suma
-- +++ OK, passed 100 tests.
  2. Responder
    angruicam1 
    import Test.QuickCheck
 
antecesoresYsucesores :: [[Integer]]
antecesoresYsucesores = iterate (>>= (sequence [pred,succ])) [1]
 
-- Propiedad
-- =========
 
-- La propiedad es
propSuma :: (Positive Int) -> Bool
propSuma (Positive n) =
  sum (antecesoresYsucesores !! n) == 2^n
 
-- La comprobación es
--    λ> quickCheckWith (stdArgs {maxSize=7}) propSuma
--    +++ OK, passed 100 tests.
  3. Responder
    albcarcas1 
    import Test.QuickCheck
 
antecesoresYsucesores :: [[Integer]]
antecesoresYsucesores = [1]:[aux x | x <- antecesoresYsucesores]
  where aux (x:xs) = [pred x] ++ [succ x] ++ aux xs
        aux _ = []
 
prop_suma :: Int -> Property
prop_suma n = n >= 0 ==> sum (antecesoresYsucesores !! (n+1)) == 2^(n+1)
 
--La comprobación es:
 
--λ>  quickCheckWith (stdArgs {maxSize=7}) prop_suma
--+++ OK, passed 100 tests.
  4. Responder
    Maria Ruiz 
     
antecesoresYsucesores :: [[Integer]]
antecesoresYsucesores = iterate sig [1]
  where sig xs = concatMap (x -> [x-1,x+1]) xs
  5. Responder
    menvealer 
    antecesoresYsucesores :: [[Integer]]
antecesoresYsucesores =
  [1] : [concatMap anteriorPosterior xs | xs <- antecesoresYsucesores]
 
anteriorPosterior :: Integer -> [Integer]
anteriorPosterior n = pred n : [n+1]
  6. Responder
    angruicam1

    Definimos el término n-ésimo de la sucesión en coq:

    Require Import Coq.Lists.List.
Import ListNotations.
Require Import ZArith.  
 
Fixpoint lap_aux (l : list Z) : list Z :=
  match l with
  | []      => []
  | n :: l' => (n-1)%Z :: (n+1)%Z :: lap_aux l'
  end.
 
Fixpoint lap (n : nat) : list Z :=
  match n with
  | 0    => [1]%Z
  | S n' => lap_aux (lap n')
  end.

    También definimos la suma de listas de enteros y un lema auxiliar:

    Fixpoint sum (l : list Z) : Z :=
  match l with
  | []      => Z0
  | n :: l' => (n + sum l')%Z
  end.
 
Lemma lap_n_Sn : forall (n : nat),
    (2 * sum (lap n))%Z = sum (lap (S n)).
Proof.
  intro n. simpl (lap (S n)).
  induction (lap n) as [| m l IHl].
  - reflexivity.
  - simpl lap_aux. simpl sum. rewrite <- IHl. auto with zarith.
Qed.

    Y con todo ello probamos la propiedad de la sucesión:

    Theorem lap_sum : forall (n : nat),
    sum (lap n) = Zpower_nat 2 n.
Proof.
  intro n. induction n as [| n'].
  - reflexivity.
  - rewrite <- lap_n_Sn. assert (H : S n' = 1 + n'). { reflexivity. }
    rewrite H. rewrite Zpower_nat_is_exp.
    rewrite IHn'. reflexivity.
Qed.

Escribe tu solución

Este sitio usa Akismet para reducir el spam. Aprende cómo se procesan los datos de tus comentarios.