search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Can we construct a subset of the given Set? #72

Open jaewooklee93 opened 9 years ago

jaewooklee93 commented 9 years ago

It is just a short question. I'm working with the function looks like exists (f:nat->nat),.

While the domain of f is all natural number, I want to restrict its domain to the natural number smaller than n.

{0,1,2,...,n-1}

Is there any simple way to construct a subset of the Set we already have?

jeehoonkang commented 9 years ago

I believe this link should be helpful: https://coq.inria.fr/library/Coq.Init.Specif.html

jeehoonkang commented 9 years ago

However, this kind of machinery, called dependent types, is known to be hard to deal with in Coq. I would rather prefer define a total function f:nat->nat, and apply f only to sub-n elements.

Jeehoon

jaewooklee93 commented 9 years ago

Okay, I understand. Then if I want to prove that every function f:{0,1,..,m}->{0,1,...,n} is not injective (one-to-one) if n<m, should I formalize the proposition like this?

Theorem pigeonhole_principle_constructive:
  forall (f:nat -> nat) m n, S n <= m ->
  (forall x, x <= m -> f x <= n) ->
  exists i, exists j, i <= m /\ j <= m /\ i <> j /\ f i = f j.
Proof.

Thank you. Jaewook Lee

jeehoonkang commented 9 years ago

That makes sense to me, but it would be equivalently good (or slightly better) to restrict I and j to be less than n.

jeehoonkang commented 9 years ago

Ah, sorry; your version already restricts them to be less than m, the (designated) domain of the function. My comment was wrong!

jaewooklee93 commented 9 years ago

You're right. In the first posting, I missed to put the bound for i, j, but I also found that error immediately after the posting, so I changed that. I am sorry to confuse you.

By the way, I proved that theorem pigeonhole_principle_constructive, finally, but the proof is really really long due to the many inequalities in the proposition.. it takes even 400 lines of tactics...

gilhur commented 9 years ago

Jaewook, this shows you why the life of a constructivist is hard. But, I think there might be a way to simplify your proof script. If you are interested, just send me your proof script.

jaewooklee93 commented 9 years ago

@gilhur I sent you my proof script. Thank you very much.

jeehoonkang commented 9 years ago

May I ask if there is any progress on this issue?

jaewooklee93 commented 9 years ago

I think this issue is completely solved, but I've left it open until now because the Professor answered it :)