Logic

Table of Contents

Homepage | Previous: Tactics.v | Code | Next: IndProp.v

1. Summary

1.1. Terms

propositions, Prop type, logical connectives, conjunctive and disjunctive hypotheses, negation, falsehood, principle of explosion, logical equivalence (<->), existential quantification (exists), setoids, logical equivalence, Setoid library, programming with propositions, boolean vs propositional reasoning, functional extensionality, constructive logic, law of excluded middle.

2. Notes

2.1. Logical Connectives

Conjunction

Copied verbatim.

  • Definition:

    The conjunction, or logical and, of propositions A and B is written A /\ B; it represents the claim that both A and B are true.

  • How to Prove (split tactic)

    To prove a conjunction, use the split tactic. This will generate two subgoals, one for each part of the statement.

  • How to Introduce (conj tactic)

    For any propositions A and B, if we assume that A is true and that B is true, we can conclude that A /\ B is also true. The Coq library provides a function conj that does this.

  • Using conjunctions (destruct tactic)

    To go in the other direction – i.e., to use a conjunctive hypothesis to help prove something else – we employ the destruct tactic.

    When the current proof context contains a hypothesis H of the form A /\ B, writing destruct H as =HA HB= will remove H from the context and replace it with two new hypotheses: HA, stating that A is true, and HB, stating that B is true.

  • Other notes

    You can use add_comm and add_assoc to shift /\ around.

    The infix notation /\ is syntactic sugar for and A B, where and : Prop -> Prop -> Prop.

Disjunction

  • Definition

    The disjunction, or logical or, of two propositions: A \/ B is true when either A or B is.

  • Using disjunction (destruct or intros tactic)

    You can proceed with case analysis using destruct, spliting a disjunction into two goals.

    You can implicitly do case analysis via intros, by using a pattern like =Hn | Hm=, which splits a conjunction A \/ B such that A is equivalent to Hn and B to Hm.

    **

  • How to Prove (left or right tactics)

    Simply show that one of the disjunction's sides holds via the tactics left or right.

Falsehood and Negation

  • Definition

    Logical negation operator is written as ~, where ~P is equivalent to P -> False. An alternate definition is ~P being equivalent to forall Q, P -> Q (principle of explosion, or ex-falso-quodlibet).

  • Falsehood

    Since False is a contradictory proposition, the principle of explosion applies to it.

    If we can get False into the context, we can use destruct on it to complete any goal.

  • Inequality (<>)

    The notation a <> b is equivalent to ~(a = b).

    To prove an equality, assume the opposite equality a = b and then deduce False (a contradiction).

  • Tips

    You can apply ex_falso_quodlibet or contradiction or exfalso to nonsensical goals like false = true.

    You can unfold ~ or not to see the negation clearer.

Truth

  • Definition

    True is a proposition that is trivially true.

    Unlike False, True is used rarely, as it is uninteresting and trivial as a goal. however, it can be used when defining complex Prop s.

  • Proving True (apply I)

    The constant I : True proves True. Simply apply it: apply I.

Logical Equivalence

  • Definition

    The "if and only if" connective asserts that two propositions have the same truth value.

    It is the conjunction of two implications. 

    Definition iff (P Q : Prop) := (P -> Q) /\ (Q -> P).

Notation "P <-> Q" := (iff P Q)
  • Tips

    We can use apply with <-> in either direction, rather than having to destruct the conjunction underneath.

Setoids

We need the setoid library to let some tactics - namely, rewrite and reflexivity - behave with iff statements. 

From Coq Require Import Setoids.Setoid.

A setoid is a set equipped with an equivalence relation.

When elements in the setoid are equivalent, rewrite can be used to replace elements in the setoid.

Existential Quantification

  • Definition

    Existential quantification is another basic connective.

    To say that there is some x of type T such that some property P holds of x, we write exists x : T, P.

  • How to prove: Witnesses (exists tactic)

    To prove a statement of the form exists x, P, we must show that P holds for some specific choice for x, known as the witness of the existential.

    This is done in two steps:

    First, we explicitly tell Coq which witness t we have in mind by invoking the tactic exists t.

    Then we prove that P holds after all occurrences of x are replaced by t.

  • How to use: (destruct tactic)

    If we have an existential hypothesis exists x, P in the context, we can destruct it to obtain a witness x and a hypothesis stating that P holds of x.

2.2. Programming with Propositions

This section talked about recursive propositions. They are still subject to the termination checker.

The next section IndProp.v will talk about inductive propositions - a different technique with its own strengths and limitations.

Example: 

Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | nil => False
  | x' :: l' => x' = x \/ In x l'
  end.

2.3. Applying Theorems to Arguments

Coq is distinguished from ACL2 and Isabelle in that it treats proofs as first class objects.

More about that is discussed in the chapters ProofObjects and IndPrinciples.

This is the type of a theorem: 

Check add_comm        : forall n m : nat, n + m = m + n.
Check plus_id_example : forall n m : nat, n = m -> n + n = m + m.

Here, add_comm refers to a proof object with the statement of the proposition being it type (See: CHC isomorphism: propositions are types).

We are able to apply theorems directly to arguments we want to instantiate it with.

Example: 

Lemma add_comm3_take3 :
  forall x y z, x + (y + z) = (z + y) + x.
