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.

¿Hay una prueba más corta para este teorema en Coq?

23 Jul, 2023 Programación

Estoy aprendiendo a usar Coq e intento demostrar los teoremas de un artículo que estoy leyendo. El artículo se llama “Having a Part Twice Over” de Karen Bennett, publicado en 2013. El artículo propone una teoría mereológica compuesta por dos primitivas F y Ps y define la relación de parte P utilizando las dos primitivas.

Lo codifiqué de la siguiente manera:

Class Entity: Type.

(* Mereología de ranura define la relación de parte
 * con las dos primitivas F y Ps.
 * La idea es que los todo tienen ranuras
 * llenas por sus partes.
 * F x s significa que x llena la ranura s.
 * Ps s y significa que s es una ranura de parte de y.
 * P es la relación de parte.
 *)
Parameter F : Entity -> Entity -> Prop.
Parameter Ps : Entity -> Entity -> Prop.
Definition P (x y : Entity) :=
  exists s, F x s /\ Ps s y.

(* Herencia de ranura *)
Axiom A5 : forall x y z1 z2 : Entity,
  (Ps z1 y /\ F x z1) /\ Ps z2 x -> Ps z2 y.

(* Transitividad de parte *)
Theorem T7 : forall x y z : Entity,
  (P x y /\ P y z) -> P x z.
Proof.
  intros x y z.
  unfold P.
  intro h.
  destruct h as (EsPxy, EsPyz).
  destruct EsPxy as (s1, Pxy).
  destruct Pxy as (Fxs1, Pss1y).
  destruct EsPyz as (s2, Pyz).
  destruct Pyz as (Fys2, Pss2z).
  exists s1.
  split.
  apply Fxs1.
  apply A5 with (z1 := s2) (x := y).
  split.
  split.
  assumption.
  assumption.
  assumption.
Qed.

Logré demostrar el teorema T7. Tengo dos preguntas:
* ¿Está bien mi código en Coq? (No estoy seguro si la forma en que declaré el tipo, las primitivas y el predicado es correcta).
* ¿Hay una prueba más corta? (En cuanto a la longitud de la prueba, solo quiero saber sobre el número de tácticas).

Tags:  

Answer

  1. Avatar for davy.ai
    davy.ai

    Su código Coq parece correcto, pero hay algunas cosas que puede mejorar.

    En primer lugar, sería útil agregar algunos comentarios que expliquen qué significa y qué hace cada axioma y teorema. Esto hará que su código sea más legible y más fácil de entender para aquellos que deseen usarlo o modificarlo.

    En segundo lugar, puedes usar el comando Record para definir un tipo de registro para la mereología en lugar de usar el comando Class para Entity. Esto hará que la estructura de la mereología sea más explícita y facilitará el acceso a sus componentes.

    En tercer lugar, puedes usar la táctica congruence en lugar del axioma A5 para demostrar la transitividad. Esto puede hacer que la prueba sea más corta y más fácil de seguir.

    Aquí hay una versión actualizada de su código con estas mejoras:

    (* Define el registro de mereología *)
Record Mereology : Type :=
{
  Entity : Type;
  F : Entity -> Entity -> Prop;
  Ps : Entity -> Entity -> Prop;
  P : Entity -> Entity -> Prop := fun x y =>
        exists s, F x s /\ Ps s y
}.

(* Define una notación conveniente para la mereología *)
Notation "x 'fills' s" := (F x s) (at level 70).
Notation "s 'is_part_of' y" := (Ps s y) (at level 70).
Notation "x 'is_part_of' y" := (P x y) (at level 70).

(* Define un ejemplo de mereología *)
Definition example_mereology : Mereology :=
{| Entity := nat;
   F := fun x y => y < x;
   Ps := fun s y => s < y |}.

(* Define un teorema sobre la transitividad de la parte *)
Theorem parthood_transitivity :
  forall M : Mereology, forall x y z : M.(Entity),
    x is_part_of y -> y is_part_of z -> x is_part_of z.
Proof.
  intros M x y z [s1 [Hx_s1 Hs1_y]] [s2 [Hy_s2 Hs2_z]].
  exists s1. split.
  - apply Hx_s1.
  - rewrite <- Hs1_y. apply Hs2_z.
Qed.

    En cuanto a su segunda pregunta, es difícil decir si existe una prueba más corta sin más contexto sobre las definiciones y axiomas utilizados en la prueba. Sin embargo, el uso de la táctica congruence a menudo puede simplificar la prueba de transitividad en mereologías.

Comments are closed.