Set Implicit Arguments.

Require Export Bvector.
Require Export ASignature.
Require Import ListUtil.
Require Import LogicUtil.
Require Import EqUtil.
Require Import BoolUtil.
Require Import NatUtil.
Require Import Max.

Notation variables := (list variable).

Section S.

Variable Sig : Signature.

Require Import VecUtil.

Unset Elimination Schemes.
Inductive term : Type :=
  | Var : variable → term
  | Fun : ∀ f : Sig, Vector.t term (arity f) → term.
Set Elimination Scheme.


Notation terms := (Vector.t term).

Section term_rect.

Variables
  (P : term → Type)
  (Q : ∀ n, terms n → Type).

Hypotheses
  (H1 : ∀ x, P (Var x))
  (H2 : ∀ f v, Q v → P (Fun f v))
  (H3 : Q Vector.nil)
  (H4 : ∀ t n (v : terms n), P t → Q v → Q (Vector.cons t v)).

Fixpoint term_rect t : P t :=
  match t as t return P t with
    | Var x ⇒ H1 x
    | Fun f v ⇒
      let fix terms_rect n (v : terms n) {struct v} : Q v :=
        match v as v return Q v with
          | Vector.nil ⇒ H3
          | Vector.cons t' n' v' ⇒ H4 (term_rect t') (terms_rect n' v')
        end
        in H2 f (terms_rect (arity f) v)
  end.

End term_rect.

Definition term_ind (P : term → Prop) (Q : ∀ n, terms n → Prop) :=
  term_rect P Q.


Lemma term_ind_forall : ∀ (P : term → Prop)
  (H1 : ∀ v, P (Var v))
  (H2 : ∀ f v, Vforall P v → P (Fun f v)),
  ∀ t, P t.

Proof.
intros. apply term_ind with (Q := Vforall P). exact H1. exact H2.
exact I. intros. simpl. split; assumption.
Qed.

Lemma term_ind_forall2 : ∀ (P : term → Prop)
  (H1 : ∀ v, P (Var v))
  (H2 : ∀ f v, (∀ t, Vin t v → P t) → P (Fun f v)),
  ∀ t, P t.

Proof.
intros. apply term_ind
with (Q := fun n (ts : terms n) ⇒ ∀ t, Vin t ts → P t).
exact H1. exact H2. contradiction. simpl. intuition. subst t1. exact H.
Qed.

Lemma var_eq : ∀ x x', x = x' → Var x = Var x'.

Proof.
intros. rewrite H. refl.
Qed.

Lemma args_eq : ∀ f v v', v = v' → Fun f v = Fun f v'.

Proof.
intros. rewrite H. refl.
Qed.

Lemma fun_eq : ∀ f v w, Fun f v = Fun f w → v = w.

Proof.
intros. inversion H. apply (inj_pairT2 (@eq_symbol_dec _) H1).
Qed.

Lemma symb_eq : ∀ f us g vs, Fun f us = Fun g vs → f = g.

Proof.
intros. inversion H. refl.
Qed.

Section beq.

Variable beq_var : variable → variable → bool.
Variable beq_var_ok : ∀ x y, beq_var x y = true ↔ x = y.

Variable beq_symb : Sig → Sig → bool.
Variable beq_symb_ok : ∀ f g, beq_symb f g = true ↔ f = g.

Fixpoint beq (t u : term) {struct t} :=
  match t, u with
    | Var x, Var y ⇒ beq_var x y
    | Fun f ts, Fun g us ⇒
      let fix beq_terms n (ts : terms n) p (us : terms p) {struct ts} :=
        match ts, us with
          | Vector.nil, Vector.nil ⇒ true
          | Vector.cons t _ ts', Vector.cons u _ us' ⇒ beq t u && beq_terms _ ts' _ us'
          | _, _ ⇒ false
        end
        in beq_symb f g && beq_terms _ ts _ us
    | _, _ ⇒ false
  end.

