gdsfh

Сегодня lj\thedeemon показал ужосы, от которых у меня волосы в жилах стынут.
А мне стало интересно, можно ли накосячить подобным образом в coq.
Но писал я быстро, поэтому код некрасивый. Например, можно спокойно попрятать многое в implicit arguments, да и для vec выбрать более кошерный тип (например, кошерный в плане strict positivity).

Require Import List.
Require Import Omega.

Definition vec A n := { lst : list A | length lst = n }.

Definition with_first_cons
  A B n (ne : n > 0) (v : vec A n)
  (f : forall h t (Heq : proj1_sig v = cons h t), B) : B
.
destruct v as [lst pf].
refine
  (match lst as lst0 return lst = lst0 -> _ with
   | nil => fun Heq => False_rect _ _
   | cons h t => fun Heq => f h t _
   end
   (eq_refl lst)
  )
.
(* nil *)
  subst.
  simpl in *.
  omega.
(* f arg *)
  subst.
  auto.
Defined.

Definition vhead A n ne v := with_first_cons A A n ne v
  (fun h _t _ => h).

Definition of_list A (lst : list A) : vec A (length lst).
exists lst.
reflexivity.
Defined.

Definition vtail A n (ne : n > 0) (v : vec A n) : vec A (n - 1).
refine (
with_first_cons A (vec A (n - 1)) n ne v
  (fun _h t pf => _)
).
assert (t_len : length t = n - 1).
(**)
  destruct v as [lst vpf].
  simpl in *.
  subst.
  simpl in *.
  omega.
(**)
exists t.
exact t_len.
Defined.


Definition vapp A n m (v1 : vec A n) (v2 : vec A m)
 : vec A (n + m)
.
destruct v1 as [l1 npf].
destruct v2 as [l2 mpf].
exists (l1 ++ l2).
SearchAbout (length (_ ++ _) = length _ + _).
rewrite app_length.
subst; reflexivity.
Defined.

Definition vone A (x : A) : vec A 1
.
exists (x :: nil).
simpl; reflexivity.
Defined.


Definition vec_cast A n m
  (v : vec A n) (H : n = m) : vec A m
.
destruct v as [l p].
exists l.
rewrite H in p.
exact p.
Defined.


Definition rot A n (v : vec A n) : vec A n.
Require Import Compare_dec.
SearchAbout ( { _ = 0 } + { _ } ).
destruct (zerop n) as [n_eq_z | z_lt_n].
(* n = 0 *)
  exists nil.
  auto.
(* 0 < n *)
  set (r :=
    vapp A _ _
      (vtail A n z_lt_n v)
      (vone A (vhead A n z_lt_n v))
  ).
assert (Ar : n - 1 + 1 = n).
(**)
  omega.
(**)
exact (vec_cast A _ _ r Ar).
Defined.

Definition list_of_vec {A n} (v : vec A n) : list A.
destruct v as [lst _].
exact lst.
Defined.


Eval compute in list_of_vec
  (rot _ _ (of_list _ (1 :: 2 :: 3 :: 4 :: nil))).

(*
     = 2 :: 3 :: 4 :: 1 :: nil
     : list nat
*)

Extraction Inline zerop.
Extraction Inline vapp vtail vhead with_first_cons vec_cast
                  vone.
(**)
Require ExtrOcamlBasic.
Require ExtrOcamlBigIntConv.
Require ExtrOcamlIntConv.
Require ExtrOcamlNatBigInt.
Require ExtrOcamlNatInt.
Require ExtrOcamlString.
Require ExtrOcamlZBigInt.
Require ExtrOcamlZInt.
Extraction Blacklist String List Not_found.
(**)
Extraction rot.

(*
(** val rot : int -> 'a1 vec -> 'a1 vec **)

let rot n v =
  let s =
    (fun fO fS n -> if n=0 then fO () else fS (n-1))
      (fun _ ->
      true)
      (fun n0 ->
      false)
      n
  in
  if s
  then []
  else app
         (match v with
          | [] -> assert false (* absurd case *)
          | h :: t -> t)
         ((match v with
           | [] -> assert false (* absurd case *)
           | h :: t -> h
          ) :: [])
*)

Однако, кое-какая лажа у меня таки была. Если rewrite, ныне вынесенный в vec_cast, натравить не на чистый пруф-терм ("n = m -> length l = n -> length l = m"), а на computational term (в том числе содержащий пруф) ("n = m -> vec A n -> vec A m"), то Eval compute выдаёт совершенно аццкий терм, содержащий в том числе пруф того, что длины равны. Но в #coq быстро объяснили, в чём дело. В этом состоит мой личный профит от этой задачки. Ну и развлёкся, и убедился, что в coq подобные косяки допустить трудно, даже если используются тактики.