Require Import Utf8 List.
Set Implicit Arguments.

Definition injective A B (f: A → B) :=
  ∀ x y, f x = f y → x = y.

Inductive vector A: nat → Type :=
  | vnil: vector A 0
  | vcons: ∀ (n: nat), A → vector A n → vector A (S n).
Arguments vnil {A}.

Notation "A ^ n" := (vector A n): vector_scope.
Notation "[ ]" := (vnil) (format "[ ]"): vector_scope.
Notation "[ x ]" := (vcons x nil): vector_scope.
Notation "[ x ; y ; .. ; z ]" := (vcons x (vcons y .. (vcons z vnil) ..)): vector_scope.

Open Scope vector_scope.

Inductive hvector A (F: A → Type): ∀ n, A^n → Type :=
  | Hnil: hvector F vnil
  | Hcons: ∀ n x v, F x → hvector F v → hvector F (@vcons _ n x v).

Structure Language F R := {
  function_arity: F → nat;
  relation_arity: R → nat
}.

Inductive Term F R V (L: Language F R) :=
  | variable: V → Term V L
  | function_term: ∀ (f: F), Term V L ^ function_arity L f → Term V L.
Arguments variable {_} {_} {_} {L}. (*?*)

Module vector.
  Fixpoint fold_right A B (f: B → A → A) (a0: A) n (v: B^n): A :=
  match v with
  | vnil => a0
  | vcons x t => f x (fold_right f a0 t)
  end.
  Definition Forall A (P: A → Prop) n (v: A^n) := fold_right (λ x, and (P x)) True v.
End vector.

Definition Term_induction F R V (L: Language F R) (P: Term V L → Prop):
  (∀ (s: V), P (variable s)) →
  (∀ (f: F) (v: Term V L ^ function_arity L f), vector.Forall P v → P (function_term f v)) →
  ∀ T, P T.
Proof.
  intros H H0. refine (fix IHt (t: Term V L) := match t with variable v => H v | function_term f T => _ end).
  refine (H0 _ T _). induction T; [exact I | split; auto].
Qed.

Definition Term_recursion F R V (L: Language F R) (P: Term V L → Type):
  (∀ v : V, P (variable v)) →
  (∀ (f : F) (v : Term V L ^ function_arity L f), hvector P v → P (function_term f v)) →
  ∀ t, P t.
Proof.
  intros H H0. refine (fix IHt (t: Term V L) := match t with variable v => H v | function_term f T => _ end).
  refine (H0 _ T _). intros. induction T.
  + constructor.
  + constructor. apply IHt. exact IHT.
Defined.

Inductive character F V: Type :=
  | function_char: F → character F V
  | variable_char: V → character F V
  | left_bracket_char
  | right_bracket_char.
Arguments function_char {F} {V}.
Arguments variable_char {F} {V}.
Arguments left_bracket_char {F} {V}.
Arguments right_bracket_char {F} {V}.

Definition term_to_character_list F R V (L: Language F R) (T: Term V L): list (character F V).
Proof.
  induction T using Term_recursion.
  + exact (left_bracket_char :: variable_char v :: right_bracket_char :: nil).
  + refine (left_bracket_char :: function_char f :: _ ++ right_bracket_char :: nil).
    revert v X. generalize (function_arity L f).
    refine (fix aux n v hv := match hv with
                | Hnil _ => nil
                | Hcons _ x t => x ++ aux _ _ t
                 end).
Defined.

Theorem term_to_character_injective F R V (L: Language F R): injective (@term_to_character_list F R V L).
Proof.
  intros x. induction x using Term_induction.
  + intros. destruct y; simpl in *; congruence.
  + induction y using Term_induction.
    - intros. simpl in *. congruence.
    - intros. assert (f = f0) by (inversion H1; subst; auto). subst. f_equal.
Admitted.

Require Import List.
Set Implicit Arguments.

Definition vector A n := { x: list A | length x = n }.

Structure Language F R := {
  function_arity: F -> nat;
  relation_arity: R -> nat
}.

Inductive Term F R V (L: Language F R) :=
  | variable: V -> Term V L
  | function_term: forall (f: F), vector (Term V L) (function_arity L f) -> Term V L.

Inductive Term F R V (L: Language F R) : nat -> Type :=
  | variable: V -> Term V L 0
  | function_term: forall f, Term V L (function_arity L f)
  | apply_term: forall n, Term V L (S n) -> Term V L 0 -> Term V L n.

Section TermsDef.
  Variables V F R: Type.

  Inductive preTerm : Type :=
    variable (v: V)
  | fun_node (f: F)(args : preTerms)
  with preTerms : Type :=
    nil : preTerms
  | cons (hd: preTerm)(tl : preTerms).


Parameter well_formed : Language F R -> preTerm ->  bool.
(* To define *)

Definition term (L : Language F R) :=
  {p : preTerm | is_true (well_formed L p)}.

End TermsDef.

Abstracting over the terms "n" and "y" leads to a term
λ (n0 : nat) (y0 : Term V L n0),
  left_bracket_char :: variable_char v :: right_bracket_char :: nil = term_to_character_list y0 → variable L v = y0
which is ill-typed.

Require Import Utf8 List.
Set Implicit Arguments.

Structure Language F := {
  function_arity: F → nat;
}.

Inductive Term F V (L: Language F): nat → Type :=
  | variable: V → Term V L 0
  | function_term: ∀ f, Term V L (function_arity L f)
  | apply_function_term: ∀ n, Term V L (S n) → Term V L 0 → Term V L n.

Definition injective A B (f: A → B) := ∀ x y, f x = f y → x = y.

Inductive character F V: Type :=
  | function_char: F → character F V
  | variable_char: V → character F V
  | left_bracket_char
  | right_bracket_char.
Arguments function_char {F} {V}.
Arguments variable_char {F} {V}.
Arguments left_bracket_char {F} {V}.
Arguments right_bracket_char {F} {V}.

Definition term_to_character_list F V (L: Language F) n (T: Term V L n): list (character F V).
Proof.
  induction T.
  + exact (left_bracket_char :: variable_char v :: right_bracket_char :: (@nil (character F V))).
  + exact (function_char f :: nil).
  + exact (left_bracket_char :: IHT1 ++ IHT2 ++ right_bracket_char :: nil).
Defined.

Theorem term_to_character_injective F V (L: Language F): injective (@term_to_character_list F V L 0).
Proof.
  unfold injective. induction x; simpl in *; intros.
  + Fail induction y.
Admitted.