Geek Answers Handbook

How to read ex_intro definition?

I am reading Coq's introductory tutorial at Mike Nahas that says:

Arguments for "ex_intro":

  • predicate
  • witness
  • proof of alleged name with witness

I looked at the definition :

Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P.

and I can’t make it out. What parts of the expression forall x:A, P x -> ex (A:=A) P correspond to these three arguments (predicate, witness, and proof)?

+5
source share
2 answers

To understand what Mike had in mind, it is better to run the Coq interpreter and an ex_intro :

 Check ex_intro.

Then you should see:

 ex_intro : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x

This suggests that ex_intro accepts not only 3, but also 4 arguments:

  • the type of thing you are measuring, A ;
  • predicate P : A -> Prop ;
  • witness x : A ; and
  • evidence of P x , claiming x is a credible witness.

If you combine all these things, you get the proof of exists x : A, P x . For example, @ex_intro nat (fun n => n = 3) 3 eq_refl is a proof of exists n, n = 3 .

So the difference between the actual ex_intro type and the one you read in the definition is that the first includes all the parameters that are indicated in the header, in this case A and P

+8
source

Yes, these inductive type definitions can be hard to read.

First part:

 Inductive ex (A:Type) (P:A -> Prop) : Prop :=

This is what is associated with the type itself. Therefore, at any time when you see ex , it will have A and P , and ex will be of type Prop . Skipping A for the moment, focus on P , which is a predicate. So, if we use “there is a natural number that is prime” as our example, P can be is_prime , where is_prime takes a nat (a natural number) as an argument and there can be proof of it if nat is prime.

In this example, A will be nat . Textbook A not mentioned because Coq can always infer it. Given a predicate, Coq can get type A by looking at the type of the predicate argument.

To summarize, here in our example the type will be ex nat is_prime . This suggests that there is a nat that is simple, but it does not say which nat. When we build a ex nat is_prime , we will need to say which one - we need a “witness”. And this leads us to the definition of a constructor:

 ex_intro : forall x:A, P x -> ex (A:=A) P.

The constructor is named ex_intro . What a complication here is that the constructor has all the parameters for the type. So, before we move on to those listed after ex_intro , we must include those that are of type: A and P

After these parameters, those appearing after ex_intro : x , which is the witness, and P x , which is proof that the predicate holds for the witness. Using our example, x may be 2, and P x will be the proof (is_prime 2) .

The constructor must specify parameters for the ex type that it creates. This is what happens after the arrow ( -> ). They do not have to match the parameters used when calling the constructor, but they usually do. For this, argument A not output - it is passed explicitly. (A:=A) says that parameter A in ex should be equal to A in the constructor call. Similarly, the parameters P of ex are set to P from the constructor call.

So, if we had proof_that_2_is_prime with type (prime 2) , we can call ex_intro is_prime 2 proof_that_2_is_prime and it would have type ex nat is_prime . This is our proof that there is a natural number that is prime.

To answer your question directly: in the expression forall x:A, P x -> ex (A:=A) , x:A is the witness, and P x is the evidence of the truth of the witness. The expression does not contain a predicate, because it is part of the type parameters that must be passed to the ex_intro constructor. The parameter list does not include A because it is derived by Coq.

I hope you understand why I thought this discussion was too detailed for my tutorial! Thanks for the question.

+1
source

More articles:


All Articles