(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega.

Require Import utils.

Set Implicit Arguments.

Inductive pos : nat -> Set :=
  | pos_fst : forall n, pos (S n)
  | pos_nxt : forall n, pos n -> pos (S n).

Arguments pos_fst {n}.
Arguments pos_nxt {n}.

Notation pos0  := (@pos_fst _).
Notation pos1  := (pos_nxt pos0).
Notation pos2  := (pos_nxt pos1).
Notation pos3  := (pos_nxt pos2).
Notation pos4  := (pos_nxt pos3).
Notation pos5  := (pos_nxt pos4).
Notation pos6  := (pos_nxt pos5).
Notation pos7  := (pos_nxt pos6).
Notation pos8  := (pos_nxt pos7).
Notation pos9  := (pos_nxt pos8).
Notation pos10 := (pos_nxt pos9).
Notation pos11 := (pos_nxt pos10).
Notation pos12 := (pos_nxt pos11).
Notation pos13 := (pos_nxt pos12).
Notation pos14 := (pos_nxt pos13).
Notation pos15 := (pos_nxt pos14).
Notation pos16 := (pos_nxt pos15).
Notation pos17 := (pos_nxt pos16).
Notation pos18 := (pos_nxt pos17).
Notation pos19 := (pos_nxt pos18).
Notation pos20 := (pos_nxt pos19).

Definition pos_iso n m : n = m -> pos n -> pos m.
(* Goal: forall _ : not (@eq (pos n) p q), and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool false true) *)
(* Goal: iff (and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool true true)) (not (@eq (pos n) p q)) *)
Proof. intros []; auto. Defined.

Section pos_inv.

  Let pos_inv_t n := 
    match n as x return pos x -> Set with 
      | 0   => fun _ => False 
      | S n => fun i => (( i = pos_fst ) + { p | i = pos_nxt p })%type
    end.

  Let pos_inv : forall n p, @pos_inv_t n p.
  Proof.
(* Goal: forall (n : nat) (p : pos n), @pos_inv_t n p *)
    intros _ [ | n p ]; simpl; [ left | right ]; auto; exists p; auto.
  Defined.

  Definition pos_O_inv : pos 0 -> False.
  Proof. apply pos_inv. Defined.

  Definition pos_S_inv n (p : pos (S n)) : ( p = pos_fst ) + { q | p = pos_nxt q }.
  Proof. apply (pos_inv p). Defined.

  Definition pos_nxt_inj n (p q : pos n) (H : pos_nxt p = pos_nxt q) : p = q :=
    match H in _ = a return 
       match a as a' in pos m return 
           match m with 
             | 0 => Prop 
             | S n' => pos n' -> Prop 
           end with
         | pos_fst   => fun _  => True 
         | pos_nxt y => fun x' => x' = y 
       end p with 
     | eq_refl => eq_refl
   end.

End pos_inv.

Arguments pos_S_inv {n} p /.

Section pos_invert.

  (* Position inversion, "singleton elimination" free version 
     One problem remains to fully use it ... it is not
     correctly traversed by type checking algorithm
     of fixpoints (structural recursion)
     
     pos_S_inv work better in that respect 
  *)

  Let pos_invert_t n : (pos n -> Type) -> Type :=
    match n with
        0   => fun P => True
      | S n => fun P => (P (pos_fst) * forall p, P (pos_nxt p))%type
    end.

  Let pos_invert n : forall (P : pos n -> Type), pos_invert_t P -> forall p, P p.
  Proof.
(* Goal: forall (P : forall _ : pos n, Type) (_ : @pos_invert_t n P) (p : pos n), P p *)
    intros P HP; induction p; simpl in HP; apply HP.
  Defined.
  
  Theorem pos_O_invert X : pos 0 -> X.
  Proof.
(* Goal: forall _ : pos O, X *)
    apply pos_invert; simpl; trivial.
  Defined.

  Theorem pos_S_invert n P : P (@pos_fst n) -> (forall p, P (pos_nxt p)) -> forall p, P p.
  Proof.
