CODEWITHSUNDEEP
coqdependent-type
Michael
Michael

Reputation: 658

How to apply theorems for definitions with restrictions in coq

I found a number of examples of definitions with restrictions in coq. Here is for example a variation of the pred function:

Lemma Lemma_NotZeroIsNotEqualToZero : ~ 0 <> 0.
Proof.
omega.
Qed.

Definition pred (s : { n : nat | n <> 0 }) : nat :=
    match s with
        | exist 0 pf => match (Lemma_NotZeroIsNotEqualToZero pf) with end
        | exist (S n') _ => n'
    end.

But I don't actually understand how to use this definition. Suppose I want to use pred for some natural number and I proved that this number is not zero. Like, for instance, suppose I proved the following lemma:

Lemma Lemma_TenIsNotEqualToZero : 10 <> 0.
Proof.
omega.
Qed.

Now, I want to compute what in essence is "pred 10" using Lemma_TenIsNotEqualToZero:

Eval compute in (pred ??).

How to do it?

Upvotes: 2

Views: 188

Answers (1)

Vinz
Vinz

Reputation: 6047

pred is a function taking a sig type (try to Print sig.). Simply put, it's an inductive type with one constructor stating that "there exists an x of type A such that P x is true".

If you want to create a term of type {n : nat | n <> 0}, you will have to build it using constructors, like any other inductive type. In your case:

Eval compute in (pred (exist 10 Lemma_TenIsNotEqualToZero)).

It is the exact same syntax you used to pattern match on the s argument of pred.

Hope it helps,

V

PS: using omega for both your proofs is really overkill...

Lemma Lemma_NotZeroIsNotEqualToZero : ~ 0 <> 0.
Proof.
intro h.
apply h; reflexivity.
Qed.

Lemma Lemma_TenIsNotEqualToZero : 10 <> 0.
Proof.
intro h.
discriminate h.
Qed.

Edit: exists takes 3 arguments in practice (use Print to get a clear idea what are they used for). Depending on the status of implicit types, you should write 

exists _ 10 Lemma_TenIsNotEqualToZero

with the additional _.

Upvotes: 3

Related Questions