<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;"><div>Using the inductive definition allows you to pattern match over the elements instead needing to match the index first.</div><div><br></div><div>Another reason to prefer inductive definitions is that they easier generalise, e.g. You could index Fin with coNats without having to change the code. The recursive definition doesn’t work with them.</div><div><br></div><div>Moreover in many cases we have to use inductive definitions, e.g. Have you tried to define typed lambda terms by recursion over the type?</div><div><br></div><div>Having said this, you are right there is this overhead. So in some cases the recursive definition has advantages.</div><div>Also I am more of an Agda user – in Coq the station may be different because the native support for dependently typed pattern matching isn’t so good.</div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br></div><span id="OLK_SRC_BODY_SECTION"><div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt"><span style="font-weight:bold">From: </span> Cedric Auger <<a href="mailto:sedrikov@gmail.com">sedrikov@gmail.com</a>><br><span style="font-weight:bold">Reply-To: </span> "<a href="mailto:coq-club@inria.fr">coq-club@inria.fr</a>" <<a href="mailto:coq-club@inria.fr">coq-club@inria.fr</a>><br><span style="font-weight:bold">Date: </span> Tue, 16 Sep 2014 10:11:19 +0100<br><span style="font-weight:bold">To: </span> "<a href="mailto:coq-club@inria.fr">coq-club@inria.fr</a>" <<a href="mailto:coq-club@inria.fr">coq-club@inria.fr</a>><br><span style="font-weight:bold">Subject: </span> Re: [Coq-Club] Questions about two theorems<br></div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div dir="ltr"><div class="gmail_default" style="font-family:courier new,monospace">Yes, that is clever.<br>By the way, I do not know why people use this definition of "fin" which I find rather inconvenient.<br><br>Inductive emptySet : Type := .<br><br>Fixpoint fin2 (n : nat) : Type := match n with O => emptySet | S n => option (fin2 n) end.<br><br>is a lot more convenient from my point of view.<br>Here, we do not have to do all these inversion stuff when inspecting an element.<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-09-15 18:06 GMT+02:00 Daniel Schepler <span dir="ltr"><<a href="mailto:dschepler@gmail.com" target="_blank">dschepler@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Mon, Sep 15, 2014 at 8:50 AM, John Wiegley <<a href="mailto:johnw@newartisans.com">johnw@newartisans.com</a>> wrote:<br>
> Thanks to you and Daniel, I am now much closer. However, I'm still having<br>
> difficulty with the above statement: what about the case where hd is not the<br>
> greatest element of fin (S n)? Then the fact that x <> hd doesn't help me,<br>
> since hd could be an element which *should* be in y, rather than x. It seems<br>
> like your proof assumes an ordered set from greatest to last, when the<br>
> original statement requires no ordering. Daniel did make reference to the<br>
> fact that having a sorting property could make things easier.<br><br>
OK, here's a complete solution. As opposed to what Auger suggested,<br>
my proof essentially proceeds by cases depending on whether or not<br>
FinO is in the list. That makes it easier to define the injection {<br>
x:Fin (S n) | x <> FinO } -> Fin n.<br><br>
Require Import List.<br>
Require Import Arith.<br><br>
Inductive Fin : nat -> Set :=<br>
| FinO : forall {n:nat}, Fin (S n)<br>
| FinS : forall {n:nat}, Fin n -> Fin (S n).<br><br>
Definition Fin_0_inv (P : Fin 0 -> Type) :<br>
forall x:Fin 0, P x :=<br>
fun x =><br>
match x in (Fin z) return<br>
(match z return (Fin z -> Type) with<br>
| 0 => P<br>
| S _ => fun _ => unit<br>
end x) with<br>
| FinO _ => tt<br>
| FinS _ _ => tt<br>
end.<br><br>
Definition Fin_Sn_inv {n:nat} (P : Fin (S n) -> Type)<br>
(PO : P FinO) (PS : forall y:Fin n, P (FinS y)) :<br>
forall x:Fin (S n), P x :=<br>
fun x =><br>
match x in (Fin Sn) return<br>
(match Sn return (Fin Sn -> Type) with<br>
| 0 => fun _ => unit<br>
| S n' => fun x => forall (P : Fin (S n') -> Type),<br>
P FinO -> (forall y:Fin n', P (FinS y)) -><br>
P x<br>
end x) with<br>
| FinO _ => fun P PO PS => PO<br>
| FinS _ y => fun P PO PS => PS y<br>
end P PO PS.<br><br>
Definition FinS_inv {n:nat} (x:Fin (S n)) :<br>
option (Fin n) :=<br>
Fin_Sn_inv (fun _ => option (Fin n)) None (@Some _) x.<br><br>
Fixpoint map_FinS_inv {n:nat} (l : list (Fin (S n))) :<br>
list (Fin n) :=<br>
match l with<br>
| nil => nil<br>
| cons x l' =><br>
let recval := map_FinS_inv l' in<br>
match FinS_inv x with<br>
| Some y => cons y recval<br>
| None => recval<br>
end<br>
end.<br><br>
Lemma map_FinS_inv_len_noO :<br>
forall {n:nat} (l : list (Fin (S n))),<br>
~ In FinO l -> length (map_FinS_inv l) = length l.<br>
Proof.<br>
induction l; simpl.<br>
+ reflexivity.<br>
+ destruct a using Fin_Sn_inv; simpl; intuition.<br>
Qed.<br><br>
Lemma map_FinS_inv_len_NoDup :<br>
forall {n:nat} (l : list (Fin (S n))),<br>
NoDup l -> length l <= S (length (map_FinS_inv l)).<br>
Proof.<br>
induction 1; simpl.<br>
+ repeat constructor.<br>
+ destruct x using Fin_Sn_inv; simpl; intros.<br>
- rewrite map_FinS_inv_len_noO; trivial.<br>
- auto with arith.<br>
Qed.<br><br>
Lemma in_map_FinS_inv : forall {n:nat} (l : list (Fin (S n)))<br>
(y : Fin n), In y (map_FinS_inv l) -> In (FinS y) l.<br>
Proof.<br>
induction l; simpl.<br>
+ trivial.<br>
+ destruct a using Fin_Sn_inv; simpl.<br>
- auto.<br>
- destruct 1.<br>
* left; f_equal; trivial.<br>
* right; auto.<br>
Qed.<br><br>
Lemma map_FinS_inv_NoDup : forall {n:nat} (l : list (Fin (S n))),<br>
NoDup l -> NoDup (map_FinS_inv l).<br>
Proof.<br>
induction 1; simpl.<br>
+ constructor.<br>
+ destruct x using Fin_Sn_inv; simpl.<br>
- trivial.<br>
- constructor; trivial. contradict H. apply in_map_FinS_inv; trivial.<br>
Qed.<br><br>
Theorem fin_list : forall {n:nat} (l : list (Fin n)),<br>
NoDup l -> length l <= n.<br>
Proof.<br>
induction n.<br>
+ destruct l.<br>
- trivial.<br>
- destruct f using Fin_0_inv.<br>
+ intros. apply le_trans with (1 := map_FinS_inv_len_NoDup l H).<br>
auto using le_n_S, map_FinS_inv_NoDup.<br>
Qed.<br><span class="HOEnZb"><font color="#888888">--<br>
Daniel Schepler<br></font></span></blockquote></div><br><br clear="all"><br>-- <br>.../Sedrikov\...
</div></blockquote></span>
<br><p>This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.</p><p>This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.</p>
<br></body></html>