(* Goal: forall (_ : P (@pos_fst n)) (_ : forall p : pos n, P (@pos_nxt n p)) (p : pos (S n)), P p *)
    intros; apply pos_invert; split; auto.
  Defined.
  
End pos_invert.

Arguments pos_S_invert [n] P _ _ p /.

Ltac pos_O_inv p := exfalso; apply (pos_O_inv p).

Ltac pos_S_inv p := 
  let H := fresh in
  let q := fresh
  in  rename p into q; destruct (pos_S_inv q) as [ H | (p & H) ]; subst q.
 
(* 
Ltac pos_O_inv p := apply (@pos_O_invert _ p).
Ltac pos_S_inv x := induction x as [ | x ] using pos_S_invert.
*)

Ltac pos_inv p :=   
  match goal with
    | [ H: pos 0     |- _ ] => match H with p => pos_O_inv p end
    | [ H: pos (S _) |- _ ] => match H with p => pos_S_inv p end
  end.

Tactic Notation "invert" "pos" hyp(H) := pos_inv H; simpl.

Ltac analyse_pos p := 
  match type of p with
    | pos 0     => pos_inv p
    | pos (S _) => pos_inv p; [ | try analyse_pos p ]
  end. 

Tactic Notation "analyse" "pos" hyp(p) := analyse_pos p.

Definition pos_O_any X : pos 0 -> X.
(* Goal: forall _ : pos O, X *)
Proof. intro p; invert pos p. Qed.

Fixpoint pos_left n m (p : pos n) : pos (n+m) :=
  match p with
    | pos_fst   => pos_fst
    | pos_nxt p => pos_nxt (pos_left m p)
  end.

Fixpoint pos_right n m : pos m -> pos (n+m) :=
  match n with 
    | 0   => fun x => x
    | S n => fun p => pos_nxt (pos_right n p)
  end.

Definition pos_both n m : pos (n+m) -> pos n + pos m.
Proof.
(* Goal: forall _ : pos (Init.Nat.add n m), sum (pos n) (pos m) *)
  induction n as [ | n IHn ]; intros p.
  + right; exact p.
  + simpl in p; pos_inv p.
    * left; apply pos_fst.
    * destruct (IHn p) as [ a | b ].
      - left; apply (pos_nxt a).
      - right; apply b.
Defined.

Definition pos_lr n m : pos n + pos m -> pos (n+m).
Proof.
(* Goal: forall _ : sum (pos n) (pos m), pos (Init.Nat.add n m) *)
  intros [ p | p ]; revert p.
  + apply pos_left.
  + apply pos_right.
Defined.

Fact pos_both_left n m p : @pos_both n m (@pos_left n m p) = inl p.
Proof.
(* Goal: @eq (sum (pos n) (pos m)) (pos_both n m (@pos_left n m p)) (@inl (pos n) (pos m) p) *)
  induction p as [ | n p IHp ]; simpl; auto.
(* Goal: @eq (sum (pos (S n)) (pos m)) match pos_both n m (@pos_left n m p) with | inl a => @inl (pos (S n)) (pos m) (@pos_nxt n a) | inr b => @inr (pos (S n)) (pos m) b end (@inl (pos (S n)) (pos m) (@pos_nxt n p)) *)
  rewrite IHp; auto.
Qed.

Fact pos_both_right n m p : @pos_both n m (@pos_right n m p) = inr p.
Proof.
(* Goal: @eq (sum (pos n) (pos m)) (pos_both n m (@pos_right n m p)) (@inr (pos n) (pos m) p) *)
  revert p; induction n as [ | n IHn]; intros p; simpl; auto.
(* Goal: @eq (sum (pos (S n)) (pos m)) match pos_both n m (@pos_right n m p) with | inl a => @inl (pos (S n)) (pos m) (@pos_nxt n a) | inr b => @inr (pos (S n)) (pos m) b end (@inr (pos (S n)) (pos m) p) *)
  rewrite IHn; auto.
Qed.

(** A bijection between pos n + pos m <-> pos (n+m) **)

