<div dir="ltr"><div class="gmail_default" style="font-family:courier new,monospace"><br></div><div class="gmail_extra"><br><div class="gmail_quote">2014-09-16 11:32 GMT+02:00 Thorsten Altenkirch <span dir="ltr"><<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="word-wrap:break-word;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></blockquote><div><br>In most of the interesting practical cases I know, with inductives, I have to pattern match against the index as well, and I have to do it inside of a return clause, which is rather annoying.<br><br>Compare<br><br>Definition no_fin_O (x : fin O) : False :=<br> match x in fin n return match n with O => False | _ => True end with<br> | FinO => I<br> | FinS _ => I<br> end.<br><br>with<br><br>Definition no_fin2_O (x : fin2 O) : False :=<br> match x with end.<br><br>There is not many lemmas or definitions involving "fin n" that I find easier to write or prove with the inductive version.<br> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><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></blockquote><div><br>It is not that often that I have to use CoNats instead of natss. Plus fin expects "nat", so you will have to change some things.<br> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><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></blockquote><div><br>That has nothing to do with the "fin" type. I know how to use induction, and I do it when I feel the need (and I often feel the need). But in the case of "fin", I find it rather cumbersome.<br> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word;color:rgb(0,0,0);font-size:14px;font-family:Calibri,sans-serif"><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><div style="font-family:Calibri;font-size:11pt;text-align:left;color:black;border-width:1pt medium medium;border-style:solid none none;border-color:rgb(181,196,223) -moz-use-text-color -moz-use-text-color;padding:3pt 0in 0in"><span style="font-weight:bold">From: </span> Cedric Auger <<a href="mailto:sedrikov@gmail.com" target="_blank">sedrikov@gmail.com</a>><br><span style="font-weight:bold">Reply-To: </span> "<a href="mailto:coq-club@inria.fr" target="_blank">coq-club@inria.fr</a>" <<a href="mailto:coq-club@inria.fr" target="_blank">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" target="_blank">coq-club@inria.fr</a>" <<a href="mailto:coq-club@inria.fr" target="_blank">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 style="BORDER-LEFT:#b5c4df 5 solid;PADDING:0 0 0 5;MARGIN:0 0 0 5"><div dir="ltr"><div 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Mon, Sep 15, 2014 at 8:50 AM, John Wiegley <<a href="mailto:johnw@newartisans.com" target="_blank">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><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></div>
</blockquote></div><br><br clear="all"><br>-- <br>.../Sedrikov\...
</div></div>