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.
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.