Fact pos_both_lr n m p : @pos_both n m (pos_lr p) = p.
Proof.
(* Goal: @eq (sum (pos n) (pos m)) (pos_both n m (@pos_lr n m p)) p *)
  destruct p as [ p | p ].
  + apply pos_both_left.
  + apply pos_both_right.
Qed.

Fact pos_lr_both n m p : pos_lr (@pos_both n m p) = p.
Proof.
(* Goal: @eq (pos (Init.Nat.add n m)) (@pos_lr n m (pos_both n m p)) p *)
  revert p; induction n as [ | n IHn ]; intros p; auto.
(* Goal: @eq (pos (Init.Nat.add (S n) m)) (@pos_lr (S n) m (pos_both (S n) m p)) p *)
  simpl in p; pos_inv p; simpl; auto.
(* Goal: @eq (pos (S (Init.Nat.add n m))) (@pos_lr (S n) m match pos_both n m p with | inl a => @inl (pos (S n)) (pos m) (@pos_nxt n a) | inr b => @inr (pos (S n)) (pos m) b end) (@pos_nxt (Init.Nat.add n m) p) *)
  specialize (IHn p).
  destruct (pos_both n m p); simpl in *; f_equal; auto.
Qed.

Section pos_left_right_rect.

  Variable (n m : nat) (P : pos (n+m) -> Type).

  Hypothesis (HP1 : forall p, P (pos_left _ p))
             (HP2 : forall p, P (pos_right _ p)).

  Theorem pos_left_right_rect : forall p, P p.
  Proof.
(* Goal: @pm_ext_eq (S l) (S n) (@pm_lift l n (@pm_comp l m n r s)) (@pm_comp (S l) (S m) (S n) (@pm_lift l m r) (@pm_lift m n s)) *)
    intros p.
    rewrite <- pos_lr_both.
(* Goal: P (@pos_lr n m (pos_both n m p)) *)
    generalize (pos_both n m p); clear p; intros [|]; simpl; auto.
  Qed.

End pos_left_right_rect.

Fixpoint pos_list n : list (pos n) :=
  match n with
    | 0   => nil
    | S n => pos0::map pos_nxt (pos_list n) 
  end.

Fact pos_list_prop n p : In p (pos_list n).
Proof.
(* Goal: @In (pos n) p (pos_list n) *)
  induction p as [ | n p Hp ].
(* Goal: @In (pos (S n)) (@pos_fst n) (pos_list (S n)) *)
(* Goal: @In (pos (S n)) (@pos_nxt n p) (pos_list (S n)) *)
  left; auto.
(* Goal: @In (pos (S n)) (@pos_nxt n p) (pos_list (S n)) *)
  simpl; right.
(* Goal: @In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) (@map (pos n) (prod (pos n) (pos n)) (fun q : pos n => @pair (pos n) (pos n) p q) (pos_list n)) *)
  apply in_map_iff.
(* Goal: @ex (pos n) (fun x : pos n => and (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n p)) (@In (pos n) x (pos_list n))) *)
  exists p; auto.
Qed.

Fact pos_list_length n : length (pos_list n) = n.
Proof.
(* Goal: @eq nat (@length (pos n) (pos_list n)) n *)
  induction n; simpl; auto.
(* Goal: @eq nat (S (@length (pos (S n)) (@map (pos n) (pos (S n)) (@pos_nxt n) (pos_list n)))) (S n) *)
  rewrite map_length; f_equal; auto.
Qed.
 
Fact pos_reification X n (R : pos n -> X -> Prop) : (forall p, exists x, R p x) -> exists f, forall p, R p (f p).
Proof.
(* Goal: forall _ : forall p : pos n, @ex X (fun x : X => R p x), @ex (forall _ : pos n, X) (fun f : forall _ : pos n, X => forall p : pos n, R p (f p)) *)
  revert R; induction n as [ | n IHn ]; intros R HR.
(* Goal: @ex (forall _ : pos O, X) (fun f : forall _ : pos O, X => forall p : pos O, R p (f p)) *)
(* Goal: @ex (forall _ : pos (S n), X) (fun f : forall _ : pos (S n), X => forall p : pos (S n), R p (f p)) *)
  exists (pos_O_any X); intros p; invert pos p.