Lemma beq_terms : ∀ n (ts : terms n) p (us : terms p),
  (fix beq_terms n (ts : terms n) p (us : terms p) {struct ts} :=
    match ts, us with
      | Vector.nil, Vector.nil ⇒ true
      | Vector.cons t _ ts', Vector.cons u _ us' ⇒ beq t u && beq_terms _ ts' _ us'
      | _, _ ⇒ false
    end) _ ts _ us = beq_vec beq ts us.

Proof.
induction ts; destruct us; refl.
Qed.

Lemma beq_fun : ∀ f ts g us,
  beq (Fun f ts) (Fun g us) = beq_symb f g && beq_vec beq ts us.

Proof.
intros. rewrite <- beq_terms. refl.
Qed.

Lemma beq_ok : ∀ t u, beq t u = true ↔ t = u.

Proof.
intro t. pattern t. apply term_ind_forall2; destruct u.
simpl. rewrite beq_var_ok. intuition. inversion H. refl.
intuition; discriminate. intuition; discriminate.
rewrite beq_fun. split; intro. destruct (andb_elim H0).
rewrite beq_symb_ok in H1. subst f0. apply args_eq.
ded (beq_vec_ok_in1 H H2). rewrite <- H1. rewrite Vcast_refl_eq. refl.
inversion H0 as [[h0 h1]]. clear h1. subst f0. simpl.
apply andb_intro. apply (beq_refl beq_symb_ok).
apply beq_vec_ok_in2. exact H. refl.
Qed.

End beq.

Implicit Arguments beq_ok [beq_var beq_symb].

Notation beq_symb := (@beq_symb Sig).
Notation beq_symb_ok := (@beq_symb_ok Sig).

Definition beq_term := beq beq_nat beq_symb.

Lemma beq_term_ok : ∀ t u, beq_term t u = true ↔ t = u.

Proof.
exact (beq_ok beq_nat_ok beq_symb_ok).
Qed.



Lemma eq_term_dec : ∀ t u : term, {t=u}+{¬t=u}.

Proof.
intro. pattern t. apply term_rect with
  (Q := fun n (ts : terms n) ⇒ ∀ u, {ts=u}+{¬ts=u}); clear t.
intros. destruct u. case (eq_nat_dec x n); intro. subst n. auto.
right. unfold not. intro. injection H. auto.
right. unfold not. intro. discriminate.
intros f ts H u. destruct u. right. unfold not. intro. discriminate.
case (eq_symbol_dec f f0); intro. subst f0. case (H t); intro. subst ts. auto.
right. intro. injection H0. intro. assert (ts=t).
Require Import Eqdep.
apply (inj_pair2 Sig (fun f ⇒ terms (arity f))). hyp. auto.
right. unfold not. intro. injection H0. intros. auto.
intro. VOtac. auto.
intros. VSntac u. case (X (Vector.hd u)); intro. rewrite e.
case (X0 (Vector.tl u)); intro. rewrite e0. auto.
right. unfold not. intro. injection H0. intro. assert (v = Vector.tl u).
apply (inj_pair2 nat (fun n ⇒ terms n)). assumption. auto.
right. unfold not. intro. injection H0. intros. auto.
Defined.

Require Import VecMax.

Fixpoint maxvar (t : term) : nat :=
  match t with
    | Var x ⇒ x
    | Fun f v ⇒
      let fix maxvars (n : nat) (v : terms n) {struct v} : nats n :=
        match v in Vector.t _ n return nats n with
          | Vector.nil ⇒ Vector.nil
          | Vector.cons t' n' v' ⇒ Vector.cons (maxvar t') (maxvars n' v')
        end
      in Vmax (maxvars (arity f) v)
  end.

Definition maxvars n (ts : terms n) := Vmax (Vmap maxvar ts).

Lemma maxvars_cons : ∀ t n (ts : terms n),
  maxvars (Vector.cons t ts) = max (maxvar t) (maxvars ts).

Proof.
refl.
Qed.

