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

[Thorsten Altenkirch]

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

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.

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?

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<mailto:sedrikov at gmail.com>>
Reply-To: "coq-club at inria.fr<mailto:coq-club at inria.fr>" <coq-club at inria.fr<mailto:coq-club at inria.fr>>
Date: Tue, 16 Sep 2014 10:11:19 +0100
To: "coq-club at inria.fr<mailto:coq-club at inria.fr>" <coq-club at inria.fr<mailto: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<mailto:dschepler at gmail.com>>:
On Mon, Sep 15, 2014 at 8:50 AM, John Wiegley <johnw at newartisans.com<mailto: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.









-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140916/c3bc08eb/attachment.html