证明 s-expressions 打印是单射的

Question

我定义了一种 s 表达式及其打印函数。

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.

（是的，我知道它可以只是字符串，而不是字符串列表，但是 Coq 有少量用于处理字符串的定理，但是有大量用于处理列表的定理。）

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

我一直在试图证明这个定理：

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

也许有一些资源可以帮助我计划定理的证明？ (books/articles/codes) 如何证明呢？（也许我需要一种特殊的归纳原理，你能制定它的陈述吗？）

我还定义了深度函数，它可能会有所帮助

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

谢谢！

p.s。一些额外的想法：

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。我觉得主要障碍是对两个列表进行归纳。

Answer 1

类型 sexp 是 嵌套归纳类型 的示例，其中一个递归事件出现在另一个归纳内部。这种类型在 Coq 中很难使用，因为它默认生成的归纳原则没有用。但是，您可以通过手写自己的归纳原理来解决这个问题。这是一种可能性：

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.

有了这个归纳原理，现在可以证明你的引理（练习！），但你需要稍微概括一下它的陈述。

有关这些嵌套归纳法的更深入讨论，您可以查看 CPDT。

证明 s-expressions 打印是单射的

Proving that s-expressions printing is injective

coq