Je suis ici avec Coq pour étudier les relations entre deux types que j'ai définis. Le premier est quelque chose comme un sous-ensemble fini de nat, avec seulement trois éléments:

Inductive N3 := zero | one | two.

Le second est un type sigma avec des éléments satisfaisant la proposition {x: nat | x < 3}. Voici sa définition:

Definition less_than_3 := {x| x < 3}.

Je veux prouver que ces deux types sont isomorphes. J'ai défini les deux fonctions impliquées de la manière suivante:

Definition lt3_to_N3 (n: less_than_3) : N3 :=
match n with
  | exist 0 _ => zero
  | exist 1 _ => one
  | exist 2 _ => two
  | exist _ _ => two
end.

Definition N3_to_lt3 (n: N3) : less_than_3 :=
match n with
  | zero => exist _ 0 l_0_3
  | one => exist _ 1 l_1_3
  | two => exist _ 2 l_2_3
end.

l_0_3, l_1_3 et l_2_3 ne sont que des axiomes:

Axiom l_0_3 : 0 < 3.
Axiom l_1_3 : 1 < 3.
Axiom l_2_3 : 2 < 3.

Je réussis à définir la première partie de l'isomorphisme

Definition eq_n3_n3 (n: N3) : lt3_to_N3 (N3_to_lt3 n) = n.
Proof.
by case n.
Defined.

Mais je ne suis pas en mesure de définir l'autre côté. Voici ce que j'ai fait jusqu'à présent:

Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
case: x.
move=> n p.
simpl.
???

Je ne suis pas du tout sûr du reste de la définition. J'ai également essayé de faire correspondre le motif sur x et sur (N3_to_lt3 (lt3_to_N3 x)), mais je ne sais pas trop quoi renvoyer.

Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)) :=
match N3_to_lt3 (lt3_to_N3 x) with
  | x => ???
end.

Merci pour l'aide.

3
burionk 4 août 2017 à 11:09

2 réponses

Puisque vous utilisez ssreflect, la méthode la plus simple consiste à utiliser la définition de calcul de < (dans ssrnat), puis à appliquer le lemme val_inj:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Inductive N3 := zero | one | two.

Definition less_than_3 := {x| x < 3}.

Definition lt3_to_N3 (n: less_than_3) : N3 :=
match n with
  | exist 0 _ => zero
  | exist 1 _ => one
  | exist 2 _ => two
  | exist _ _ => two
end.

Definition N3_to_lt3 (n: N3) : less_than_3 :=
match n with
  | zero => exist _ 0 erefl
  | one => exist _ 1 erefl
  | two => exist _ 2 erefl
end.

Lemma eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
by apply: val_inj; case: x => [[| [|[|x]]] Px].
Qed.

L'instruction de val_inj est un peu compliquée, mais l'idée de base est simple: pour tout prédicat booléen P sur un type T, la projection canonique { x : T | P x = true } -> T est injective. Comme l'a dit Vinz, cela repose sur le fait que les égalités booléennes sont une preuve non pertinente; c'est-à-dire que deux preuves d'égalité entre des booléens sont elles-mêmes égales. Pour cette raison, l'égalité sur {x | P x = true} est entièrement déterminée par l'élément x; le composant de preuve n'est pas pertinent.

2
Arthur Azevedo De Amorim 4 août 2017 à 14:08

Vous pouvez également vous amuser si vous profitez de la machinerie finType dans math-comp.

Par exemple, vous pouvez utiliser l'énumération des ordinaux [isomorphes à votre type] pour prouver votre lemme en énumérant toutes les valeurs au lieu de faire des cas encombrants:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma falseP T : false -> T.
Proof. by []. Qed.

Inductive N3 := zero | one | two.

Definition lt3_to_N3 (n: 'I_3) : N3 :=
  match n with
  | Ordinal 0 _ => zero
  | Ordinal 1 _ => one
  | Ordinal 2 _ => two
  | Ordinal _ f => falseP _ f
  end.

Definition N3_to_lt3 (n: N3) : 'I_3 :=
  match n with
  | zero => @Ordinal 3 0 erefl
  | one  => @Ordinal 3 1 erefl
  | two  => @Ordinal 3 2 erefl
  end.

Lemma eq_lt3_lt3 : cancel lt3_to_N3 N3_to_lt3.
Proof.
apply/eqfunP; rewrite /FiniteQuant.quant0b /= /pred0b cardE /enum_mem.
by rewrite unlock /= /ord_enum /= !insubT.
Qed.

(* We can define an auxiliary lemma to make our proofs cleaner *)
Lemma all_by_enum (T : finType) (P : pred T) :
  [forall x, P x] = all P (enum T).
Proof.
apply/pred0P/allP => /= H x; first by have/negbFE := H x.
suff Hx : x \in enum T by exact/negbF/H.
by rewrite mem_enum.
Qed.

Lemma eq_lt3_lt3' : cancel lt3_to_N3 N3_to_lt3.
Proof.
by apply/eqfunP; rewrite all_by_enum enumT unlock /= /ord_enum /= !insubT.
Qed.

Comme vous pouvez le voir, la conception actuelle de math-comp n'est pas très bien adaptée pour faire ce travail, mais il est néanmoins amusant d'apprendre à connaître un peu plus la bibliothèque.

Un autre exercice amusant consiste à définir l'instance finType pour votre type de données personnalisé, puis à établir que les deux ensembles ont la même cardinalité! Il existe de nombreuses combinaisons de lemmes à essayer ici pour que vous vous amusiez!

3
ejgallego 6 août 2017 à 16:49