The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 19.05.2013 21:50, schrieb Wilayat Khan:
> Hello Jonas
>
> Thank you for your reply.
>
> >> The way you currently do things you lose any kind of meaning of, 
> e.g., ascii_eqb a a' = true. How do you conclude from such a statement 
> that a = a'?
>
> >> Next, I suggest proving this on a more general level;
>
>  I dont know how to generalize it and then instantiate it with string. 
> I fear, eventually, I have to use string function like "str_le_gt_dec".
>   Although, general definition is good programming practice, but at 
> the moment I would like to proceed for string if possible.

I believe it only makes the proof more complicated, but it's your call.

>   1) I dont understand by "...you do not have any meaning of 
> "str_le_gt_dec"". To me, it decides correctly if two strings should be 
> swaped or not. Is there
>     any other way to decidability on strings and prove it?


How do you know it decides it "correctly"? What is the meaning of 
"correctly"?

I give you a definition of correctly, and then show you how to use it:


(*=================*)

(* str_lt a b <-> a comes before b in lexicographic ordering *)
Inductive str_lt : string -> string -> Prop :=
| empty : forall hd tl, str_lt EmptyString (String hd tl)
| head_lt hd1 hd2 : nat_of_ascii hd1 < nat_of_ascii hd2 -> forall tl1 
tl2, str_lt (String hd1 tl1) (String hd2 tl2)
| head_eq hd1 hd2 : hd1 = hd2 -> forall tl1 tl2, str_lt tl1 tl2 -> 
str_lt (String hd1 tl1) (String hd2 tl2)
.

Definition ascii_lt_eq_lt_dec a b : {nat_of_ascii a < nat_of_ascii b} + 
{a = b} + {nat_of_ascii b < nat_of_ascii a}.
destruct lt_eq_lt_dec with (nat_of_ascii a) (nat_of_ascii b) as 
[[de|de]|de] ; auto.
left ; right.
rewrite <- ascii_nat_embedding with a.
rewrite <- ascii_nat_embedding with b.
now f_equal.
Defined.

Definition str_lt_eq_lt_dec (s1 s2 : String.string)
 : {str_lt s1 s2} + {s1 = s2} + {str_lt s2 s1}.

revert s2.
induction s1 ; destruct s2 ; auto.
  left. left. now constructor.

  right. now constructor.

  destruct ascii_lt_eq_lt_dec with a a0 as [[de|de]|de].
    left. left. now constructor.

    subst. destruct IHs1 with s2 as [[de|de]|de].
      left. left. now constructor 3.

      subst ; auto.

      right. now constructor 3.

    right. now constructor.
Defined.


Definition str_lt_ge_dec (s1 s2 : String.string)
 : {str_lt s1 s2} + {s1 = s2 \/ str_lt s2 s1}.

destruct str_lt_eq_lt_dec with s1 s2 as [[de|de]|de] ; auto.
Defined.

(*=================*)

As you can see, str_lt_ge_dec no longer says "yes" or "no"; it says "s1 
< s2" or "s1 = s2 or s1 > s2".


>  2) If I use the updated [str_le_gt_dec] definition specified for 
> [string], then I get stuck as before in the loop of strings (I do 
> induction on zm).

Induction on zm is good. I don't see how you were able to prove the base 
case.
As far as I can tell, you end up with something as:

(if str_lt_ge_dec z1 z2 then [z1, z2] else [z2, z1]) =
(if str_lt_ge_dec z2 z1 then [z2, z1] else [z1, z2])

You can not prove this if you can not prove that if "str_lt_ge_dec z1 
z2" lands in the left case, that "str_lt_ge_dec z2 z1" lands in the 
right case. Even with the new definitions, you still need a lemma that 
proves str_lt is an ordering (i.e., antireflexive, antisymetrical, 
transitive).

Regards, Jonas