toggle_binary.v

Require Import Program.Equality.
Require Import Relations.Relation_Operators.
Require Relations.Operators_Properties.
Require Import Vectors.Vector.

Import VectorDef.VectorNotations.

Module OP := Operators_Properties.

Definition binseq n := VectorDef.t bool n.

Notation "'b0'" := false.
Notation "'b1'" := true.

Fixpoint zeros n : VectorDef.t bool n :=
  match n with
  | 0 => nil bool
  | S n => VectorDef.cons bool b0 n (zeros n)
  end
.

Inductive step : forall n, binseq n -> binseq n -> Prop :=
| step_change_first {n} b bs : step (S n) (b :: bs) (negb b :: bs)
| step_change_next n {m} b bs : step (n + S (S m)) (zeros n ++ b1 :: b :: bs) (zeros n ++ b1 :: negb b :: bs)
.
Local Hint Constructors step : core.

Definition steps n := clos_refl_trans_1n (binseq n) (step n).

Lemma step_reachability_0_extension : forall {n bs0 bs1}
    (subreachability : step n bs0 bs1),
    steps (S n) (b0 :: bs0) (b0 :: bs1).
Proof with eauto.
  intros.
  destruct subreachability.
  - do 3 try eapply rt1n_trans; try (now apply rt1n_refl); [| now apply (step_change_next 0) |]; now constructor.
  - assert (one_more_zero : b0 :: zeros n = zeros (S n))...
    repeat rewrite append_comm_cons, one_more_zero.
    now apply OP.clos_rt1n_step, (step_change_next (S n)).
Qed.

Lemma steps_reachability_0_extension : forall {n bs0 bs1}
    (subreachability : steps n bs0 bs1),
    steps (S n) (b0 :: bs0) (b0 :: bs1).
Proof with eauto.
  intros.
  induction subreachability as [bs | bs0 bs1 bs2 step_subreachability _ subreachability_IH];
    try (now constructor).
  apply step_reachability_0_extension in step_subreachability.
  eapply OP.clos_rt_rt1n_iff, rt_trans; apply OP.clos_rt_rt1n_iff...
Qed.

Lemma steps_reachability_extension : forall {n} b {bs0 bs1}
    (subreachability : steps n bs0 bs1),
    steps (S n) (b :: bs0) (b :: bs1).
Proof with eauto using rt1n_refl, rt1n_trans.
  destruct b; intros; try (now apply steps_reachability_0_extension)...
  eapply rt1n_trans...
  eapply OP.clos_rt_rt1n_iff, rt_trans; apply OP.clos_rt_rt1n_iff;
    try eapply (steps_reachability_0_extension subreachability)...
Qed.

Theorem steps_reachability : forall {n bs0 bs1},
    steps n bs0 bs1.
Proof with eauto.
  induction n as [| n IH];
    dependent destruction bs0; dependent destruction bs1; try (now apply rt1n_refl).
  rename h into h0, h0 into h1.
  destruct h0, h1;
    try apply steps_reachability_extension; eauto;
      try eapply rt1n_trans; eauto;
        now apply steps_reachability_extension.
Qed.