coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cedric Auger <sedrikov AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Questions about two theorems
- Date: Mon, 15 Sep 2014 19:41:55 +0200
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\...
- Re: [Coq-Club] Questions about two theorems, (continued)
- Re: [Coq-Club] Questions about two theorems, Cedric Auger, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, John Wiegley, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, Daniel Schepler, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, John Wiegley, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, Cedric Auger, 09/16/2014
- Re: [Coq-Club] Questions about two theorems, Thorsten Altenkirch, 09/16/2014
- Re: [Coq-Club] Questions about two theorems, Cedric Auger, 09/16/2014
- Re: [Coq-Club] Questions about two theorems, flicky frans, 09/16/2014
- Re: [Coq-Club] Questions about two theorems, Daniel Schepler, 09/16/2014
- Re: [Coq-Club] Questions about two theorems, Cedric Auger, 09/16/2014
- Re: [Coq-Club] Questions about two theorems, Thorsten Altenkirch, 09/16/2014
- Re: [Coq-Club] Questions about two theorems, Cedric Auger, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, flicky frans, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, Daniel Schepler, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, John Wiegley, 09/15/2014
- Re: [Coq-Club] Questions about two theorems, Cedric Auger, 09/15/2014
Archive powered by MHonArc 2.6.18.