CODEWITHSUNDEEP
coq
Vor
Vor

Reputation: 405

What is the exactly the term "10" in Coq?

A very basic question about Coq (with Init libraries): the term 10 is of type nat, and the type nat is defined inductively:

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Q1. But is "10" a "shortcut" of S(S(...S(0)...))?

Q2. Is there a shortest (formal) proof of the following lemma? (without using omega)

Lemma gg : 3 <= 10.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_n.
Qed.

In other words does a proof of n <= m (with only Peano axioms), require exponential length?

Upvotes: 2

Views: 186

Answers (3)

user3551663
user3551663

Reputation:

Below is an example for Ptival's answer.

Require Import Coq.Arith.Arith.

Check @eq_refl.
Check leb_complete.

Goal 3 <= 10. Proof. apply leb_complete. apply eq_refl. Qed.

Goal 30 <= 100. Proof. apply leb_complete. apply eq_refl. Qed.

Goal 300 <= 1000. Proof. apply leb_complete. apply eq_refl. Qed.

Come to think of it, isn't omega also a form of proof by reflection? Or is it programmed in OCaml?

Upvotes: 5

osa1
osa1

Reputation: 7088

A1. Right.

A2. As far as I can tell from definition of le(<=), you have to use le_S and le_n to construct a proof of it.

Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

... unless you define a lemma to make your work easier.

You can do something like this:

Lemma gg : 3 <= 10.
Proof.
  do 7 (apply le_S).
  apply le_n.
Qed.

... or

Lemma gg' : 3 <= 10.
Proof. repeat constructor. Qed.

... or go the other way around:

Lemma le_s : forall n m, n <= m -> S n <= S m.
Proof.
  intros. induction H. constructor.
  constructor. apply IHle.
Qed.

Lemma gg'' : 3 <= 10.
Proof.
  pose proof (le_n 0).
  do 3 (apply le_s in H).
  do 7 (apply le_S in H).
  apply H.
Qed.

Upvotes: 5

Ptival
Ptival

Reputation: 9447

Q1: Yes.

Q2: You can probably use the technique of proof by reflection to eliminate such trivial large proofs. This chapter explains how and why you would want to do that:

http://adam.chlipala.net/cpdt/html/Reflection.html

Upvotes: 6

Related Questions