Proving that s-expressions printing is injective

Question

I defined a type of s-expressions and it's printing functions.

Inductive sexp : Set :=
 K : string -> (list sexp) -> sexp
.
Fixpoint sexpprint (s:sexp) : list string :=
match s with
K n l => ["("%string]++[n]++(concat (map sexpprint l))++[")"%string]
end.

(Yes, I understand it can be just string, not the list of strings, but Coq have small amount of theorems for working with strings, but a big amount for working with lists.)

(* more usual function
Fixpoint sexpprint (s:sexp) :string :=
match s with
K n l => ("(":string)++n++(String.concat "" (map sexpprint l))++")"
end.
*)

And I've got stuck trying to prove this theorem:

Theorem sexpprint_inj s1 s2:
sexpprint s1 = sexpprint s2 -> s1 = s2.

Maybe there are some sources which can help me to plan the theorem's proof? (books/articles/codes) How to prove it? (Maybe I need a special kind of inductive principle, could you formulate its statement?)

Also I defined depth function, it may somehow help

Fixpoint depth (s:sexp) : nat :=
match s with
K n l => 
(match l with
  nil => 0
 | _ => S (list_max (map depth l))
 end)
end.

Thanks!

p.s. some additional thoughts:

Theorem depth_decr n l s m:
depth (K n l) = m
->
In s l
->
depth s < m
.
Proof.
Admitted.

Theorem step_lem (m:nat) :
(forall s1 s2,
depth s1 < m ->
depth s2 < m ->
sexpprint s1 = sexpprint s2 -> s1 = s2
) ->
(forall s1 s2,
depth s1 = m ->
depth s2 = m ->
sexpprint s1 = sexpprint s2 -> s1 = s2
).
Proof.
intros H s1 s2 Q1 Q2 E.
destruct s1 as [n1 l1], s2 as [n2 l2].
simpl in E.
inversion E as [E1].
apply (app_inv_tail) in H0.
Search "concat".
cut (l1=l2).
intros []; reflexivity.
Search "In".
induction l1, l2.
+ trivial.
+ simpl in H0. 
destruct s.
unfold sexpprint in H0.
simpl in H0.
inversion H0.
+ simpl in H0. 
destruct a.
unfold sexpprint in H0.
simpl in H0.
inversion H0.
+ admit.
Admitted.

p.p.s. I feel like the main obstacle is performing induction on two lists.

user_1633770 · Answer

The type sexp is an example of a nested inductive type, where one of the recursive occurrences appears inside of another induction. Such types are hard to work with in Coq, because the induction principles that it generates by default are not useful. However, you can fix this issue by writing down your own induction principle by hand. Here is one possibility:

Require Import Coq.Lists.List Coq.Strings.String.
Import ListNotations.

Unset Elimination Schemes.
Inductive sexp : Type :=
| K : string -> list sexp -> sexp.
Set Elimination Schemes.

Definition tuple (T : sexp -> Type) (es : list sexp) :=
  fold_right (fun e R => T e * R)%type unit es.

Definition sexp_rect
  (T : sexp -> Type)
  (H : forall s es, tuple T es -> T (K s es)) :
  forall e, T e :=
  fix outer (e : sexp) : T e :=
    match e with
    | K s es =>
      let fix inner (es : list sexp) : tuple T es :=
        match es return tuple T es with
        | [] => tt
        | e :: es => (outer e, inner es)
        end in
      H s es (inner es)
    end.

Definition sexp_ind (T : sexp -> Prop) := sexp_rect T.

With this induction principle, it is now possible to prove your lemma (exercise!), but you will need to generalize its statement a bit.

For a deeper discussion about these nested inductives, you can have a look at CPDT.

Proving that s-expressions printing is injective

1 Answers