Lemma maxvar_fun : ∀ f ts, maxvar (Fun f ts) = maxvars ts.

Proof.
intros. simpl. apply (f_equal (@Vmax (arity f))).
induction ts. auto. rewrite IHts. auto.
Qed.

Lemma maxvar_var : ∀ k x, maxvar (Var x) ≤ k → x ≤ k.

Proof.
intros. simpl. intuition.
Qed.

Definition maxvar_le k t := maxvar t ≤ k.

Lemma maxvar_le_fun : ∀ m f ts,
  maxvar (Fun f ts) ≤ m → Vforall (maxvar_le m) ts.

Proof.
intros until ts. rewrite maxvar_fun. intro. generalize (Vmax_forall H).
clear H. intro H. generalize (Vforall_map_elim H). intuition.
Qed.

Lemma maxvar_le_arg : ∀ f ts m t,
  maxvar (Fun f ts) ≤ m → Vin t ts → maxvar t ≤ m.

Proof.
intros. assert (Vforall (maxvar_le m) ts). apply maxvar_le_fun. assumption.
change (maxvar_le m t). eapply Vforall_in with (n := arity f). apply H1.
assumption.
Qed.

Fixpoint vars (t : term) : variables :=
  match t with
    | Var x ⇒ x :: nil
    | Fun f v ⇒
      let fix vars_vec n (ts : terms n) {struct ts} : variables :=
        match ts with
          | Vector.nil ⇒ nil
          | Vector.cons t' n' ts' ⇒ vars t' ++ vars_vec n' ts'
        end
      in vars_vec (arity f) v
  end.

Fixpoint vars_vec n (ts : terms n) {struct ts} : variables :=
  match ts with
    | Vector.nil ⇒ nil
    | Vector.cons t' _ ts' ⇒ vars t' ++ vars_vec ts'
  end.

Lemma vars_fun : ∀ f ts, vars (Fun f ts) = vars_vec ts.

Proof.
auto.
Qed.

Lemma vars_vec_cast : ∀ n (ts : terms n) m (h : n=m),
  vars_vec (Vcast ts h) = vars_vec ts.

Proof.
induction ts; intros; destruct m; simpl; try (refl || discriminate).
apply (f_equal (fun l ⇒ vars h ++ l)). apply IHts.
Qed.

Lemma vars_vec_app : ∀ n1 (ts1 : terms n1) n2 (ts2 : terms n2),
  vars_vec (Vapp ts1 ts2) = vars_vec ts1 ++ vars_vec ts2.

Proof.
induction ts1; intros; simpl. refl. rewrite app_ass.
apply (f_equal (fun l ⇒ vars h ++ l)). apply IHts1.
Qed.

Lemma vars_vec_cons : ∀ t n (ts : terms n),
  vars_vec (Vector.cons t ts) = vars t ++ vars_vec ts.

Proof.
intros. refl.
Qed.

Lemma in_vars_vec_elim : ∀ x n (ts : terms n),
  In x (vars_vec ts) → ∃ t, Vin t ts ∧ In x (vars t).

Proof.
induction ts; simpl; intros. contradiction. generalize (in_app_or H). intro.
destruct H0. ∃ h. intuition. generalize (IHts H0). intro.
destruct H1 as [t].
∃ t. intuition.
Qed.

Lemma in_vars_vec_intro : ∀ x t n (ts : terms n),
  In x (vars t) → Vin t ts → In x (vars_vec ts).

Proof.
intros. ded (Vin_elim H0). do 5 destruct H1. subst ts.
rewrite vars_vec_cast. rewrite vars_vec_app. simpl.
apply in_appr. apply in_appl. exact H.
Qed.

Lemma vars_vec_in : ∀ x t n (ts : terms n),
  In x (vars t) → Vin t ts → In x (vars_vec ts).

Proof.
induction ts; simpl; intros. contradiction. destruct H0. subst t.
apply in_appl. assumption. apply in_appr. apply IHts; assumption.
Qed.

