The Coq mailing list

[flicky frans <flickyfrans AT gmail.com>]

I proved this in Agda, maybe it would be useful for you:
http://lpaste.net/111082

2014-09-15 21:41 GMT+04:00, Cedric Auger 
<sedrikov AT gmail.com>:
> 2014-09-15 17:50 GMT+02:00 John Wiegley 
> <johnw AT newartisans.com>:
>
>> >>>>> Cedric Auger 
>> >>>>> <sedrikov AT gmail.com>
>> >>>>>  writes:
>>
>> > You can then define a injection f which sends any (x:fin (S n)) such
>> > that
>> > (x≠hd) to some (y:fin n).
>>
>> Thanks to you and Daniel, I am now much closer.  However, I'm still
>> having
>> difficulty with the above statement: what about the case where hd is not
>> the
>> greatest element of fin (S n)?  Then the fact that x <> hd doesn't help
>> me,
>> since hd could be an element which *should* be in y, rather than x.  It
>> seems
>> like your proof assumes an ordered set from greatest to last, when the
>> original statement requires no ordering.  Daniel did make reference to
>> the
>> fact that having a sorting property could make things easier.
>>
>> John
>>
>
>
> In what you wrote, there is a natural ordering. In my initial proof, you
> could omit the notion of order.
>
> I rewrite the fin type as I do not remember its exact definition.
>
> Fixpoint fin (n : nat) : Type :=
>   match n with
>   | O => emptySet
>   | S n => option (fin n)
>   end.
>
> The injection I was thinking of was:
>
> Fixpoint inj (n : nat) : fin (S (S n)) -> fin (S (S n)) -> fin (S n) :=
>   match n with
>   | S n => fun x y =>
>     match x with
>     | None => match y with None => @None (fin (S n)) | Some y => y end
>     | Some x => match y with None => @None (fin (S (S n)) | Some y => Some
> (inj n x y) end
>   | O => fun _ _ => @None (fin O)
>   end.
>
> Lemma inj_spe : forall n (x y z : fin (S (S n))), x<>y -> x<>z -> inj x y =
> inj x z -> y = z.
> …
>
> Here, there is no notion of order. But you can use the following one if you
> want:
>
> Fixpoint lt (n : nat) : fin n -> fin n -> Prop :=
>   match n with
>   | O => fun x _ => match x with end
>   | S n => fun x y => match x with None => False | Some x => match y with
> None => True | Some y => lt n x y end
>   end.
>
>
> --
> .../Sedrikov\...
>