Lvc.Infra.LengthEq

Require Import Arith Coq.Lists.List Setoid Coq.Lists.SetoidList Omega.
Require Export Infra.Option EqDec AutoIndTac Util.

Set Implicit Arguments.

Inductive length_eq X Y : list Xlist YType :=
  | LenEq_nil : length_eq nil nil
  | LenEq_cons x XL y YL : length_eq XL YLlength_eq (x::XL) (y::YL).

Lemma length_eq_refl X (XL:list X)
  : length_eq XL XL.
Proof.
  induction XL; eauto using length_eq.
Qed.

Lemma length_eq_sym X Y (XL:list X) (YL:list Y)
  : length_eq XL YLlength_eq YL XL.
Proof.
  intros. general induction X0; eauto using length_eq.
Qed.

Lemma length_eq_trans X Y Z (XL:list X) (YL:list Y) (ZL:list Z)
  : length_eq XL YLlength_eq YL ZLlength_eq XL ZL.
Proof.
  intros. general induction X0; inv X1; eauto using length_eq.
Qed.

Lemma length_length_eq X Y (L:list X) (:list Y)
  : length L = length length_eq L .
Proof.
  intros H; general induction L; destruct ; inv H; eauto using length_eq.
Qed.

Lemma length_eq_length X Y (L:list X) (:list Y)
  : length_eq L length L = length .
Proof.
  intros H; general induction L; destruct ; inv H; simpl; eauto.
Qed.

Lemma length_eq_dec {X} (L : list X)
  : length_eq L + (length_eq L False).
Proof.
  decide(length L = length ).
  left. eapply length_length_eq; eauto.
  right. intro. eapply length_eq_length in X0. congruence.
Defined.

Ltac length_equify :=
  repeat (match goal with
            | [ H : length ?A = length ?B |- _ ] ⇒
              eapply length_length_eq in H
          end).