What strategy should be used to prove this result (at the end, with Admitted)? Thanks in advance for any hints. :slight_smile:
Hopefully it is true theorem. I already got burned when I had wrong intuition and there was counterexample found.
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.
Edit: Based on counterexample found by Yves, one should add at least two more conditions.
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.
Even then there are counterexamples, for example:
assignments (assign aux (num x1) :: assign (num x1) (num x0) :: nil) ::
conditional (GT x0 x1)
(assignments nil)
(assignments (assign (num x0) aux :: nil)) :: nil.
This is more a question of mathematics than a Coq question.
there is probably a counter example. Please investigate this: an assignment shuffles the values of registers aux, x1, x2, ..., x7. However, when you look for permutations, you only look at values of x1, x2, ..., x7.
suppose you have one step that stores the value of x1 into aux, duplicates the value of x2 into x1 and x2, and leaves all other registers unchanged. When looking only at the list of values in x1, ..., x7, this step is not a permutation (because of the duplication). Let's call this step s1.
Then consider the step s2 that duplicates the value of aux into aux and x1 and leaves all other values unchanged. Again, when looking only at registers x1, ..., x7, this is not a permutation, because it introduces a value that was not in these registers before.
Now s1::s2::nil is the identity function on registers x1, ..., x7. It is a permutation. But neither s1 nor (s2::nil) are permuting steps or permutation algorithms.
For a Coq counter example, it is enough to prove that s1 is not a permuting step. Here it is:
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.