16 Logic in Rocq🔗

Borrowed from https://www.cs.cornell.edu/courses/cs3110/2018sp/l/20-coq-logic/notes.html

16.1 Propositions and proofs🔗

Recall that the Check command type checks an expression and causes Rocq to output the type in the output window.

Check list.

Think of Rocq’s list as a type-level function: it is a function that takes types as inputs and produces types as outputs. OCaml doesn’t have anything exactly equivalent to that.

Rocq responds:

obvious_fact : 1 + 1 = 2

So the type of obvious_fact is 1 + 1 = 2. That might seem rather mysterious. After all, 1 + 1 = 2 is definitely not an OCaml type. But Rocq’s type system is far richer than OCaml’s. In OCaml, we could think of 42 : int as meaning that 42 is a meaningful expression of type int. There are likewise meaningless expressions—for example, 42+true is meaningless in OCaml, and it therefore cannot be given a type. The meaning of int in OCaml is that of a computation producing a value that fits within 2^63 bits and can be interpreted as an element of Z, the mathematical set of integers.

Regardless of the exact proof, it is an argument for, or evidence for, the assertion that 1 + 1 = 2. So when we say that obvious_fact : 1 + 1 = 2, what we’re really saying is that obvious_fact is a proof of 1 + 1 = 2.

Likewise, when we write Definition x := 42. in Rocq, and then observe that [x : nat], what we’re saying is not just that x has type nat, but also that there is evidence for the type nat, i.e., that there do exist values of that type. Many of them, in fact—just like there are many proofs of 1 + 1 = 2.

So now we have an explanation for what the type of obvious_fact is. But what is its value? Let’s ask Rocq.

Print obvious_fact.

Rocq responds:

obvious_fact = eq_refl : 1 + 1 = 2

Print eq_refl.

Amidst all the output that produces, you will spy

eq_refl : x = x 

So the proof of 1 + 1 = 2 in Rocq is really just that equality is reflexive. It turns out that Rocq evaluates expressions before applying that fact, so it evaluates 1+1 to 2, resulting in 2 = 2, which holds by reflexivity. Thus the proof we found above, using the trivial tactic, corresponds to the first of the two possible proofs we sketched.

16.2 Prop and Set🔗

We’ve now seen that there are programs and proofs in Rocq. Let’s investigate their types. We already know that 42, a program, has type nat, and that eq_refl : 1 + 1 = 2. But let’s now investigate what the types of nat and 1 + 1 = 2 are. First, nat:

Check nat.

Rocq says that nat : Set. Here, Set is a predefined keyword in Rocq that we can think of as meaning all program data types. Further, we can ask what the type of Set is:

Check Set.

Next, let’s investigate what the type of 1 + 1 = 2 is.

Check 1 + 1 = 2.

Rocq says that 1 + 1 = 2 : Prop. This is the type of propositions, which are logical formulas that we can attempt to prove. Note that propositions are not necessarily provable though. For example, 330 = 433 has type Prop, even though it obviously does not hold. What is the type of Prop?

Check Prop.

Rocq says that Prop : Type. So Prop is also a type. So far we have seen one way of creating a proposition, by using the equality operator. We could attempt to learn more about that operator with Check =., but that will result in an error: Check doesn’t work on this kind of notation, and there isn’t something like in OCaml where we can wrap an operator in parentheses. Instead, we need to find out what function name that operator corresponds to. The command for that is Locate.

Locate "=".

Rocq tells us two possible meanings for =, and the second is what we want:

"x = y" := eq x y

That means that anywhere x = y appears, Rocq understands it as the function eq applied to x and y. Now that we know the name of that function, we can check it:

Check eq.

The output of that is a bit mysterious because of the ?A that shows up in it. What’s going on is that eq has an implicit type argument. (Implicit arguments were discussed in the previous set of notes.) If we prefix eq with @ to treat the argument as explicit, we can get more readable output.

Check @eq

Rocq says that

 @eq : forall A : Type, A -> A -> Prop