(* Goal: @ex (forall _ : pos (S n), X) (fun f : forall _ : pos (S n), X => forall p : pos (S n), R p (f p)) *)
  set (R' q x := R (pos_nxt q) x).
(* Goal: @ex (forall _ : pos (S n), X) (fun f : forall _ : pos (S n), X => forall p : pos (S n), R p (f p)) *)
  destruct (IHn R') as (f & Hf).
(* Goal: forall p : pos n, @ex X (fun x : X => R' p x) *)
(* Goal: @ex (forall _ : pos (S n), X) (fun f : forall _ : pos (S n), X => forall p : pos (S n), R p (f p)) *)
  intros p; apply HR.
(* Goal: @ex (forall _ : pos (S n), X) (fun f : forall _ : pos (S n), X => forall p : pos (S n), R p (f p)) *)
  unfold R' in Hf.
(* Goal: @ex (forall _ : pos (S n), X) (fun f : forall _ : pos (S n), X => forall p : pos (S n), R p (f p)) *)
  destruct (HR pos_fst) as (x & Hx).
(* Goal: @ex (forall _ : pos (S n), X) (fun f : forall _ : pos (S n), X => forall p : pos (S n), R p (f p)) *)
  exists (fun p => match pos_S_inv p with inl _ => x | inr (exist _ q _) => f q end).
(* Goal: forall p : pos (S n), R p match @pos_S_inv n p with | inl e => x | inr (exist _ q e as s) => f q end *)
  intros p; invert pos p; auto.
Qed.

Fact pos_reif_t X n (R : pos n -> X -> Prop) : (forall p, { x | R p x }) -> { f | forall p, R p (f p) }.
Proof.
(* Goal: forall _ : forall p : pos n, @sig X (fun x : X => R p x), @sig (forall _ : pos n, X) (fun f : forall _ : pos n, X => forall p : pos n, R p (f p)) *)
  intros H.
(* Goal: @sig (forall _ : pos n, X) (fun f : forall _ : pos n, X => forall p : pos n, R p (f p)) *)
  exists (fun p => (proj1_sig (H p))).
(* Goal: forall p : pos n, R p (@proj1_sig X (fun x : X => R p x) (H p)) *)
  intros; apply (proj2_sig (H p)).
Qed.

Section pos_eq_dec.

  Definition pos_eq_dec n (x y : pos n) : { x = y } + { x <> y }.
  Proof.
(* Goal: sumbool (@eq (pos n) x y) (not (@eq (pos n) x y)) *)
    revert n x y.
(* Goal: forall (n : nat) (x y : pos n), sumbool (@eq (pos n) x y) (not (@eq (pos n) x y)) *)
    induction x as [ x | n x IH ]; intros y; invert pos y.
(* Goal: sumbool (@eq (pos (S x)) (@pos_fst x) (@pos_fst x)) (not (@eq (pos (S x)) (@pos_fst x) (@pos_fst x))) *)
(* Goal: sumbool (@eq (pos (S x)) (@pos_fst x) (@pos_nxt x y)) (not (@eq (pos (S x)) (@pos_fst x) (@pos_nxt x y))) *)
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_fst n)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_fst n))) *)
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y))) *)
    left; trivial.
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_fst n)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_fst n))) *)
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y))) *)
    right; discriminate.
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_fst n)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_fst n))) *)
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y))) *)
    right; discriminate.
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y))) *)
    destruct (IH y) as [ | C ].
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y))) *)
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y))) *)
    left; subst; trivial.
(* Goal: sumbool (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y)) (not (@eq (pos (S n)) (@pos_nxt n x) (@pos_nxt n y))) *)
    right; contradict C; revert C; apply pos_nxt_inj.
  Defined.

End pos_eq_dec.

Section pos_map.

  Definition pos_map m n := pos m -> pos n.
 
  Definition pm_ext_eq m n (r1 r2 : pos_map m n) := forall p, r1 p = r2 p.  

  Definition pm_lift m n (r : pos_map m n) : pos_map (S m) (S n).
  Proof.
