coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club]Defining function with dependent structure in goal, rcp
- <Possible follow-ups>
- Re: [Coq-Club]Defining function with dependent structure in goal, rcp
Archive powered by MhonArc 2.6.16.