Intro to ITPs, Part 3

As noted before, logical negation is defined in terms of False, and notation is provided as ~A for not A.

That is, ~P holds if P -> False. This is a constructive view of negation: the negation of P is true if, from P, you can construct a proof of False. It is also why we end up using False a lot in proofs, even while we rarely use True, since whenever we are reasoning about negation, we end up reasoning about False.

One obvious consequence of this is that the statement and P (not P) is nonsense: a statement can never be both true and false. If we unfold the definition of not, we see that what that statement is saying is that P -> False and P. Thus, we can project out the P -> False function and the P, and apply the first to the second and get a proof of False.

Parameter P : Prop.
Theorem F : (and P (not P)) -> False.
Proof.
  exact (fun andpnotp => (proj2 andpnotp) (proj1 andpnotp)).
Qed.

Now that we have a proof of False (a term that has type False), we truly are in an impossible situation, as if you recall, there are no terms of type False. It is defined as an inductive type with no constructors:

Inductive False : Prop :=   .

As a result, there is an elimination rule (a rule for using the term) that says, if we have a proof of False, we can conclude anything.

Check False_ind. -- forall P : Prop, False -> P

For example, if we wanted to prove the statement 1 = 2 (which is a valid statement, but not provable), and we knew and P (not P), we could do that as follows:

Theorem T1 : (and P (not P)) -> 1 = 2.
Proof.
  exact (fun andpnotp => False_ind _ ((proj2 andpnotp) (proj1 andpnotp))).
Qed.

i.e., we first pull out the two components of the conjunction, applying the second to the first, which gives us a term of type False. We can then use False_ind, which takes a property and something of type False and returns something of the type of that property (i.e., a proof)! In particular, it will produce a proof of 1 = 2 in this case. Note one special detail: rather than actually writing down the type of the property (i.e., False_ind (1 = 2) ...) we used an underscore. This can be done in many positions, as an indication that we would like Rocq to infer it (if it can).

Tactics

Up to now, we've mostly been writing proofs as explicit terms, but that is something that is actually done quite rarely. It turns out, rather than constructing the terms directly, which for complicated proofs, might be rather involved, we can instead invoke higher-level tactics that will construct a term for us. This is the incredibly important legacy of Milner's LCF.

For the rest of this lecture, we're going to focus primarily on the "Goals" panel, and how it, along with tactics, allow us to much more easily, and interactively, construct proofs.

By default, whenever we start a Proof, we switch to tactic mode. Indeed, we've been using a tactic in all our proofs: exact, which takes a complete term that satisfies the type of the goal. But now we'll see more interactive, step-by-step tactics.

