Stream: Coq users

Topic: Any hints how to prove injectivity?


view this post on Zulip Lessness (Aug 07 2022 at 20:05):

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 08 2022 at 04:47):

Lessness has marked this topic as resolved.

view this post on Zulip 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

view this post on Zulip Notification Bot (Aug 08 2022 at 19:07):

Lessness has marked this topic as unresolved.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Aug 08 2022 at 21:09):

why preTerms instead of list preTerm?

view this post on Zulip 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.

view this post on Zulip 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. :(

view this post on Zulip Paolo Giarrusso (Aug 08 2022 at 22:50):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Notification Bot (Aug 09 2022 at 17:17):

Lessness has marked this topic as resolved.

view this post on Zulip 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.
Admitted.

view this post on Zulip Notification Bot (Aug 10 2022 at 13:53):

Lessness has marked this topic as unresolved.

view this post on Zulip Lessness (Aug 10 2022 at 13:53):

How to work around this error? Thank you!

view this post on Zulip 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: Mar 29 2024 at 10:01 UTC