The Coq mailing list

["plastyx" <plastyx AT free.fr>]

May be, this could help :

(* Add Rec LoadPath ".." as My. *)
(** * n-uplet ([{0,..,n}] and [{1,..,n}])

See also
- #<a 
href="http://coq.inria.fr/distrib/current/stdlib/Coq.Vectors.Fin.html";>Coq.Vectors.Fin</a>#
  %http://coq.inria.fr/distrib/current/stdlib/Coq.Vectors.Fin.html%
*)
Require Import My.Unicode.Utf8.

(** ** [{0,..,n}] and [{1,..,n}]
- [uplet0 n] is the n+1-uplet [{0,..,n}]
- [uplet n] is the n-uplet [{1,..,n}]

[uplet0] et [uplet] sont conçus de sorte qu'il existe exactement
[n+1] objets dans [{0,..,n}] (i.e., [n+1] constructions possibles d'un 
objet de [{0,..,n}])
et [n] objets dans [{1,..,n}]. Donc [{1,..,0}] est inhabité (uninhabited).

Un objet de [{0,.., n}]  (de [{1,.., n}]) est un indice dans [{0,.., n}] 
(un indice dans [{1,.., n}], respectivement).

Il y a 2 conceptions envisageables :
- [last0] et [last] sont les derniers éléments de [{0,.., n}] et  [{1,.., 
n}] respectivement, à savoir, [n] ;
  [cast0] et [cast] sont les transtypages d'un même indice [i] ([i≤n]) de 
[{0,.., n}] dans [{0,..,S n}] ; de  [{1,.., n}] dans [{1,..,S n}] 
respectivement.
- en renommant [last0] ; [last] ; [cast0] et [cast] en [first0] ; [first] ; 
[next0] et [next] ;
  on aurait pu assimiler  [first0] ; [first] à [0] et [1] respectivement et 
[next0] et [next] à des fonctions qui incrémentent l'indice.

Il y a donc endomorphismes.

Attention au décalage,  [last n] est l'indice [S n] de [{1,..,S n}] car 
[{1,..,0}] n'a pas d'indice.
*)
Reserved Notation "{0,.., n }"  (at level 0, n at level 99, no 
associativity).

Inductive uplet0 : nat → Set :=
 | last0 : ∀ n:nat, {0,..,n}
 | cast0 : ∀ {n:nat}, {0,..,n} → {0,..,S n}

where "{0,.., n }" := (uplet0 n).

Reserved Notation "{1,.., n }"  (at level 70, no associativity).

Inductive uplet : nat → Set :=
|last : ∀ n:nat, {1,..,S n}
|cast : ∀ {n:nat}, {1,..,n} → {1,..,S n}

where "{1,.., n }" := (uplet n).

(** ** [rank], [rank0] and reverse functions : [th0], [th]

Attention : au sens courant, il n'y a pas de de 0-ème élément, et le rang 
est strictement positif.
Cependant, en mathématique, il est plus usuel et plus pratique de partir de 
0
(car partir de 1 pose le problème de la définition de [th0 n 0] et [ n 0]).
C'est ce que nous ferons et dirons.
Ainsi, le premier indice de [{0,.., n}] ou  [{1,.., n}] sera le 0-ème ; 
celui de rang 0.

Note:
- donc, [rank0] transtype les indices en [nat], alors que [rank] retourne 
le prédécesseur de l'indice ;
  mais attention [rank (last n)=n]  car [last n] est l'indice [S n] de 
[{1,..,S n}] donc le [n]-ème
- [th0], [th] sont les fonctions inverses qui transforment un [k:nat] en 
l'indice [k] de [{0,.., n}] (ou en l'indice [k+1] de [{1,.., n}], 
respectivement).
   Le dernier indice est retourné en cas de débordement.

We say that [0] is the [0]-th item of  [{0,.., n}] and [1] is the [0]-th 
item of [{1,.., n}] and [rank] of the [0]-th item is [0].

For [k:nat] :
- [th0 n k]  is the [k]-th item of  [{0,.., n}] or the last item when 
[n<k].
- [th n k]  is the [k]-th item of  [{1,.., n}] or the last item when [n≤k].
- [rank0 n e=k]  means that [e] is the [k]-th item of  [{0,.., n}], and 
therefore, [k≤n].
- [rank n e=k]  means that [e] is the [k]-th item of  [{1,.., n}], and 
therefore, [k<n].

