From af8e8176a6ca63c59621e4775d50faf51627b4cc Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 5 May 2008 13:55:24 +0000 Subject: Mise en place d'un algorithme d'inversion des contraintes de type lors du filtrage. Cela permet de détecter les cas impossibles et de simuler les contraintes d'inversion exprimables sous la forme d'un assignement des arguments du constructeurs (cf le cas de Vtail dans Bvector.v). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi) avec vi composé uniquement de constructeurs, et que le résultat final est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on construit le prédicat Q:=fun x1 .. xn y => match x1 .. xn y with | v1(z) .. vn(z) t => P(z) | _ .. _ _ => ?evar-speciale-cas-impossible end qui vérifiera bien que Q u1 .. un = P(w1,..,wp). En raison de limitations de l'unification (on aurait besoin d'eta conversion pour résoudre des problèmes du genre "terme rigide == match x with _ => ?evar end", et besoin d'instanciation par constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"), je n'ai pas réussi à traiter le cas général. Aussi, on adopte une stratégie pragmatique consistant à tester plusieurs prédicats possibles : - si un type final est donné, on essaie d'abord l'algorithme de Matthieu et sinon le nouvel algorithme (permet par exemple de traiter certains cas d'élimination dépendante de Bvector.v), - s'il n'y a pas de type final, on essaie d'abord le nouvel algo et sinon, on essaie avec un prédicat sans dépendance (permet de traiter des cas compliqués comme celui de par cas sur I' dans le fichier Case13.v de la test-suite). Dans la pratique, il y a beaucoup de changement dans le code de compile_case. - Par exemple, la compilation est maintenant toujours appelé avec un prédicat (là où l'on pouvait avoir None, on a maintenant toujours au moins une evar). - En revanche, le membre droit des clauses est maintenant optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une branche impossible au moment du calcul du prédicat de retour. - Aussi, on renonce aux PrLetIn et PrProd dans l'expression du predicat de retour mais il faut savoir que c'est maintenant la liste des tomatchs qui spécifie le contexte exact dans lequel le prédicat de retour est bien typé. - Et d'autres... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bvector.v | 136 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 97 insertions(+), 39 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index d4d8386c4..e48dd9a5b 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -25,10 +25,10 @@ Malheureusement, cette verification a posteriori amene a faire de nombreux lemmes pour gerer les longueurs. La seconde idée est de faire un type dépendant dans lequel la longueur est un paramètre de construction. Cela complique un -peu les inductions structurelles, la solution qui a ma préférence -est alors d'utiliser un terme de preuve comme définition, car le -mécanisme d'inférence du type du filtrage n'est pas aussi puissant que -celui implanté par les tactiques d'élimination. +peu les inductions structurelles et dans certains cas on +utilisera un terme de preuve comme définition, car le +mécanisme d'inférence du type du filtrage n'est pas toujours +aussi puissant que celui implanté par les tactiques d'élimination. *) Section VECTORS. @@ -52,39 +52,88 @@ Inductive vector : nat -> Type := | Vnil : vector 0 | Vcons : forall (a:A) (n:nat), vector n -> vector (S n). -Definition Vhead : forall n:nat, vector (S n) -> A. -Proof. - intros n v; inversion v; exact a. -Defined. +Definition Vhead (n:nat) (v:vector (S n)) := + match v with + | Vcons a _ _ => a + end. -Definition Vtail : forall n:nat, vector (S n) -> vector n. -Proof. - intros n v; inversion v as [|_ n0 H0 H1]; exact H0. -Defined. +Definition Vtail (n:nat) (v:vector (S n)) := + match v with + | Vcons _ _ v => v + end. Definition Vlast : forall n:nat, vector (S n) -> A. Proof. induction n as [| n f]; intro v. inversion v. exact a. - + inversion v as [| n0 a H0 H1]. exact (f H0). Defined. -Definition Vconst : forall (a:A) (n:nat), vector n. -Proof. - induction n as [| n v]. - exact Vnil. +(* This works... - exact (Vcons a n v). -Defined. +Notation "'!rew' a -> b [ Heq ] 'in' t" := (eq_rect a _ t b Heq) + (at level 10, a, b at level 80). + +Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A := + match v with + | Vnil => I + | Vcons a n v => + match v in vector q return n=q -> A with + | Vnil => fun _ => a + | Vcons _ q _ => fun Heq => Vlast q (!rew n -> (S q) [Heq] in v) + end (refl_equal n) + end. +*) + +(* Remarks on the definition of Vlast... + +(* The ideal version... still now accepted, even with Program *) +Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A := + match v with + | Vnil => I + | Vcons a _ Vnil => a + | Vcons a n v => Vlast (pred n) v + end. + +(* This version does not work because Program Fixpoint expands v with + violates the guard condition *) + +Program Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A := + match v in vector p return match p with O => True | _ => A end with + | Vnil => I + | Vcons a _ Vnil => a + | Vcons a _ (Vcons _ n _ as v) => Vlast n v + end. + +(* This version works *) + +Program Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A := + match v in vector p return match p with O => True | _ => A end with + | Vnil => I + | Vcons a n v => + match v with + | Vnil => a + | Vcons _ q _ => Vlast q v + end + end. +*) + +Fixpoint Vconst (a:A) (n:nat) := + match n return vector n with + | O => Vnil + | S n => Vcons a _ (Vconst a n) + end. + +(** Shifting and truncating *) Lemma Vshiftout : forall n:nat, vector (S n) -> vector n. Proof. induction n as [| n f]; intro v. exact Vnil. - + inversion v as [| a n0 H0 H1]. exact (Vcons a n (f H0)). Defined. @@ -123,28 +172,35 @@ Proof. auto with *. Defined. -Lemma Vextend : forall n p:nat, vector n -> vector p -> vector (n + p). -Proof. - induction n as [| n f]; intros p v v0. - simpl in |- *; exact v0. - - inversion v as [| a n0 H0 H1]. - simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)). -Defined. +(** Concatenation of two vectors *) + +Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) := + match v with + | Vnil => w + | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w) + end. + +(** Uniform application on the arguments of the vector *) Variable f : A -> A. -Lemma Vunary : forall n:nat, vector n -> vector n. -Proof. - induction n as [| n g]; intro v. - exact Vnil. - - inversion v as [| a n0 H0 H1]. - exact (Vcons (f a) n (g H0)). -Defined. +Fixpoint Vunary n (v:vector n) : vector n := + match v with + | Vnil => Vnil + | Vcons a n' v' => Vcons (f a) n' (Vunary n' v') + end. Variable g : A -> A -> A. +(* Would need to have the constraint n = n' ... + +Fixpoint Vbinary n (v w:vector n) : vector n := + match v, w with + | Vnil, Vnil => Vnil + | Vcons a n' v', Vcons b _ w' => Vcons (g a b) n' (Vbinary n' v' w') + end. +*) + Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n. Proof. induction n as [| n h]; intros v v0. @@ -154,14 +210,16 @@ Proof. exact (Vcons (g a a0) n (h H0 H2)). Defined. +(** Eta-expansion of a vector *) + Definition Vid : forall n:nat, vector n -> vector n. Proof. - destruct n; intro X. + destruct n; intro v. exact Vnil. - exact (Vcons (Vhead _ X) _ (Vtail _ X)). + exact (Vcons (Vhead _ v) _ (Vtail _ v)). Defined. -Lemma Vid_eq : forall (n:nat) (v:vector n), v=(Vid n v). +Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v. Proof. destruct v; auto. Qed. -- cgit v1.2.3