seance4 : autre Vcast

seance4.v

@@ -333,18 +333,54 @@ Fixpoint Vrev {A} {n} (v:vect A n) : vect A n :=
 
 Compute Vrev (Vcons 1 (Vcons 2 (Vcons 3 Vnil))).
 
-(** Solution : faire une preuve "transparente", ou s'embeter
-    un peu plus lors de la définition du [Vcast]. *)
+(** Une solution : faire une preuve "transparente" ... *)
 
 Lemma add_1_r n : n + 1 = S n.
 Proof.
  induction n; simpl; trivial. now f_equal.
 Defined.  (** Et pas Qed ! *)
 
-Fixpoint Vrev' {A} {n} (v:vect A n) : vect A n :=
+Fixpoint Vrev_transp {A} {n} (v:vect A n) : vect A n :=
   match v with
   | Vnil => Vnil
-  | Vcons x v => Vcast (Vapp (Vrev' v) (Vcons x Vnil)) (add_1_r _)
+  | Vcons x v => Vcast (Vapp (Vrev_transp v) (Vcons x Vnil)) (add_1_r _)
   end.
 
-Compute Vrev' (Vcons 1 (Vcons 2 (Vcons 3 Vnil))).
+Compute Vrev_transp (Vcons 1 (Vcons 2 (Vcons 3 Vnil))).
+
+(** Autre solution : s'embêter sensiblement plus lors de la définition du
+    [Vcast]. Pour l'instant, ne pas chercher à saisir tous les détails... *)
+
+Definition Vcast2: forall {A m} (v: vect A m) {n}, m = n -> vect A n.
+Proof.
+ refine (fix cast {A m} (v: vect A m) {struct v} :=
+  match v in vect _ m' return forall n, m' = n -> vect A n with
+  |Vnil => fun n => match n with
+    | 0 => fun H => Vnil
+    | S _ => fun H => False_rect _ _
+  end
+  |Vcons h w => fun n => match n with
+    | 0 => fun H => False_rect _ _
+    | S n' => fun H => Vcons h (cast w n' (f_equal pred H))
+  end
+ end); discriminate.
+Defined.
+
+(** Au niveau calculatoire, cette fonction [Vcast2] déconstruit
+    le vecteur [v] avant de tout reconstruire. *)
+
+Print Vcast2.
+
+(** NB : Pour inspecter l'algorithme sous-jacent, on peut utiliser
+    l'extraction (cf ultérieurement). *)
+
+Require Extraction.
+Extraction Vcast2.
+
+Fixpoint Vrev2 {A} {n} (v:vect A n) : vect A n :=
+  match v with
+  | Vnil => Vnil
+  | Vcons x v => Vcast2 (Vapp (Vrev2 v) (Vcons x Vnil)) (Nat.add_1_r _)
+  end.
+
+Compute Vrev2 (Vcons 1 (Vcons 2 (Vcons 3 Vnil))).