построение термов тактиками в coq -- безопасно

[gds]

Сегодня 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 подобные косяки допустить трудно, даже если используются тактики.