(* Goal: @pm_ext_eq (S l) (S n) (@pm_lift l n (@pm_comp l m n r s)) (@pm_comp (S l) (S m) (S n) (@pm_lift l m r) (@pm_lift m n s)) *)
    intros p.
(* Goal: pos (S n) *)
    invert pos p.
(* Goal: pos (S m) *)
(* Goal: pos O *)
(* Goal: pos (S m) *)
    apply pos_fst.
(* Goal: pos (S n) *)
    apply pos_nxt, (r p).
  Defined.
  
  Fact pm_lift_fst m n (r : pos_map m n) : pm_lift r pos0 = pos0.
  Proof. auto. Qed.  
  
  Fact pm_lift_nxt m n (r : pos_map m n) p : pm_lift r (pos_nxt p) = pos_nxt (r p).
  Proof. auto. Qed.

  Arguments pm_lift [ m n ] r p.

  Fact pm_lift_ext m n r1 r2 : @pm_ext_eq m n r1 r2 -> pm_ext_eq (pm_lift r1) (pm_lift r2). 
  Proof.
(* Goal: forall _ : @pm_ext_eq m n r1 r2, @pm_ext_eq (S m) (S n) (@pm_lift m n r1) (@pm_lift m n r2) *)
    intros H12 p; unfold pm_lift.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    invert pos p; simpl; auto.
(* Goal: @eq (pos (S n)) (@pos_nxt n (r1 p)) (@pos_nxt n (r2 p)) *)
    f_equal; apply H12.
  Qed.

  Definition pm_comp l m n : pos_map l m -> pos_map m n -> pos_map l n.
  Proof.
(* Goal: forall (_ : pos_map l m) (_ : pos_map m n), pos_map l n *)
    intros H1 H2 p.
(* Goal: pos n *)
    exact (H2 (H1 p)).
  Defined. 
 
  Fact pm_comp_lift l m n r s : pm_ext_eq (pm_lift (@pm_comp l m n r s)) (pm_comp (pm_lift r) (pm_lift s)).
  Proof.
(* Goal: @pm_ext_eq (S l) (S n) (@pm_lift l n (@pm_comp l m n r s)) (@pm_comp (S l) (S m) (S n) (@pm_lift l m r) (@pm_lift m n s)) *)
    intros p.
(* Goal: @eq (pos (S n)) (@pm_lift l n (@pm_comp l m n r s) p) (@pm_comp (S l) (S m) (S n) (@pm_lift l m r) (@pm_lift m n s) p) *)
    unfold pm_comp, pm_lift; simpl.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    invert pos p; simpl; auto.
  Qed.

  Definition pm_id n : pos_map n n := fun p => p.

End pos_map.

Arguments pm_lift { m n } _ _ /.
Arguments pm_comp [ l m n ] _ _ _ /.
Arguments pm_id : clear implicits.

Section pos_nat.

  Fixpoint pos_nat n (p : pos n) : { i | i < n }.
  Proof.
    refine (match p with 
              | pos_fst   => exist _ 0 _
              | pos_nxt q => exist _ (S (proj1_sig (pos_nat _ q))) _
            end).
(* Goal: lt O (S n0) *)
(* Goal: lt (S (@proj1_sig nat (fun i : nat => lt i n0) (pos_nat n0 q))) (S n0) *)
    apply lt_O_Sn.
(* Goal: lt (S (@proj1_sig nat (fun i : nat => lt i n0) (pos_nat n0 q))) (S n0) *)
    apply lt_n_S, (proj2_sig (pos_nat _ q)).
  Defined.

  Definition pos2nat n p := proj1_sig (@pos_nat n p).
  
  Fact pos2nat_prop n p : @pos2nat n p < n.
  Proof. apply (proj2_sig (pos_nat p)). Qed.

  Fixpoint nat2pos n : forall x, x < n -> pos n.
  Proof.
     refine (match n as n' return forall x, x < n' -> pos n' with 
              | O   => fun x H => _
              | S i => fun x H => _
            end).