On their own, tactics can make our code harder to read, as they allow you to leave out details apparent in the terms, but the interactive nature of the "Goals" provides interactive feedback that results in a really nice environment for constructing proofs. The most basic tactic (beyond exact!) is `reflexivity}, which performs evaluation on both sides, and then solves trivial equalities: equalities that are the exact same on both sides.

Tactic Use	Tactic Description
reflexivity	If the goal is an equality, complete the proof if the two sides are either the same, or can be made the same by evaluation.

Let's see how this works:

Lemma L1 : 1 + 1 = 2.
Proof.
  reflexivity.
Qed.

Lemma is a synonym for Theorem that you can use to hint that these are smaller results. It has to internal significance to Rocq.

To learn more about tactics, let's see a slightly more involved example, returning to our simple theorem about and:

Theorem and_2'' : forall {P  Q : Prop}, P /\ Q -> Q.
Proof.
  intros P Q pq.
  destruct pq as [p q].
  exact q.
Qed.

Here, we use three tactics. The first, intros, takes identifiers from the goal and moves them into the premise of the proof. This corresponds, in the underlying term, to creating a function. Here we give explicit names to the propositions P and Q, and name the proof of P /\ Q as pq.

The Goals panel will always show information about the current goal and how many remain (none if the proof is complete), and each goal will have assumptions or premises (or hypotheses) that are available to use in the proof of that goal. The assumptions are separate from the obligation with a horizontal line, and the goal is the proposition that we are trying to prove.

Tactic Use	Tactic Description
intros id1 id2 ... or intro id1	intro id1 adds new hypothesis id1 : P1, id2 : P2, etc to premises, assuming goal is of the form P1 -> P2 -> P or ∀ x : P1, y : P2, P The new goal will now be P Note that if id is _, then Rocq will generate a name for it.

We then do case analysis on one of my hypotheses: which one? The one called pq. Case analysis is done with destruct, and on a pair will produce two new hypotheses for the two conjuncts. In this case, we matched the two produced hypotheses to the names p q; if we had left out the as [p q] part, then Rocq would choose names for our two hypotheses, which can make proofs harder to read.

Note that it does not manipulate the goal in this case, but simply changes the form of the hypotheses. If we did case analysis on a disjunction (also known as a sum), we would get multiple goals, as there would be multiple different cases to consider. Case analysis in tactics corresponds to pattern matching in the underlying terms, though the Goal state can make it a bit easier to manage.

Tactic Use	Tactic Description
destruct id	if id is a hypothesis of some inductive type, perform case analysis on it, either constructing multiple hypotheses (if it is a product type) or multiple goals (if it is a sum type).
destruct id as [v1 v2...]	like destruct, but gives explicit names to produced names in case there is only a single case. More complicated patterns can handle disjuncts.

At this point, we can complete the proof with the term q, since it has the type Q which is our goal. We do this using the tactic exact. This is a tactic that takes a term, and if it matches the goal, it completes the proof.

Tactic Use	Tactic Description
exact term	if term is a term of the same type as the goal, then this tactic completes the proof.

There are many other ways we could write this. First, we could use the tactic assumption to complete the proof: it looks for a hypothesis that matches the goal.

Theorem and_2'' : forall {P  Q : Prop}, P /\ Q -> Q.
Proof.
  intros P Q pq.
  destruct pq as [p q].
  assumption.
Qed.

Tactic Use	Tactic Description
assumption	if there is some hypothesis that has the same type as the goal, then this tactic completes the proof by using that hypothesis.

Since we no longer need to refer to q by name, we now can allow Rocq to determine the names when we use destruct:

Theorem and_2'' : forall {P  Q : Prop}, P /\ Q -> Q.
Proof.
  intros P Q pq.
  destruct pq.
  assumption.
Qed.

De Morgan's Law

Let's prove a basic theorem in propositional logic:

\(\neg (P \lor Q) \equiv \neg P \land \neg Q\)

Here we've written \(\equiv\) as "if-and-only-if" double implication, rather than propositional equality, which is more natural in Rocq, since Prop cannot be computed (and thus typical equality does not work).

Theorem demorgan1 : forall P Q : Prop, ~(P \/ Q) <-> ~P /\ ~Q.
Proof.
     intros P Q.
     constructor.
     - intro mp.
       constructor.
       * intro p.
         apply mp.
         apply or_introl.
         assumption.
       * intro q.
         apply mp.
         apply or_intror.
         assumption.
     - intro mpr.
       intro pq.
       destruct mpr as [mp mq].
       destruct pq as [p | q].
       * apply mp. assumption.
       * apply mq. assumption.
Qed.

Here we used two new tactics:

Tactic Use	Tactic Description
constructor	if the goal is an inductive type, try applying its constructors to see if any match.
apply H	H must be a hypothesis or theorem with type P1 -> P2 -> ... -> PN -> Q, where the goal has type Q. This tactic will replace the goal with N separate goals, P1, through PN, as it corresponds to deciding to prove the premises of H and then using it to prove the goal. In the simply case where you just have P -> Q this will replace Q with P

Interestingly, the other proof that you did:

\(\neg (P \land Q) \equiv \neg P \lor \neg Q\)

cannot be done in the core logic of Rocq. The issue is that it is not constructive; it can be done if we add classical axioms.

Stepping back: proofs here vs. proofs with truth tables

Now that we've seen a few proofs, including doing a proof that you did in propositional logic, it's important to understand the difference between proofs in Rocq and proofs in propositional logic.

In propositional logic, all variables can be either true or false, and thus any formula can be computed via a finite truth table. In a higher order logic like Rocq, propositional variables are not either true or false, but rather, they are either provable or not provable. For a statement to be provable, it means that we have constructed a proof term with that type, but that type may involve data of arbitrary size, and thus the truth or falseness of a given statement cannot be determined by a finite truth table.

While the proof we just did of one of De Morgan's laws is syntactically the same as the classical approach, it is a much more powerful proof, as it holds for any provable propositions, not just for T/F propositional variables. Another way to think about this is that Rocq has propositional logic embedded, by way of the boolean data type. The classical proof would be the following:

Theorem demorganprop :
  forall P Q : bool, negb (orb P Q) = andb (negb P) (negb Q).
Proof.
  intros P Q.
  destruct P; destruct Q; try reflexivity.
Qed.

Here we can see a new tactic (or, technically, a "tactical", since it operates on other tactics): ;, which is used to chain tactics together by applying what follows to everything that comes out of the former. Here we can see that by doing case analysis on the two boolean inputs, we can complete the proof trivially, as once we have constants, simply evaluating the expression will give us the result.

Tactic Use	Tactic Description
tactic1 ; tactic2	Apply tactic1 to the current goal, and then apply tactic2 to all goals that are generated by the result of tactic1 (0, 1, or more).

Attempting to do that for the other proof will fail, as we cannot do case analysis on Prop: it is not an inductive type with a finite number of constructors.

Full code

Parameter P : Prop.
Check not P.
Check ~ P.
Check not.
Check P -> False.
Print Scopes.

(* 
Theorem F : (and P (~ P)) 
                   (* P , (P -> False) *))
 *)

Theorem F : (and P (~ P)) -> False.
Proof.
  exact (fun pandnp => (proj2 pandnp) (proj1 pandnp)).
Qed.

Theorem F' : (and P (~ P)) -> False.
  Proof.
    intro.
    exact ((proj2 H) (proj1 H)).
Qed.

(* Inductive False : Prop := . *)
Check False_ind. 

Theorem T1 : (and P (~ P)) -> 1 = 2.
Proof.
  intro H.
  Check (proj2 H) (proj1 H).
  Check False_ind.
  Check False_ind (1 = 2).
  exact (False_ind _ ((proj2 H) (proj1 H))).
  Qed.

(*********************************************************)

Lemma L1 : 1 + 1 = 2.
Proof.
  Eval simpl in (1 + 1).
  Eval cbv in (1 + 1).
  simpl. (* we don't write this *)
  reflexivity.
Qed.

Lemma and2' : forall (P Q : Prop), P /\ Q -> Q.
(* Lemma and2'' : forall {P Q : Prop}, P /\ Q -> Q. *)
Proof.
  intros P Q pq.
  destruct pq as [p q].
  exact q.
Qed.

Lemma and2'' : forall {P Q : Prop}, P /\ Q -> Q.
(* Lemma and2'' : forall {P Q : Prop}, P /\ Q -> Q. *)
Proof.
  intros P Q pq.
  destruct pq. (* case analysis, corresponds to pattern matching! *)
  exact H0.
Qed.

Lemma or2''' : forall {P Q : Prop}, P \/ Q -> Q.
(* Lemma and2'' : forall {P Q : Prop}, P /\ Q -> Q. *)
Proof.
  intros P Q pq.
  destruct pq. (* case analysis, corresponds to pattern matching! *)
  admit.
  exact H.
Admitted.

Theorem and_2''' : forall (P  Q : Prop), P /\ Q -> Q.
Proof.
  intros P Q pq.
  destruct pq (* as [p q] *).
  assumption.
Qed.

Theorem demorgan : forall P Q : Prop, ~ ( P \/ Q ) <-> ~ P /\ ~Q.
Proof.
  intros P Q.
  constructor. (* split. *)
  - intro npq.
    constructor.
    * intro p.
      apply npq.
      apply or_introl. (* P \/ Q -> P *)
      assumption.
    * intro q.
      apply npq. 
      apply or_intror.
      exact q.
  - intro npq.
    intro p_q.
    destruct npq as [np nq]. 
    destruct p_q as [p | q]. 
    * apply np. assumption.
    * apply nq. assumption.
Qed.

Theorem demorgan_prop :
  forall P Q : bool, negb (orb P Q) = andb (negb P) (negb Q).
Proof.
  intros P Q.
  destruct P.
  - destruct Q.
    * simpl. reflexivity.
    * simpl. reflexivity.
  - destruct Q.
    * simpl. reflexivity.
    * simpl. reflexivity.
Qed.

Theorem demorgan_prop' :
  forall P Q : bool, negb (orb P Q) = andb (negb P) (negb Q).
Proof.
  intros P Q.
  destruct P.
  - destruct Q; simpl.
    * reflexivity.
    * reflexivity.
  - destruct Q; simpl.
    * reflexivity.
    * reflexivity.
Qed.

Theorem demorgan_prop'' :
  forall P Q : bool, negb (orb P Q) = andb (negb P) (negb Q).
Proof.
  intros P Q.
  destruct P.
  - destruct Q; simpl; reflexivity.
  - destruct Q; simpl; reflexivity.
Qed.


Theorem demorgan_prop''' :
  forall P Q : bool, negb (orb P Q) = andb (negb P) (negb Q).
Proof.
  intros P Q.
  destruct P; destruct Q; simpl; reflexivity.
Qed.



Theorem demorgan_prop'''' :
  forall P Q : bool, negb (orb P Q) = andb (negb P) (negb Q).
Proof.
  intros.
  destruct P0; destruct Q; simpl; reflexivity.
Qed.