Require Import Extraction.
Require Export ListExt NatExt Matrix.

Generalizable Variable A Aadd Azero Aopp Amul Aone Ainv.

Lemma in_concat_length : forall {A} (d : dlist A) n,
    (forall l, In l d -> length l = n) -> length (concat d) = n * length d.
Proof.
  induction d; intros; simpl in *; auto.
  rewrite app_length. rewrite IHd with (n:=n); auto. rewrite H; auto. lia.
Qed.

Lemma nat_S_ltb_S : forall n m : nat, ((S n <? S m) = (n <? m))%nat.
Proof. intros. bdestruct (n <? m)%nat; bdestruct (S n <? S m)%nat; auto; lia. Qed.

Lemma lswap_cons_S_S : forall {A Azero} (l : list A) (a : A) (i j : nat),
    i < length l -> j < length l ->
    lswap Azero (a :: l) (S i) (S j) = a :: (lswap Azero l i j).
Proof.
  intros. unfold lswap. simpl. rewrite !nat_S_ltb_S.
  bdestruct (length l >? i); bdestruct (length l >? j); auto.
Qed.

Lemma lswap_cons_0_S : forall {A Azero} (l : list A) (a : A) (j : nat),
    j < length l ->
    lswap Azero (a :: l) 0 (S j) = nth j l Azero :: lset l j a.
Proof.
  intros. unfold lswap. simpl.
  rewrite nat_S_ltb_S. bdestruct (length l >? j); try easy.
Qed.

Lemma fold_left_rebase :
  forall {A B} (f : A -> B -> A) (fa : A -> A -> A) (l : list B) (a1 a2 : A),
    (forall a1 a2 b, f (fa a1 a2) b = fa (f a1 b) a2) ->
    fold_left f l (fa a1 a2) = fa (fold_left f l a1) a2.
Proof.
  intros. revert a1 a2.
  induction l; intros; simpl in *; auto.
  rewrite <- IHl. f_equal. auto.
Qed.

Module method1.

  Section def.
    Context {A} {Azero : A}.

    Fixpoint pick (l : list A) (k : nat) : A * list A :=
      match k with
      | 0 => (hd Azero l, tl l)
      | S k' =>
          match l with
          | [] => (Azero, [])
          | x :: l' =>
              let (a,l0) := pick l' k' in
              (a, ([x] ++ l0)%list)
          end
      end.

    Fixpoint permAux (n : nat) (l : list A) : list (list A) :=
      match n with
      | 0 => [[]]
