coq - 证明 s-expression 打印是单射的
问题描述
我定义了一种 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.
也许有一些资料可以帮助我计划定理的证明?(书籍/文章/代码)如何证明?(也许我需要一种特殊的归纳原理,你能制定它的陈述吗?)
我还定义了深度函数,它可能会有所帮助
Fixpoint depth (s:sexp) : nat :=
match s with
K n l =>
(match l with
nil => 0
| _ => S (list_max (map depth l))
end)
end.
谢谢!
ps一些额外的想法:
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.
pps 我觉得主要障碍是对两个列表进行归纳。
解决方案
该类型是嵌套归纳类型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。
推荐阅读
- python - 从两个列表创建更新的数据框
- node.js - 'Access-Control-Allow-Origin' CORS 尝试执行 firebase 功能时
- javascript - 当您更改路线时,meta 不会更改,尽管标题会更改
- java - Spring Scheduler 失败
- php - 在php中将整数转换为十进制值
- python-3.6 - Wsgi 错误:ModuleNotFoundError:没有名为“django_webapp”的模块
- node.js - Express 服务器在 EC2 上没有响应
- html - 在 CSS 中调整滚动球的高度
- python - 谁能解释一下这个代码中successful_frame_read的目的是什么?
- node.js - 使用 icognito 身份池时,在 Lambda 函数中获取 context.identity 中的用户信息