The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Ashish Darbari wrote:
> 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 c1andc2 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.
> intuition.
> 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
>
>
>       
>   
You cannot progress because you made a few wrong choices: these is no point
in performing a case analysis on (Z_eq_dec l1 l2) when l1 and l2 are not 
the first two
elements of the two lists passed as argument to foo.  At the moment you 
call the case
tactics, you have not made sure that l1 and l2 are equal to a and a0, 
but in the code
of foo,, the values that are compared are a and a0.

Second, you prove by induction a statement about foo where the third 
argument is fixed to
nil, but in recursive call, the accumulator gets to change.  You need to 
let the third argument
be a a variable that already satisfies suitable property.

Last, your foo function is cleverly encoded by nesting two recursive 
functions one inside the other but your initial intent is a function 
that is structural recursive on both its argument.
I suggest that you prove the equation corresponding to  you initial 
intent and use this equation
to unroll the function instead of unfold.  In this way you will avoid 
having foo_l1 and foo_l2
popping in your goals.

Here is the equation and the proof:

Lemma foo_equation : forall l1 l2 acc,
foo l1 l2 acc =
  match l1, l2 with x::xs, y::ys =>
    if Z_eq_dec x y then foo xs ys (x::acc)
   else if Z_lt_dec (Zabs x) (Zabs y) then foo xs (y::ys) (x::acc)
   else if Z_eq_dec (x + y) 0 then foo xs ys acc else foo (x::xs) ys 
(y::acc)
 | nil, _ => acc++l2
 | _, nil => acc++l1
 end.
intros [ | x xs] [ | y ys]; auto.
Qed.


Please note that foo_equation would be produced for you if you had used 
"Function" to
define foo.

Now, use "rewrite foo_equation" instead of "unfold foo".  The result 
will be more readable.
Also I suggest you unroll foo much earlier in your proof (right at the 
start, for instance).  At
least, you should unroll foo to expose "Z_eq_dec a a0" before you call 
the tactic
(case (Z_eq_dec a a0)).

Yves