The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-09-16 11:32 GMT+02:00 Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>:

Using the inductive definition allows you to pattern match over the elements instead needing to match the index first.

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.

Compare

Definition no_fin_O (x : fin O) : False :=
  match x in fin n return match n with O => False | _ => True end with
  | FinO => I
  | FinS _ => I
  end.

with

Definition no_fin2_O (x : fin2 O) : False :=
  match x with end.

There is not many lemmas or definitions involving "fin n" that I find easier to write or prove with the inductive version.
 

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.

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.
 

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?

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.
 

Having said this, you are right there is this overhead. So in some cases the recursive definition has advantages.

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.

Cheers,

Thorsten

From: Cedric Auger <sedrikov AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tue, 16 Sep 2014 10:11:19 +0100
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Questions about two theorems

Yes, that is clever.
By the way, I do not know why people use this definition of "fin" which I find rather inconvenient.

Inductive emptySet : Type := .

Fixpoint fin2 (n : nat) : Type := match n with O => emptySet | S n => option (fin2 n) end.

is a lot more convenient from my point of view.
Here, we do not have to do all these inversion stuff when inspecting an element.

2014-09-15 18:06 GMT+02:00 Daniel Schepler <dschepler AT gmail.com>:

On Mon, Sep 15, 2014 at 8:50 AM, John Wiegley <johnw AT newartisans.com> wrote:
> 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.

OK, here's a complete solution.  As opposed to what Auger suggested,
my proof essentially proceeds by cases depending on whether or not
FinO is in the list.  That makes it easier to define the injection {
x:Fin (S n) | x <> FinO } -> Fin n.

Require Import List.
Require Import Arith.

Inductive Fin : nat -> Set :=
| FinO : forall {n:nat}, Fin (S n)
| FinS : forall {n:nat}, Fin n -> Fin (S n).

Definition Fin_0_inv (P : Fin 0 -> Type) :
  forall x:Fin 0, P x :=
fun x =>
match x in (Fin z) return
  (match z return (Fin z -> Type) with
   | 0 => P
   | S _ => fun _ => unit
   end x) with
| FinO _ => tt
| FinS _ _ => tt
end.

Definition Fin_Sn_inv {n:nat} (P : Fin (S n) -> Type)
  (PO : P FinO) (PS : forall y:Fin n, P (FinS y)) :
  forall x:Fin (S n), P x :=
fun x =>
match x in (Fin Sn) return
  (match Sn return (Fin Sn -> Type) with
   | 0 => fun _ => unit
   | S n' => fun x => forall (P : Fin (S n') -> Type),
     P FinO -> (forall y:Fin n', P (FinS y)) ->
     P x
   end x) with
| FinO _ => fun P PO PS => PO
| FinS _ y => fun P PO PS => PS y
end P PO PS.

Definition FinS_inv {n:nat} (x:Fin (S n)) :
  option (Fin n) :=
Fin_Sn_inv (fun _ => option (Fin n)) None (@Some _) x.

Fixpoint map_FinS_inv {n:nat} (l : list (Fin (S n))) :
  list (Fin n) :=
match l with
| nil => nil
| cons x l' =>
  let recval := map_FinS_inv l' in
  match FinS_inv x with
  | Some y => cons y recval
  | None => recval
  end
end.

Lemma map_FinS_inv_len_noO :
  forall {n:nat} (l : list (Fin (S n))),
  ~ In FinO l -> length (map_FinS_inv l) = length l.
Proof.
induction l; simpl.
+ reflexivity.
+ destruct a using Fin_Sn_inv; simpl; intuition.
Qed.

Lemma map_FinS_inv_len_NoDup :
  forall {n:nat} (l : list (Fin (S n))),
  NoDup l -> length l <= S (length (map_FinS_inv l)).
Proof.
induction 1; simpl.
+ repeat constructor.
+ destruct x using Fin_Sn_inv; simpl; intros.
  - rewrite map_FinS_inv_len_noO; trivial.
  - auto with arith.
Qed.

Lemma in_map_FinS_inv : forall {n:nat} (l : list (Fin (S n)))
  (y : Fin n), In y (map_FinS_inv l) -> In (FinS y) l.
Proof.
induction l; simpl.
+ trivial.
+ destruct a using Fin_Sn_inv; simpl.
  - auto.
  - destruct 1.
    * left; f_equal; trivial.
    * right; auto.
Qed.

Lemma map_FinS_inv_NoDup : forall {n:nat} (l : list (Fin (S n))),
  NoDup l -> NoDup (map_FinS_inv l).
Proof.
induction 1; simpl.
+ constructor.
+ destruct x using Fin_Sn_inv; simpl.
  - trivial.
  - constructor; trivial. contradict H. apply in_map_FinS_inv; trivial.
Qed.

Theorem fin_list : forall {n:nat} (l : list (Fin n)),
  NoDup l -> length l <= n.
Proof.
induction n.
+ destruct l.
  - trivial.
  - destruct f using Fin_0_inv.
+ intros. apply le_trans with (1 := map_FinS_inv_len_NoDup l H).
  auto using le_n_S, map_FinS_inv_NoDup.
Qed.
--
Daniel Schepler

--
.../Sedrikov\...

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.

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.

--
.../Sedrikov\...