Global Set Asymmetric Patterns.

Require Export Eqdep.
Require Export Eqdep_dec.
Require Export Peano_dec.
Require Export Omega.

Axiom proof_irr : ∀ (A : Prop) (p q : A), p = q.

Lemma two_step_ind :
 ∀ P : nat → Prop,
 P 0 → P 1 → (∀ n : nat, P n → P (S (S n))) → ∀ n : nat, P n.
intros P h0 h1 hr n; cut (P n ∧ P (S n)).
intros H; elim H; trivial.
elim n.
split; trivial.
intros n0 H; try assumption.
elim H.
intros H0 H1; try assumption.
split; [ trivial | apply hr; trivial ].
Qed.

Section vect_def.
Variable A : Set.

Inductive vect : nat → Set :=
  | vnil : vect 0
  | vcons : ∀ n : nat, A → vect n → vect (S n).

Lemma uniq : ∀ v : vect 0, v = vnil.
intros v.
change (v = eq_rec _ vect vnil _ (refl_equal 0)) in |- ×.
generalize (refl_equal 0).
change
  ((fun (n : nat) (v : vect n) ⇒
    ∀ e : 0 = n, v = eq_rec _ vect vnil _ e) 0 v)
 in |- ×.
case v; intros.
apply K_dec_set with (p := e).
exact eq_nat_dec.
reflexivity.
discriminate e.
Qed.

Definition eq_vect := eq_dep nat vect.

Lemma decompose_dep :
 ∀ n m : nat,
 m = S n →
 ∀ v : vect (S n),
 {a : A & {v' : vect n | eq_vect (S n) v (S n) (vcons n a v')}}.
intros n m H v.
generalize H; clear H.
dependent inversion_clear v
 with
  (fun (n' : nat) (vl : vect n') ⇒
   m = n' → {a : A & {v' : vect n | eq_vect n' vl (S n) (vcons n a v')}}).
unfold eq_vect in |- ×.
intros H; ∃ a; ∃ v0.
apply eq_dep_intro.
Qed.

Lemma decompose :
 ∀ (n : nat) (v : vect (S n)),
 {a : A & {v' : vect n | v = vcons n a v'}}.
intros n v.
cut {a : A & {t : vect n | eq_vect (S n) v (S n) (vcons n a t)}}.
intros H; elim H; clear H.
intros a H; elim H; clear H.
intros v' H.
∃ a; ∃ v'.
apply eq_dep_eq with (U := nat) (P := vect) (p := S n).
unfold eq_vect in H; trivial.
apply (decompose_dep n (S n)); trivial.
Qed.

