[Agda] Re: [Coq-Club] Questions about two theorems

[Cedric Auger]

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\...
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140916/df87ad69/attachment-0001.html