gistfile1.coq

Require Import String.
Definition named_goal (A : Type) (s : string) := A.
Notation _as s := (_ : named_goal _ s).


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



Record r_eq_dec (t : Type) :=
  { ed_dec : forall a b : t, {a = b} + {a <> b}
  }
.


Section Listset.

Require Import List.

Variable kt : Type.
Variable ed : r_eq_dec kt.

Definition keq_dec := ed.(ed_dec kt).

Definition keq a b : Prop :=
  if keq_dec a b
  then True
  else False
.

Lemma ed_eq : forall R a (th el : R),
  (if keq_dec a a then th else el) = th.
intros.
destruct (keq_dec a a); tauto.
Defined.
Hint Rewrite ed_eq.

Lemma ed_neq : forall R a b (th el : R) (N : a <> b),
  (if keq_dec a b then th else el) = el.
intros.
destruct (keq_dec a b);
tauto.
Defined.
Hint Rewrite ed_neq.


Ltac au :=
  subst;
  unfold keq in *;
  unfold keq_dec in *;
  try rewrite ed_eq in *;
  (match goal with
   | H : if ed_dec ?t ?ed ?a ?b then _ else _ |- ?a = ?b =>
      (destruct (ed_dec t ed a b); try contradiction; now auto)
      || fail
   | _ => idtac
   end
  );
  (tauto ||
   auto
  )
.

Definition eq_of_keq : forall a b, keq a b -> (a = b).
intros.
au.
Defined.
Hint Resolve eq_of_keq.

Definition keq_of_eq : forall a b, (a = b) -> keq a b.
intros.
au.
Defined.
Hint Resolve keq_of_eq.


Inductive in_list (k : kt) : list kt -> Prop :=
| In_head : forall h t, keq k h -> in_list k (h :: t)
| In_tail : forall h t, in_list k t -> in_list k (h :: t)
.

Inductive unique_set : list kt -> Prop :=
| Su_nil : unique_set nil
| Su_cons : forall h t,
    ~ in_list h t -> unique_set t -> unique_set (h :: t)
.


Inductive find_in_list_res k s : Type :=
| Found : in_list k s -> find_in_list_res k s
| Not_found :
    ~ in_list k s ->
    in_list k (k :: s) ->
    find_in_list_res k s
.

(* Extraction find_in_list_res. *)

Fixpoint find k lst :=
  match lst with
  | nil => false
  | cons h t =>
      if keq_dec k h
      then true
      else find k t
  end
.


Definition find_pf k lst : find_in_list_res k lst.
refine
  (match find k lst as fres return (fres = find k lst) -> _ with
   | true => fun Hf => Found (_as "f1") (_as "f2") (_as "f3")
   | false => fun Hf => Not_found (_as "nf1") (_as "nf2") (_as "nf3") (_as "nf4")
   end
   (eq_refl (_as "refl"))
  ).

proving goal "f3"%string.
  induction lst.
  (* nil *)
    simpl in *.
    congruence.
  (* cons *)
    simpl in *.
    destruct (keq_dec k a).
    (* = *)
      subst; apply In_head.
      au.
    (* <> *)
      apply In_tail.
      auto.

proving goal "nf3"%string.
  induction lst.
  (* nil *)
    now (intro F; inversion F).
  (* cons *)
    simpl in *.
    destruct (keq_dec k a).
    (* = *)
      congruence.
    (* <> *)
      intro H.
      inversion H; now au.

proving goal "nf4"%string.
  apply In_head; au.

Defined.

(*
Extraction find.
Extraction keq_dec.
Extraction ed_dec.
 -- to inline it
*)


Inductive replace_in_list_res k lst : list kt -> Prop :=
| Replaced : in_list k lst -> replace_in_list_res k lst lst
| Added : ~ in_list k lst ->
          in_list k (k :: lst) ->
          replace_in_list_res k lst (k :: lst)
.


Definition replace_in_list (k : kt) (lst : list kt)
 : { r : list kt | replace_in_list_res k lst r }.