Exemples :
- [last 0] est le dernier indice de [{1,..,S 0}], c'est donc le [1] de 
[{1,..,1}] ; [rank (last 0)=0]
- [last 2] est le [3] de [{1,..,3}]
- [cast (last 2)] est [@cast 3 (last 2)], le [3] de [{1,..,4}]
- [rank (cast  (last 2))=(@rank 4 (@cast 3 (last 2)))=(rank (last 
2))=(@rank 3 (last 2))=pred 3=2]
- [(th0 4 1)=(cast0 (cast0 (last0 2)))]. [2] est successivement convertit 
en indice de [{0,..,2}] (par [last0]), de [{0,..,3}] et  de [{0,..,4}] (par 
[cast0])
*)
Fixpoint rank0 {n:nat} (e: {0,..,n}) : nat :=
 match e with
 | last0 _ => n
 | cast0 _ e' => rank0  e'
 end.

Fixpoint rank {n:nat} (e: {1,..,n}) : nat :=
 match e with
 | last n' => n'
 | cast _ e' => rank  e'
 end.

Fixpoint uplet_to_nat {n:nat} (e: {1,..,n}) : nat :=
 match e with
 | last _ => n  (* or [ | last n' => S n' ] *)
 | cast _ e' => uplet_to_nat  e'
 end.

Lemma uplet_to_nat_def : ∀ {n:nat}, ∀ e: {1,..,n}, uplet_to_nat  e = S (rank 
e).
Proof. induction e; [  reflexivity | exact IHe ]. Qed.


Require Import Coq.Arith.Compare_dec.
(**
- [th0 {n:nat} (k:nat) : {0,..,n}],  (la fonction inverse de [rank0]) 
retourne le [k]-th (ou le dernier) item de [{0,..,n}]
- [th {n:nat} (k:nat) : {1,.., S n}],  (la fonction inverse de [rank]) 
retourne le [k]-th (ou le dernier) item de [{1,.., S n}]
*)
Fixpoint th0 (n:nat) (k:nat) : {0,..,n} :=
 match n with
 | 0 => last0 _
 | S n' => if (le_lt_dec n k) then (*n <= k *) last0 _ else (* k < n *) 
cast0 (th0 _ k)
 end.

Fixpoint th (n:nat) (k:nat) : {1,.., S n} :=
 match n with
 | 0 => last _
 | S n' => if (le_lt_dec n k) then (*n <= k *) last _ else (* k < n *) cast 
(th _ k)
 end.






(** *** Missing stuff about decidability : *)

Lemma not_else : ∀ T: Type, ∀ Th El : T, ∀ A B : Prop, ∀ dec: { A } + { B }, 
¬ B → (if dec then Th else El)=Th.
Proof. intros. destruct dec; [ reflexivity | exfalso; apply H; assumption ]. 
Qed.

Lemma not_then : ∀ T: Type, ∀ Th El : T, ∀ A B : Prop, ∀ dec: { A } + { B }, 
¬ A → (if dec then Th else El)=El.
Proof. intros. destruct dec; [ exfalso; apply H; assumption | reflexivity ]. 
Qed.

Lemma _then : ∀ T: Type, ∀ Th El : T, ∀ A : Prop, ∀ dec: { A } + { ¬A }, A → 
(if dec then Th else El)=Th.
Proof. intros. destruct dec; [ reflexivity | exfalso; revert H; 
assumption ]. Qed.



(** ** Facts *)
Require Import Coq.Arith.Le.
Require Import Coq.Arith.Lt.
Require Import Coq.Setoids.Setoid.

Lemma uninhabited_uplet_0 : ¬inhabited (uplet 0).
Proof.
assert( H : ∀ n: nat, ∀ x:{1,..,n}, 0<n ); [ intros; induction x; apply 
lt_0_Sn | ].
intro I; induction I. apply (lt_irrefl 0), (H 0 H0).
Qed.


Fact rank0_last0  :  ∀ n:nat, rank0 (last0 n) = n.
Proof. intro; reflexivity. Qed.

Fact rank_last  :  ∀ n:nat, rank (last n) = n.
Proof. intro; reflexivity. Qed.


Fact rank0_cast0 : ∀ {n:nat}, ∀ e: {0,..,n}, (rank0 (cast0 e))=(rank0 e).
Proof. intro; reflexivity. Qed.

Fact rank_cast  :  ∀ n:nat, ∀ e:{1,..,n}, rank (cast e) = rank e.
Proof. intro; reflexivity. Qed.


