The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

muad a écrit :
> Taral wrote:
>   
> > On Thu, Aug 27, 2009 at 7:54 AM, Celia 
> > Picard<celia.picard AT irit.fr>
> >  wrote:
> >     
> > > (* By the way, we have a proof of injectivity of Fin that looks a bit
> > > complicated.
> > >   Is there a well-known (easier) proof of Fin n = Fin m ->  n = m ? *)
> > >       
> > Not really. Any such proof of type equivalence would necessarily
> > involve proving things about the cardinality of Fin n and Fin m by
> > example.
> >
> > --
> > Taral 
> > <taralx AT gmail.com>
> > "Please let me know if there's any further trouble I can give you."
> >     -- Unknown
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.saclay.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >           http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> >
> >
> >     
>
>
> My proof of this Fin injectivity is the culmination of about 500 line script
> using pigeonhole principle, I assume you have something similar?
>   
I just did one of less than 200 loc (but the very specific part is about 
130 loc):

Set Implicit Arguments.

Inductive SFalse : Set :=.

Definition not_nul n : Set :=
 match n with
 | 0 => SFalse
 | S _ => unit
 end.

Inductive Fin : nat -> Set :=
| first : forall n, Fin (S n)
| succ : forall n, Fin n -> Fin (S n).

Inductive head card ord :=
| Fh : ord = first card -> head card ord
| Sh : forall x, ord = succ x -> head card ord.

Definition decompose card (ord : Fin (S card)) : head ord :=
 match
   ord as f in (Fin n)
   return
     (match n as u0 return (Fin u0 -> Set) with
      | 0 => fun _ : Fin 0 => SFalse
      | S k => fun H0 : Fin (S k) => head H0
      end f)
 with
 | first n => Fh (refl_equal (first n))
 | succ n H0 => Sh (refl_equal (succ H0))
 end.

Ltac decomp x :=
let e := fresh in
let y := fresh x in
destruct (decompose x) as [e|y e];
rewrite e in *; clear e x.

Definition noset (fn : Fin 0) : SFalse :=
 match fn in (Fin n) return not_nul n with
 | first _ => tt
 | succ _ _ => tt
 end.

Ltac no_set x :=
destruct (noset x).

Fixpoint depth n (fn : Fin n) :=
 match fn with
 | first _ => 0
 | succ _ m => S (depth m)
 end.

(** The following lemma states that two values of [Fin m] are the same iff
   they have same depth *)
Lemma depth_eq : forall m (fm fn : Fin m), depth fm = depth fn -> fm = fn.
Proof.
 induction fm; intros fn H; decomp fn; simpl in *; inversion H; auto.
 rewrite IHfm with fn0; auto.
Qed.

