我是这样fold_length定义的：
Inductive list (X: Type) : Type :=
| nil : list X
| cons : X -> list X -> list X.
Arguments nil {X}.
Arguments cons {X} _ _.
Notation "x :: y" := (cons x y)
(at level 60, right associativity).
Notation "[ ]" := nil.
Fixpoint fold {X Y:Type} (f: X -> Y -> Y) (l:list X) (b:Y) : Y :=
match l with
| nil => b
| h :: t => f …考虑以下部分证明：
Theorem test : forall (n m : nat),
n = m -> S n = S m.
Proof.
intros n m H.
执行到这一点给我以下内容：
1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
S n = S m
我想S从目标中删除s ，获得目标n = m。有没有一种策略可以做到这一点？
我正在阅读Coq的线性逻辑机械化http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf和https://github.com/brunofx86/LL我无法term从https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v了解归纳类型的类型构造函数:
Inductive term :=
|var (t: T) (* variables *)
|cte (e:A) (* constants from the domain DT.A *)
|fc1 (n:nat) (t: term) (* family of functions of 1 argument *)
|fc2 (n:nat) (t1 t2: term). (* family of functions of 2 argument *)
关于这个样本,我有两个问题(我正在阅读本文中的https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html):
term？Software Foundations总是指定新类型的(超级)类型,例如Inductive color : Type;var (t: T)？.Software Foundation在其第一章中仅提供了两种类型的构造函数:常量white : color和函数primary : rgb …我试图在 CoqIDE（学校）中证明一些东西。我挡住了一步，这是
`Print length. (* la longueur de listes *)
Lemma mystere A: forall l : list A, length l = 0 <-> l = nil.
intros.
destruct l.
* split.
- intros.
reflexivity.
- intros.
simpl.
reflexivity.
* split.
- intros.
???? <- I have tried many things, but without success..
Admitted.
`
谢谢各位的考虑！
试图理解@keep_learning的答案，我一步一步地浏览了这段代码：
Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).
Example test_nostutter_4: not (nostutter [3;1;1;4]).
Proof.
intro.
inversion_clear H.
inversion_clear H0.
unfold not in H2.
(* We are here *)
specialize (H2 eq_refl).
apply H2.
Qed.
这是我们在执行 specialize 之前所拥有的
H1 : 3 …我坚持要证明以下公认的引理。请帮助我如何继续。
函数sumoneseq以相反的顺序添加并返回“true”的重复列表。鉴于 [真;假; 真;真;假; true;true;true ]，它返回 [3;2;1]。该功能sumones在NAT表增加值。给定 [3;2;1]，它返回 6。
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Fixpoint sumoneseq (lb: list bool) (ln: list nat) : list nat :=
match lb, ln with
| nil, 0::tl'' => tl''
| nil, _ => ln
| true::tl', nil => …外延公理说，如果两个函数在域的每个参数上的动作相等，则它们是相等的。
Axiom func_ext_dep : forall (A : Type) (B : A -> Type) (f g : forall x, B x),
(forall x, f x = g x) -> f = g.
平等=的定理声明的两侧是命题平等（具有单个数据类型eq_refl构造函数）。使用这个公理可以证明f = a + b和g = b + a在命题上是相等的。
但是f和g显然不等于数据结构。
你能解释一下我在这里遗漏了什么吗？可能函数对象没有正常形式？
考虑以下目标：
Goal forall (x y: I = I), x = y.
Proof.
Abort.
Goal forall (x y: tt = tt), x = y.
Proof.
Abort.
这两个I和tt是单类型的成员。前者住Prop，后者住Set。这些是非常简单的类型，因此我不希望它们在任何设置中都支持丰富的相等类型。这些目标是否可以在 Coq 中证明而不诉诸身份证明公理的唯一性？
构造函数策略允许您通过自动应用构造函数来实现归纳数据类型的目标。然而，定义相等在 Coq 中不是归纳产品。那么为什么 Coq 接受这个证明呢？
Example zeqz : 0 = 0. constructor.
在 Haskell 中寻找一个可以将任意深度嵌套列表展平的函数时，即一个concat递归应用并在最后一次迭代（使用非嵌套列表）时停止的函数，我注意到这需要有一个更灵活的类型系统，因为列表深度不同，输入类型也不同。事实上，有几个 stackoverflow 问题——比如这个问题——其中的回答指出“不存在一个函数可以‘查看’不同深度的不同嵌套列表”。
编辑：一些答案提供哈斯克尔的解决方法，无论是对自定义数据类型或具有帮助TypeFamilies或MultiParamTypeClasses（如在由Noughtmare下面的答案，或者通过“Landei”在回答上述职位或由“约翰·L”回答这个职位）。然而，这些家族和类似乎也是因为缺少/替代haskell 中的依赖类型而引入的（例如，haskell wiki声明“类型家族 [...] 很像依赖类型”。
我现在的问题是，如果这是真的，哈斯克尔的确originially没有定义此类功能（即如扁平化不同深度的列表），而且，如果这些问题就会消失，一旦一个移动到语言实现由依赖类型？（例如 Idris、Agda、Coq 等）我没有使用这些语言的经验，这就是我问的原因。
例如，在 Idris 网站上，据说“类型可以作为参数传递给函数”，因此，我认为，在列表扁平化的情况下，可以简单地将列表的类型作为参数传递并实现以直接的方式获得所需的功能。这可能吗？
一个后续问题也将是：在haskell 中解决这个问题的那些族和类是否在haskell 中提供了依赖类型理论的完整实现，或者如果没有，有什么重要区别？