computing n perm k the stupid way

perms.v

 Require Import SetoidClass Nat.

Fixpoint Fin n :=
  match n with
  | 0 => Empty_set
  | S m => (unit + Fin m)%type
  end.

Class Finite(X : Type)`{Setoid X} := {
  card : nat;
  to_fin : X -> Fin card;
  to_fin_morph : forall x x', x == x' -> to_fin x = to_fin x;
  from_fin : Fin card -> X;
  to_from : forall i, to_fin (from_fin i) = i;
  from_to : forall x, from_fin (to_fin x) == x;
  }.

Instance function_setoid{X Y} : Setoid (X -> Y) := {|
  equiv := fun f g => forall x, f x = g x
  |}.
Proof.
  split; intros f g; congruence.
Defined.

Class Equiv(X Y : Type) := {
  equiv_to : X -> Y;
  equiv_from : Y -> X;
  equiv_to_from : forall y, equiv_to (equiv_from y) = y;
  equiv_from_to : forall x, equiv_from (equiv_to x) = x;
  }.

Instance equiv_refl{X} : Equiv X X := {|
  equiv_to := fun x => x;
  equiv_from := fun x => x;
  equiv_to_from := @eq_refl _;
  equiv_from_to := @eq_refl _
  |}.

Instance equiv_sym{X Y}`{Equiv X Y} : Equiv Y X := {|
  equiv_to := equiv_from;
  equiv_from := equiv_to;
  equiv_to_from := equiv_from_to;
  equiv_from_to := equiv_to_from
  |}.

Instance equiv_trans{X Y Z}`{Equiv X Y, Equiv Y Z} : Equiv X Z.
Proof.
  refine {| equiv_to := fun x => equiv_to (equiv_to x);
            equiv_from := fun z => equiv_from (equiv_from z);
            equiv_to_from := _;
            equiv_from_to := _
         |}.
  - intro.
    repeat rewrite equiv_to_from; reflexivity.
  - intro.
    repeat rewrite equiv_from_to; reflexivity.
Defined.

Instance equiv_plus_times_distr{X Y Z} : Equiv ((X + Y) * Z) (X * Z + Y * Z).
Proof.
  refine {| equiv_to := fun p => match p with
                                 | (inl x,z) => inl (x,z)
                                 | (inr y,z) => inr (y,z)
                                 end;
            equiv_from := fun s => match s with
                                   | inl (x,z) => (inl x,z)
                                   | inr (y,z) => (inr y,z)
                                   end;
            equiv_to_from := _;
            equiv_from_to := _
         |}.
  - intros [[x z]|[y z]]; reflexivity.
  - intros [[x|y] z]; reflexivity.
Defined.

Instance equiv_times_one{X} : Equiv (unit * X) X.
Proof.
  refine {| equiv_to := snd;
            equiv_from := pair tt;
            equiv_to_from := _;
            equiv_from_to := _
         |}.
  - intro; reflexivity.
  - intros [[]]; reflexivity.
Defined.

Instance equiv_plus_zero{X} : Equiv (Empty_set + X) X.
Proof.
  refine {| equiv_to := fun s => match s with
                                 | inl e => match (e : Empty_set) with end
                                 | inr x => x
                                 end;
            equiv_from := fun x => inr x;
            equiv_to_from := _;
            equiv_from_to := _
         |}.
  - intro; reflexivity.
  - intros [[]|x]; reflexivity.
Defined.

Instance equiv_plus_assoc{X Y Z} : Equiv (X + (Y + Z)) ((X + Y) + Z).
Proof.
  refine {| equiv_to := fun s => match s with
                        | inl x => inl (inl x)
                        | inr (inl y) => inl (inr y)
                        | inr (inr z) => inr z
                        end;
            equiv_from := fun s => match s with
                                   | inl (inl x) => inl x
                                   | inl (inr y) => inr (inl y)
                                   | inr z => inr (inr z)
                                   end;
            equiv_to_from := _;
            equiv_from_to := _
         |}.
  - intros [[|]|]; reflexivity.
  - intros [|[|]]; reflexivity.
Defined.

Instance equiv_l_cong{X Y Z}`{Equiv Y Z} : Equiv (X + Y) (X + Z).
Proof.
  refine {| equiv_to := fun s => match s with
                                 | inl x => inl x
                                 | inr y => inr (equiv_to y)
                                 end;
            equiv_from := fun s => match s with
                                   | inl x => inl x
                                   | inr z => inr (equiv_from z)
                                   end;
            equiv_to_from := _;
            equiv_from_to := _
         |}.
  - intros [|].
    * reflexivity.
    * rewrite equiv_to_from; reflexivity.
  - intros [|].
    * reflexivity.
    * rewrite equiv_from_to; reflexivity.
Defined.

