Skip to Content.
Sympa Menu

coq-club - [Coq-Club]Defining function with dependent structure in goal

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Defining function with dependent structure in goal


chronological Thread 
  • From: rcp AT Cs.Nott.AC.UK
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club]Defining function with dependent structure in goal
  • Date: 12 Mar 2007 14:03:11 +0000
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Source-info: From (or Sender) name not authenticated.

Hello,


I am having some trouble defining the following function,
 Definition finsum (n m: nat) (i : Fin (n + m)): FinSum n m i,

which, given these datatypes and definitions:
Inductive Fin : nat -> Set :=
| fz : forall n :nat, Fin (S n) | fs : forall n:nat, Fin n -> Fin (S n).
     Implicit Arguments fs [n].
Implicit Arguments fz [n].

 Fixpoint fin_inl (n m : nat) (i : Fin n) {struct i} : Fin (n + m) :=
         match i  in Fin n return Fin (n + m) with
| fz p => fz | fs x k => fs (fin_inl x m k)
end. Fixpoint fin_inr (n m : nat) (i:Fin m) {struct n}: Fin (n + m) :=
       match n return Fin (n + m) with
       | O => i
       | S n' => fs (fin_inr n' m i)
      end.

 Inductive FinSum  (n m: nat)  : Fin (n + m) -> Set :=
       | is_inl : forall i: Fin n ,  FinSum n m  (fin_inl n m i)
       | is_inr : forall j: Fin m, FinSum  n m  (fin_inr n m j).

allocates elements of Fin (n + m) to their appropriate place in FinSum.

I proceeded:
Definition FinSum (n m: nat) (i : Fin (n + m)): FinSum n m i.
       intros.
       induction n.
       exact (is_inr i).

but am stuck with the goal "FinSum (S n) m i". I will like to examine the cases of i, so should think "dependent inversion i" should do the trick. However, this does not help. Can anyone suggest a way to proceed?


Rawle.

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.





Archive powered by MhonArc 2.6.16.

Top of Page