refine
  (match (find_pf k lst) with
   | Found f =>
       exist
         (fun q => replace_in_list_res k lst q)
         lst
         (Replaced k lst f)
   | Not_found not_in_lst in_k_ks =>
       exist
         (fun q => replace_in_list_res k lst q)
         (cons k lst)
         (Added k lst not_in_lst in_k_ks)
   end
  )
.
Defined.

End Listset.



Module Type EQDEC.
  Parameter t : Type.
  Parameter eq_dec : forall (a b : t), {a = b} + {a <> b}.
End EQDEC.



Module Make (K : EQDEC).

Require List.

Definition kt := K.t.

Definition key vt (pair : (kt * vt)) : kt :=
  match pair with (k, _v) => k end
.

Definition rd : r_eq_dec kt :=
  {| ed_dec := K.eq_dec |}
.

Definition key_eq_prop := keq kt rd.

Definition ukeys vt mr := unique_set kt rd (List.map (key vt) mr).

Definition t vt :=
  { mr : list (kt * vt) | unique_set kt rd (List.map (key vt) mr) }
.

Hint Constructors unique_set.


Ltac au :=
  subst;
  unfold keq in *;
  unfold keq_dec in *;
  try rewrite ed_eq in *;
  try rewrite ed_neq in *;
  try assumption;
  (match goal with
   | H : if ed_dec ?t ?ed ?a ?b then _ else _ |- ?a = ?b =>
      (destruct (ed_dec t ed a b); try contradiction; now auto)
      || fail
   | N : ?k <> ?a, H : if keq ?kt ?rd ?k ?a then _ else _
       |- _ => 
         unfold keq in H;
         destruct (keq_dec kt rd k a);
         [ (contradiction || (subst; tauto)) | assumption ]
   | N : ?a <> ?b |- if K.eq_dec ?a ?b then _ else _ =>
       destruct (K.eq_dec a b);
       now ( tauto || assumption )
   | _ => idtac
   end
  );
  (contradiction ||
   tauto ||
   auto
  )
.



Definition empty vt : t vt.
exists nil.
simpl.
au.
Defined.


Lemma unique_set_1 : forall (x : kt), unique_set kt rd (x :: nil).
intros x.
apply Su_cons; auto.
intro H.
inversion H.
Qed.
Hint Resolve unique_set_1.


Lemma unique_drop :
  forall (h0 : kt) (t0 : list kt) (uq : unique_set kt rd (h0 :: t0)),
  unique_set kt rd t0.
intros h0 t0 uq.
inversion uq.
auto.
Defined.
Hint Resolve unique_drop.


Definition keys (vt : Type) (m : t vt) :
  { ks : list kt | unique_set kt rd ks }.
destruct m as [ mr uq ].
exists (List.map (key vt) mr).
exact uq.
Defined.

Lemma eq_keys : forall (ks1 ks2 : list kt),
  (ks1 = ks2) -> unique_set kt rd ks1 -> unique_set kt rd ks2.
intros; subst; auto.
Defined.

Definition map_of_set :
  forall vt (mr : list (kt * vt)),
  unique_set kt rd (List.map (key vt) mr) ->
  t vt.
intros vt mr uq.
exists mr.
exact uq.
Defined.

Definition map_on_lists (vt1 vt2 : Type) (f : vt1 -> vt2)
  (mr1 : list (kt * vt1))
  : list (kt * vt2)
  :=
    List.map
      (fun kv1 =>
         match kv1 with
         | (k, v1) => (k, f v1)
         end
      )
      mr1
.

Definition map (vt1 vt2 : Type) (f : vt1 -> vt2)
  (m1 : t vt1)
  : t vt2.
destruct m1 as [mr1 uq1].
exists (map_on_lists vt1 vt2 f mr1).
 assert (Ke : List.map (key vt1) mr1
    = List.map (key vt2) (map_on_lists vt1 vt2 f mr1)).
