gistfile1.coq

(* внимание, Coq >=8.4 только. *)

(* манатка: *)

Axiom m : Type -> Type.

Axiom ret : forall {A}, A -> m A.

Axiom bind : forall {A B}, (A -> m B) -> m A -> m B.

Notation "x <- y ;; z" := (@bind _ _ (fun x => z) y)
 (at level 64, y at next level, right associativity)
.

Notation "y ;; z" := (@bind _ _ (fun (_ : unit) => z) y)
 (at level 64)
.

Notation "x $ y" := (x y)
 (at level 63, right associativity, only parsing)
.


(* прочитать целое: *)

Require Import ZArith.

Axiom input_int : m Z.


(* список с зависимым типом -- размер в типе: *)

Require Import List.

Definition vec (sz : nat) (A : Type) :=
  { r : list A | length r = sz }
.

Extraction vec.
(*
экстрактится в обычный список:

type 'a vec = 'a list

где размер?  нету размера.
*)


Definition vec_empty A : vec 0 A.
 exists nil; auto.
Defined.

Definition vec_snoc {A n} (v : vec n A) (x : A) : vec (n + 1) A.
 destruct v as [r pf].
 exists (List.app r (x :: nil)).
 (* proof *)
 rewrite List.app_length.
 rewrite pf.
 simpl length.
 reflexivity.
Defined.

Extraction Implicit vec_snoc [n].
(* coq мог бы сам догадаться, что в рантайме n не используется.
   ну да пофиг, вреда от n не было бы.
   но уберём для красоты.
*)

Extraction vec_snoc.
(*

(** val vec_snoc : 'a1 vec -> 'a1 -> 'a1 vec **)

let vec_snoc v x =
  app v (Cons (x, Nil))

*)


(* named goals (с ними удобнее доказывать факты --
   видно, что конкретно доказываешь):
*)

Require Import String.

Definition named_goal (A : Type) (s : string) := A.
Notation _as s := (_ : named_goal _ s).
Definition named_goalp (A : Prop) (s : string) := A.
Notation _asp s := (_ : named_goalp _ s).


Tactic Notation "proving" "goal" constr(name) :=
  match goal with
  | |- named_goal _ name => unfold named_goal
  | _ => fail 1 "current goal is not '" name "'"
  end
.
Tactic Notation "proving" "goalp" constr(name) :=
  match goal with
  | |- named_goalp _ name => unfold named_goalp
  | _ => fail 1 "current Prop-goal is not '" name "'"
  end
.


(* собственно код: *)

Open Scope Z_scope.
Open Scope string_scope.

Require Import Zwf.

(* для того, чтобы константы не загромождали экстракченный код *)
Definition limit := 100500100500.
Definition one := 1.
Definition zero := 0.


Definition input_list_int
: m { s : nat & vec s Z }.
refine
 ( (fix _self_ (maxsz : Z) (maxsz_ge_0 : maxsz >= 0)
      cursz (acc : vec cursz Z)
      (Hacc : Acc (Zwf 0) maxsz)
      {struct Hacc}
    : m { s : nat & vec s Z } :=
      match Hacc with
      | Acc_intro acc_pf =>
          match Z_lt_dec zero maxsz with
          | right pf_le =>
              ret $ existT _ cursz acc
          | left pf_gt =>
              x <- input_int;;
              if x =? zero
              then
                ret $ existT _ cursz acc
              else
                _self_ (maxsz - one) (_as "rec ge")
                  (cursz + 1)%nat (vec_snoc acc x)
                  (_as "rec Hacc")
          end
      end
    )
    limit
    (_as "init ge")
    0%nat
    (@vec_empty Z)
    (_as "init Hacc")
 ); try clear _self_
.

proving goal "rec ge".

  Lemma minus1 : forall n, 0 < n -> (n - 1) >= 0.
    intros n H.
    omega.
  Defined.

  now exact (minus1 maxsz pf_gt).

proving goal "rec Hacc".
  assert (W : Zwf 0 (maxsz - 1) maxsz).
  (**)
    constructor.
    (* 1 *)
      unfold ">=", "<=" in *.
      rewrite Zcompare_Gt_Lt_antisym.
      now assumption.
    (* 2 *)
      now omega.
  (**)
  exact (acc_pf (maxsz - 1) W).

proving goal "init ge".
  simpl; now discriminate.

proving goal "init Hacc".
  refine (Zwf_well_founded _ _).

Defined.

Extraction input_list_int.

(*

(** val input_list_int : (nat, z vec) sigT m **)

let input_list_int =
  let rec _self_ maxsz cursz acc =
    match z_lt_dec zero0 maxsz with
    | Left ->
      bind (fun x ->
        match Z.eqb x zero0 with
        | True -> ret (ExistT (cursz, acc))
        | False ->
          _self_ (Z.sub maxsz one0) (plus cursz (S O)) (vec_snoc acc x))
        input_int
    | Right -> ret (ExistT (cursz, acc))
  in _self_ limit O vec_empty

*)


Open Scope nat_scope.


Definition vec_get
  {A sz} (i_arg : nat) (v_arg : vec sz A) (range_pf_arg : i_arg < sz)
 : A.
refine
  ( (fix _self_ i (lst : list A) (range_pf : i < List.length lst) : A :=
       match lst as lst' return lst = lst' -> _ with
       | nil => fun Leq => False_rect _ (_as "fin lst")
       | cons h t =>
           match i as i' return i = i' -> _ with
           | 0 => fun Leq Ieq => h
           | S i' => fun Leq Ieq => _self_ i' t (_as "range rec")
           end
           (eq_refl _)
       end
       (eq_refl _)
    )
    i_arg
    (proj1_sig v_arg)
    (_as "range init")
  ); try clear _self_; try clear i_arg; try clear v_arg
.

proving goal "fin lst".
  rewrite Leq in range_pf.
  simpl Datatypes.length in *.
  now omega.

proving goal "range rec".
  rewrite Leq in *; clear Leq.
  rewrite Ieq in *; clear Ieq.
  simpl in *.
  unfold "<" in *.
  now omega.

proving goal "range init".
  destruct v_arg as [v pf].
  unfold proj1_sig.
  now omega.

Defined.

Extraction Implicit vec_get [sz].

Extraction vec_get.

(*

(** val vec_get : nat -> 'a1 vec -> 'a1 **)

let rec vec_get i = function
| Nil -> assert false (* absurd case *)
| Cons (h, t) ->
  (match i with
   | O -> h
   | S i' -> vec_get i' t)

*)


(* этим будем выводить целое: *)
Axiom print_int : Z -> m unit.

(* этим будем брать случайный индекс: *)
Axiom random_int : forall range, m { r : nat | r < range }.
(* замечу, что реализация этой функции должна иметь тип
   nat -> m nat
   , а пруф как всегда стирается.
*)

Definition main : m unit.
refine
  ( lst <- input_list_int;;
    match lst with
    | existT inp_sz inp_vec =>
        index_and_range <- random_int inp_sz;;
        match index_and_range with
        | exist ind random_range_pf =>
            let item := vec_get ind inp_vec (_as "range") in
            print_int item
        end
    end
  )
.

proving goal "range".
  assumption.

Defined.

Extraction main.

(*

(** val main : unit0 m **)

let main =
  bind (fun lst ->
    let ExistT (inp_sz, inp_vec) = lst in
    bind (fun index_and_range ->
      let item = vec_get index_and_range inp_vec in print_int item)
      (random_int inp_sz)) input_list_int

*)