CODEWITHSUNDEEP
coq
Stefan
Stefan

Reputation: 243

Proving theorems about inductive types using _ind; App rule

Variables A B : Prop.

Theorem proj1 : A /\ B -> A.

In order to learn, I'm trying to prove this theorem by explicitly writing down a proof term using and_ind.

I would assume the correct proof term is

fun (H : A /\ B) => and_ind A B A (fun a _ => a) H

But this raises an error, and instead the correct term is

fun (H : A /\ B) => and_ind (fun a _ => a) H

I don't understand this. The definition of and_ind is

and_ind = 
fun (A B P : Prop) (f : A -> B -> P) (a : A /\ B) => match a with
                                                     | conj x x0 => f x x0
                                                     end
     : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P

How can I see from that that the parameters (A B P : Prop) have to be omitted?

The "App" rule

App rule

from the Reference Manual seems to state clearly that quantified variables have to be explicitly "instantiated" using the function application syntax that I tried.

Upvotes: 1

Views: 49

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

In Coq, you can declare some arguments of a function as implicit. When you call the function, you don't supply values for the implicit arguments; Coq automatically tries to infer suitable values, based on other information available during type checking. The A, B and P arguments of and_ind are all declared as implicit, and can be inferred from the type of the H argument and the result type of the function argument.

You can see what arguments are considered implicit with the About command:

About and_ind.
(* and_ind : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P *)

(* Arguments A, B, P are implicit *)
(* Argument scopes are [type_scope type_scope type_scope function_scope _] *)
(* and_ind is transparent *)
(* Expands to: Constant Coq.Init.Logic.and_ind *)

You can turn off implicit arguments with an individual call with an @ sign:

Check fun A B H => @and_ind A B A (fun a _ => a) H.
(* fun (A B : Prop) (H : A /\ B) => and_ind (fun (a : A) (_ : B) => a) H *)
(*      : forall A B : Prop, A /\ B -> A *)

(Notice that Coq automatically omits implicit arguments when printing a term as well.)

The Coq manual has more information on that subject.

Upvotes: 2

Related Questions