Lemma vars_max : ∀ x t, In x (vars t) → x ≤ maxvar t.

Proof.
intros x t. pattern t. apply term_ind with (Q := fun n (ts : terms n) ⇒
  In x (vars_vec ts) → x ≤ maxvars ts); clear t; intros.
simpl in ×. intuition. rewrite maxvar_fun. rewrite vars_fun in H0. auto.
contradiction. simpl in ×.
destruct (in_app_or H1); unfold maxvars; simpl. apply le_max_intro_l. auto.
apply le_max_intro_r. auto.
Qed.

Lemma maxvar_in : ∀ x t n (v : terms n),
  x ≤ maxvar t → Vin t v → x ≤ maxvars v.

Proof.
induction v; unfold maxvars; simpl; intros. contradiction. destruct H0.
subst t. apply le_max_intro_l. hyp. apply le_max_intro_r. apply IHv; hyp.
Qed.

Require Import ListMax.

Lemma maxvar_lmax : ∀ t, maxvar t = lmax (vars t).

Proof.
intro t. pattern t.
set (Q := fun n (ts : terms n) ⇒ maxvars ts = lmax (vars_vec ts)).
apply term_ind with (Q := Q); clear t.
intro. simpl. apply (sym_equal (max_l (le_O_n x))).
intros f ts H. rewrite maxvar_fun. rewrite vars_fun. assumption.
unfold Q. auto.
intros t n ts H1 H2. unfold Q. simpl. rewrite lmax_app.
unfold Q in H2. rewrite maxvars_cons. rewrite H1. rewrite H2. refl.
Qed.

Section var_occurs_in.

Variable x : variable.

Fixpoint var_occurs_in t :=
  match t with
    | Var y ⇒ beq_nat x y
    | Fun f ts ⇒
      let fix var_occurs_in_terms n (ts : terms n) :=
        match ts with
          | Vector.nil ⇒ false
          | Vector.cons t _ ts' ⇒ var_occurs_in t || var_occurs_in_terms _ ts'
        end
        in var_occurs_in_terms _ ts
  end.

End var_occurs_in.

Fixpoint nb_symb_occs t :=
  match t with
    | Var x ⇒ 0
    | Fun f ts ⇒
      let fix nb_symb_occs_terms n (ts : terms n) {struct ts} :=
        match ts with
          | Vector.nil ⇒ 0
          | Vector.cons u p us ⇒ nb_symb_occs u + nb_symb_occs_terms p us
        end
        in 1 + nb_symb_occs_terms _ ts
  end.

Fixpoint nb_symb_occs_terms n (ts : terms n) {struct ts} :=
  match ts with
    | Vector.nil ⇒ 0
    | Vector.cons u p us ⇒ nb_symb_occs u + nb_symb_occs_terms us
  end.

Lemma nb_symb_occs_fix : ∀ n (ts : terms n),
  (fix nb_symb_occs_terms n (ts : terms n) {struct ts} :=
    match ts with
      | Vector.nil ⇒ 0
      | Vector.cons u p us ⇒ nb_symb_occs u + nb_symb_occs_terms p us
    end) _ ts = nb_symb_occs_terms ts.

Proof.
induction ts; simpl; intros. refl. rewrite IHts. refl.
Qed.

Lemma nb_symb_occs_fun : ∀ f ts,
  nb_symb_occs (Fun f ts) = 1 + nb_symb_occs_terms ts.

Proof.
intros. simpl. rewrite nb_symb_occs_fix. refl.
Qed.

Lemma Vin_nb_symb_occs_terms_ge : ∀ n (ts : terms n) t,
  Vin t ts → nb_symb_occs_terms ts ≥ nb_symb_occs t.

Proof.
induction ts; simpl; intros. contradiction. destruct H. subst h. omega.
ded (IHts _ H). omega.
Qed.

