'else' in definitions - Coq

2
votes

First of all I'm new to proof theory and coq, so I'd appreciate answers to be easy to understand.

I'm trying to build up definitions to eventually define prime numbers; I'm currently trying to define divisibility, and in my definition I've written the true cases.

  1. Every nat is divisible with 1.
  2. Every nat is divisible with itself.

And my inductive case (applyable when '(i > j)' ):

  1. Every nat 'i' is divisible by 'j' if '(i - j)' is divisible by 'j'.

Now in some of my subsequent lemmas I need that everything not fulfilling this is false.

How would I go about encoding this in my definition? I'm thinking something alike, when none of the above is applicable --> false. - In a sense an else statement for definitions.

2
coq
(1) It'd be better if you presented some code, at least the inductive definition for divisibility. (2) The inductive case should be applicable when i >= j. (3) I'd change the 3d rule to "Every i + j is divisible by j if i is divisible by j". It makes proofs easier. (4) It seems to me that you'd need a rule for handling the case "Zero is divisible by every nat". (5) The 1st rule is redundant, it can be obtained from the 2nd and the 3d rules. Intuitively, start with 1 divides 1, then proceed to 1 divides (1 + 1), etc., up to arbitrary n. – Anton Trunov
Also, imo, a nice way to check this inductive definition is to prove its logical equivalence with something like Definition divides' x y := exists z, y = z*x. – Anton Trunov

2 Answers

3
votes

In constructive logic, which Coq is built upon, a proposition is only considered "true" when we have direct evidence, i.e. proof. So, one doesn't need such "else" part, because anything that cannot be constructed is in a sense false. If none of the cases for your "is divisible by" relation are applicable, you'll be able to prove your statement by contradiction, i.e. derive False.

For example, if we have this definition of divisibility:

(* we assume 0 divides 0 *)
Inductive divides (m : nat) : nat -> Prop :=
  | div_zero: divides m 0
  | div_add: forall n, divides m n -> divides m (m + n).
Notation "( x | y )" := (divides x y) (at level 0).

Then we can prove the fact that 3 does not divide 5, using inversion, which handles the impossible cases:

Fact three_does_not_divide_five:
  ~(3 | 5).
Proof.
  intro H. inversion H. inversion H2.
Qed.

Note: we can check that our divides relation captures the notion of divisibility by introducing an alternative ("obvious") definition:

Definition divides' x y := exists z, y = z*x.
Notation "( x |' y )" := (divides' x y) (at level 0).

and proving their equivalence:

Theorem divides_iff_divides' (m n : nat) :
    (m | n) <-> (m |' n).
Admitted. (* it's not hard *)
1
votes

A different approach is to define divisibility from with division and remainder:

  • Define a divn : nat -> nat -> nat * nat operation that divides two numbers and returns the remainder.
  • Then, divisibility is expressed as "remainder is equal to 0". You'll need to work out some details, such as what happens with 0.
  • Then, a falsified divisibility hypothesis amounts to a false equality which can be usually solved by congruence. You can manipulate the equality with the standard theory for the remainder.

This is the approach used in the math-comp library, see http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.div.html