Library unfinished

Check types in Coq

Require Import Bool.
Search bool.

These are "bool" datatypes - lowercase "true" and "false" used just to manipulate Boolean values.

Check true.
Check false.

Eval compute in orb true false.
Eval compute in true || false.
Eval compute in andb true false.
Eval compute in true && false.
Eval compute in negb false.
Eval compute in if true then 3 else 4.

Definition a := true.
Eval compute in orb a (negb a).

Definition eMiddle (a:bool): bool :=
orb a (negb a).
Eval compute in eMiddle true.

Definition Nor (a b:bool): bool :=
negb (orb a b).
Eval compute in Nor true true.

Eval compute in andb true false.
Eval compute in true && false.
Eval compute in orb true false. Eval compute in true || false.
Eval compute in negb false.
Eval compute in if true then 3 else 4.
Eval compute in (3=4).

Warning! The following expression is wrong, because "if" expression needs "bool" type, but "1=2" evaluates to "Prop" type. In short, "false" and "False" are two very different things.
Eval compute in if 1 = 2 then 3 else 4.
If you want to write such conditionals, compare two numbers so that it returns "bool".

Require Import Coq.Arith.EqNat.
Eval compute in if beq_nat 1 2 then 3 else 4.

This function takes two natural numbers and returns "bool"

Check beq_nat.

These are propositions of type "Prop". In this case "True" embodies statement that is always true. And "False" is a statement that is a falsehood.

Check True.
Check False.

You can check types of other expressions; and you can also evaluate them.

These are simply natural numbers.

Check 3.
Check (3+4).

This is a pair of natural numbers of type (nat*nat).

Check (3,4).

Function mult takes two natural arguments.
Expression mult 3 has got one argument already it wants one more.
Finally, expression mult 3 5 has got both arguments, it can be computed.

Check mult.
Check mult 3.
Check mult 3 5.

Unlike "mult" which should precede both arguments, some operators are infix operators: they are written in the middle.

Locate "*".
Locate "/\".
Locate "->".
Locate "_ <= _".

These are propositions (you can ask, if they are True or not). They are not "bool" datatype! They are "Prop" datatype. Notation 3<>6 stands for "not equal".

Check (3=5).
Check ((3=5)/\True).
Check (3 <= 6).
Check (3 <> 6).

This is a function type. Not a value, just a type notation.

Check nat -> Prop.

Definition g (x: nat): (nat*nat) :=
(x*x, x).
Check g.

Eval compute in
let f := fun x => (x * x, x) in f 4.

Use and build truth tables

These examples are adopted from this source: Software Foundations by Benjamin C. Pierce et al. - Basics

Example test_orb1: (orb true false) = true.
Proof.
simpl.
reflexivity.
Qed.

This definition is of Peirce's arrow or the logical NOR operator (see also Problem 3 in HW1). It has two Boolean arguments and produces a Boolean value. It is true when both b1 and b2 are false, and it is false otherwise.

Definition norb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => false
  | false => negb b2
  end.

Example test_norb1: (norb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_norb2: (norb false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_norb3: (norb true false) = false.
Proof. simpl. reflexivity. Qed.
Example test_norb4: (norb true true) = false.
Proof. simpl. reflexivity. Qed.

Use precedence and associativity

Eval compute in 3+4.
Eval compute in Nat.add 3 4.

Eval compute in 3*4.
Eval compute in Nat.mul 3 4.

Eval compute in 2+3*5.
Eval compute in (Nat.add 2 (Nat.mul 3 5)).

Lemma sample1_1: forall a: Prop, ~(~a /\ a).
Proof.
  intros a.
  unfold not.
  intros.
  destruct H as [H1 H2].
  apply H1.
  exact H2.
Qed.

Do not modify this line: sample1_2

Lemma sample1_2: forall a: Prop, a -> ~~a.
Proof.
  intros a.
  unfold not.
  intros H1.
  intros H2.
  apply H2.
  exact H1.
Qed.

Require Import ClassicalFacts.
Require Import Classical_Prop.

Print excluded_middle.
Check excluded_middle.

Variable xx: Prop.

Check (classic xx).
Check classic.

Lemma NNPeirce : forall A B: Prop, ~~(((A -> B) -> A) -> A).
Proof.
  tauto.
Qed.

Require Import ClassicalFacts.
Require Import Classical_Prop.

Theorem restricted_excluded_middle : forall (P:Prop) (b:bool),
  (P <-> b = true) -> P \/ ~P.
Proof.
  intros P [] H.
  - left. rewrite H. reflexivity.
  - right. rewrite H. intros contra. discriminate contra.
Qed.

Require Import Bool.
Require Import Arith.

Theorem restricted_excluded_middle_eq : forall n m : nat,
  n = m \/ n <> m.
Proof.
  intros n m.
  apply (restricted_excluded_middle (n = m) (beq_nat n m)).
  symmetry.
  apply eqb_eq.
Qed.