coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with a Proof

chronological Thread

From: Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Problem with a Proof
Date: Tue, 10 Feb 2009 11:44:24 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.co.uk; h=Message-ID:Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type; b=K16QNGj4WxjglqxfF03J0c1mPnd8lPTVJSV3/3AK6uHp04IZH1hyAW/Ms2KIE3UvIkZbxJUn/yAj69LkcXv/lIhES1h/ZrzkeHBOXL4+mFaLUNrtzC9WtPrwpZj9FlM5ig4ZlcsBzPJiurxPyt0s6wOCFd38bI56a4IMUa7nwv4=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I'm trying to do a proof about the following function in which I'm finding myself stuck.

Definition foo (l1 l2:list Z)(acc:list Z):(list Z).

refine (fix foo_l1 (l1 :list Z):list Z -> list Z -> (list Z) := _).

refine (fix foo_l2 (l2: list Z):list Z -> (list Z) := _).

refine (

fun acc =>

match l1,l2 with

| nil,l2 => app acc l2

| l1,nil => app acc l1

| x::xs, y::ys =>

if Z_eq_dec x y then

foo_l1 xs ys (x::acc)

else if Z_lt_dec (Zabs x)(Zabs y) then

foo_l1 xs (y::ys) (x::acc)

else if (Z_eq_dec (x + y) Z0) then foo_l1 xs ys acc

else foo_l2 ys (y::acc)

end).

Defined.

I have the following two propositions:

Lemma Prop1 : forall x y:Z, (x <> 0) -> (y <> 0) -> (x+y = 0) -> (x <> y).

Lemma Prop2 :

forall x y:Z, (x+y = 0) -> (~(Zabs x < Zabs y)) /\ (~(Zabs y < Zabs x)).

The theorem am trying to prove is the following:

Goal forall c1 c2 l1 l2, (l1 <> 0) -> (l2 <> 0) ->

NoDup c1 -> NoDup c2 -> In l1 c1 -> In l2 c2 ->

~In l1 c2 -> ~In l2 c1 -> (l1+l2=0) -> (~In l1 (foo c1 c2 nil)).

I start with induction on c1 and c2 and easily discharge 3 out of 4 sub-goals, but in the

4th one I find myself stuck when having to unfold foo and not able to reduce the goal

any further.

Proof.

induction c1;induction c2.

intros.

inversion H3.

intros.

inversion H3.

intros.

inversion H4.

intros.

generalize (Prop2 (l1:Z) (l2:Z));intros.

generalize (Prop1 (l1:Z) (l2:Z));intros.

case (Z_eq_dec (l1 + l2) 0);

case (Z_lt_dec (Zabs l1) (Zabs l2));

case (Z_eq_dec l1 l2); intros.

intuition.

inversion H1;inversion H2.

unfold In in H3;unfold In in H4.

elim H3;elim H4;intros.

rewrite H19;rewrite H18.

The state I have looks like

H13 : NoDup c1

H10 : x = a

H11 : l = c1

x0 : Z

l0 : list Z

H16 : ~ In a0 c2

H17 : NoDup c2

H14 : x0 = a0

H15 : l0 = c2

H18 : a0 = l2

H19 : a = l1

============================

~ In l1 (foo (l1 :: c1) (l2 :: c2) nil)

unfold foo.

at this stage leads me to a state where not sure how to proceed.

Any help is appreicated,

Thank you

Ashish

[Coq-Club] Problem with a Proof, Ashish Darbari
- Re: [Coq-Club] Problem with a Proof, Yves Bertot
- Re: [Coq-Club] Problem with a Proof, Yves Bertot