(** [rewrite th0_S] and [rewrite th_S] are substitutes for [simpl]. *)
Fact th0_S : ∀ n k:nat,  th0 (S n) k=if (le_lt_dec (S n) k) then last0 _ 
else cast0 (th0 _ k).
Proof. intros; reflexivity. Qed.

Fact th_S : ∀ n k:nat,  th (S n) k=if (le_lt_dec (S n) k) then last _ else 
cast (th _ k).
Proof. intros; reflexivity. Qed.


Lemma rank0_le : ∀ {n:nat}, ∀ e: {0,.., n }, rank0 e ≤ n.
Proof. induction e; [ exact (le_refl n) | exact (le_S _ _ IHe) ]. Qed.

Lemma rank_lt : ∀ {n:nat}, ∀ e: {1,.., n }, rank e < n.
Proof. induction e; [ exact (le_refl _) | exact (le_S _ _ IHe) ]. Qed.

Lemma rank0_nn : ∀ {n:nat}, ∀ e: {0,..,n}, rank0 e=n ↔ e=last0 n.
Proof. induction e.
split; intro H; reflexivity.
split; intro H; exfalso; [ apply (le_Sn_n n); rewrite <-H, rank0_cast0; 
apply rank0_le | discriminate ].
Qed.

(*
Inductive uplet : nat → Set :=
|last : ∀ n:nat, {1,..,S n}
|cast : ∀ {n:nat}, {1,..,n} → {1,..,S n}
*)

Fixpoint uplet_rect' (P : ∀ n : nat, {1,..,n} → Type)
                                  (f : ∀ n : nat, P (S n) (last n))
                                  (f0 : ∀ n : nat, ∀ u : {1,..,n}, P n u → 
P (S n) (cast u))
                                  (n : nat) (u : {1,..,n}) : P n u :=
 match u as u0 in ({1,..,n0}) return (P n0 u0) with
 | last n0 => f n0
 | cast n0 u0 => f0 n0 u0 (uplet_rect' P f f0 n0 u0)
 end.

Definition case_uplet_S (P: ∀ n : nat, {1,..,S n} → Type)
                                      (Pl: ∀ n, P n (last n) )
                                      (Pc : ∀ n:nat, ∀ e: {1,..,n}, P n 
(cast e))
                                      (n:nat) (e: {1,..,S n}) : P n e :=
 match e with
 |last k => Pl k
 |cast k e' => Pc _ e'
 end.


Lemma rank_nn : ∀ {n:nat}, ∀ e: {1,..,S n}, rank e=n ↔ e=last n.
Proof. split; [ | intro H; rewrite H; reflexivity ].
apply (case_uplet_S (fun (n : nat) (e : {1,..,S n}) => rank e = n → e = last 
n)).
intros; reflexivity.
intros; exfalso; apply (lt_irrefl n0). rewrite <-H at 1; rewrite rank_cast. 
apply rank_lt.
Qed.



Lemma th0_nn : ∀ n:nat, th0 n n = last0 n.
Proof. induction n; [ reflexivity | rewrite th0_S, not_else; [ reflexivity | 
apply lt_irrefl ] ]. Qed.

Lemma th_nn : ∀ n:nat, th n n = last n.
Proof. induction n; [ reflexivity | rewrite th_S, not_else; [ reflexivity | 
apply lt_irrefl ] ]. Qed.


Lemma rank0_th0 : ∀ n k:nat, rank0 (th0 n k) = if (le_lt_dec n k) then n 
else k.
Proof. intros.
induction n; [ reflexivity | rewrite th0_S ].
destruct(le_lt_dec (S n) k); [ reflexivity | rewrite rank0_cast0, IHn ].
destruct(le_lt_dec n k); [ exact (le_antisym _ _ l0 (lt_n_Sm_le _ _ l)) | 
reflexivity ].
Qed.

Lemma rank_th : ∀ n k:nat, rank (th n k) = if (le_lt_dec n k) then n else k.
Proof. intros.
induction n; [ reflexivity | rewrite th_S ].
destruct(le_lt_dec (S n) k); [ reflexivity | rewrite rank_cast, IHn ].
destruct(le_lt_dec n k); [ exact (le_antisym _ _ l0 (lt_n_Sm_le _ _ l)) | 
reflexivity ].
Qed.


Lemma th0_rank0 : ∀ {n:nat}, ∀ e: {0,..,n}, (th0 _ (rank0 e)) = e.
Proof. induction e; [ apply th0_nn | rewrite rank0_cast0, th0_S, not_then; 
[ rewrite IHe; reflexivity | apply le_not_lt, rank0_le ] ]. Qed.

Lemma th_rank : ∀ {n:nat}, ∀ e: {1,..,S n}, (th _ (rank e)) = e.
Proof.
apply case_uplet_S; intros; [ apply th_nn | ].
rewrite rank_cast.
induction e; (rewrite th_S, not_then; [ | apply le_not_lt, lt_n_Sm_le, 
rank_lt ]); [ rewrite th_nn | rewrite rank_cast, IHe ]; reflexivity.
Qed.


Lemma uplet0_0 : ∀ e:{0,..,0}, e=last0 0.
Proof. intros; apply (uplet0_ind (fun n e => 0=n → e=last0 n)); intros; [ | 
exfalso; exact (O_S _ H0) | ]; reflexivity. Qed.


Require Import My.Sets.Image_facts.

Lemma cast0_inj : ∀ n:nat,  Image.injective (@cast0 n).
Proof. intros n k k'; split; intro e; [ rewrite <-th0_rank0, <-rank0_cast0, 
<-e, rank0_cast0, th0_rank0 | rewrite e ]; reflexivity. Qed.