16.3 Propositional logic🔗

All of these are ways of creating propositions in Rocq. Implication is so primitive that it’s simply "baked in" to Rocq. But the other connectives are defined as part of Rocq’s standard library under the very natural names of and, or, and not.

In addition to those connectives, there are two propositions True and False which always and never hold, respectively. And we can have variables representing propositions. Idiomatically, we usually choose names like P, Q, R, ... for those variables.

Check and.
Check or.
Check not.

and : Prop -> Prop -> Prop
or  : Prop -> Prop -> Prop
not : Prop -> Prop

There is a uniform way to think about both uses of ->, which is as a transformer. A function of type t1 -> t2 transforms a value of type t1 into a value of type t2. An implication P -> Q in a way transforms P into Q: if P holds, then Q also holds; or better yet, a proof of P -> Q can be thought of as a function that transforms evidence for P into evidence for Q.

Let’s do some proofs with these connectives to get a better sense of how they work.

16.4 Implication🔗

That proposition says that for any proposition P, it holds that P implies P.

Intuitively, why should be able able to prove this proposition? That is, what is an argument you could give to another human? We always encourage you to try to answer that question before launching into a Rocq proof—for the same reason your introductory programming instructor always encouraged you to think about programs before you begin typing them.

So why does this proposition hold? It’s rather trivial, really. If P holds, then certainly P holds. That is, P implies itself. An example in English could be "if 433 is fun, then 433 is fun." If you’ve already assumed P, then necessarily P follows from your assumptions: that’s what it means to be an assumption.

The Rocq proof below uses that reasoning.

Let’s look at the type of p_implies_p.

Check p_implies_p.

Rocq says p_implies_p : forall P : Prop, P -> P. So p_implies_p is proof of, or evidence for, forall P : Prop, P -> P, as we discussed above. What is that evidence? We can use [Print] to find out:

Print p_implies_p.

Rocq responds

p_implies_p = 
fun (P : Prop) (P_assumed : P) => P_assumed
     : forall P : Prop, P -> P

Note that the names of the arguments to that function are the names that we chose with the intros tactic.

Let’s clarify a subtle piece of terminology, "proof". The proof of forall P:Prop, P -> P is the anonymous function fun (P : Prop) (P_assumed : P) => P_assumed. That is, the proof of a proposition P is a program that has type P. On the other hand, the commands we used above

Proof.
    intros P. 
    intros P_assumed. 
    assumption.
Qed.

The first assumption in that proof, "all humans are mortal", is an implication: if X is a human, then X is mortal. The second assumption is that Socrates is a human. Putting those two assumptions together, we conclude that Socrates is mortal.

The Rocq proof below uses that style of argument.

Proof.
  intros P Q evPimpQ evP.
  apply evPimpQ. 
  assumption.
Qed.

The first line of the proof, intros P Q evPimpQ evP introduces four assumptions. The first two are the variables P and Q. The third is P->Q, which we give the name evPimpQ as a human-readable hint that it is evidence that P implies Q. The fourth is P, which we give the name evP as a hint that we have assumed we have evidence for P.

The second line of the proof, apply evPimpQ, uses a new tactic apply to apply the evidence that P -> Q to the goal of the proof, which is Q. This transforms the goal to be P. Think of this as backward reasoning: we know we want to show Q, and since we have evidence that P -> Q, we can work backward to conclude that if we could only show P, then we’d be done.

The third line concludes by pointing out to Rocq that in fact we do already have evidence for P as an assumption.

Let’s look at the proof that these tactics cause Rocq to create:

Print syllogism.

We see that

syllogism = 
fun (P Q : Prop) (evPimpQ : P -> Q) (evP : P) => evPimpQ evP
     : forall P Q : Prop, (P -> Q) -> P -> Q

The deep point here is: all of these are really the same interpretation. There’s no difference between them. The value evPimpQ is a function, and it is evidence, and it is an evidence transformer.

