[personal profile] 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 подобные косяки допустить трудно, даже если используются тактики.
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org


 
Notice: This account is set to log the IP addresses of people who comment anonymously.
Links will be displayed as unclickable URLs to help prevent spam.

Profile

gdsfh

August 2013

S M T W T F S
    123
45678910
111213 14151617
18192021222324
25262728293031

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 23rd, 2017 02:35 pm
Powered by Dreamwidth Studios