CODEWITHSUNDEEP
coq
wt.cc
wt.cc

Reputation: 333

What's the exact rule of applying a theorem in Coq?

I'm studying the SoftwareFoundation at https://softwarefoundations.cis.upenn.edu/lf-current/toc.html. The section Logic states that theorem can be used just like a function. I tried some examples but failed to get common rules.

The first try:

Example xxx:
  (0 = 2) -> (0 = 3).
Proof. Admitted.
Example yyy:
  (0 = 2) -> (0 = 3).
Proof.
  intros H.
  apply (xxx H). (* this works *)
  apply (xxx (0 = 2)). (* this fails. *)
Qed.

Coq give me an error on failed version as below. Except that it fails, I still cannot understand why is strange type 0 = 2 required instead of Prop ?

The term "0 = 2" has type "Prop" while it is expected to have type "0 = 2".

If I use relation <-> in xxx instead of ->, (xxx H) fails either...

Example xxx:
  (0 = 2) <-> (0 = 3).
Proof. Admitted.
Example yyy:
  (0 = 2) -> (0 = 3).
Proof.
  intros H.
  apply (xxx H). (* this fails either *)
Qed.

The most important, SF shows how to apply a Theorem in Lemma lemma_application_ex (the below example), I have totally no idea about how does (proj1 _ _ (In_map_iff _ _ _ _ _) H) work ...

Lemma proj1 : forall P Q : Prop,
  P /\ Q -> P.
Proof.
  intros P Q [HP HQ].
  apply HP.  Qed.

Lemma In_map_iff :
  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
    In y (map f l) <->
    exists x, f x = y /\ In x l.
Proof.
  (* FILL IN HERE *) Admitted.

Example lemma_application_ex :
  forall {n : nat} {ns : list nat},
    In n (map (fun m => m * 0) ns) ->
    n = 0.
Proof.
  intros n ns H.
  destruct (proj1 _ _ (In_map_iff _ _ _ _ _) H)
           as [m [Hm _]]. (* I cannot understand this application *)
  rewrite mult_0_r in Hm. rewrite <- Hm. reflexivity.
Qed.

Upvotes: 0

Views: 329

Answers (2)

hengxin
hengxin

Reputation: 1999

To understand (proj1 _ _ (In_map_iff _ _ _ _ _) H), you can use Check to analyze it step by step:

  • Check proj1.

    : forall P Q : Prop, P /\ Q -> P

  • Check proj1 _ _.

    : ?P /\ ?Q -> ?P

  • Check In_map_iff.

    : forall (A B : Type) (f : A -> B) 
    (l : list A) (y : B),
  In y (map f l) <->
  (exists x : A, f x = y /\ In x l)

  • Check In_map_iff _ _ _ _ _.

    : In ?y (map ?f ?l) <->
 (exists x : ?A, ?f x = ?y /\ In x ?l)

  • Check @proj1 _ _ (In_map_iff _ _ _ _ _).

    : In ?y (map ?f ?l) ->
 exists x : ?A, ?f x = ?y /\ In x ?l

  • Check proj1 _ _ (In_map_iff _ _ _ _ _) H.

    : exists x : nat, x * 0 = n /\ In x ns

Upvotes: 0

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

As explained in that chapter, the type of a theorem or lemma is the statement that it proves. For instance,

Check xxx.
(* 0 = 2 -> 0 = 3 *)

The same holds for hypotheses when you are proving a theorem:

Example yyy:
  (0 = 2) -> (0 = 3).
Proof.
  intros H.
  Check H. (* 0 = 2 *)

The first error message you saw says that you need to pass the proof of a proposition as an argument, rather than the proposition itself. The type of 0 = 2 is Prop, not 0 = 2 itself. Similarly, when you use the plus function, the argument must be of type nat, but nat itself won't work:

Check plus 1 2. (* nat *)
Check plus nat nat.
(* Error: The term "nat" has type "Set"
   while it is expected to have type "nat". *)

Edit

Note that the application syntax only works for implication statements and universal quantification. You get an error when using a theorem of type A <-> B in this way because this statement means (A -> B) /\ (B -> A), which doesn't fall into these cases. However, you can use the proj1 : forall A B, A /\ B -> A lemma to extract the first side of the equivalence and apply it to something. For instance, we could fill in the implicit arguments of proj1 _ _ ... in the example you mentioned:

proj1 (In n (map (fun m => m * 0) ns))
      (exists x, (fun m => m * 0) x = n)
      (In_map_iff nat nat (fun m => m * 0) ns n)
      H

If we remove the H part, this application has type

In n (map (fun m => m * 0) ns) ->
exists x, (fun m => m * 0) x = n

which can be applied to H : In n (map .. ns) to get a proof of an existential statement.

Upvotes: 3

Related Questions