| S n' =>
          concat
            (map
               (fun k =>
                  let '(x, lx) := k in
                  map (cons x) (permAux n' lx))
               (map (fun i => pick l i) (seq 0 n)))
      end.

    Definition perm (l : list A) : list (list A) := permAux (length l) l.
  End def.


End method1.

Module method2.
  Open Scope list_scope.

  Section def.
    Context {A} {Azero : A}.

    Fixpoint pick {A} (l : list A) (remaining : list A) : list (A * list A) :=
      match l with
      | [] => []
      | hl :: tl =>
          (hl, remaining ++ tl) :: (pick tl (remaining ++ [hl]))
      end.

    Fixpoint permAux {A} (n : nat) (l : list A) : list (list A) :=
      match n with
      | 0 => [[]]
| S n' =>
          concat
            (map
               (fun k =>
                  let '(x, lx) := k in
                  map (cons x) (permAux n' lx))
               (pick l []))
      end.

    Definition perm (l : list A) : list (list A) := permAux (length l) l.
  End def.


End method2.

Module Export method3.

  Section def.
    Context {A : Type}.

    Fixpoint perm1 (a : A) (l : list A) : list (list A) :=
      match l with
      | [] => [[a]]
| hl :: tl => (a :: l) :: (map (cons hl) (perm1 a tl))
      end.

    Fixpoint perm (l : list A) : list (list A) :=
      match l with
      | [] => [[]]
| hl :: tl => concat (map (perm1 hl) (perm tl))
      end.
  End def.



  Section props.
    Context {A : Type}.
    Context {AeqDec : Dec (@eq A)}.

    Lemma perm1_length : forall a (l : list A), length (perm1 a l) = S (length l).
    Proof. induction l; simpl; auto. rewrite map_length. auto. Qed.

    Lemma perm1_not_nil : forall a (l : list A), perm1 a l <> [].
    Proof. induction l; simpl; try easy. Qed.

    Lemma perm_not_nil : forall (l : list A), perm l <> [].
    Proof.
      induction l; simpl; try easy.
      destruct (perm l) eqn:E; simpl; try easy.
      destruct (perm1 a l0) eqn:E1; try easy.
      apply perm1_not_nil in E1; auto.
    Qed.

    Lemma hd_perm : forall (l : list A), hd [] (perm l) = l.
    Proof.
      induction l; auto. simpl.
      destruct (perm l) as [|l0 dl] eqn:H1.
      - apply perm_not_nil in H1. easy.
      - simpl in *. subst. destruct l; simpl in *; auto.
    Qed.

    Lemma in_perm1_length : forall (l : list A) (a : A) (x : list A),
        In x (perm1 a l) -> length x = S (length l).
    Proof.
      induction l; intros; simpl in *.
      - destruct H; try easy. subst; auto.
      - destruct H; subst; auto.
        apply in_map_iff in H. destruct H as [x0 [H H1]]. subst.
        apply IHl in H1. simpl. auto.
    Qed.

    Lemma in_perm_length : forall (l x : list A),
        In x (perm l) -> length x = length l.
    Proof.
      induction l; intros; simpl in *.
      - destruct H; try easy. subst. auto.
      - apply in_concat in H. destruct H as [dl [H1 H2]].
        apply in_map_iff in H1. destruct H1 as [l0 [H3 H4]].
        subst. apply IHl in H4. rewrite <- H4.
        apply in_perm1_length in H2; auto.
    Qed.

    Lemma perm_cons_length : forall (l : list A) (a : A),
        length (perm (a :: l)) = (S (length l)) * (length (perm l)).
    Proof.
      destruct l; intros; auto.
      unfold perm; fold (perm (a :: l)).
      rewrite in_concat_length with (n:=S (length (a::l))).
      - rewrite map_length. auto.
      - intros. remember (a :: l) as d.
        apply in_map_iff in H. destruct H as [x [H H1]].
        apply in_perm_length in H1. rewrite <- H. rewrite perm1_length. auto.
    Qed.

    Lemma length_perm : forall (l : list A), length (perm l) = fact (length l).
    Proof.
      induction l. auto.
      rewrite perm_cons_length.
      simpl. rewrite IHl. auto.
    Qed.

    Lemma in_perm1 : forall (l : list A) (a : A) (l0 : list A),
        In l0 (perm1 a l) -> (forall x, In x l0 -> x = a \/ In x l).
    Proof.
      induction l; intros; simpl in *.
      - destruct H; try easy. subst; simpl in *. destruct H0; auto.
      - destruct H; subst; simpl in *.
        + destruct H0; auto.
        + apply in_map_iff in H. destruct H as [l1 [H1 H2]]. subst. simpl in *.
          destruct H0; auto. apply IHl with (x:=x) in H2; auto. tauto.
    Qed.

    Lemma in_perm : forall (l : list A) (l0 : list A),
        In l0 (perm l) -> (forall x, In x l0 -> In x l).
    Proof.
      induction l; intros; simpl in *.
      - destruct H; try easy. subst; auto.
      - destruct (Aeqdec a x); auto. right.
        apply in_concat in H. destruct H as [d [H H1]].
        apply in_map_iff in H. destruct H as [l1 [H2 H3]].
        rewrite <- H2 in H1.
        apply IHl with (l0:=l1); auto.
        apply in_perm1 with (x:=x) in H1; auto. destruct H1; auto.
        subst; easy.
    Qed.
  End props.

  Section wf_perm.
    Context {A : Type}.
    Context {AeqDec : Dec (@eq A)}.

    Definition wf_perm (l : list A) : Prop := NoDup l.
  End wf_perm.

  Section perm_index.
    Open Scope nat_scope.
    Notation perm := (@perm nat).

    Lemma perm_index_lt : forall n i a, In a (perm (seq 0 n)) -> i < n -> nth i a 0 < n.
    Proof.
      intros. apply in_perm with (x:=nth i a 0) in H.
      - apply in_seq in H. lia.
      - apply nth_In. apply in_perm_length in H. rewrite seq_length in H. lia.
    Qed.

  End perm_index.

End method3.

Section ronum.
  Context {A} {Altb : A -> A -> bool}.
  Infix "<?" := Altb.

  Definition ronum1 (a : A) (l : list A) : nat :=
    fold_left (fun (n : nat) (b : A) => n + (if b <? a then 1 else 0)) l 0.

  Fixpoint ronum (l : list A) : nat :=
    match l with
    | [] => 0
    | x :: l' => ronum1 x l' + ronum l'
    end.

  Context {Azero : A}.
  Notation lswap := (lswap Azero).

  Lemma ronum1_cons : forall (l : list A) a b,
      ronum1 b (a :: l) = (if a <? b then 1 else 0) + ronum1 b l.
  Proof.
    intros. unfold ronum1. simpl.
    remember (fun (n : nat) (b0 : A) => n + (if b0 <? b then 1 else 0)) as f.
    remember (if a <? b then 1 else 0) as n.
    replace n with (0 + n) by lia.
    rewrite fold_left_rebase; try lia.
    intros. rewrite Heqf. fin.
  Qed.

  Lemma ronum1_gt0 : forall (l : list A) (i : nat) (a : A),
      i < length l -> nth i l Azero <? a = true -> ronum1 a l > 0.
  Proof.
    induction l; intros; simpl in *. lia. destruct i.
    - rewrite ronum1_cons. rewrite H0. lia.
    - rewrite ronum1_cons.
      apply lt_S_n in H. specialize (IHl i a0 H H0). lia.
  Qed.

  Lemma ronum1_lset_invariant : forall (l : list A) (i : nat) (a b : A),
      i < length l ->
      ronum1 b (lset l i a) + (if nth i l Azero <? b then 1 else 0) =
        ronum1 b l + (if a <? b then 1 else 0).
  Proof.
    induction l; intros; simpl in *. lia. destruct i.
    - unfold ronum1. simpl.
      remember (fun (n : nat) (b0 : A) => n + (if b0 <? b then 1 else 0)) as f.
      remember (if a0 <? b then 1 else 0) as n.
      remember (if a <? b then 1 else 0) as m.
      replace n with (0 + n) by lia.
      replace m with (0 + m) at 2 by lia.
      rewrite !fold_left_rebase; try lia; intros.
      all: rewrite Heqf; lia.
    - rewrite !ronum1_cons. rewrite <- !Nat.add_assoc. rewrite IHl; auto. lia.
  Qed.

  Lemma ronum1_lset : forall (l : list A) (i : nat) (a b : A),
      i < length l ->
      ronum1 b (lset l i a) =
        ronum1 b l + (if a <? b then 1 else 0) -
        (if nth i l Azero <? b then 1 else 0).
  Proof. intros. pose proof (ronum1_lset_invariant l i a b H). lia. Qed.

  Lemma ronum1_lswap : forall (l : list A) (a : A) (i j : nat),
      i < length l -> j < length l -> i < j ->
      ronum1 a (lswap l i j) = ronum1 a l.
  Proof.
    induction l; intros; simpl in *. lia.
    destruct i, j; simpl in *; try easy.
    - rewrite lswap_cons_0_S; try lia. rewrite !ronum1_cons.
      pose proof (ronum1_lset_invariant l j a a0). lia.
    - apply lt_S_n in H,H0,H1.
      rewrite lswap_cons_S_S; auto.
      rewrite !ronum1_cons. rewrite IHl; auto.
  Qed.

  Lemma ronum_lswap : forall (l : list A) (i j : nat),
      i < length l -> j < length l -> i < j ->
      ronum (lswap l i j) = ronum l + S (2 * (j - S i)).
  Proof.
    induction l; intros; simpl in *. lia.
    destruct i, j; try lia; simpl in *.
    2:{
      apply lt_S_n in H,H0,H1.
      rewrite lswap_cons_S_S; auto. simpl. rewrite IHl; auto.
      pose proof (nat_add_ASGroup).
      asgroup.       rewrite ronum1_lswap; auto. }
    - clear IHl.
      rewrite lswap_cons_0_S; try lia. simpl.
      rewrite ronum1_lset; try lia.

    Admitted.

End ronum.

Section test.
  Let ronum1 := @ronum1 nat Nat.leb.
  Let ronum := @ronum nat Nat.leb.

End test.

Section parity.
  Context {A} {Altb : A -> A -> bool}.

  Definition oddPerm (l : list A) : bool := odd (ronum (Altb:=Altb) l).

End parity.

Section permExchg.
  Context {A} {Altb : A -> A -> bool} (Azero : A).

  Notation ronum := (ronum (Altb:=Altb)).
  Notation oddPerm := (oddPerm (Altb:=Altb)).
  Notation lswap := (lswap Azero).

  Theorem swap_perm_parity : forall (l : list A) (i0 i1 : nat),
      NoDup l ->
      i0 < length l -> i1 < length l -> i0 < i1 ->
      oddPerm (lswap l i0 i1) = negb (oddPerm l).
  Proof.
    intros.
    unfold oddPerm. rewrite ronum_lswap; auto.
    rewrite Nat.add_succ_r. rewrite Nat.odd_succ. rewrite Nat.negb_odd.
    rewrite Nat.even_add_mul_2. auto.
  Qed.

End permExchg.