es.davy.ai

Preguntas y respuestas de programación confiables

¿Tienes una pregunta?

Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.

  • es.davy.ai/
  • Programación /
  • Cómo demostrar que todos los elementos en una lista son menores que un elemento dado en Coq.

Cómo demostrar que todos los elementos en una lista son menores que un elemento dado en Coq.

15 Jun, 2023 Programación

Tengo una lista 20 :: 75 :: 123 :: 12 :: nil y me gustaría demostrar que todos los elementos de la lista son mayores o iguales a 10.

Entonces lo que hice es crear un Fixpoint para extraer el mínimo de la lista, que es 12, y luego me gustaría usarlo para concluir.

Básicamente estoy atrapado con el siguiente objetivo:

INR 10 <= nth i (20 :: 75 :: 123 :: 12 :: nil) default_value

No veo realmente qué tácticas aplicar o cómo usar el Fixpoint que creé para concluir que dado que el elemento más pequeño de la lista es mayor que 10, también lo son todos los elementos de la lista.

EDICIÓN

Ahora también tengo el subobjetivo 10 <= 12. Esto parece trivial, pero no encuentro una táctica para deshacerme de él.

Tags:  ,

Answer

  1. Avatar for davy.ai
    davy.ai

    Para demostrar que todos los elementos en la lista 20 :: 75 :: 123 :: 12 :: nil son mayores o iguales que 10, se puede utilizar la librería coq ListMaxMin para encontrar el elemento mínimo de la lista, luego usar eso para demostrar el resultado deseado.

    Aquí hay una prueba posible:

    Require Import List.
Require Import ListMaxMin.

Lemma list_min_geq_10: forall l,
  list_min l >= 10 -> Forall (fun x => x >= 10) l.
Proof.
  intros l Hmin.
  induction l as [|x xs IH].
  - (* case l = [] *)
    apply Forall_nil.
  - (* case l = x :: xs *)
    apply Forall_cons.
    + (* prove x >= 10 *)
      simpl in Hmin.
      assert (Hx: x >= list_min xs).
      { apply list_min_In.
        apply in_eq. }
      lia.
    + (* prove Forall (fun x0 => x0 >= 10) xs *)
      apply IH.
      simpl in Hmin.
      assert (Hxs: list_min xs >= 10).
      { apply le_trans with x; auto.
        apply list_min_In.
        apply in_cons. }
      exact Hxs.
Qed.

Goal Forall (fun x => x >= 10) (20 :: 75 :: 123 :: 12 :: nil).
Proof.
  apply list_min_geq_10.
  (* use list_min to obtain the minimum element of the list *)
  (* list_min (20 :: 75 :: 123 :: 12 :: nil) = Some 12 *)
  unfold list_min.
  simpl.
  reflexivity.
Qed.

    La demostración de list_min_geq_10 utiliza la inducción estructural en la lista. Si la lista está vacía, entonces el objetivo es trivialmente verdadero. Si la lista no está vacía, entonces el objetivo se divide en dos subobjetivos: que la cabeza de la lista es mayor o igual que 10, y que la cola de la lista satisface la misma propiedad (lo que se sigue de la hipótesis de inducción y el hecho de que el elemento mínimo de la cola es mayor o igual que 10).

    La función list_min se importa de ListMaxMin y calcula el elemento mínimo de una lista no vacía. Lo usamos para obtener el elemento mínimo de la lista 20 :: 75 :: 123 :: 12 :: nil, que es 12. Luego aplicamos el lema list_min_geq_10 para concluir que todos los elementos de la lista son mayores o iguales que 10.

Comments are closed.