Instance equiv_r_cong{X Y Z}`{Equiv X Y} : Equiv (X + Z) (Y + Z).
Proof.
  refine {| equiv_to := fun s => match s with
                                 | inl x => inl (equiv_to x)
                                 | inr z => inr z
                                 end;
            equiv_from := fun s => match s with
                                   | inl y => inl (equiv_from y)
                                   | inr z => inr z
                                   end;
            equiv_to_from := _;
            equiv_from_to := _
         |}.
  - intros [|].
    * rewrite equiv_to_from; reflexivity.
    * reflexivity.
  - intros [|].
    * rewrite equiv_from_to; reflexivity.
    * reflexivity.
Defined.

Instance equiv_cong{X X' Y Y'}`{Equiv X X', Equiv Y Y'} : Equiv (X + Y) (X' + Y').
Proof.
  apply (@equiv_trans _ (X' + Y) _).
  exact equiv_r_cong.
  exact equiv_l_cong.
Defined.

Instance Fin_plus{m n} : Equiv (Fin (m + n)) (Fin m + Fin n)%type.
Proof.
  induction m.
  simpl.
  exact equiv_sym.
  simpl.
  apply (@equiv_trans _ (unit + (Fin m + Fin n)) _).
  exact equiv_l_cong.
  apply equiv_sym.
Defined.

Instance Fin_mult{m n} : Equiv (Fin (m * n)) (Fin m * Fin n)%type.
Proof.
  induction m.
  - refine {| equiv_to := fun (e : Empty_set) => match e with end;
              equiv_from := fun '(e,_) => match (e : Empty_set) with end;
              equiv_to_from := _;
              equiv_from_to := _
           |}.
    * intros [[]].
    * intros [].
  - simpl.
    apply (@equiv_trans _ ((unit * Fin n) + (Fin m * Fin n)) _).
    * apply (@equiv_trans _ (Fin n + Fin (m * n)) _).
      ** exact Fin_plus.
      ** apply (@equiv_cong).
        *** apply equiv_sym.
        *** exact IHm.
    * apply equiv_sym.
Defined.

Instance Fin_func_Finite{m n} : Finite (Fin m -> Fin n).
Proof.
  induction m.
  - refine {| card := 1;
           to_fin := fun _ => inl tt;
           from_fin := fun _ (e : Empty_set) => match e with end;
           to_fin_morph := _;
           to_from := _;
           from_to := _
         |}.
    * intros; reflexivity.
    * intros [[]|[]]; reflexivity.
    * intros f [].
  - simpl.
    refine {| card := n * card;
              to_fin := fun f => @equiv_from _ _ (@Fin_mult _ _) (f (inl tt), to_fin (fun s => f (inr s)));
              from_fin := fun i => let '(j,k) := @equiv_to _ _ (@Fin_mult _ _) i in fun s => match s with
                 | inl _ => j
                 | inr m => from_fin k m
                 end;
              to_fin_morph := _;
              to_from := _;
              from_to := _
           |}.
    * intros. reflexivity.
    * intro.
      destruct (equiv_to i) eqn:G.
      rewrite to_from.
      rewrite <- G.
      rewrite equiv_from_to.
      reflexivity.
    * intros f s.
      rewrite equiv_to_from.
      destruct s as [[]|].
      ** reflexivity.
      ** destruct IHm.
      simpl.
      apply from_to0.
Defined.

Class Dec(P : Prop) := {
  dec : {P} + {~P}
  }.

Instance Dec_impl{P Q}`{Dec P, Dec Q} : Dec (P -> Q).
Proof.
  destruct H,H0.
  constructor.
  tauto.
Defined.

Lemma Fin_dec_eq : forall n (i j : Fin n), {i = j} + {i <> j}.
Proof.
  induction n.
  - intros [].
  - intros [[]|] [[]|].
    * left; reflexivity.
    * right; discriminate.
    * right; discriminate.
    * destruct (IHn f f0).
      ** left; congruence.
      ** right; congruence.
Defined.

Instance Dec_Fin_eq{n}(i j : Fin n) : Dec (i = j) := {|
  dec := Fin_dec_eq n i j
  |}.

Instance Dec_Fin_forall{n P}{Pd : forall i : Fin n, Dec (P i)} : Dec (forall i, P i).
Proof.
  constructor.
  induction n.
  - left; intros [].
  - destruct (Pd (inl tt)) as [[|]].
    * destruct (IHn _ (fun j => Pd (inr j))).
      ** left; intros [[]|]; auto.
      ** right; intro.
         apply n0.
         intro; apply H.
    * right; intro.
      apply n0.
      apply H.
Defined.

Fixpoint count(n : nat) : forall (P : Fin n -> Prop), (forall i, Dec (P i)) -> nat :=
  match n return forall (P : Fin n -> Prop), (forall i, Dec (P i)) -> nat with
  | 0 => fun _ _ => 0
  | S m => fun P Pd => let k := count m _ (fun j => Pd (inr j)) in
              match @dec (P (inl tt)) (Pd (inl tt)) with
              | left _ => S k
              | right _ => k
              end
  end.

Definition inj{X Y}(f : X -> Y) := forall x x', f x = f x' -> x = x'.

Lemma dec_inj : forall m n (f : Fin m -> Fin n), Dec (inj f).
Proof.
  intros.
  unfold inj.
  apply Dec_Fin_forall.
Defined.

Definition dec_count{X}`{Finite X}(P : X -> Prop)(Pd : forall x, Dec (P x)) : nat :=
  count _ (fun i => P (from_fin i)) _.

Definition perm : nat -> nat -> nat :=
  fun m n => dec_count inj (dec_inj n m).

Compute perm 4 3.