We can see that evPimpQ is being used as a function in the body evPimpQ evP of the anonymous function, above. It is applied to evP, which is the evidence for P, thus producing evidence for Q. So "apply" really is a great name for the tactic: it causes a function application to occur in the proof.

Proof.
  intros P Q R evPimpQ evQimpR.
  intros evP.
  apply evQimpR.
  apply evPimpQ.
  assumption.
Qed.

The second line, intros evP, wouldn’t actually need to be separated from the first line; we could have introduced evP along with the rest. We did it separately just so that we could see that it peels off the P from P -> R.

The third line, apply evQimpR applies the evidence that Q -> R to the goal R, causing the goal to become Q. Again, this is backward reasoning: we want to show R, and we know that Q -> R, so if we could just show Q we’d be done.

The fourth line, apply evPimpQ, applies the evidence that P -> Q to the goal Q, causing the goal to become P.

Finally, the fifth line, assumption, finishes the proof by pointing out that P is already an assumption.

Let’s look at the resulting proof:

Print imp_trans.

Rocq says

imp_trans = 
fun (P Q R : Prop) (evPimpQ : P -> Q) (evQimpR : Q -> R) (evP : P) =>
evQimpR (evPimpQ evP)
     : forall P Q R : Prop, (P -> Q) -> (Q -> R) -> P -> R

16.5 Conjunction🔗

Having established that intuition, let’s create a proof with Rocq.

Proof. 
    intros P Q PandQ.
    destruct PandQ as [P_holds Q_holds]. 
    assumption.
Qed.

After destructing the evidence for PandQ into evidence for P and evidence for Q, we can easily finish the proof with assumption.

Let’s look at the proof of and_fst.

Print and_fst.

Let’s dissect that. We see that and_fst is a function that takes three arguments. The third is evidence for P /\ Q. The function then pattern matches against that evidence, providing just a single branch in the pattern match. The pattern it uses is conj P_holds _. As in OCaml, _ is a wildcard that matches anything. The identifier conj is a constructor; unlike OCaml, it’s fine for constructors to begin with lowercase characters. So the pattern matches against conj applied to two values, extracts the first value with the name P_holds, and doesn’t give a name to the second value. The branch then returns that argument P_holds. So we can already see that the function is splitting apart the evidence into two pieces, and forgetting about one piece.

Print and.

It might help to compare to lists.

Print list.

Rocq says

Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A

In Rocq, Inductive defines a so-called inductive type, and provides its constructors. In OCaml, the type keyword serves a similar purpose. So list in Rocq is a type with two constructors named nil and cons. Similarly, and is a type with a single constructor named conj, which is a function that takes in a value of type A, a value of type B, and returns a value of type A /\ B, which is just infix notation for and A B. Another way of putting that is that conj takes in evidence of A, evidence of B, and returns evidence of and A B.

So there’s only one way of producing evidence of A /\ B, which is to separately produce evidence of A and of B, both of which are passed into conj. That’s why when we destructed A /\ B, it had to produce both evidence of A and of B.

Given all that, the following theorem and its program should be unsurprising.

Rocq

Theorem and_snd : forall P Q : Prop,
  P /\ Q -> Q.
Proof.
  intros P Q PandQ.
  destruct PandQ as [P_holds Q_holds].
  assumption.
Qed.

Print and_snd.

In that program the pattern match returns the second piece of evidence, which shows Q holds, rather than the first, which would show that P holds.

Proof. 
  split. 
  trivial. trivial.
Qed.

The first line of that proof, split, is a new tactic. It splits a goal of the form P /\ Q into two separate subgoals, one for P, and another for Q. Both must be proved individually. In the proof above, trivial suffices to prove them, because they are both trivial equalitiies.

What is and_ex?

Print and_ex.

So and_ex is conj applied to eq_refl as its first argument and eq_refl as its second argument.

Proof.
    intros P Q PandQ. 
    destruct PandQ as [P_holds Q_holds]. 
    split. 
    all: assumption.
Qed.

There’s nothing new in that proof: we split the evidence into two pieces using pattern matching, then reassemble them in a different order. We can see that in the program:

Print and_comm.

Note how the pattern match binds two variables, then returns the conj constructor applied to those variables in the opposite order.

Proof.
  intros P Q R evPandQimpR evP evQ.
  apply evPandQimpR.
  split.
  all: assumption.
Qed.

That program matches against evidence for P /\ Q, then swaps the order of evidence around, thus producing evidence for Q /\ P.

16.6 Disjunction🔗

As always, what’s the intuition? Well, if we have evidence for P, then we have evidence for P \/ Q, because we have evidence already for the left-hand side of that connective.

Let’s formalize that argument in Rocq.

Proof.
    intros P Q P_holds. 
    left. 
    assumption.
Qed.

The second line of that proof, left, uses a new tactic that tells Rocq we want to prove the left-hand side of a disjunction. Specifically, the goal at that point is P \/ Q, and left tells Rocq the throw out Q and just focus on proving P. That’s easy, because P is already an assumption.

Let’s investigate the resulting program.

Print or_left.

Those constructors take evidence for either the left-hand side or right-hand side of the disjuncation. So the body of or_left is just taking evidence for A and using or_introl to construct a value with that evidence.

In other words, the theorem is proved by applying the or_introl constructor to eq_refl. It matters, though, that we provided Rocq with the guidance to prove the left-hand side. If we had chosen the right-hand side, we would have been stuck trying to prove that 330 = 433, which of course it does not.

Next, let’s prove that disjunction is commutative, as we did for conjunction above.

In the second line of that proof, we destruct the disjunction PorQ with a slightly different syntax than when we destructed conjunction above. There’s now a vertical bar. The reason for that has to do with the definitions of and and or.

After the destruction occurs, we get two new subgoals to prove, corresponding to whether PorQ matched or_introl or or_intror. In the third line of the proof, which corresponds to PorQ matching or_introl, we have evidence for P, so we choose to prove the right side of Q \/ P by assumption. The fourth line does a similar thing, but using evidence for Q hence proving the left side of Q \/ P.

Let’s look at the resulting proof.

Print or_comm.

That function takes an argument PorQ is evidence for P \/ Q, pattern matches against that argument, extracts the evidence for either P or Q, then returns that evidence wrapped in the "opposite" constructor: evidence that came in in the left constructor is returned with the right constructor, and vice versa.

Next, let’s prove a theorem involving both conjunction and disjunction.

We used nested bullets in that proof to keep the structure of the proof clear to the reader, and to make it easier to follow the proof in the proof window when we step through it.

The nested pattern match in that proof corresponds to the nested destruct above. Note that Rocq omits some parentheses around conjunction, because it is defined to have higher precedence than disjunction—just like * has higher precedence than +.

16.7 False and True🔗

False is the proposition that can never hold: we can never actually have evidence for it. If we did somehow have evidence for False, our entire system of reasoning would be broken. There’s a Latin phrase often used for that idea: ex falso quodlibet, meaning "from false, anything". In English it’s sometimes known as the _Principle of Explosion_: if you’re able to show False, then everything just explodes, and in fact anything at all becomes provable.

Here’s the definition of PFalse:

Print False.

Rocq responds

Inductive False : Prop :=  

No, that isn’t a typo above. There is nothing on the right-hand side of the :=. The definition is saying that False is an inductive type, like and and or, but it has zero constructors. Since it has no constructors, we can never create a value of type False—and that means we can never create evidence that False holds.

The second line of the proof uses a new tactic, contradiction. This tactic looks for any contradictions or assumptions of False, and uses those to conclude the proof. In this case, it immediately finds False as an assumption named false_holds.

The proof that Rocq finds for explosion given the above tactics is a little bit hard to follow because it uses two functions False_ind and False_rect that are already defined for us. Their definitions are given below, but it’s okay if you want to skip over reading them at first.

Rocq

explosion =
fun (P : Prop) (false_holds : False) => False_ind P false_holds
     : forall P : Prop, False -> P