Proof.
  intros x y z.
  rewrite add_comm.
  rewrite (add_comm y z).
  reflexivity.
Qed.

Tips

Other ways to apply theorems:

apply ... with ... (use a theorem with a particular argument), apply ... in ... (apply a theorem into something in the context).

You can also let the values of the other parameters be inferred by using _ placeholders when applying the theorem/lemma.

2.4. Working with Decidable Properties

Elements that are typed bool are decidable, usable with match, but does not work with the rewrite tactic.

The type Prop includes both decidable and undecidable propositions.

We can choose to represent a property using a boolean computation or a function into Prop.

You cannot test whether a Prop is true or not (= expects a bool).

There are nuanced reasons why we would use Prop or Bool over the other.

bool allows for proof by reflection.

2.5. The Logic of Coq

Coq's logical core is called the _Calculus of Inductive Constructions. It differs from Zermelo-Fraenkel Set Theory (ZFC).

Functional extensionality

Two functions f and g are equal if they produce the same output on every input.

Informally, an "extensional property" is one that pertains to an object's observable behavior. Thus, functional extensionality simply means that a function's identity is completely determined by what we can observe from it – i.e., the results we obtain after applying it.

Function intensionality considers whether two objects are equal based on their internal definitions.

Functional extensionality, however, is not built part of Coq's built-in logic.

However, if we like, we can add functional extensionality to Coq using the Axiom command. 

Axiom functional_extensionality : forall {X Y: Type}
                                    {f g : X -> Y},
  (forall (x:X), f x = g x) -> f = g.

We need to be careful when adding new axioms, as it could render Coq inconsistent.

However, it is known that adding functional extensionality is consistent.

To check whether a particular proof relies on any additional axioms, use the Print Assumptions command.

Classical vs constructive logic

The law of excluded middle does not hold in Coq, as Coq's logic is constructive. 

Definition excluded_middle := forall P : Prop,
  P \/ ~ P.

More conventional logical systems such as ZFC, in which the excluded middle does hold for arbitrary propositions, are referred to as classical.

A restricted form of excluded middle does work in constructive logics, if working with decidable propositions, like propositions on nat. 

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

As useful as constructive logic is, it does have its limitations: There are many statements that can easily be proven in classical logic but that have only much more complicated constructive proofs, and there are some that are known to have no constructive proof at all! (Which?)

Fortunately,like functional extensionality, the excluded middle is known to be compatible with Coq's logic, allowing us to add it safely as an axiom. However, we will not need to do so here: the results that we cover can be developed entirely within constructive logic at negligible extra cost.

3. Exercises

3.1. plus_is_O

2 stars, standard

3.2. proj2

1 star, standard, optional

3.3. and_assoc

1 star, standard

3.4. mult_is_O

2 stars, standard

3.5. or_commut

1 star, standard

3.6. not_implies_our_not

2 stars, standard, optional

3.7. double_neg_informal

2 stars, advanced

3.8. contrapositive

1 star, standard, especially useful

3.9. not_both_true_and_false

1 star, standard

3.10. not_PNP_informal

1 star, advanced

3.11. de_morgan_not_or

2 stars, standard

3.12. not_S_inverse_pred

1 star, standard, optional

3.13. nil_is_not_cons

2 stars, advanced, optional

3.14. iff_properties

1 star, standard, optional

3.15. or_distributes_over_and

3 stars, standard

3.16. dist_not_exists

1 star, standard, especially useful

3.17. dist_exists_or

2 stars, standard

3.18. leb_plus_exists

3 stars, standard, optional

3.19. In_map_iff

2 stars, standard

3.20. In_app_iff

2 stars, standard

3.21. All

3 stars, standard, especially useful

3.22. combine_odd_even

2 stars, standard, optional

3.23. even_double_conv

3 stars, standard

3.24. logical_connectives

2 stars, standard

3.25. eqb_neq

1 star, standard

3.26. eqb_list

3 stars, standard

3.27. All_forallb

2 stars, standard, especially useful

3.28. TODO tr_rev_correct

4 stars, standard

3.29. TODO excluded_middle_irrefutable

3 stars, standard

3.30. TODO not_exists_dist

3 stars, advanced

3.31. TODO classical_axioms

5 stars, standard, optional

Total: 64

4. Scores

49/64

Did not do: tr_rev_correct, excluded_middle_irrefutable, not_exist_dist, and classical_axioms. There are several ungraded problems too, that I counted as graded.

Run coqc -Q . LF LogicTest.v in the lf directory for more information.

5. Questions

5.1. TODO Classical proofs that do not have constructive equivalents

As useful as constructive logic is, it does have its limitations: There are many statements that can easily be proven in classical logic but that have only much more complicated constructive proofs, and there are some that are known to have no constructive proof at all!

Which proofs do not have constructive proofs?

Does this mean constructive logic is weaker than classical?

6. Metacognition

The exercises were quite substantial this time. I think this lesson is very useful - we are finally going into the territory of logic and proof theory. In particular, how falsehood and negation works is important, as it opens up proofs by contradiction, and using ex-falso-quodlibet. Other important lessons: existential quantification.

7. Further Knowledge

N/A.

8. TODOs

8.1. Finish the rest of the exercises.

The exercises are very interesting - but difficult. We will come back to them.

Back to Top

Author: selffins

Created: 2025-04-03 Thu 23:01

Validate