Vengo de un fondo de programación de JavaScript / Ruby y estoy acostumbrado a que esto sea cómo funciona verdadero / falso (en JS):

!true
// false
!false
// true

Entonces puede usar esos valores verdaderos / falsos con&& me gusta

var a = true, b = false;
a && !b;

Entoncesy yno (y otros operadores lógicos / booleanos) son parte de un solo sistema; parece que el sistema "lógico" y el sistema "booleano" son uno y lo mismo.

Sin embargo, en Coq, la lógica y los booleanos son dos cosas separadas. ¿Por qué es esto? La cita / enlace a continuación demuestra cómo es necesario un teorema para relacionarlos.

Ya hemos visto varios lugares donde se pueden encontrar estructuras análogas en los mundos computacional (Tipo) y lógico (Prop) de Coq. Aquí hay uno más: los operadores booleanos andb y orb son claramente análogos de los conectores lógicos ∧ y ∨. Esta analogía se puede hacer más precisa mediante los siguientes teoremas, que muestran cómo traducir el conocimiento sobre los comportamientos de andb y orb en ciertas entradas en hechos proposicionales sobre esas entradas.

Theorem andb_prop : ∀b c,
  andb b c = true → b = true ∧ c = true.

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211