Is this the difference between Prop and Set?

[jaewooklee93]

My idea is that if I have an evidence for x∈l, where x is an element and l is a list, I can construct a function to find the leftmost appearing position of x in the list l. My first try was this.

Fixpoint find (X:Type) (x: X) (l: list X) (ev: appears_in x l): nat :=
  match ev with
  | ai_here l => 0
  | ai_later b l ev => S (find X x l ev)
  end.

However, it only gave me an unfamiliar error.

Error:
Incorrect elimination of "ev" in the inductive type "appears_in":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

I guess that this error is related to what professor explained in the last lecture. He said Prop is similar to Set, but Prop only cares whether it is empty or nonempty. I think that is the reason of impossibility of doing case analysis for ev. Is that correct?

In contrast, I can easily prove the following theorem

Fixpoint nth (X:Type) (l:list X) (n:nat) : option X :=
match l with
| [] => None
| h::t => (match n with
           | 0 => Some h
           | S n' => nth X t n'
           end)
end.

Theorem find: forall (X:Type) (x:X) (l:list X) (ev:appears_in x l),
exists n:nat, nth X l n = Some x.
Proof.

At this point, I'm little bit confused. While we can prove the existence of such function, even in a constructive way, why cannot we define that function with Fixpoint? Are such functions only living in the world of Theorem?

[gilhur]

This is a good point.

You are right that you cannot define 'find' directly because 'appears_in' is Prop. It is intuitively natural that there should not be any algorithm for find in case X is not a decidable set. The proposition "appears_in x l" only tells you the fact that x is in the list l somewhere, but does not tell you at which position the element x locates. If you want such information, you can define a proposition like

 appears_in_at x n l  (meaning that x appears at nth location in l)

Also, the theorem is provable because "exists n:nat, nth X l n = Some x" is Prop. As I said in the lecture, you can do a case analysis when you go from Prop to Prop.

[jaewooklee93]

It seems that the world of Props and the world of computable functions are strictly separated. I should be careful about their difference.

[gilhur]

The rule is simple.

• For inductive types: If you use "Prop" at the end of "Inductive", the set becomes a proposition. Otherwise, it becomes a proper set.
• For function types: forall (x:A), B[x] : Prop if B[x] : Prop forall (x:A), B[x] : Type if B[x] : Type

Note that technically Prop is a subset of Type. So, strictly speaking, anything in Type but not in Prop is a proper set.

On Mon, Apr 20, 2015 at 8:52 PM, jaewooklee93 notifications@github.com wrote:

It seems that the world of Props and the world of computable functions are strictly separated. I should be careful about their difference.

— Reply to this email directly or view it on GitHub https://github.com/snu-sf/pl2015/issues/74#issuecomment-94431903.

[jaewooklee93]

I think now I catch the point. I can perform the case analysis for Prop only in the form of Prop -> Prop but I can't do it in Prop -> Set.

Require Import Omega.

Inductive even: nat -> Prop :=
  | ev_0  : even 0
  | ev_SS : forall n, even n -> even (2+n).

Theorem Prop2Prop:
  forall n (H: even n),
  0=n \/ 2<=n.
Proof.
  intros.
  inversion H; omega.
Qed.

Theorem Prop2Set:
  forall n (H: even n),
  {0=n} + {2<=n}.
Proof.
  intros.
  inversion H. (* Error *)
Abort.

I thought sumbool has almost the same semantic to or, but it seems that the meaning of sumbool is much more restrictive.

[jaewooklee93]

Ah, of course, Set like nat and list are always eliminable.