Lemma cast_inj : ∀ n:nat,  Image.injective (@cast n).
Proof.
intros n; destruct n; intros k k'; [ exfalso; apply uninhabited_uplet_0, 
(inhabits k) | ].
split; intro e; [ rewrite <-th_rank, <-rank_cast, <-e, rank_cast, th_rank | 
rewrite e ]; reflexivity.
Qed.


Require Import My.Sets.Ensembles.
(*
Require Import My.Sets.Extensionality.
*)
Require Import My.Sets.Finite_sets_facts.
Import Finite_sets_notations. (* Symbols : ∈ ⊆ ≡ ∅ Ω ∁ ∩ ∪ \ ＋ － ｛｝ |  |= *)

Lemma uplet0_card : ∀ n:nat, | Full_set {0,..,n} |= S n.
Proof.
induction n.
exists (Empty_set {0,..,0}); exists (last0 0).
split; [ split; intro H; [ right; rewrite uplet0_0; reflexivity | apply I ] 
| split; [ intro H; apply H | apply Cardinal_Empty_set; reflexivity ] ].

unfold Full_set in IHn.
exists (fun e=> match e with | cast0 _ _ => True | last0 _ => False end). 
exists (last0 (S n)).
split; [  | split; [ intro H; apply H | ] ].
split; intro H; [ induction x; [ right; reflexivity | left; apply I ] | 
apply I ].
revert IHn. apply (same_card_cond _ _ (@cast0 n)).

intros x _ y _; apply cast0_inj.
intros; apply I.
intros. rewrite <-(th0_rank0 b). exists (th0 _ (rank0 b)). split; [ apply I 
| ].
simpl; rewrite not_then; [ reflexivity | ].
destruct (le_lt_eq_dec _ _ (rank0_le b) ); [ apply (lt_not_le _ _ l) | apply 
rank0_nn in e; rewrite e in H; exfalso; apply H ].
Qed.

Lemma uplet_card : ∀ n:nat, | Full_set ({1,..,n}) |= n.
Proof.
induction n.
split; intro H; [ apply uninhabited_uplet_0, (inhabits x) | apply I ] .

unfold Full_set in IHn.
set(Ω':=(fun e:{1,..,S n} => match e with | cast _ _ => True | last _ => 
False end)).
exists Ω'. exists (last n).
split; [  | split; [ intro H; apply H | ] ].
split; intros H; [ | apply I ]. clear IHn H. revert n x Ω'; apply 
case_uplet_S; intros; [ right; reflexivity | left; apply I ].
revert IHn. apply (same_card_cond _ _ (@cast n)).

intros x _ y _; apply cast_inj.
intros; apply I.
intros. rewrite <-(th_rank b).
destruct n.
assert( T := le_n_0_eq _ (lt_n_Sm_le _ _ (rank_lt b)) ).
symmetry in T. rewrite rank_nn in T. rewrite T in H. exfalso; apply H.

exists (th _ (rank b)); split; [ apply I | ].
simpl; rewrite not_then; [ reflexivity | ].
destruct (le_lt_eq_dec _ _ (lt_n_Sm_le _ _ (rank_lt b)) ); [ apply 
(lt_not_le _ _ l) | apply rank_nn in e; rewrite e in H; exfalso; apply H ].
Qed.