proposition: Lemma read_show_quoted_string : forall (s : string), read_quoted_string (show_quoted_string s) = Some s.
proof: Proof. induction s. - auto. - unfold show_quoted_string. destruct (ascii_dec a "009") as [is_tab | isn_tab]. { fold show_quoted_string. simpl. rewrite IHs. rewrite is_tab; auto. } destruct (ascii_dec a "010") as [is_nl | isn_nl]. { fold show_quoted_string. simpl; rewrite IHs. rewrite is_nl; auto. } destruct (ascii_dec a "013") as [is_cr | isn_cr]. { fold show_quoted_string. simpl; rewrite IHs. rewrite is_cr; auto. } destruct (ascii_dec a """") as [is_dq | isn_dq]. { fold show_quoted_string. simpl; rewrite IHs. rewrite is_dq; auto. } destruct (ascii_dec a "\") as [is_bs | isn_bs]. { fold show_quoted_string. simpl; rewrite IHs. rewrite is_bs; auto. } destruct ((nat_of_ascii a <? 32) || (126 <? nat_of_ascii a))%bool. { fold show_quoted_string. simpl. destruct (ascii_dec _ "n") as [is_n2 | isn_n2]. { apply not_digit_when in is_n2. contradict is_n2. compute. right. lia. } destruct (ascii_dec _ "r") as [is_r2 | isn_r2]. { apply not_digit_when in is_r2. contradict is_r2. compute. right. lia. } destruct (ascii_dec _ "t") as [is_t2 | isn_t2]. { apply not_digit_when in is_t2. contradict is_t2. compute. right. lia. } destruct (ascii_dec _ "\") as [is_bs2 | isn_bs2]. { apply not_digit_when in is_bs2. contradict is_bs2. compute. right; lia. } destruct (ascii_dec _ """") as [is_dq2 | isn_dq2]. { apply not_digit_when in is_dq2. contradict is_dq2. compute. left; lia. } fold (Nat.div (nat_of_ascii a) 100). fold (Nat.div (nat_of_ascii a) 10). rewrite unthree_three_digit. rewrite IHs. rewrite ascii_nat_embedding. auto. } { fold show_quoted_string. simpl. destruct (ascii_dec a """"); [contradiction |]. destruct (ascii_dec a "\"); [contradiction |]. rewrite IHs. auto. } Qed.
imports: List Coq.Strings.String Coq.Strings.Ascii Lia Arith QuickChick.Show