False_ind = fun P : Prop => False_rect P
     : forall P : Prop, False -> P

False_rect =
fun (P : Type) (f : False) => match f return P with
                              end
     : forall P : Type, False -> P

(The return P in the pattern match above is a type annotation: it says that the return type of the entire match expression is P.)

Note that False_ind just calls False_rect, and False_rect immediately does a pattern match. So we could simplify the proof of explosion by just directly writing that pattern match ourselves. Let’s do that using the Definition command we saw above.

Rocq

Definition explosion' : forall (P:Prop), False -> P :=
  fun (P : Prop) (f : False) =>
    match f with
    end.

The proof of explosion’ is a function that takes two inputs, a proposition P and a value f of type False. As usual, we should understand that second argument as being evidence for False. But it should be impossible to construct such evidence! And indeed it is, because False has no constructors. So we have a function that we could never actually apply.

In the body of that function is a pattern match against f. That pattern match has zero branches in it, exactly because False has zero constructors. There is nothing that could ever possibly match f.

The return type of the function is P, meaning it purportedly is evidence for P. But of course no such evidence is ever constructed by the function, nor coud it be. So it’s a good thing that it’s impossible to apply the function. Were it possible, it would have to fabricate evidence for any proposition P whatsoever—which is not possible.

True is the proposition that is always true, i.e., for which we can always provide. It is defined by Rocq as an inductive type:

Print True.

Rocq responds:

Inductive True : Prop :=  I : True

16.8 Negation🔗

The negation connective can be the trickiest to work with in Rocq. Let’s start by seeing how it is defined.

Locate "~".
Print not.

Rocq responds

not = fun A : Prop => A -> False
     : Prop -> Prop

Unlike conjunction and disjunction, negation is defined as a function, rather than an inductive type. Anywhere we write ~P, it really means not P, which is (fun A => A -> False) P, which reduces to P -> False. In short, ~P is effectively syntactic sugar for P -> False.

The first line of that proof, unfold not, is a new tactic, which replaces the ~ in the goal with its definition and simplifies it. So ~False becomes False -> False. The second line uses a familiar tactic in a new way. We don’t provide any names to intros, which causes Rocq to choose its own names. Normally we consider it good style to choose them ourselves, but here, we don’t care what they are, because we are never going to use them. Finally, the third line uses I to prove True.

Looking at the actual program produced, we see that it’s very simple:

Print notFalse.

Rocq responds

notFalse = fun _ : False -> False => I

which is a function that takes an argument that is never used, and simply returns I, which is the evidence for True.

The first line of the proof replaces ~True with True -> False. The rest of the proof proceeds by moving True -> False into the assumptions, then applying it to do backward reasoning, leaving us with needing to prove True. That holds by the I constructor.

The program that proof produces is interesting:

Print notTrue.

Rocq responds

notTrue = fun t_imp_f : True -> False => t_imp_f I
     : ~ True -> False

That proof is actually a higher-order function that takes in a function t_imp_f and applies that function to I, thus transforming evidence for True into evidence for False, and returning that evidence. If that seems impossible, it is! We’ll never be able to apply this function, because we’ll never be able to construct a value to pass to it whose type is ~True, i.e., True -> False.

Next, let’s return to the idea of explosion. From a contradiction we should be able to derive anything at all. One kind of contradiction is for a proposition and its negation to hold simultaneously, e.g., P /\ ~P.

Rocq

Theorem contra_implies_anything : forall P Q, P /\ ~P -> Q.
Intuition:  principle of explosion
Proof.
    unfold not.
    intros P Q PandnotP.
    destruct PandnotP as [P_holds notP_holds].
    contradiction.
Qed.

This proof proceeds along familiar lines: We destruct the evidence of [P /\ ~P] into two pieces. That leaves us with P as an assumption as well as ~P. The contradiction tactic detects those contradictory assumptions and finished the proof. By the way, we could have left out the as clause in the destruct here, since we are never going to use the names we chose, but they will help make the following program more readable:

