coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonas Oberhauser <s9joober AT gmail.com>
- To: Wilayat Khan <wilayatk AT gmail.com>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq - String List Sort Lemma
- Date: Sun, 19 May 2013 22:32:14 +0200
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
- [Coq-Club] Coq - String List Sort Lemma, Wilayat Khan, 05/19/2013
- Re: [Coq-Club] Coq - String List Sort Lemma, Jonas Oberhauser, 05/19/2013
- Re: [Coq-Club] Coq - String List Sort Lemma, Daniel Schepler, 05/19/2013
- Re: [Coq-Club] Coq - String List Sort Lemma, Jonas Oberhauser, 05/19/2013
- Re: [Coq-Club] Coq - String List Sort Lemma, Daniel Schepler, 05/19/2013
- Re: [Coq-Club] Coq - String List Sort Lemma, Jonas Oberhauser, 05/19/2013
- Re: [Coq-Club] Coq - String List Sort Lemma, Daniel Schepler, 05/19/2013
- Message not available
- Message not available
- Re: [Coq-Club] Coq - String List Sort Lemma, Jonas Oberhauser, 05/19/2013
- Message not available
- Re: [Coq-Club] Coq - String List Sort Lemma, Jonas Oberhauser, 05/19/2013
- Message not available
- Message not available
- Re: [Coq-Club] Coq - String List Sort Lemma, Jonas Oberhauser, 05/20/2013
- Message not available
Archive powered by MHonArc 2.6.18.