Buenas tardes.
Quería hacer una consulta sobre la forma de interpretar afirmaciones sobre mapas parciales en lo que refiere a la existencia de elementos.
En el práctico 7 hay algunas instancias de afirmaciones que hablan sobre propiedades de mapeos, pero no me termina de quedar claro si estas propiedades implican la existencia de las imágenes del mapeo.
Para plantearlo de forma abstracta, supongamos que tenemos las siguientes afirmaciones:
"P1. The map ABMap maps an element of A to an element of B that fulfills BProp"
"P2. The map BCMap maps an element of B that fulfills BProp to an element of C that fulfills CProp"
Y supongamos que tenemos el siguiente código de Coq:
Definition partial a b := a -> option b.
Notation "a ->> b" := (partial a b) (at level 51, right associativity).
Parameter A: Set.
Parameter B: Set.
Parameter C: Set.
Parameter ABMap: A ->> B.
Parameter BCMap: B ->> C.
Parameter BProp: B -> Prop.
Parameter CProp: C -> Prop.
Definition p1v1 := forall (a: A) (b: B), ABMap a = Some b -> BProp b.
Definition p1v2 := forall (a: A), exists (b: B), ABMap a = Some b /\ BProp b.
Definition p2v1 := forall (b: B) (c: C), BProp b -> BCMap b = Some c -> CProp c.
Definition p2v2 := forall (b: B), BProp b -> exists (c: C), BCMap b = Some c /\ CProp c.
Para la afirmación P1:
Tanto p1v1 como p1v2 son diferentes formas de intepretar la afirmación. La única diferencia real entre uno y otro es que p1v2 afirma que el mapeo ABmap está definido para todo elemento de A y (ABMap a) siempre cumple BProp, mientras que v1 solamente afirma que (ABMap a) cumple BProp en el caso de que el mapeo esté definido para a.
Para la afirmación P2:
El caso es similar, p2v1 no supone la existencia del mapeo y solamente afirma que se cumple la afirmación cuando el mapeo esté definido. Por otra parte, p2v2 afirma que (BCMap b) está definido por lo menos si b cumple BProp, y luego (BCMap b) cumple CProp.
Quería consultar entonces cuál de las dos interpretaciones sería la más correcta para este par de situaciones.
Saludos.