Here's the code. I'm stuck.

Thanks in advance for your hints!

```
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.
```

I haven't looked (too much code, you should probably try to reduce your examples before asking questions) but as a side note your `vector`

type is known to be rather hard to work with. It is often much more convenient to work with a list and a proof about the size of that list, see the `tuple`

type in MathComp for instance.

Thank you! Yes, it seems that's better to change to your suggestion instead, as `vector`

seems to be too difficult.

Lessness has marked this topic as resolved.

It is also possible to define _pre-terms_ (just nested labelled trees), then define well-formedness (i.e respect of function's arity) by a boolean function. Sea also MathComp's way of using generic trees and subtypes for building countable types: https://math-comp.github.io/htmldoc_1_14_0/mathcomp.ssreflect.choice.html

Lessness has marked this topic as unresolved.

```
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.
```

This gets stuck with `Non strictly positive occurrence`

error.

`tuple`

like type won't work for me here. Back to `vector`

type...

I think it should be possible to fix strict positivity by pulling `length x = n`

out of the recursion

An alternative approach is to consider partially applied terms:

```
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.
```

Then proper terms are partially applied terms of arity 0, ie of type `Term V L 0`

.

Oh, I was thinking about a definition like below (to be completed)

```
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.
```

why `preTerms`

instead of `list preTerm`

?

It allows to derive principles of mutual induction with the `Scheme ... with ...`

command.

Some time ago, we had to define ourselves induction principles out of the definition with `list preTerm`

. Have to check whether it's still true.

Thank you all! I will choose Pierre's suggestion, but with `list preTerm`

. At least for now.

The `vector`

slowly became too difficult to handle. :(

@Pierre Castéran still true — `Scheme`

will give induction principles but they're too weak

For (an old) discussion about mutual induction, you may look at https://www-sop.inria.fr/members/Yves.Bertot/coqart-chapter14.pdf (p. 400).

About vectors: Russel O'connor's definition of primitive recursive functions uses heavily stdlib's vector. It's very interesting to look at this construction (projects https://github.com/coq-community/goedel and https://github.com/coq-community/hydra-battles).

The pre-term approach is used in hydra-battles and https://github.com/coq-community/gaia to define ordinal notations with a base inductive type and a boolean well-formedness predicate.

Lessness said:

This gets stuck with

`Non strictly positive occurrence`

error.

MathComp has a way around that, summarized by the following quote at the start of the finfun file:

`(T ^ n)%type`

is notation for`{ffun 'I_n -> T}`

, which is isomorphic

to`n.-tuple T`

, but is structurally positive and thus can be used to

define inductive types, e.g.,`Inductive tree := node n of tree ^ n`

(see

mid-file for an expanded example)

Lessness has marked this topic as resolved.

I was trying Olivier's approach too and got stuck with a problem, when trying do induction. See the error message:

```
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.
```

And the code:

```
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.
```

Lessness has marked this topic as unresolved.

How to work around this error? Thank you!

You can generalize your notion of injectivity to allow for different indices. `hinjective I (A : I -> Type) (B : Type) (f : forall i, A i -> B) : Prop := forall i x j y, f i x = f j x -> eq_dep I A i x j y`

, allowing you to destruct `x`

and `y`

separately. And then `eq_dep`

can be related to `=`

as a separate step: `eq_dep_eq_nat : eq_dep nat A i x i y -> x = y`

Last updated: Jan 28 2023 at 07:30 UTC