(** The following lemma is an inversion principle for [Fin m];
   funny remark: the proof uses depth_eq as I didn't find better proof *)
Lemma succ_inversion : forall m (fm fn : Fin m), succ fm = succ fn -> fm 
= fn.
Proof.
 intros.
 assert (depth (succ fm) = depth (succ fn)).
   rewrite H; auto.
 inversion H0.
 apply depth_eq; auto.
Qed.

Definition nat_eq : forall (m n : nat), {m=n}+{m<>n}.
decide equality.
Qed.

Definition Fin_eq : forall m (fm fn : Fin m), {fm=fn}+{fm<>fn}.
Proof.
 intros.
 destruct (nat_eq (depth fm) (depth fn)).
 left; apply depth_eq; auto.
 right; intro H; destruct n; rewrite H; auto.
Qed.

(** The following structure is quite weird:
   
[@at_least
 set n P] means that [set] contains at least n elements;
   for any [v] in [set], [P v] implies that v is not one of the considered
   elements *)
Inductive at_least (A : Set) : nat -> (A -> Prop) -> Prop :=
| Nothing : forall (P : A -> Prop),
at_least 0 P
| Something : forall x card P (Q : A -> Prop) (l : at_least card P),
  P x -> (forall y, Q y -> (x<>y /\ P y)) ->
at_least (S card) Q.

Lemma at_least_card :
forall card, exists notin : Fin card -> Prop, at_least card notin.
Proof.
 induction card.
   (* The case when [card] is 0 is trivial *)
     exists (fun _ => True); apply Nothing.
   (* The case where [card] is [S card'] is a lot more complex *)
     destruct IHcard;
     set (P_ := fun (K : Prop) card x (y : Fin (S card)) =>
          match decompose y with Fh _ => K|Sh H _ => x H end).
     (* we assume that we can build a "not in" property without
        using [first card']*)
     cut (at_least card (P_ True card x)).
       (* now we have to add [first card'] *)
         clear H; intro; exists (P_ False card x);
         apply Something with (first card) (P_ True card x);
         subst P_; simpl; auto; intros.
         (* and to check it is not in the set *)
         decomp y; simpl; auto; intuition; discriminate H1.
       (* now we prove our assumption by induction,
          but before running into it, we must isolate
          [card'] which is not part of the induction *)
         revert H; set (t := card) at 2 4; generalize t;
         subst t; intros.
         (* here begin our induction *)
         induction H.
           (* the trivial case *)
             apply Nothing.
           (* the other (not too hard) case *)
             apply Something with (succ x) (P_ True card P);
             simpl; auto.
             clear IHat_least H; intros; subst P_; simpl in *.
             (* we use the fact we have build our set
                without using [first] *)
             decomp y.
             intuition; discriminate H2.
             destruct (H1 _ H); clear H1 H.
             intuition; apply H2; apply succ_inversion; auto.
Qed.

Lemma at_most_card : forall n m (notin : Fin m -> Prop),
 at_least (m + 1 + n) notin -> False.
Proof.
 induction m.
   (* The trivial case *)
     simpl in *; generalize (refl_equal (S n));
     set (t := n) at 1; generalize (S n); subst t;
     intros; destruct H0.
       discriminate H.
       no_set x.
   (* The non trivial case *)
     (* first, we simplify our hypothesis *)
     revert IHm; simpl; generalize (m + 1 + n);
     intros; clear n.
     apply IHm with (fun y => notin (succ y)); clear IHm.
     assert {m:_&m=S n0}.
       exists _; auto.
     destruct H0; rewrite <- e in H; generalize dependent n0.
     (* now we can begin the first part of our induction,
        which consists in finding an occurence of [first],
        which is the exceeding element *)
     induction H; intros; inversion e; clear e.
     (* the trivial case is automatically solved *)
     (* for the other case, we first simplify our hypothesis *)
     destruct n0; [apply Nothing|];
     assert (L := IHat_least n0 H3);
     rewrite H3 in H; clear H3 IHat_least card.
     decomp x.
       (* now we can eliminate first from our set *)
         assert (at_least (S n0) (fun y : Fin m => P (succ y))).
         clear H1 L Q.
         (* here begin the second part of the induction *)
         induction H.
           apply Nothing.
           destruct (H2 (first m) H0); clear H0;
           assert (L := IHat_least H4); clear IHat_least H4.
           decomp x.
             (* as we have eliminated [first] *)
               destruct H3; auto.
             (* but if our value is not [first] *)
               apply Something with x0 (fun y : Fin m => P (succ y)); auto;
               clear L H card H1.
               intros; destruct (H2 _ H); clear H2 H; intuition;
               rewrite H in H0; auto.
         (* we finish the [first] case of the first part of the 
induction *)
         clear L H.
         assert {M : _& M = fun y : Fin m => P (succ y)}.
           exists _; auto.
         destruct X; rewrite <- e in H2; destruct H2.
           apply Nothing.
           rewrite e in *; clear e Q0; apply Something with x P0; auto;
           intros; apply H3; exact (proj2 (H1 _ H4)).
       (* if [first] has not yet been eliminated *)
         apply Something with x0 (fun y : Fin m => P (succ y)); auto.
         intros; destruct (H1 (succ y) H2).
         intuition; apply H3; rewrite H5; auto.
Qed.

(** Here ends the main lemma, what follows is mainly irrelevant *)

(** Some other lemmas *)
Record bijection A B := bij
{ pi1 : A -> B;
 pi2 : B -> A;
 pi2pi1 : forall a, pi2 (pi1 a) = a;
 pi1pi2 : forall b, pi1 (pi2 b) = b
}.

Inductive le_set n : nat -> Set :=
| le_set_n : le_set n n
| le_set_S : forall m, le_set n m -> le_set n (S m).

Inductive Fin2 m : Set :=
Inf : forall n, le_set (S n) m -> Fin2 m.

Definition noset2 (f : Fin2 0) : SFalse :=
match f with
| Inf n l =>
    match l in (le_set _ n0) return (n0 = 0 -> SFalse) with
    | le_set_n =>
        fun e : S n = 0 =>
        match e in (_ = y) return not_nul y
        with
        | refl_equal => tt
        end
    | le_set_S m _ =>
        fun e : S m = 0 =>
        match e in (_ = y) return not_nul y
        with
        | refl_equal => tt
        end
    end (refl_equal 0)
end.

Fixpoint Pi1 m : Fin m -> Fin2 m :=
   match m as n0 return (Fin n0 -> Fin2 n0) with
   | 0 => fun x : Fin 0 => match noset x return (Fin2 0) with
                           end
   | S n0 =>
       fun H : Fin (S n0) =>
       match decompose H with
       | Fh _ => Inf (le_set_n (S n0))
       | Sh x _ => match Pi1 x with
                   | Inf n1 l => Inf (le_set_S l)
                   end
       end
   end.

Definition Pi2_aux r :=
   fix pi2 n (u : le_set (S r) n) : Fin n :=
       match u with
       | le_set_n => first r
       | le_set_S _ k => succ (pi2 _ k)
       end.

Definition Pi2 m (fm : Fin2 m) : Fin m :=
   match fm with
   | Inf r l => Pi2_aux l
   end.

Theorem Fin_Fin2 : forall m, bijection (Fin m) (Fin2 m).
Proof.
 intro m; refine (bij (@Pi1 m) (@Pi2 m) _ _).
 (**)
   induction a; auto.
   simpl; destruct (Pi1 a).
   simpl in *; rewrite IHa; auto.
 (**)
   destruct b; simpl.
   induction l; auto.
   simpl; destruct (Pi1 (Pi2_aux l)).
   inversion IHl; auto.
Qed.

Lemma depth_in_Fin2_spe : forall m (fm : Fin m),
 match Pi1 fm with Inf d _ => 1 + depth fm + d = m end.
Proof.
 induction fm; simpl in *; auto.
 destruct (Pi1 fm).
 rewrite IHfm; auto.
Qed. 

Unset Implicit Arguments.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay