From Coq Require Import List Arith.
From hydras Require Import more_list list_permut list_set.

Set Implicit Arguments.

Module Type Signature.

  Parameter symb : Set.
  Axiom eq_symbol_dec : ∀ f1 f2 : symb, {f1 = f2} + {f1 ≠ f2}.

  Inductive arity_type : Set :=
  | AC : arity_type
  | C : arity_type
  | Free : nat → arity_type.

  Parameter arity : symb → arity_type.
End Signature.

Module Type Variables.

  Parameter var : Set.
  Axiom eq_variable_dec : ∀ v1 v2 : var, {v1 = v2} + {v1 ≠ v2}.

End Variables.

Module Type Term.

  Declare Module F : Signature.
  Declare Module X : Variables.

  Definition symbol := F.symb.
  Definition variable := X.var.

  Import F.
  Import X.


  Ltac destruct_arity f n Af :=
    generalize (refl_equal (arity f)); pattern f at 1; destruct (arity f) as [ | | n]; intro Af.

  Inductive term : Set :=
  | Var : variable → term
  | Term : symbol → list term → term.

  Definition direct_subterm t1 t2 : Prop :=
    match t2 with
    | Var _ ⇒ False
    | Term _ l ⇒ In t1 l
    end.

  Fixpoint size (t:term) : nat :=
    match t with
    | Var v ⇒ 1
    | Term f l ⇒ 1 + fold_left (fun size_acc e ⇒ size_acc + size e) l 0
    end.

  Axiom size_unfold :
    ∀ t, size t = match t with
                       | Var _ ⇒ 1
                       | Term f l ⇒ 1 + list_size size l
                       end.

  Axiom size_ge_one : ∀ t, 1 ≤ size t.

  Axiom size_direct_subterm :
    ∀ t1 t2, direct_subterm t1 t2 → size t1 < size t2.

  Section Recursion.
    Variable P : term → Type.
    Variable Pl : list term → Type.

    Axiom term_rec2 : (∀ n t, size t ≤ n → P t) → ∀ t, P t.
    Axiom term_rec3 :
      (∀ v, P (Var v)) → (∀ f l, (∀ t, In t l → P t) → P (Term f l)) → ∀ t, P t.
    Axiom term_rec4 :
      (∀ v, P (Var v)) → (∀ f l, Pl l → P (Term f l)) →
      (∀ l, (∀ t, In t l → P t) → Pl l) → ∀ t, P t.
  End Recursion.

  Section DoubleRecursion.
    Variable P2 : term → term → Type.
    Variable Pl2 : list term → list term → Type.

    Axiom term_rec7 :
      (∀ v1 t2, P2 (Var v1) t2) →
      (∀ t1 v2, P2 t1 (Var v2)) →
      (∀ f1 f2 l1 l2, Pl2 l1 l2 → P2 (Term f1 l1) (Term f2 l2)) →
      (∀ l1 l2, (∀ t1 t2, In t1 l1 → In t2 l2 → P2 t1 t2) → Pl2 l1 l2) →
      ∀ t1 t2, P2 t1 t2.

    Axiom term_rec8 :
      (∀ v1 t2, P2 (Var v1) t2) →
      (∀ t1 v2, P2 t1 (Var v2)) →
      (∀ f1 f2 l1 l2, Pl2 l1 l2 → P2 (Term f1 l1) (Term f2 l2)) →
      (∀ l1 l2, (∀ t1 t2, In t1 l1 → In t2 l2 → P2 t1 t2) → Pl2 l1 l2) →
      ∀ l1 l2, Pl2 l1 l2.
  End DoubleRecursion.

  Axiom eq_term_dec : ∀ t1 t2:term, {t1 = t2} + {t1 ≠ t2}.
  Declare Module Term_eq_dec : decidable_set.S with Definition A:= term
    with Definition eq_A_dec := eq_term_dec.

  Fixpoint well_formed (t:term) : Prop :=
    match t with
    | Var _ ⇒ True
    | Term f l ⇒
      let well_formed_list :=
          (fix well_formed_list (l:list term) : Prop :=
             match l with
             | nil ⇒ True
             | h :: tl ⇒ well_formed h ∧ well_formed_list tl
             end) in
      well_formed_list l ∧
      (match arity f with
       | Free n ⇒ length l = n
       | _ ⇒ length l = 2
       end)
    end.

  Axiom well_formed_unfold :
    ∀ t, well_formed t →
              match t with
              | Var _ ⇒ True
              | Term f l ⇒
                (∀ u, In u l → well_formed u) ∧
                (match arity f with
                 | Free n ⇒ length l = n
                 | _ ⇒ length l = 2
                 end)
              end.

  Axiom well_formed_fold :
    ∀ t,
      match t with
      | Var _ ⇒ True
      | Term f l ⇒
        (∀ u, In u l → well_formed u) ∧
        (match arity f with
         | Free n ⇒ length l = n
         | _ ⇒ length l = 2
         end)
      end → well_formed t.

  Fixpoint well_formed_list (l : list term) : Prop :=
    match l with
    | nil ⇒ True
    | h :: tl ⇒ well_formed h ∧ well_formed_list tl
    end.

  Definition substitution := list (variable × term).

  Fixpoint apply_subst (sigma : substitution) (t : term) {struct t} : term :=
    match t with
    | Var v ⇒
      match find eq_variable_dec v sigma with
      | None ⇒ t
      | Some v_sigma ⇒ v_sigma
      end
    | Term f l ⇒ Term f (map (apply_subst sigma) l)
    end.

  Axiom empty_subst_is_id : ∀ t, apply_subst nil t = t.
  Axiom empty_subst_is_id_list : ∀ l, map (apply_subst nil) l = l.

  Definition map_subst (f : variable → term → term) sigma :=
    map (fun x ⇒
           match (x : variable × term) with
           | (v, v_sigma) ⇒ (v, f v v_sigma)
           end)
        sigma.

  Definition subst_comp sigma1 sigma2 :=
    (map_subst (fun _ t ⇒ apply_subst sigma1 t) sigma2)
      ++
      (map_subst (fun v t ⇒
                    match find eq_variable_dec v sigma2 with
                    | None ⇒ t
                    | Some v_sigma2 ⇒ apply_subst sigma1 v_sigma2
                    end)
                 sigma1).

  Axiom subst_comp_is_subst_comp_aux1 :
    ∀ v sigma f,
      find eq_variable_dec v (map_subst f sigma) =
      match find eq_variable_dec v sigma with
      | None ⇒ None
      | Some t ⇒ Some (f v t)
      end.

  Axiom subst_comp_is_subst_comp :
    ∀ sigma1 sigma2 t,
      apply_subst (subst_comp sigma1 sigma2) t =
      apply_subst sigma1 (apply_subst sigma2 t).

  Definition well_formed_subst sigma :=
    ∀ v, match find eq_variable_dec v sigma with
              | None ⇒ True
              | Some t ⇒ well_formed t
              end.

  Axiom well_formed_apply_subst :
    ∀ sigma, well_formed_subst sigma →
                  ∀ t, well_formed t → well_formed (apply_subst sigma t).

  Fixpoint is_a_pos (t : term) (p : list nat) {struct p}: bool :=
    match p with
    | nil ⇒ true
    | i :: q ⇒
      match t with
      | Var _ ⇒ false
      | Term _ l ⇒
        match nth_error l i with
        | Some ti ⇒ is_a_pos ti q
        | None ⇒ false
        end
      end
    end.

  Fixpoint subterm_at_pos (t : term) (p : list nat) {struct p}: option term :=
    match p with
    | nil ⇒ Some t
    | i :: q ⇒
      match t with
      | Var _ ⇒ None
      | Term _ l ⇒
        match nth_error l i with
        | Some ti ⇒ subterm_at_pos ti q
        | None ⇒ None
        end
      end
    end.

  Axiom size_subterm_at_pos :
    ∀ t i p, match subterm_at_pos t (i :: p) with
                  | Some u ⇒ size u < size t
                  | None ⇒ True
                  end.

  Axiom is_a_pos_exists_subtem :
    ∀ t p, is_a_pos t p = true → ∃ u, subterm_at_pos t p = Some u.

  Fixpoint replace_at_pos (t u : term) (p : list nat) {struct p} : term :=
    match p with
    | nil ⇒ u
    | i :: q ⇒
      match t with
      | Var _ ⇒ t
      | Term f l ⇒
        let replace_at_pos_list :=
            (fix replace_at_pos_list j (l : list term) {struct l}: list term :=
               match l with
               | nil ⇒ nil
               | h :: tl ⇒
                 match j with
                 | O ⇒ (replace_at_pos h u q) :: tl
                 | S k ⇒ h :: (replace_at_pos_list k tl)
                 end
               end) in
        Term f (replace_at_pos_list i l)
      end
    end.

  Fixpoint replace_at_pos_list (l : list term) (u : term) (i : nat) (p : list nat)
           {struct l}: list term :=
    match l with
    | nil ⇒ nil
    | h :: tl ⇒
      match i with
      | O ⇒ (replace_at_pos h u p) :: tl
      | S j ⇒ h :: (replace_at_pos_list tl u j p)
      end
    end.

  Axiom replace_at_pos_unfold :
    ∀ f l u i q,
      replace_at_pos (Term f l) u (i :: q) = Term f (replace_at_pos_list l u i q).

  Axiom replace_at_pos_is_replace_at_pos1 :
    ∀ t u p, is_a_pos t p = true →
                  subterm_at_pos (replace_at_pos t u p) p = Some u.

  Axiom replace_at_pos_is_replace_at_pos2 :
    ∀ t p u, subterm_at_pos t p = Some u → replace_at_pos t u p = t.

  Axiom subterm_at_pos_apply_subst_apply_subst_subterm_at_pos :
    ∀ t p sigma,
      match subterm_at_pos t p with
      | Some u ⇒
        subterm_at_pos (apply_subst sigma t) p = Some (apply_subst sigma u)
      | None ⇒ True
      end.

  Axiom replace_at_pos_list_replace_at_pos_in_subterm :
    ∀ l1 ui l2 u i p, length l1 = i →
                           replace_at_pos_list (l1 ++ ui :: l2) u i p =
                           l1 ++ (replace_at_pos ui u p) :: l2.

End Term.

Module Make (F1 : Signature) (X1 : Variables) <:
  Term with Module F := F1 with Module X := X1.

  Module F := F1.
  Module X := X1.

  Definition symbol := F.symb.
  Definition variable := X.var.

  Import F.
  Import X.

  Module DecVar <: decidable_set.S.
    Definition A := variable.

    Lemma eq_A_dec : ∀ x y : A, { x = y } + { x ≠ y }.

  End DecVar.

  Module VSet <: list_set.S with Definition DS.A := variable :=
    list_set.Make (DecVar).

  Inductive term : Set :=
  | Var : variable → term
  | Term : symbol → list term → term.

  Definition direct_subterm t1 t2 : Prop :=
    match t2 with
    | Var _ ⇒ False
    | Term _ l ⇒ In t1 l
    end.

  Fixpoint size (t:term) : nat :=
    match t with
    | Var v ⇒ 1
    | Term f l ⇒ 1 + fold_left (fun size_acc e ⇒ size_acc + size e) l 0
    end.

  Lemma size_unfold :
    ∀ t,
      size t = match t with
               | Var _ ⇒ 1
               | Term f l ⇒ 1 + list_size size l
               end.

  Lemma size_ge_one : ∀ t, 1 ≤ size t.

  Lemma size_direct_subterm :
    ∀ t1 t2, direct_subterm t1 t2 → size t1 < size t2.

  Section Recursion.
    Variable P : term → Type.
    Variable Pl : list term → Type.

    Definition term_rec2 : (∀ n t, size t ≤ n → P t) → ∀ t, P t.

    Definition term_rec3 :
      (∀ v, P (Var v)) → (∀ f l, (∀ t, In t l → P t) → P (Term f l)) → ∀ t, P t.

    Definition term_rec4 :
      (∀ v, P (Var v)) → (∀ f l, Pl l → P (Term f l)) →
      (∀ l, (∀ t, In t l → P t) → Pl l) → ∀ t, P t.
  End Recursion.

  Section DoubleRecursion.
    Variable P2 : term → term → Type.
    Variable Pl2 : list term → list term → Type.

    Definition term_rec7 :
      (∀ v1 t2, P2 (Var v1) t2) →
      (∀ t1 v2, P2 t1 (Var v2)) →
      (∀ f1 f2 l1 l2, Pl2 l1 l2 → P2 (Term f1 l1) (Term f2 l2)) →
      (∀ l1 l2, (∀ t1 t2, In t1 l1 → In t2 l2 → P2 t1 t2) → Pl2 l1 l2) →
      ∀ t1 t2, P2 t1 t2.

    Definition term_rec8 :
      (∀ v1 t2, P2 (Var v1) t2) →
      (∀ t1 v2, P2 t1 (Var v2)) →
      (∀ f1 f2 l1 l2, Pl2 l1 l2 → P2 (Term f1 l1) (Term f2 l2)) →
      (∀ l1 l2, (∀ t1 t2, In t1 l1 → In t2 l2 → P2 t1 t2) → Pl2 l1 l2) →
      ∀ l1 l2, Pl2 l1 l2.
  End DoubleRecursion.

  Theorem eq_term_dec :
    ∀ t1 t2:term, {t1 = t2} + {t1 ≠ t2}.

  Module Term_eq_dec : decidable_set.S with Definition A:= term
    with Definition eq_A_dec := eq_term_dec.
    Definition A := term.
    Definition eq_A_dec := eq_term_dec.
  End Term_eq_dec.

  Fixpoint well_formed (t:term) : Prop :=
    match t with
    | Var _ ⇒ True
    | Term f l ⇒
      let well_formed_list :=
          (fix well_formed_list (l:list term) : Prop :=
             match l with
             | nil ⇒ True
             | h :: tl ⇒ well_formed h ∧ well_formed_list tl
             end) in
      well_formed_list l ∧
      (match arity f with
       | Free n ⇒ length l = n
       | _ ⇒ length l = 2
       end)
    end.

  Lemma well_formed_unfold :
    ∀ t, well_formed t →
              match t with
              | Var _ ⇒ True
              | Term f l ⇒
                (∀ u, In u l → well_formed u) ∧
                (match arity f with
                 | Free n ⇒ length l = n
                 | _ ⇒ length l = 2
                 end)
              end.

  Lemma well_formed_fold :
    ∀ t,
      match t with
      | Var _ ⇒ True
      | Term f l ⇒
        (∀ u, In u l → well_formed u) ∧
        (match arity f with
         | Free n ⇒ length l = n
         | _ ⇒ length l = 2
         end)
      end → well_formed t.

  Fixpoint well_formed_list (l : list term) : Prop :=
    match l with
    | nil ⇒ True
    | h :: tl ⇒ well_formed h ∧ well_formed_list tl
    end.

  Definition substitution := list (variable × term).

  Fixpoint apply_subst (sigma : substitution) (t : term) {struct t} : term :=
    match t with
    | Var v ⇒
      match find eq_variable_dec v sigma with
      | None ⇒ t
      | Some v_sigma ⇒ v_sigma
      end
    | Term f l ⇒ Term f (map (apply_subst sigma) l)
    end.

  Lemma empty_subst_is_id : ∀ t, apply_subst nil t = t.

  Lemma empty_subst_is_id_list : ∀ l, map (apply_subst nil) l = l.

  Definition map_subst (f : variable → term → term) sigma :=
    map (fun x ⇒
           match (x : variable × term) with
           | (v, v_sigma) ⇒ (v, f v v_sigma)
           end)
        sigma.

  Definition subst_comp sigma1 sigma2 :=
    (map_subst (fun _ t ⇒ apply_subst sigma1 t) sigma2)
      ++
      (map_subst (fun v t ⇒
                    match find eq_variable_dec v sigma2 with
                    | None ⇒ t
                    | Some v_sigma2 ⇒ apply_subst sigma1 v_sigma2
                    end)
                 sigma1).

  Lemma subst_comp_is_subst_comp_aux1 :
    ∀ v sigma f,
      find eq_variable_dec v (map_subst f sigma) =
      match find eq_variable_dec v sigma with
      | None ⇒ None
      | Some t ⇒ Some (f v t)
      end.

  Lemma subst_comp_is_subst_comp_aux2 :
    ∀ v sigma1 sigma2,
      find (B:= term) eq_variable_dec v (sigma1 ++ sigma2) =
      match find eq_variable_dec v sigma1 with
      | Some _ ⇒ find eq_variable_dec v sigma1
      | None ⇒ find eq_variable_dec v sigma2
      end.

  Theorem subst_comp_is_subst_comp :
    ∀ sigma1 sigma2 t,
      apply_subst (subst_comp sigma1 sigma2) t =
      apply_subst sigma1 (apply_subst sigma2 t).

  Definition well_formed_subst sigma :=
    ∀ v, match find eq_variable_dec v sigma with
              | None ⇒ True
              | Some t ⇒ well_formed t
              end.

  Theorem well_formed_apply_subst :
    ∀ sigma, well_formed_subst sigma →
                  ∀ t, well_formed t → well_formed (apply_subst sigma t).

  Fixpoint is_a_pos (t : term) (p : list nat) {struct p}: bool :=
    match p with
    | nil ⇒ true
    | i :: q ⇒
      match t with
      | Var _ ⇒ false
      | Term _ l ⇒
        match nth_error l i with
        | Some ti ⇒ is_a_pos ti q
        | None ⇒ false
        end
      end
    end.

  Fixpoint subterm_at_pos (t : term) (p : list nat) {struct p}: option term :=
    match p with
    | nil ⇒ Some t
    | i :: q ⇒
      match t with
      | Var _ ⇒ None
      | Term _ l ⇒
        match nth_error l i with
        | Some ti ⇒ subterm_at_pos ti q
        | None ⇒ None
        end
      end
    end.

  Lemma size_subterm_at_pos :
    ∀ t i p, match subterm_at_pos t (i :: p) with
                  | Some u ⇒ size u < size t
                  | None ⇒ True
                  end.

  Lemma is_a_pos_exists_subtem :
    ∀ t p, is_a_pos t p = true → ∃ u, subterm_at_pos t p = Some u.

  Fixpoint replace_at_pos (t u : term) (p : list nat) {struct p} : term :=
    match p with
    | nil ⇒ u
    | i :: q ⇒
      match t with
      | Var _ ⇒ t
      | Term f l ⇒
        let replace_at_pos_list :=
            (fix replace_at_pos_list j (l : list term) {struct l}: list term :=
               match l with
               | nil ⇒ nil
               | h :: tl ⇒
                 match j with
                 | O ⇒ (replace_at_pos h u q) :: tl
                 | S k ⇒ h :: (replace_at_pos_list k tl)
                 end
               end) in
        Term f (replace_at_pos_list i l)
      end
    end.

  Fixpoint replace_at_pos_list (l : list term) (u : term) (i : nat) (p : list nat)
           {struct l}: list term :=
    match l with
    | nil ⇒ nil
    | h :: tl ⇒
      match i with
      | O ⇒ (replace_at_pos h u p) :: tl
      | S j ⇒ h :: (replace_at_pos_list tl u j p)
      end
    end.

  Lemma replace_at_pos_unfold :
    ∀ f l u i q,
      replace_at_pos (Term f l) u (i :: q) = Term f (replace_at_pos_list l u i q).

  Lemma replace_at_pos_is_replace_at_pos1 :
    ∀ t u p, is_a_pos t p = true →
                  subterm_at_pos (replace_at_pos t u p) p = Some u.

  Lemma replace_at_pos_is_replace_at_pos2 :
    ∀ t p u, subterm_at_pos t p = Some u → replace_at_pos t u p = t.

  Lemma subterm_at_pos_apply_subst_apply_subst_subterm_at_pos :
    ∀ t p sigma,
      match subterm_at_pos t p with
      | Some u ⇒
        subterm_at_pos (apply_subst sigma t) p = Some (apply_subst sigma u)
      | None ⇒ True
      end.

  Lemma replace_at_pos_list_replace_at_pos_in_subterm :
    ∀ l1 ui l2 u i p, length l1 = i →
                           replace_at_pos_list (l1 ++ ui :: l2) u i p =
                           l1 ++ (replace_at_pos ui u p) :: l2.

End Make.