有证明给定定理的好策略吗？

如何解决有证明给定定理的好策略吗？

应该使用什么策略来证明这个结果（最后，被承认）？预先感谢您的任何提示。 ：slight_smile：

希望这是真的定理。直觉错误时我已经很生气，发现了反例。

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.

编辑：根据Yves发现的反例，应该再添加至少两个条件。

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，...，x7的值。但是，当您寻找排列时，您只会看到x1，x2，...，x7的值。

假设您有一个步骤将x1的值存储到aux，将x2的值复制到x1和x2，并使所有其他寄存器保持不变。仅查看x1，...，x7中的值列表时，此步骤不是置换（由于重复）。叫这个 步骤s1。

然后考虑步骤s2，该步骤将aux的值复制到aux和x1中，并使所有其他值保持不变。同样，仅查看寄存器x1，...，x7时，这不是排列，因为它引入了以前不在这些寄存器中的值。

现在s1::s2::nil是寄存器x1，...，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.