Ich komme aus einem JavaScript / Ruby-Programmierhintergrund und bin daran gewöhnt, wie wahr / falsch funktioniert (in JS):

!true
// false
!false
// true

Dann können Sie diese wahren / falschen Werte mit @ verwend&& möge

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

Soun undnich (und andere logische / boolesche Operatoren) sind Teil eines einzelnen Systems. es scheint, als ob das "logische" System und das "boolesche" System ein und dasselbe sind.

In Coq sind Logik und Boolesche Werte jedoch zwei getrennte Dinge. Warum ist das? Das Zitat / der Link unten zeigt, wie ein Theorem notwendig ist, um sie in Beziehung zu setzen.

Wir haben bereits mehrere Stellen gesehen, an denen sich analoge Strukturen in der Computerwelt (Typ) und der logischen Welt (Prop) von Coq befinden. Hier ist noch eines: Die booleschen Operatoren andb und orb sind eindeutig Analoge der logischen Verknüpfungen ∧ und ∨. Diese Analogie kann durch die folgenden Theoreme präzisiert werden, die zeigen, wie das Wissen über das Verhalten von andb und orb bei bestimmten Eingaben in aussagekräftige Tatsachen über diese Eingaben umgewandelt werden kan

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

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