(* proving Ke *)
  clear uq1.
  induction mr1 as [ | [ mr1_k mr1_v ] mr1_t ].
  (* nil *)
    auto.
  (* cons *)
    simpl.
    Lemma decons :
      forall A (h : A) t1 t2, (t1 = t2) -> ((cons h t1) = (cons h t2)).
      intros.
      subst.
      reflexivity.
    Qed.
    apply decons.
    assumption.
(* getting uq2 *)
  rewrite <- Ke.
  assumption.
Defined.


Definition in_mr
  vt
  (k : kt)
  (mr : list (kt * vt))
 : Prop
 :=
   in_list kt rd k (List.map (key vt) mr)
.


Lemma in_mr_empty : forall vt (k : kt), in_mr vt k nil -> False.
intros vt k H.
unfold in_mr in *.
simpl in *.
now inversion H.
Qed.


(* *)


Definition get_existent
  vt
  (k : kt)
 :
  forall (mr : list (kt * vt)) (H_in_mr : in_mr vt k mr), vt
.
refine
  ( (fix _self_ lst :=
       match lst as lst0 return in_mr vt k lst0 -> vt with
       | nil => fun Hin => (_as "nil")
       | cons hkv t =>
           match hkv as hkv0 return in_mr vt k (hkv0 :: t) -> vt with
           | (hk, hv) => fun Hin =>
               if K.eq_dec k hk
               then
                 hv
               else
                 _self_ t (_as "new Hin")
           end
       end
    )
  )
.

proving goal "nil"%string.
eapply in_mr_empty in Hin; now contradiction.

proving goal "new Hin"%string.
inversion Hin; au.
Defined.

Extraction get_existent.



Definition get_opt
  vt
  (k : kt)
  (mr : list (kt * vt))
 :
  option vt
.
refine
  ( (fix _self_ mr :=
       match mr with
       | nil => None
       | cons hkv t =>
           match hkv with
           | (hk, hv) =>
               if K.eq_dec k hk
               then Some hv
               else _self_ t
           end
       end
    )
    mr
  )
.
Defined.


Lemma get_opt_res
  vt
  (k : kt)
  (mr : list (kt * vt))
 :
  (match get_opt vt k mr with
   | None => ~ in_mr vt k mr
   | Some _ => in_mr vt k mr
   end
  ).
induction mr as [ | [hk hv] t ].
(* nil *)
  simpl.
  intro H; apply in_mr_empty in H; au.
(* cons *)
  simpl in *.
  destruct (K.eq_dec k hk).
  (* = *)
    apply In_head.
    au.
  (* <> *)
    destruct (get_opt vt k t).
    (* ? *)
      apply In_tail; now auto.
    (* ? *)
      contradict IHt.
      inversion IHt.
      (* in head *)
        subst.
        au.
      (* in tail *)
        subst.
        auto.
Defined.

Lemma in_mr_drop1 :
  forall vt k hk hv t (n : k <> hk) (Hin : in_mr vt k t),
  in_mr vt k ((hk, hv) :: t).
intros.
apply In_tail.
unfold in_mr in Hin.
auto.
Defined.



Inductive find_in_mr_res vt k (mr : list (kt * vt))
 : Prop
 :=
   | Mr_found :
       forall
         (v : vt)
         (H_in_mr : in_mr vt k mr),
       find_in_mr_res vt k mr
   | Mr_not_found : ~ in_mr vt k mr ->
                    find_in_mr_res vt k mr
.


Definition find_in_mr
  vt
  (k : kt)
  (mr : list (kt * vt))
 :
  find_in_mr_res vt k mr
.
Open Scope string_scope.
refine
  (match get_opt vt k mr as get_opt_res
   return (get_opt_res = get_opt vt k mr)
          -> find_in_mr_res vt k mr
   with
   | None => fun Hg =>
       Mr_not_found (_as "nf1") (_as "nf2") (_as "nf3") (_as "nf4")
   | Some v => fun Hg =>
       ((fun Hin =>
          Mr_found vt k mr v Hin
        )
        (_as "f5")
       )
   end
   (eq_refl _)
  )
