From 56f7b49e1f46e495a215d65b7d2acaa03fe3b9cf Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 11 Mar 2011 17:26:07 +0000 Subject: Inference of match predicate produces ill-typed unification problem, revert to manual building of the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13906 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Vectors/VectorDef.v | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'theories/Vectors') diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 1b3c3d3b6..d26af7876 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -17,7 +17,7 @@ Names should be "caml name in list.ml" if exists and order of arguments have to be the same. complain if you see mistakes ... *) Require Import Arith_base. -Require Fin. +Require Vectors.Fin. Open Local Scope nat_scope. (** @@ -33,14 +33,19 @@ Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity). Section SCHEMES. (** An induction scheme for non-empty vectors *) + Definition rectS {A} (P:forall {n}, t A (S n) -> Type) (bas: forall a: A, P (a :: [])) (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) := fix rectS_fix {n} (v: t A (S n)) : P v := - match v with + match v in t _ n' return match n' return t _ n' -> Type with + | 0 => fun _ => ID + | S n => fun v => P v + end v + with |nil => @id |cons a 0 v => - match v as vnn in t _ nn + match v as vnn in t _ nn return match nn as nnn return t A nnn -> Type with |0 => fun vm => P (a :: vm) @@ -84,14 +89,15 @@ end. (** A vector of length [0] is [nil] *) Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v := -match v with +match v as v0 in t _ n return match n return t _ n -> Type with 0 => fun v => P v | S n => fun v => ID end v0 with |[] => H + | _ => @id end. (** A vector of length [S _] is [cons] *) Definition caseS {A} (P : forall n, t A (S n) -> Type) (H : forall h {n} t, @P n (h :: t)) {n} v : P n v := -match v with +match v as v0 in t _ n return match n return t _ n -> Type with 0 => fun v => ID | S n => fun v => P n v end v0 with |[] => @id (* Why needed ? *) |h :: t => H h t end. -- cgit v1.2.3