Lemma eq_vect_vcons :
 ∀ (c n : nat) (vc : vect c) (vn : vect n) (a a' : A),
 a = a' →
 eq_vect c vc n vn → eq_vect (S c) (vcons c a vc) (S n) (vcons n a' vn).
intros c n vc vn a a' H H'.
rewrite H.
cut (eq_vect (S c) (vcons c a' vc) (S c) (vcons c a' vc)).
intros Hcut.
unfold eq_vect in |- ×.
apply
 (eq_dep_ind nat vect c vc
    (fun (n0 : nat) (v0 : vect n0) ⇒
     eq_dep nat vect (S c) (vcons c a' vc) (S n0) (vcons n0 a' v0)) Hcut n vn
    H').
unfold eq_vect in |- *; apply eq_dep_intro.
Qed.

Lemma vcons_lemma :
 ∀ (n : nat) (x y : A) (xs ys : vect n),
 x = y → xs = ys → vcons n x xs = vcons n y ys.
intros n x y xs ys Hxy Hxsys.
rewrite Hxy.
rewrite Hxsys.
trivial.
Qed.

Lemma induc1 :
 ∀ P : ∀ n : nat, vect n → Prop,
 P 0 vnil →
 (∀ (n : nat) (v : vect n), P n v → ∀ a : A, P (S n) (vcons n a v)) →
 ∀ (n : nat) (v : vect n), P n v.
intros P Hnil Hvcons n.
elim n.
intros v.
replace v with vnil; [ idtac | rewrite uniq; auto ].
exact Hnil.
intros n0 HR v.
elim (decompose n0 v).
intros ve Hve; elim Hve; intros xe Heq.
rewrite Heq.
apply Hvcons.
apply HR.
Qed.

Lemma induc2 :
 ∀ P : ∀ n : nat, vect n → vect n → Prop,
 P 0 vnil vnil →
 (∀ (n : nat) (v v' : vect n),
  P n v v' → ∀ a b : A, P (S n) (vcons n a v) (vcons n b v')) →
 ∀ (n : nat) (v v' : vect n), P n v v'.
intros P Hnil Hvcons n.
elim n.
intros v v'.
replace v with vnil; [ idtac | rewrite uniq; auto ].
replace v' with vnil; [ idtac | rewrite uniq; auto ].
exact Hnil.
intros n0 HR v v'.
elim (decompose n0 v).
intros ve Hve; elim Hve; intros xe Heq.
rewrite Heq.
elim (decompose n0 v').
intros ve' Hve'; elim Hve'; intros xe' Heq'.
rewrite Heq'.
apply Hvcons.
apply HR.
Qed.

Lemma induc3 :
 ∀ P : ∀ n : nat, vect n → vect n → vect n → Prop,
 P 0 vnil vnil vnil →
 (∀ (n : nat) (v v' v'' : vect n),
  P n v v' v'' →
  ∀ a b c : A, P (S n) (vcons n a v) (vcons n b v') (vcons n c v'')) →
 ∀ (n : nat) (v v' v'' : vect n), P n v v' v''.
intros P Hvnil Hvcons n.
elim n.
intros v v' v''.
replace v with vnil; [ idtac | rewrite uniq; auto ].
replace v' with vnil; [ idtac | rewrite uniq; auto ].
replace v'' with vnil; [ idtac | rewrite uniq; auto ].
exact Hvnil.
intros n0 HR v v' v''.
elim (decompose n0 v).
intros ve Hve; elim Hve; intros xe Heq.
rewrite Heq.
elim (decompose n0 v').
intros ve' Hve'; elim Hve'; intros xe' Heq'.
rewrite Heq'.
elim (decompose n0 v'').
intros ve'' Hve''; elim Hve''; intros xe'' Heq''.
rewrite Heq''.
apply Hvcons.
apply HR.
Qed.

Definition head (n : nat) (v : vect n) :=
  match v in (vect n) return (0 < n → A) with
  | vnil ⇒ fun h : 0 < 0 ⇒ False_rec A (lt_irrefl 0 h)
  | vcons p a v' ⇒ fun h : 0 < S p ⇒ a
  end.

Lemma head_lemma_1 :
 ∀ v v' : vect 1, v = v' → head 1 v (le_n 1) = head 1 v' (le_n 1).
intros v v' H; rewrite H; trivial.
Qed.

Definition tail (n : nat) (v : vect n) :=
  match v in (vect m) return (vect (pred m)) with
  | vnil ⇒ vnil
  | vcons p a v' ⇒ v'
  end.

Lemma le_S_lt_O : ∀ n m : nat, S m ≤ n → 0 < n.
intros; apply lt_le_trans with (S m); auto with arith.
Qed.

Lemma lt_le_pred : ∀ n m : nat, n < m → n ≤ pred m.
simple induction n; simple induction m; auto with arith.
Qed.

Lemma le_Sn_le_n_pred : ∀ n m : nat, S n ≤ m → n ≤ pred m.
intros; apply lt_le_pred; trivial.
Qed.

Theorem zerop : ∀ n : nat, {n = 0} + {0 < n}.
destruct n; auto with arith.
Defined.

Fixpoint nth (i : nat) : ∀ n : nat, vect n → 0 < i → i ≤ n → A :=
  fun (n : nat) (v : vect n) ⇒
  match i as j return (0 < j → j ≤ n → A) with
  | O ⇒ fun (h' : 0 < 0) h'' ⇒ False_rec A (lt_irrefl 0 h')
  | S p ⇒
      fun (h' : 0 < S p) (h'' : S p ≤ n) ⇒
      match zerop p with
      | left _ ⇒ head n v (le_S_lt_O _ _ h'')
      | right h ⇒ nth p (pred n) (tail n v) h (le_Sn_le_n_pred _ _ h'')
      end
  end.

Remark nth_lemma_aux : ∀ (i n : nat) (Hi2 : S i ≤ S n), i ≤ n.
intros; apply le_S_n; trivial.
Qed.

Lemma nth_lemma :
 ∀ (i n : nat) (a : A) (v : vect n) (Hi1 : 0 < S (S i))
   (Hi2 : S (S i) ≤ S n) (Hi1' : 0 < S i),
 nth (S (S i)) (S n) (vcons n a v) Hi1 Hi2 =
 nth (S i) n v Hi1' (le_Sn_le_n_pred (S i) (S n) Hi2).
intros i; elim i using two_step_ind.
intros n a v Hi1 Hi2 Hi1'; simpl in |- *; trivial.
intros i' a v Hi1 Hi2 Hi1'; simpl in |- *; trivial.
intros i' HR n' a v Hi1 Hi2 Hi1'; simpl in |- *; trivial.
Qed.

Lemma nth_lemma' :
 ∀ (c n : nat) (w : vect n) (a : A) (H1 : 0 < S c)
   (H2 : S c ≤ S n) (H1' : 0 < c),
 nth (S c) (S n) (vcons n a w) H1 H2 =
 nth c n w H1' (le_Sn_le_n_pred c (S n) H2).
intros c; elim c.
intros n w a H1 H2 H1'; inversion H1'.
intros c' HR.
simpl in |- *; trivial.
Qed.

Lemma last_o1 : ∀ n c' : nat, S c' ≤ n → 0 < n - c'.
intros; omega.
Qed.

Lemma last_o2 : ∀ n c' : nat, n - c' ≤ n.
intros; omega.
Qed.

Lemma last_o3 : ∀ c' : nat, 0 ≤ c'.
intros; omega.
Qed.

Lemma last_o4 : ∀ c' n : nat, S c' ≤ n → c' ≤ n.
intros; omega.
Qed.

Definition last :
  ∀ (n : nat) (v : vect n) (c : nat), 0 ≤ c → c ≤ n → vect c.
intros n v; fix 1.
intros c; case c.
intros; apply vnil.
intros c' Hc1' Hc2'.
apply vcons.
apply (nth (n - c') n v).
apply last_o1; assumption.
apply last_o2; assumption.
apply last.
apply last_o3; assumption.
apply last_o4; assumption.
Defined.

Lemma last_vcons :
 ∀ (n : nat) (w : vect n) (c : nat) (H1 : 0 < n - c)
   (H2 : n - c ≤ n) (H1c' : 0 ≤ S c) (H2c' : S c ≤ n)
   (H1c : 0 ≤ c) (H2c : c ≤ n),
 vcons c (nth (n - c) n w H1 H2) (last n w c H1c H2c) =
 last n w (S c) H1c' H2c'.
intros n w c H1 H2 H1c' H2c' H1c H2c.
unfold last at 2 in |- ×.
apply vcons_lemma.
rewrite (proof_irr _ H1 (last_o1 n c H2c')).
rewrite (proof_irr _ H2 (last_o2 n c)).
trivial.
rewrite (proof_irr _ H1c (last_o3 c)).
rewrite (proof_irr _ H2c (last_o4 c n H2c')).
trivial.
Qed.

Lemma last_S :
 ∀ (c n : nat) (a : A) (v : vect n) (H1 : 0 ≤ c)
   (H2 : c ≤ n) (H2' : c ≤ S n),
 last n v c H1 H2 = last (S n) (vcons n a v) c H1 H2'.
intros c; elim c.
intros n a v H1 H2 H2'; try assumption.
rewrite (uniq (last n v 0 H1 H2)).
rewrite (uniq (last (S n) (vcons n a v) 0 H1 H2')); trivial.
intros c' HR.
intros n a v H1 H2 H2'.
unfold last in |- ×.
apply vcons_lemma.
generalize (last_o1 (S n) c' H2') (last_o2 (S n) c').
rewrite <- minus_Sn_m.
intros Hcut1 Hcut2.
symmetry in |- ×.
rewrite (nth_lemma' (n - c') n v a Hcut1 Hcut2 (last_o1 n c' H2)).
rewrite (proof_irr _ (le_Sn_le_n_pred (n - c') (S n) Hcut2) (last_o2 n c')).
trivial.
replace
 (fix last (c0 : nat) : 0 ≤ c0 → c0 ≤ n → vect c0 :=
    match c0 as c1 return (0 ≤ c1 → c1 ≤ n → vect c1) with
    | O ⇒ fun (_ : 0 ≤ 0) (_ : 0 ≤ n) ⇒ vnil
    | S c'0 ⇒
        fun (_ : 0 ≤ S c'0) (Hc2' : S c'0 ≤ n) ⇒
        vcons c'0 (nth (n - c'0) n v (last_o1 n c'0 Hc2') (last_o2 n c'0))
          (last c'0 (last_o3 c'0) (last_o4 c'0 n Hc2'))
    end) with (last n v); [ idtac | trivial ].
replace
 (fix last (c0 : nat) : 0 ≤ c0 → c0 ≤ S n → vect c0 :=
    match c0 as c1 return (0 ≤ c1 → c1 ≤ S n → vect c1) with
    | O ⇒ fun (_ : 0 ≤ 0) (_ : 0 ≤ S n) ⇒ vnil
    | S c'0 ⇒
        fun (_ : 0 ≤ S c'0) (Hc2' : S c'0 ≤ S n) ⇒
        vcons c'0
          (nth (S n - c'0) (S n) (vcons n a v) (last_o1 (S n) c'0 Hc2')
             (last_o2 (S n) c'0))
          (last c'0 (last_o3 c'0) (last_o4 c'0 (S n) Hc2'))
    end) with (last (S n) (vcons n a v)); [ idtac | trivial ].
omega.
apply (HR n a v (last_o3 c') (last_o4 c' n H2) (last_o4 c' (S n) H2')).
Qed.

Lemma last_vcons' :
 ∀ (n : nat) (w : vect n) (c : nat) (a : A) (H1 : 0 < n - c)
   (H2 : n - c ≤ n) (H1c' : 0 ≤ S c) (H2c' : S c ≤ S n)
   (H1c : 0 ≤ c) (H2c : c ≤ n),
 vcons c (nth (n - c) n w H1 H2) (last n w c H1c H2c) =
 last (S n) (vcons n a w) (S c) H1c' H2c'.
intros n; elim n.
intros w c a H1 H2 H1c' H2c' H1c H2c; cut (c = 0).
intros Hrew; generalize w a H1 H2 H1c' H2c' H1c H2c;
 clear w a H1 H2 H1c' H2c' H1c H2c.
rewrite Hrew.
intros w a H1; simpl in H1; inversion H1.
omega.
intros n0 HR v c.
intros a H1 H2 H1c' H2c' H1c H2c.
cut (c ≤ n0).
intros Hcut; generalize a H1 H2 H1c' H2c' H1c H2c;
 clear a H1 H2 H1c' H2c' H1c H2c.
rewrite <- (minus_Sn_m _ _ Hcut).
2: omega.
intros a H1 H2 H1c' H2c' H1c H2c.
unfold last at 2 in |- ×.
apply vcons_lemma.
generalize (last_o1 (S (S n0)) c H2c') (last_o2 (S (S n0)) c).
replace (S (S n0) - c) with (S (S (n0 - c))); [ idtac | omega ].
intros Hcut1 Hcut2.
symmetry in |- ×.
rewrite (nth_lemma' (S (n0 - c)) (S n0) v a Hcut1 Hcut2 H1).
rewrite (proof_irr _ H2 (le_Sn_le_n_pred (S (n0 - c)) (S (S n0)) Hcut2)).
trivial.
replace
 (fix last (c : nat) : 0 ≤ c → c ≤ S (S n0) → vect c :=
    match c as c1 return (0 ≤ c1 → c1 ≤ S (S n0) → vect c1) with
    | O ⇒ fun (_ : 0 ≤ 0) (_ : 0 ≤ S (S n0)) ⇒ vnil
    | S c' ⇒
        fun (_ : 0 ≤ S c') (Hc2' : S c' ≤ S (S n0)) ⇒
        vcons c'
          (nth (S (S n0) - c') (S (S n0)) (vcons (S n0) a v)
             (last_o1 (S (S n0)) c' Hc2') (last_o2 (S (S n0)) c'))
          (last c' (last_o3 c') (last_o4 c' (S (S n0)) Hc2'))
    end) with (last (S (S n0)) (vcons (S n0) a v));
 [ idtac | trivial ].
generalize (last_S c (S n0) a v H1c H2c (last_o4 c (S (S n0)) H2c')).
rewrite (proof_irr _ H1c (last_o3 c)).
trivial.
Qed.

Lemma last_n :
 ∀ (c n : nat) (v : vect n) (H : c = n) (H1 : 0 ≤ c) (H2 : c ≤ n),
 eq_vect c (last n v c H1 H2) n v.
intros c; elim c.
intros n v H; simpl in |- ×.
intros H1 H2.
generalize H v; case n.
intros; rewrite uniq.
unfold eq_vect in |- *; apply eq_dep_intro.
intros n' Hd; discriminate Hd.
intros c' HR n; case n.
intros v Hd; discriminate Hd.
intros n' v' Heq H1 H2.
cut (0 < S n' - c'); [ intros Hcut1 | omega ].
cut (S n' - c' ≤ S n'); [ intros Hcut2 | omega ].
cut (0 ≤ S c'); [ intros Hcut3 | omega ].
cut (S c' ≤ S n'); [ intros Hcut4 | omega ].
cut (0 ≤ c'); [ intros Hcut5 | omega ].
cut (c' ≤ S n'); [ intros Hcut6 | omega ].
elim (decompose _ v').
intros x0 Hx; elim Hx; clear Hx; intros v0 Heq'.
rewrite Heq'.
rewrite <-
 (last_vcons (S n') (vcons n' x0 v0) c' Hcut1 Hcut2 H1 H2 Hcut5 Hcut6)
 .
apply
 (eq_vect_vcons c' n' (last (S n') (vcons n' x0 v0) c' Hcut5 Hcut6) v0
    (nth (S n' - c') (S n') (vcons n' x0 v0) Hcut1 Hcut2) x0).
cut (S n' - c' = 1); [ intros Hcut'' | omega ].
generalize Hcut1 Hcut2; rewrite Hcut''.
simpl in |- *; trivial.
rewrite <- (last_S c' n' x0 v0 Hcut5 (le_S_n _ _ Hcut4) Hcut6).
apply HR.
omega.
Qed.

Lemma last_n' :
 ∀ (n : nat) (v : vect n) (H1 : 0 ≤ n) (H2 : n ≤ n),
 last n v n H1 H2 = v.
intros; apply (eq_dep_eq nat vect n (last n v n H1 H2) v).
apply last_n.
trivial.
Qed.

End vect_def.

Fixpoint map (A B : Set) (f : A → B) (n : nat) (v : vect A n) {struct v} :
 vect B n :=
  match v in (vect _ p) return (vect B p) with
  | vnil ⇒ vnil B
  | vcons p x v' ⇒ vcons B p (f x) (map A B f p v')
  end.

Lemma map_2 :
 ∀ (A B : Set) (n : nat) (t : vect A n) (f : A → B)
   (g : B → A) (H : ∀ x : A, g (f x) = x),
 map B A g n (map A B f n t) = map A A (fun x : A ⇒ g (f x)) n t.
intros A2 B n; elim n.
intros t f g H; rewrite (uniq A2).
rewrite (uniq B (map A2 B f 0 t)).
simpl in |- *; trivial.
intros n0 H t f g H0; try assumption.
elim (decompose A2 n0 t).
intros x Hx; elim Hx; intros v Hvx; rewrite Hvx; clear Hx Hvx.
simpl in |- ×.
rewrite H.
trivial.
apply H0.
Qed.

Lemma map_2' :
 ∀ (A B : Set) (n : nat) (t : vect A n) (f : A → B)
   (g : B → A) (H : ∀ x : A, g (f x) = x),
 map B A g n (map A B f n t) = t.
intros A2 B n; elim n.
intros t f g H; rewrite (uniq A2).
rewrite (uniq B (map A2 B f 0 t)).
simpl in |- *; trivial.
intros n0 H t f g H0; try assumption.
elim (decompose A2 n0 t).
intros x Hx; elim Hx; intros v Hvx; rewrite Hvx; clear Hx Hvx.
simpl in |- ×.
rewrite H.
rewrite H0; trivial.
apply H0.
Qed.