## Stream: Coq users

### Topic: Any hints how to prove injectivity?

#### Lessness (Aug 07 2022 at 20:05):

Here's the code. I'm stuck.

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

#### Pierre Roux (Aug 07 2022 at 21:34):

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.

#### Lessness (Aug 08 2022 at 04:47):

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

#### Notification Bot (Aug 08 2022 at 04:47):

Lessness has marked this topic as resolved.

#### Pierre Castéran (Aug 08 2022 at 07:56):

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

#### Notification Bot (Aug 08 2022 at 19:07):

Lessness has marked this topic as unresolved.

#### Lessness (Aug 08 2022 at 19:09):

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

#### Paolo Giarrusso (Aug 08 2022 at 19:42):

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

#### Olivier Laurent (Aug 08 2022 at 20:13):

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

#### Pierre Castéran (Aug 08 2022 at 21:04):

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

#### Gaëtan Gilbert (Aug 08 2022 at 21:09):

why `preTerms` instead of `list preTerm`?

#### Pierre Castéran (Aug 08 2022 at 21:30):

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.

#### Lessness (Aug 08 2022 at 21:36):

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. :(

#### Paolo Giarrusso (Aug 08 2022 at 22:50):

@Pierre Castéran still true — `Scheme` will give induction principles but they're too weak

#### Pierre Castéran (Aug 09 2022 at 05:26):

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.

#### Ana de Almeida Borges (Aug 09 2022 at 11:45):

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)

#### Notification Bot (Aug 09 2022 at 17:17):

Lessness has marked this topic as resolved.

#### Lessness (Aug 10 2022 at 13:52):

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

#### Notification Bot (Aug 10 2022 at 13:53):

Lessness has marked this topic as unresolved.

#### Lessness (Aug 10 2022 at 13:53):

How to work around this error? Thank you!

#### Li-yao (Aug 10 2022 at 14:24):

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: Sep 30 2023 at 06:01 UTC