.
proving goal "f5".
induction mr as [ | [hk hv] t].
(* nil *)
  simpl in *.
  congruence.
(* cons *)
  simpl in *.
  destruct (K.eq_dec k hk).
  (* = *)
    subst.
    apply In_head.
    au.
  (* <> *)
    apply In_tail.
    tauto.

proving goal "nf4".
intro H.
induction mr as [ | [hk hv] t].
(* nil *)
  apply in_mr_empty in H.
  assumption.
(* cons *)
  simpl in *.
  destruct (K.eq_dec k hk).
  (* = *)
    congruence.
  (* <> *)
    inversion H.
    (* ? *)
      subst; au.
    (* ? *)
      subst.
      tauto.
Defined.


Definition replace_existent
  vt
  (k : kt)
  (v : vt)
  (mr : list (kt * vt))
  (Hin : in_mr vt k mr)
 :
  { r : list (kt * vt)
  | List.map (key vt) mr = List.map (key vt) r
  }
.
refine
 (
  (fix _self_ lst
     (Hin : in_mr vt k lst)
    :=
     match lst
       as lst0
       return (lst = lst0) -> _
     with
     | nil => fun Heq => False_rect _ (_as "nil")
     | cons (hk, hv) t =>
         fun Heq =>
         (fun (eqd : {k = hk} + {k <> hk}) =>
         if eqd
         then
           exist _ ((hk, v) :: t) (_as "keys eq found")
         else
           (fun new_Hin =>
           match _self_ t new_Hin
           with
           | exist t' pf_keys_eq =>
               exist _ ((hk, hv) :: t') (_as "t keys eq")
           end
           ) (_as "new Hin")
         )
         (K.eq_dec k hk)
     end
     (eq_refl _)
  )
  mr
  Hin
 ); clear _self_
.

proving goal "nil".
subst.
apply in_mr_empty in Hin0; now assumption.

proving goal "keys eq found".
subst.
simpl.
reflexivity.

proving goal "t keys eq".
subst.
simpl in *.
f_equal.
now assumption.

proving goal "new Hin".
subst.
unfold in_mr in *.
simpl in *.
inversion Hin0; now au.

Defined.

(* Extraction replace_existent. *)


Inductive replace_in_mr_res vt : list (kt * vt) -> Prop :=
| Replaced : forall k mr (Hin : in_mr vt k mr)
               (uq : unique_set kt rd (List.map (key vt) mr)),
             replace_in_mr_res vt mr
| Added : forall k v mr (Hnotin : ~ in_mr vt k mr)
               (uq : unique_set kt rd (List.map (key vt) mr))
               (uq_new : unique_set kt rd (List.map (key vt) ((k, v) :: mr))),
             replace_in_mr_res vt ((k, v) :: mr)
.


Fixpoint replace_in_mr
  vt
  (k : kt)
  (v : vt)
  (mr : list (kt * vt))
  (uq : unique_set kt rd (List.map (key vt) mr))
 :
  { r : list (kt * vt) | replace_in_mr_res vt r }
.

refine
  (
   let go := get_opt vt k mr in
   match go
     as get_opt_r
     return (get_opt vt k mr = get_opt_r) -> { r : list (kt * vt) | replace_in_mr_res vt r }
   with
   | Some _ => fun Heq =>
       let Hin := (_as "in") in
       let re :=
        (replace_existent vt k v mr Hin)
       in
       (
        (  match re with
           | exist r r_keys_eq =>
             exist _ r
               (Replaced vt k r (_as "replaced in")
                  (_as "replaced uq"))
           end
        )
       )
   | None => fun Heq => exist _ ((k, v) :: mr)
       (Added vt k v mr (_as "added not in") (_as "uq mr") (_as "uq new"))
   end
   (eq_refl go)
  )
.
proving goal "in".
set (gr := get_opt_res vt k mr).
rewrite Heq in gr.
now auto.

proving goal "replaced in".
rewrite <- r_keys_eq.
now auto.

proving goal "replaced uq".
rewrite <- r_keys_eq.
now assumption.

proving goal "added not in".
set (gr := get_opt_res vt k mr).
rewrite Heq in gr.
now assumption.

proving goal "uq mr".
now assumption.

proving goal "uq new".
set (gr := get_opt_res vt k mr).
rewrite Heq in gr.
simpl in *.
apply Su_cons.
(* ? *)
  assumption.
(* ? *)
  assumption.

Defined.


Definition replace vt (k : kt) (v : vt) (m : t vt) : t vt.
destruct m as [mr1 uq1].
set (rr := replace_in_mr vt k v mr1 uq1).
destruct rr as [mr2 rres].
exists mr2.
inversion rres.
(* ? *)
  now assumption.
(* ? *)
  now assumption.
Defined.

End Make.



Module Deep_fail.

Inductive deep_failure (A : Type) (s : A) : Type :=
  Deep_failure : deep_failure A s.

Ltac fail_deep s := set (deep_failure := Deep_failure _ s).

Ltac with_deep_failure := fun tac =>
  match goal with
  | [ F : deep_failure _ ?s |- _ ] =>
        let ss := eval compute in s in
        clear F;
        tac ss
  | _ => idtac
  end
.

Ltac show_deep_failure :=
  with_deep_failure ltac:(fun ss => fail 1 ss)
.

Ltac map_deep_failure f :=
  with_deep_failure ltac:(fun ss => fail_deep (f ss))
.

End Deep_fail.



Module Unique_tac.

Inductive keys_equal kt rd (a b : kt) : Prop :=
| Keys_equal : (keq kt rd a b) -> keys_equal kt rd a b
.


Definition step_in_list kt rd k h t
  (Hin : in_list kt rd k (h :: t))
 :
  { in_list kt rd k t }
  +
  { keys_equal kt rd k h }
.
destruct (ed_dec kt rd k h).
right.
constructor.
subst.
unfold keq.
rewrite ed_eq.
exact I.
left.
inversion Hin.
subst.
unfold keq in *.
rewrite ed_neq in H0.
contradiction.
assumption.
assumption.
Defined.


(* из "(k <> h) -> False" либо решает эту дырку, если k <> h,
   либо генерирует deep failure. *)
Ltac destruct_keys_eq :=
  match goal with
  | H : keys_equal ?kt ?rd ?k ?k |- _ => Deep_fail.fail_deep k
  | H : keys_equal ?kt ?rd ?k ?h |- _ =>
      let Hkeq := fresh "Hkeq" in
      inversion H as [Hkeq];
      now inversion Hkeq
end
.

(* из гипотезы in_list k (h :: (m :: t)) пытается доказать,
   что k <> h и превратить её в in_list k (m :: t).
   Если же k = h -- генерируется deep failure.
 *)
Ltac tac_not_in Hin :=
  (now inversion Hin)
  ||
  (let Hin' := fresh "Hin" in
   destruct (step_in_list _ _ _ _ _ Hin) as [ Hin' | ];
   [ tac_not_in Hin'
   | destruct_keys_eq
   ]
  )
.

(* разбирает unique_set, отбрасывая голову на каждом шаге *)
Ltac tac_uq_init :=
  match goal with
  | |- unique_set ?kt ?rd nil =>
         now apply Su_nil
  | |- unique_set ?kt ?rd (?h :: ?t) =>
         let Hnotin := fresh "Hnotin" in
         assert (Hnotin : ~ in_list kt rd h t);
         [ (let Hin := fresh "Hin" in
            intro Hin; tac_not_in Hin
           )
         | apply (Su_cons _ _ _ _ Hnotin);
           clear Hnotin;
           tac_uq_init
         ]
  end
.

End Unique_tac.