Fixpoint size t :=
  match t with
    | Var x ⇒ 1
    | Fun f ts ⇒
      let fix size_terms n (ts : terms n) {struct ts} :=
        match ts with
          | Vector.nil ⇒ 0
          | Vector.cons u p us ⇒ size u + size_terms p us
        end
        in 1 + size_terms _ ts
  end.

Fixpoint size_terms n (ts : terms n) {struct ts} :=
  match ts with
    | Vector.nil ⇒ 0
    | Vector.cons u _ us ⇒ size u + size_terms us
  end.

Lemma size_fix : ∀ n (ts : terms n),
  (fix size_terms n (ts : terms n) {struct ts} :=
    match ts with
      | Vector.nil ⇒ 0
      | Vector.cons u p us ⇒ size u + size_terms p us
    end) _ ts = size_terms ts.

Proof.
induction ts; simpl; intros. refl. rewrite IHts. refl.
Qed.

Lemma size_fun : ∀ f ts, size (Fun f ts) = 1 + size_terms ts.

Proof.
intros. simpl. rewrite size_fix. refl.
Qed.

Lemma size_non_zero : ∀ t, size t > 0.

Proof.
intro. pattern t. apply term_ind with (Q := fun n (ts : terms n) ⇒
  size_terms ts ≥ 0); clear t.
intro. simpl. omega.
intros. rewrite size_fun. omega.
simpl. omega.
intros. simpl. omega.
Qed.

Lemma Vin_size_terms_ge : ∀ n (ts : terms n) t,
  Vin t ts → size_terms ts ≥ size t.

Proof.
induction ts; simpl; intros. contradiction. destruct H. subst h. omega.
ded (IHts _ H). omega.
Qed.

Implicit Arguments Vin_size_terms_ge [n ts t].

Lemma Vin_size_terms_gt : ∀ n (ts : terms n) t,
  Vin t ts → n > 1 → size_terms ts > size t.

Proof.
destruct ts. intros; omega.
destruct ts. intros; omega.
simpl. intros.

ded (size_non_zero h). ded (size_non_zero h0).
destruct H. subst t. omega. destruct H. subst t. omega.
ded (Vin_size_terms_ge H). omega.
Qed.

Lemma size_terms_Vcast : ∀ n (ts : terms n) m (h : n=m),
  size_terms (Vcast ts h) = size_terms ts.

Proof.
induction ts. intro. destruct m. intro. castrefl h. intro. discriminate.
intro. destruct m. intro. discriminate. intro. inversion h0. simpl. rewrite IHts.
refl.
Qed.

Lemma size_terms_Vapp : ∀ n (ts : terms n) m (us : terms m),
  size_terms (Vapp ts us) = size_terms ts + size_terms us.

Proof.
induction ts; simpl; intros. refl. rewrite IHts. omega.
Qed.

Definition direct_subterms (t : term) : list term :=
  match t with
  | Var x ⇒ nil
  | Fun f fs ⇒ list_of_vec fs
  end.

End S.

Implicit Arguments Var [Sig].
Implicit Arguments maxvar_var [Sig k x].
Implicit Arguments maxvar_le_fun [Sig m f ts].
Implicit Arguments maxvar_le_arg [Sig f ts m t].
Implicit Arguments in_vars_vec_elim [Sig x n ts].
Implicit Arguments in_vars_vec_intro [Sig x t n ts].
Implicit Arguments vars_vec_in [Sig x t n ts].
Implicit Arguments vars_max [Sig x t].
Implicit Arguments Vin_nb_symb_occs_terms_ge [Sig n ts t].
Implicit Arguments Vin_size_terms_ge [Sig n ts t].
Implicit Arguments Vin_size_terms_gt [Sig n ts t].

Ltac Funeqtac :=
  match goal with
    | H : @Fun _ ?f _ = @Fun _ ?f _ |- _ ⇒ ded (fun_eq H); clear H
    | H : @Fun _ ?f _ = @Fun _ ?g _ |- _ ⇒
      ded (symb_eq H); try ((subst g || subst f); ded (fun_eq H); clear H)
  end.