(* Goal: pos O *)
(* Goal: pos (S i) *)
    exfalso; revert H; apply lt_n_O.
(* Goal: pos (S i) *)
    destruct x as [ | x ].
(* Goal: pos (S m) *)
(* Goal: pos O *)
(* Goal: pos (S m) *)
    apply pos_fst.
(* Goal: pos (S m) *)
    apply pos_nxt. 
(* Goal: pos i *)
    apply (nat2pos i x); revert H; apply lt_S_n.
  Defined.

  Definition nat_pos n : { i | i < n } -> pos n.
  Proof. intros (? & H); revert H; apply nat2pos. Defined.

  Arguments pos2nat n !p /.

  Fact pos2nat_inj n (p q : pos n) : pos2nat p = pos2nat q -> p = q.
  Proof.
(* Goal: forall _ : @eq nat (@pos2nat n p) (@pos2nat n q), @eq (pos n) p q *)
    revert q.
(* Goal: forall (q : pos n) (_ : @eq nat (@pos2nat n p) (@pos2nat n q)), @eq (pos n) p q *)
    induction p as [ n | n p IHp ]; intros q; invert pos q; simpl; auto; try discriminate 1.
(* Goal: forall _ : @eq nat (S (@proj1_sig nat (fun i : nat => lt i n) (@pos_nat n p))) (S (@proj1_sig nat (fun i : nat => lt i n) (@pos_nat n q))), @eq (pos (S n)) (@pos_nxt n p) (@pos_nxt n q) *)
    intros H; f_equal; apply IHp; injection H; trivial.
  Qed.

  Fact pos2nat_nat2pos n i (H : i < n) : pos2nat (nat2pos H) = i.
  Proof.
    revert i H;
    induction n as [ | n IHn ]; intros [ | i ] H; simpl; auto; try omega.
(* Goal: @eq nat (S (@proj1_sig nat (fun i : nat => lt i n) (@pos_nat n (@nat2pos n i (lt_S_n i n H))))) (S i) *)
    f_equal.
(* Goal: @eq nat (@proj1_sig nat (fun i : nat => lt i n) (@pos_nat n (@nat2pos n i (lt_S_n i n H)))) i *)
    apply IHn.
  Qed.
  
  Fact nat2pos_pos2nat n p (H : pos2nat p < n) : nat2pos H = p.
  Proof.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    apply pos2nat_inj; rewrite pos2nat_nat2pos; auto.
  Qed.
  
  Fact pos2nat_fst n : pos2nat (@pos_fst n) = 0.
  Proof. auto. Qed.
  
  Fact pos2nat_nxt n p : pos2nat (@pos_nxt n p) = S (pos2nat p).
  Proof. auto. Qed. 

  Fact pos2nat_left n m p : pos2nat (@pos_left n m p) = pos2nat p.
  Proof. induction p; simpl; auto. Qed.

  Fact pos2nat_right n m p : pos2nat (@pos_right n m p) = n+pos2nat p.
  Proof.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    revert m p; induction n as [ | n IHn ]; intros m p; auto.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    simpl pos_right; simpl plus; rewrite pos2nat_nxt; f_equal; auto.
  Qed.

  Fixpoint pos_sub n (p : pos n) { struct p } : forall m, n < m -> pos m.
  Proof.
(* Goal: forall (m : nat) (_ : lt n m), pos m *)
    destruct p as [ | n p ]; intros [ | m ] Hm.
(* Goal: pos O *)
(* Goal: pos (S m) *)
    exfalso; clear pos_sub; abstract omega.
(* Goal: pos (S m) *)
(* Goal: pos O *)
(* Goal: pos (S m) *)
    apply pos_fst.
(* Goal: pos O *)
(* Goal: pos (S m) *)
    exfalso; clear pos_sub; abstract omega.
(* Goal: pos (S m) *)
    apply pos_nxt.
(* Goal: pos m *)
    apply (pos_sub n p), lt_S_n, Hm.
  Defined.
  
  Fact pos_sub2nat n p m Hm : pos2nat (@pos_sub n p m Hm) = pos2nat p.
  Proof.