Print contra_implies_anything.

The really interesting part of this is the body of the pattern match, False_rect Q (notP_holds P_holds). It applies notP_holds to P_holds, thus transforming evidence for P into evidence for False. It passes that hypothetical evidence for False to False_rect, which as we’ve seen before uses such evidence to produce evidence for anything at all that we would like—in this case, Q, its first argument.

When we get to the point in the proof above where we need to prove Q, we have no means to do so. (The same problem would occur for P if instead of left we had gone right.) Why does this happen? One reason is that the intuition we gave above is wrong! There’s no reason that "if evidence for P and Q would produce an explosion" implies "either evidence for P would produce an explosion, or evidence for Q would". It’s the combined evidence for P and Q that produces the explosion in that assumption—nothing is said about evidence for them individually.

But a deeper reason is that this theorem simply doesn’t hold in Rocq’s logic: there isn’t any way to prove it. That might surprise you if you’ve studied some logic before, and you were taught that both De Morgan laws are sound reasoning principles. Indeed they are in some logics, but not in others.

In classical logic, which is what you almost certainly would have studied before (e.g., in CMSC250), we are permitted to think of every proposition as having a truth value, which is either True or False. And one way to prove a theorem is to construct a truth table showing what truth value a proposition has for any assignment of True or False to its variables. For example (writing T and F as abbreviations):

Rocq

P  Q  ~(P/\Q) (~P \/ ~Q) (~(P/\Q) -> (~P \/ ~Q))
T  T  F       F          T
T  F  T       T          T
F  T  T       T          T
F  F  T       T          T

For every possible assignment of truth values to P and Q, we get that the truth value of ~(P/\Q) -> (~P \/ ~Q) is True. So in classical logic, ~(P/\Q) -> (~P \/ ~Q) is a theorem.

But Rocq uses a different logic called _constructive logic_. Constructive logic is more convervative than classical logic, in that it always requires evidence to be produced as part of a proof. As we saw above when we tried to prove deMorgan2, there just isn’t a way to construct evidence for ~P \/ ~Q out of evidence for ~(P/\Q).

There are many other propositions that are provable in classical logic but not in constructive logic. Another pair of such propositions involves _double negation_: P -> ~~P is provable in both logics, but ~~P -> P is provable in classical logic and not provable in constructive logic. Let’s try proving both just to see what happens.

In that proof, we have a new use for the apply tactic: we use it with the name of a theorem we’ve already proved, because our goal is in fact that theorem. In the resulting program, we saw this indeed becomes an application of the syllogism’ function:

Print p_imp_nnp'.

Rocq responds:

p_imp_nnp' = 
fun P : Prop => syllogism' P False
     : forall P : Prop, P -> ~ ~ P

Once we get past introducing assumptions in that proof, we’re stuck. There’s nothing we can do with (P -> False) -> False to prove P. Why? Because in constructive logic, to prove P, we must produce evidence for P. Nothing in (P -> False) -> False gives us such evidence.

That’s very different from classical logic, where we could just construct a truth table:

Rocq

P ~~P  (~~P -> P)
T T    T
F F    T

Whether we go left or right in the second step of that proof, we immediately get stuck. If we go left, Rocq challenges us to construct evidence for P, but we don’t have any. If we go right, Rocq challenges us to construct evidence for P -> False, but we don’t have any.

Why does Rocq use constructive logic rather than classical logic? The reason goes back to why we started looking at Rocq, namely, program verification. We’d like to be able to extract verified programs. Well, there simply is no program whose type is P \/ ~P, because such a program would have to use either or_introl or or_intror to construct its result, and it would have to magically guess which one to use, then magically somehow produce the appropriate evidence.

Rocq

Axiom excluded_middle : forall P : Prop, P \/ ~P.

Theorem deMorgan2' : forall P Q : Prop,
  ~(P /\ Q) -> ~P \/ ~Q.
