应该使用什么策略来证明这个结果(最后，使用Admitted(？提前感谢您的任何提示。：轻微微笑：
希望它是真定理。当我有错误的直觉时，我已经被烧伤了，并且发现了反例。
Require Import Permutation List Lia FunInd Recdef.
Set Implicit Arguments.
Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
Inductive variable := aux | num: value -> variable.
Definition variable_eq_dec (x y: variable): {x=y} + {x<>y}.
Proof.
destruct x, y.
+ left; auto.
+ right; abstract congruence.
+ right; abstract congruence.
+ destruct v, v0; try (left; abstract congruence); (right; abstract congruence).
Defined.
Inductive assignment := assign: variable -> variable -> assignment.
Inductive comparison := GT: forall (more less: value), comparison.
Inductive step :=
| assignments: forall (L: list assignment), step
| conditional: forall (c: comparison) (positive negative: step), step.
Definition algorithm := list step.
Definition instantation := variable -> nat.
Definition list_of_values (i: instantation) :=
i (num x0) :: i (num x1) :: i (num x2) :: i (num x3) :: i (num x4) :: i (num x5) :: i (num x6) :: i (num x7) :: nil.
Definition is_permutation (i1 i2: instantation) := Permutation (list_of_values i1) (list_of_values i2).
Definition run_assignment (a: assignment) (i: instantation): instantation :=
match a with
| assign v1 v2 => fun x => if variable_eq_dec x v1 then i v2 else i x end.
Fixpoint run_assignment_list (L: list assignment): instantation -> instantation :=
match L with
| nil => fun i => i
| a :: l => fun i => run_assignment_list l (run_assignment a i)
end.
Fixpoint run_step (s: step) (i: instantation): instantation :=
match s with
| assignments L => run_assignment_list L i
| conditional (GT more less) pos neg =>
if Compare_dec.gt_dec (i (num more)) (i (num less)) then run_step pos i else run_step neg i
end.
Fixpoint run_algorithm (a: algorithm): instantation -> instantation :=
match a with
| nil => fun i => i
| s :: t => fun i => run_algorithm t (run_step s i)
end.
Definition permuting_step (s: step) := forall (i: instantation), is_permutation i (run_step s i).
Definition permuting_algorithm (a: algorithm) := forall (i: instantation), is_permutation i (run_algorithm a i).
Theorem permuting_algorithm_aux00 (a: algorithm) (s: step):
permuting_algorithm (s :: a) -> permuting_algorithm a / permuting_step s.
Proof.
Admitted.
编辑：根据伊夫发现的反例，至少应该再添加两个条件。
Fixpoint compact_assignments (a: algorithm): Prop :=
match a with
| nil => True
| assignments L :: assignments L0 :: t => False
| x :: t => compact_assignments t
end.
Fixpoint no_useless_comparisons_in_step (s: step): Prop :=
match s with
| assignments L => True
| conditional (GT a b) pos neg => a <> b / no_useless_comparisons_in_step pos / no_useless_comparisons_in_step neg
end.
Definition no_useless_comparisons (a: algorithm) := forall x, In x a -> no_useless_comparisons_in_step x.
Definition compact_algorithm (a: algorithm) := compact_assignments a / no_useless_comparisons a.
Theorem permuting_algorithm_aux00 (a: algorithm) (s: step):
compact_algorithm (s :: a) -> permuting_algorithm (s :: a) -> permuting_algorithm a / permuting_step s.
Proof.
Admitted.
即便如此，也有反例，例如：
assignments (assign aux (num x1) :: assign (num x1) (num x0) :: nil) ::
conditional (GT x0 x1)
(assignments nil)
(assignments (assign (num x0) aux :: nil)) :: nil.
这更像是一个数学问题，而不是一个Coq问题。
可能还有一个反例。请研究一下：赋值搅乱寄存器aux、x1、x2、…的值。。。，然而，当你寻找排列时，你只会看到x1，x2，…的值。。。，x7.
假设您有一个步骤，将x1的值存储到aux中，将x2的值复制到x1和x2中，并保持所有其他寄存器不变。当仅查看x1、…中的值的列表时。。。，x7，这个步骤不是置换(因为重复(。让我们称之为步骤s1。
然后考虑将aux的值复制到aux和x1中并保持所有其他值不变的步骤s2。再次，当仅查看寄存器x1、…时。。。，x7，这不是一个置换，因为它引入了一个以前不在这些寄存器中的值。
现在CCD_。。。，x7.它是一个排列。但s1和(s2:：nil(都不是置换步骤或置换算法。
对于Coq反例，足以证明s1不是置换步骤。这是：
Definition la1 :=
assign aux (num x1) ::
assign (num x1) (num x2):: nil.
Definition la2 :=
assign (num x1) aux :: nil.
Definition s1 := assignments la1.
Definition s2 := assignments la2.
Lemma pa_all : permuting_algorithm (s1 :: s2:: nil).
Proof.
intros i.
unfold s1, s2, is_permutation.
unfold list_of_values; simpl.
apply Permutation_refl.
Qed.
Lemma not_permuting_step_s1 : ~permuting_step s1.
Proof.
unfold s1, permuting_step, is_permutation.
set (f := fun x => if variable_eq_dec x (num x1) then 0 else 1).
intros abs.
assert (abs1 := abs f).
revert abs1.
unfold list_of_values, f; simpl; intros abs1.
absurd (In 0 (1::1::1::1::1::1::1::1::nil)).
simpl; intuition easy.
apply (Permutation_in 0 abs1); simpl; right; left; easy.
Qed.