(* Goal: @eq nat (@pos2nat m (@pos_sub n p m Hm)) (@pos2nat n p) *)
    revert m Hm; induction p as [ n | n p IH ]; intros [ | m ] Hm; try omega. 
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    simpl; auto.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    simpl pos_sub; repeat rewrite pos2nat_nxt; f_equal; auto.
  Qed.
  
End pos_nat.

Global Opaque pos_nat.

Fact pos_list2nat n : map (@pos2nat n) (pos_list n) = list_an 0 n.
Proof.
(* Goal: @eq nat (S (@proj1_sig nat (fun i : nat => lt i n) (@pos_nat n (@nat2pos n i (lt_S_n i n H))))) (S i) *)
  induction n as [ | n IHn ]; simpl; f_equal.
  rewrite <- (map_S_list_an 0), <- IHn.
(* Goal: @eq (list nat) (@map (pos (S n)) nat (@pos2nat (S n)) (@map (pos n) (pos (S n)) (@pos_nxt n) (pos_list n))) (@map nat nat S (@map (pos n) nat (@pos2nat n) (pos_list n))) *)
  do 2 rewrite map_map.
(* Goal: @eq (list nat) (@map (pos n) nat (fun x : pos n => @pos2nat (S n) (@pos_nxt n x)) (pos_list n)) (@map (pos n) nat (fun x : pos n => S (@pos2nat n x)) (pos_list n)) *)
  apply map_ext.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
  intros; rewrite pos2nat_nxt; auto.
Qed.

Section pos_prod.
  
  Variable n : nat.
  
  Let ll := flat_map (fun p => map (fun q => (p,q)) (pos_list n)) (pos_list n).
  Let ll_prop p q : In (p,q) ll.
  Proof. 
(* Goal: @In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll *)
    apply in_flat_map; exists p; split.
(* Goal: @In (pos n) q (pos_list n) *)
    apply pos_list_prop.
(* Goal: @In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) (@map (pos n) (prod (pos n) (pos n)) (fun q : pos n => @pair (pos n) (pos n) p q) (pos_list n)) *)
    apply in_map_iff.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    exists q; split; auto.
(* Goal: @In (pos n) q (pos_list n) *)
    apply pos_list_prop.
  Qed.
  
  Definition pos_not_diag := filter (fun c => if pos_eq_dec (fst c) (snd c) then false else true) ll.

  Fact pos_not_diag_spec p q : In (p,q) pos_not_diag <-> p <> q.
  Proof.
(* Goal: iff (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) pos_not_diag) (not (@eq (pos n) p q)) *)
    unfold pos_not_diag.
(* Goal: iff (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) (@filter (prod (pos n) (pos n)) (fun c : prod (pos n) (pos n) => if @pos_eq_dec n (@fst (pos n) (pos n) c) (@snd (pos n) (pos n) c) then false else true) ll)) (not (@eq (pos n) p q)) *)
    rewrite filter_In; simpl.
(* Goal: iff (and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool (if @pos_eq_dec n p q then false else true) true)) (not (@eq (pos n) p q)) *)
    destruct (pos_eq_dec p q).
(* Goal: iff (and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool false true)) (not (@eq (pos n) p q)) *)
(* Goal: iff (and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool true true)) (not (@eq (pos n) p q)) *)
    split. 
(* Goal: forall _ : and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool false true), not (@eq (pos n) p q) *)
(* Goal: forall _ : not (@eq (pos n) p q), and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool false true) *)
(* Goal: iff (and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool true true)) (not (@eq (pos n) p q)) *)
    intros (_ & ?); discriminate.
(* Goal: forall _ : not (@eq (pos n) p q), and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool false true) *)
(* Goal: iff (and (@In (prod (pos n) (pos n)) (@pair (pos n) (pos n) p q) ll) (@eq bool true true)) (not (@eq (pos n) p q)) *)
    intros []; auto.
(* Goal: @eq nat (@pos2nat (S n) (@pos_nxt n p)) (S (@pos2nat n p)) *)
    split; try tauto; split; auto.
  Qed.
  
End pos_prod.