Proof.
  intros P Q PQ.
  destruct (excluded_middle P).
    - destruct (excluded_middle Q).
      + unfold not in *. left. intros. apply PQ. split;assumption.
      +  unfold not in *. right. assumption.
    - destruct (excluded_middle Q).
    + unfold not in *. left. assumption.
    +  unfold not in *. right. assumption.
Qed.

16.9 Equality and implication🔗

Let’s return to the two connectives with which we started, equality and implication. Earlier we didn’t explain them fully, but now we’re equipped to appreciate their definitions.

Reading that carefully, we see that eq is parameterized on

- a type A, and

- a value x whose type is A.

We also see that A is implicit, so let’s use @eq from now on in our discussion just to be clear about A.

When we apply @eq to a type A and a value x, we get back a function of type A -> Prop. The idea is that function will take its argument, let’s call it y, and construct the proposition that asserts that x and y are equal. For example:

Definition eq42 := @eq nat 42.
Check eq42.  
Check (eq42 42).
Check (eq42 43). 

eq42 : nat -> Prop
eq42 42 : Prop
eq42 43 : Prop

Note how the constructor above takes just a single argument of type nat, not two arguments: it will only ever show that argument is equal to itself, never to anything else. There’s literally no way to write an expression using eq_refl to construct evidence that (e.g.) 42 and 43 are equal.

Equality, therefore, is not something that has to be "baked in" to Rocq, but rather something that is definable as an inductive type—much like and and or.

What is such a "thing"? A function! It transforms evidence for one proposition into evidence for another proposition.

So of all the logic we’ve coded up in Rocq in this file, the only truly primitive pieces are Inductive definitions and forall types. Everything else—equality, implication, conjunction, disjunction, true, false, negation—can all be expressed in terms of those two primitives.

And although we had to learn many tactics, every proof we constructed with them was really just a program that used functions, application, and pattern matching.

16.10 Tautologies🔗

We needed to learn the tactics and definitions above for the more complicated proofs we will later want to do in Rocq. But if all you care about is proving simple logical propositions, there’s a tactic for that: tauto. It will succeed in finding a proof of any propositional _tautology_, which is a formula that must always hold regardless of the values of variables in it.

Rocq responds:

Rocq

deMorgan' =
fun (P Q : Prop) (H : ~ (P \/ Q)) =>
let H0 := (fun H0 : P => H (or_introl H0)) : P -> False in
let H1 := (fun H1 : Q => H (or_intror H1)) : Q -> False in
conj (fun H2 : P => let H3 := H0 H2 : False in False_ind False H3)
  (fun H2 : Q => let H3 := H1 H2 : False in False_ind False H3)
     : forall P Q : Prop, ~ (P \/ Q) -> ~ P /\ ~ Q

That’s a bit more complicated of a proof than the one we constructed ourselves, mainly because of the let expressions, but it still is correct.

So if you want you to prove a propositional tautology, and if it’s a proposition that holds in constructive logic, Rocq’s got your back: just use tauto to do it.

16.11 Summary🔗

Rocq’s built-in logic is constructive: it isn’t sufficient to argue that a proposition must be true or false; rather, we have to construct evidence for the proposition. Programs are how we construct and transform evidence. All of the propositional connectives, except implication, are "coded up" in Rocq using inductive types, and proofs about them routinely use pattern matching and function application.

16.11.1 Terms and concepts🔗

• assumption

• classical logic

• conjunction

• constructive logic

• constructor

• contradiction

• De Morgan’s laws

• disjunction

• double negation

• evidence

• excluded middle

• implication

• inductive type

• negation

• Principle of Explosion

• Prop

• proposition

• reflexivity

• Set

• syllogism

• tautology

• transitivity

• truth table

16.11.2 Tactics🔗

• apply

• assumption

• contradiction

• destruct..as

• exact

• left

• right

• split

• tauto

• tacticals: nested bullets [-], [*], [+]

16.12 Further reading🔗

• Software Foundations, Volume 1: Logical Foundations Chapter 6: Logic.

• Interactive Theorem Proving and Program Development. Chapters 5 and 8.