5

I am reading the ssreflect tutorial, which reads:

Below, we prove the ... by translating the propositional statement into its boolean counterpart, which is easily proved using brute force. This proof technique is called reflection. Ssreflect’s design allows for and ssreflect’s spirit recommends wide use of such a technique.

Does this (reflection) mean that the ssreflect assumes the excluded middle (forall A:Prop, A \/ ~A)?

It looks that it's the case because all boolean values satisfy the E.M. If so, this would be a big assumption to make for following the ssreflect style.

Also, I don't quite understand the "local" or "small scale" part of it that follows:

Since it is usually used locally to handle efficiently small parts of the proofs (instead of being used in the overall proof structure), this is called small scale reflection, hence the name ssreflect.

What does it mean small parts v.s. the overall proof structure. Is this implying that we can assume E.M. locally sometimes with no harm and do not use E.M. in general, or does the local here mean something else?

Also, I am not experienced enough in Coq, and don't quite see how this "brute force" style on the "boolean counterparts" (mostly based on case analysis from what I read so far) is more efficient than the vanilla Coq way. To me, brute force is not very intuitive and not easy to guess beforehand until you see the result.

Any concrete examples to illustrate the efficiency here?

thor
  • 21,418
  • 31
  • 87
  • 173

2 Answers2

7

Ssreflect does not assume the excluded middle, but large parts of the library are built on boolean propositions, that is, of type bool, for which it indeed holds that

forall b : bool, b = true \/ b = false

An equivalent version of the above is usually written, using the implicit is_true casting, as:

forall b : bool, b \/ ~ b.

"Reflectable" predicates are those which have a version in bool; a good example is the "less than or equal" relation between natural numbers.

In standard Coq, le is encoded as an inductive type, whereas in ssreflect it's a computational function leq: nat -> nat -> bool.

Using the leq function for proofs is more "efficient" for the following reason: imagine you want to prove that 102 < 203. Using the standard Coq definition, you will have to build a large proof term, you must explicitly encode every step of the proof.

However, with its computational counterpart, the proof is just the term erefl, witnessing that the algorithm returned true. This is crucial in large proofs, apart from many other advantages IMO.

To end, I must disagree with the statement that "ssreflect is only concerned with decidable types". While large parts of the libraries are based on decidable (boolean) predicates, there are many others where this assumption is not made or can be very useful with the presence of some axioms.

ejgallego
  • 6,709
  • 1
  • 14
  • 29
4

Ssreflect does not assume the excluded middle in general, you won't be able to prove that 

forall A: Prop, A \/ ~A

However, ssreflect is only concerned with decidable types: types where equality can be decided, usually stated as

Definition decidable (T:Type) := forall x y:T, {x = y}+{x <> y}.

in Coq. This means that for any two elements of the type T, you can get a constructive (in Set, not in Prop like the excluded middle) proof that they are either equal or different. Therefore, most of the reasoning can be done in bool and not in Prop, so you have some kind of restricted form of excluded middle, only for boolean statements.

Vinz
  • 5,997
  • 1
  • 31
  • 52