text:
(** * Finite Modular Maps : Unordered Lists *)

(** Author : Pierre Letouzey (Université de Paris - INRIA),
    adapted from earlier works in Coq Standard Library, see README.md.
    Licence : LGPL 2.1, see file LICENSE. *)

(** This file proposes an implementation of the interface
 [Tries.MMaps.Interface.WS] using lists of pairs, unordered but without
 redundancy. Most operations are linear, with the notable exception
 of [merge] which is quadratic. *)

From Coq Require Import EqualitiesFacts.
From Tries.MMaps Require Interface Raw.
Import Interface.

Set Implicit Arguments.
Unset Strict Implicit.

Module MakeRaw (K:DecidableType) <: Raw.WS K.

Module Import P := KeyDecidableType K.

Definition key := K.t.
Definition t (elt:Type) := list (K.t * elt).

Definition eq_key {elt} := @P.eqk elt.
Definition eq_key_elt {elt} := @P.eqke elt.
Definition IsOk {elt} := NoDupA (@eqk elt).
Class Ok {elt}(m:t elt) : Prop := ok : NoDupA eqk m.

Ltac chok :=
 match goal with
 | H : context [NoDupA (@eqk ?elt)] |- _ =>
   change (NoDupA (@eqk elt)) with (@Ok elt) in H; chok
 | |- context [NoDupA (@eqk ?elt)] =>
   change (NoDupA (@eqk elt)) with (@Ok elt); chok
 | _ => idtac
 end.

Ltac autok := chok; auto with typeclass_instances.

Ltac dec := match goal with
 | |- context [ K.eq_dec ?x ?x ] =>
   let E := fresh "E" in destruct (K.eq_dec x x) as [E|E]; [ | now elim E]
 | H : K.eq ?x ?y |- context [ K.eq_dec ?x ?y ] =>
   let E := fresh "E" in destruct (K.eq_dec x y) as [_|E]; [ | now elim E]
 | H : ~K.eq ?x ?y |- context [ K.eq_dec ?x ?y ] =>
   let E := fresh "E" in destruct (K.eq_dec x y) as [E|_]; [ now elim H | ]
 | |- context [ K.eq_dec ?x ?y ] =>
   let E := fresh "E" in destruct (K.eq_dec x y) as [E|E]
end.

Section Elt.

Variable elt : Type.

(** * [find] *)

Fixpoint find (k:key) (s: t elt) : option elt :=
  match s with
   | nil => None
   | (k',x)::s' => if K.eq_dec k k' then Some x else find k s'
  end.

Lemma find_spec m x e {Hm:Ok m} :
  find x m = Some e <-> MapsTo x e m.
Proof.
 unfold P.MapsTo.
 induction m as [ | (k,v) m IH]; simpl.
 - split; inversion 1.
 - rewrite InA_cons.
   change (eqke (x,e) (k,v)) with (K.eq x k /\ e = v).
   inversion_clear Hm. dec.
   + setoid_replace (Some v = Some e) with (v = e) by (split; congruence).
     intuition. elim H. apply InA_eqk with (x,e); auto.
   + rewrite IH; intuition.
Qed.

(** * [mem] *)

Fixpoint mem (k : key) (s : t elt) : bool :=
  match s with
   | nil => false
   | (k',_) :: l => if K.eq_dec k k' then true else mem k l
  end.

Lemma mem_spec m x {Hm:Ok m} : mem x m = true <-> In x m.
Proof.
 induction m as [ | (k,e) m IH]; simpl.
 - split. discriminate. inversion_clear 1. inversion H0.
 - inversion_clear Hm. rewrite P.In_cons; simpl.
   rewrite <- IH by trivial.
   dec; intuition.
Qed.

Fixpoint isok (m: t elt) : bool :=
  match m with
   | nil => true
   | (k,_)::m' => negb (mem k m') && isok m'
  end.

Lemma isok_spec (m: t elt) : isok m = true <-> Ok m.
Proof.
 induction m as [|(x,e) m IH]; simpl.
 - split; constructor.
 - rewrite andb_true_iff, IH. split.
   + intros (H,O). constructor; auto.
     rewrite <- In_alt', <- mem_spec; auto. now destruct mem.
   + inversion 1; subst; split; auto.
     rewrite <- In_alt', <- mem_spec in H2; auto. now destruct mem.
Qed.

Lemma isok_Ok (m:t elt) : isok m = true -> Ok m.
Proof. apply isok_spec. Qed.

(** * [empty] *)

Definition empty : t elt := nil.

Lemma empty_spec x : find x empty = None.
Proof.
 reflexivity.
Qed.

Global Instance empty_ok : Ok empty.
Proof.
 unfold empty; red; auto.
Qed.

(** * [is_empty] *)

Definition is_empty (l : t elt) : bool := if l then true else false.

Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None.
Proof.
 destruct m as [|(x,e) m]; simpl; intuition; try discriminate.
 specialize (H x).
 revert H. now dec.
Qed.

(* Not part of the exported specifications, used later for [merge]. *)

Lemma find_eq : forall m (Hm:Ok m) x x',
   K.eq x x' -> find x m = find x' m.
Proof.
 induction m; simpl; auto; destruct a; intros.
 inversion_clear Hm.
 rewrite (IHm H1 x x'); auto.
 dec; dec; trivial.
 elim E0. now transitivity x.
 elim E. now transitivity x'.
Qed.

(** * [add] *)

Fixpoint add (k : key) (x : elt) (s : t elt) : t elt :=
  match s with
   | nil => (k,x) :: nil
   | (k',y) :: l => if K.eq_dec k k' then (k,x)::l else (k',y)::add k x l
  end.

Lemma add_spec1' m x e : find x (add x e m) = Some e.
Proof.
 induction m as [ | (k,e') m IH]; simpl.
 - now dec.
 - dec; simpl; now dec.
Qed.

Lemma add_spec2' m x y e : ~K.eq x y -> find y (add x e m) = find y m.
Proof.
 intros N.
 assert (N' : ~K.eq y x) by now contradict N.
 induction m as [ | (k,e') m IH]; simpl.
 - dec; trivial.
 - repeat (dec; simpl); trivial. elim N. now transitivity k.
Qed.

Lemma add_spec1 m x e `{!Ok m} : find x (add x e m) = Some e.
Proof. apply add_spec1'. Qed.
Lemma add_spec2 m x y e `{!Ok m} : ~K.eq x y -> find y (add x e m) = find y m.
Proof. apply add_spec2'. Qed.

Lemma add_InA : forall m x y e e',
  ~ K.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m.
Proof.
 induction m as [ | (k,e') m IH]; simpl; intros.
 - inversion_clear H0. elim H. symmetry; apply H1. inversion_clear H1.
 - revert H0; dec; rewrite !InA_cons.
   + rewrite E. intuition.
   + intuition. right; eapply IH; eauto.
Qed.

Global Instance add_ok m x e (Hm:Ok m) : Ok (add x e m).
Proof.
 induction m as [ | (k,e') m IH]; simpl.
 - constructor; auto. now inversion 1.
 - inversion_clear Hm. dec; constructor; autok.
   + contradict H. apply InA_eqk with (x,e); auto.
   + contradict H; apply add_InA with x e; auto.
Qed.

(** * [remove] *)

Fixpoint remove (k : key) (s : t elt) : t elt :=
  match s with
   | nil => nil
   | (k',x) :: l => if K.eq_dec k k' then l else (k',x) :: remove k l
  end.

Lemma remove_spec1 m x {Hm: Ok m} : find x (remove x m) = None.
Proof.
 induction m as [ | (k,e') m IH]; simpl; trivial.
 inversion_clear Hm.
 repeat (dec; simpl); auto.
 destruct (find x m) eqn:F; trivial.
 apply find_spec in F; trivial.
 elim H. apply InA_eqk with (x,e); auto.
Qed.

Lemma remove_spec2 m x y {Hm: Ok m} : ~K.eq x y ->
  find y (remove x m) = find y m.
Proof.
 induction m as [ | (k,e') m IH]; simpl; trivial; intros E.
 inversion_clear Hm.
 repeat (dec; simpl); auto.
 elim E. now transitivity k.
Qed.

Lemma remove_InA : forall m (Hm:Ok m) x y e,
  InA eqk (y,e) (remove x m) -> InA eqk (y,e) m.
Proof.
 induction m as [ | (k,e') m IH]; simpl; trivial; intros.
 inversion_clear Hm.
 revert H; dec; rewrite !InA_cons; intuition.
 right; eapply H; eauto.
Qed.

Global Instance remove_ok m x (Hm:Ok m) : Ok (remove x m).
Proof.
 induction m.
 simpl; intuition.
 intros.
 inversion_clear Hm.
 destruct a as (x',e').
 simpl; case (K.eq_dec x x'); auto.
 constructor; autok.
 contradict H; apply remove_InA with x; auto.
Qed.

(** * [bindings] *)

Definition bindings (m : t elt) := m.

Lemma bindings_spec1 m x e : InA eqke (x,e) (bindings m) <-> MapsTo x e m.
Proof.
 reflexivity.
Qed.

Lemma bindings_spec2w m (Hm:Ok m) : Ok (bindings m).
Proof.
 trivial.
Qed.

(** * [fold] *)

Fixpoint fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc : A) :  A :=
  match m with
   | nil => acc
   | (k,e)::m' => fold f m' (f k e acc)
  end.

Lemma fold_spec : forall m (A:Type)(i:A)(f:key->elt->A->A),
  fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
Proof.
 induction m as [ | (k,e) m IH]; simpl; auto.
Qed.

(** * [singleton] *)

Definition singleton k (e:elt) : t elt := (k,e)::nil.

Lemma singleton_spec x e : bindings (singleton x e) = (x,e)::nil.
Proof. reflexivity. Qed.

Global Instance singleton_ok x e : Ok (singleton x e).
Proof.
 constructor; auto. inversion 1.
Qed.

(** * [equal] *)

Definition check (cmp : elt -> elt -> bool)(k:key)(e:elt)(m': t elt) :=
  match find k m' with
   | None => false
   | Some e' => cmp e e'
  end.

Definition submap (cmp : elt -> elt -> bool)(m m' : t elt) : bool :=
  fold (fun k e b => andb (check cmp k e m') b) m true.

Definition equal (cmp : elt -> elt -> bool)(m m' : t elt) : bool :=
  andb (submap cmp m m') (submap (fun e' e => cmp e e') m' m).

Definition Submap (cmp:elt->elt->bool) m m' :=
  (forall k, In k m -> In k m') /\
  (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).

Definition Equal m m' := forall y, find y m = find y m'.
Definition Eqdom m m' := forall y, @In elt y m <-> @In elt y m'.
Definition Equiv (R:elt->elt->Prop) m m' :=
  Eqdom m m' /\
  (forall k e e', MapsTo k e m -> MapsTo k e' m' -> R e e').
Definition Equivb (cmp:elt->elt->bool) := Equiv (Cmp cmp).

Lemma submap_1 : forall m (Hm:Ok m) m' (Hm': Ok m') cmp,
  Submap cmp m m' -> submap cmp m m' = true.
Proof.
 unfold Submap, submap.
 induction m.
 simpl; auto.
 destruct a; simpl; intros.
 destruct H.
 inversion_clear Hm.
 assert (H3 : In t0 m').
 { apply H; exists e; auto with *. }
 destruct H3 as (e', H3).
 assert (H4 : find t0 m' = Some e') by now apply find_spec.
 unfold check at 2. rewrite H4.
 rewrite (H0 t0); simpl; auto with *.
 eapply IHm; auto.
 split; intuition.
 apply H.
 destruct H6 as (e'',H6); exists e''; auto.
 apply H0 with k; auto.
Qed.

Lemma submap_2 : forall m (Hm:Ok m) m' (Hm': Ok m') cmp,
  submap cmp m m' = true -> Submap cmp m m'.
Proof.
 unfold Submap, submap.
 induction m.
 simpl; auto.
 intuition.
 destruct H0; inversion H0.
 inversion H0.

 destruct a; simpl; intros.
 inversion_clear Hm.
 rewrite andb_b_true in H.
 assert (check cmp t0 e m' = true).
  clear H1 H0 Hm' IHm.
  set (b:=check cmp t0 e m') in *.
  generalize H; clear H; generalize b; clear b.
  induction m; simpl; auto; intros.
  destruct a; simpl in *.
  destruct (andb_prop _ _ (IHm _ H)); auto.
 rewrite H2 in H.
 destruct (IHm H1 m' Hm' cmp H); auto.
 unfold check in H2.
 case_eq (find t0 m'); [intros e' H5 | intros H5];
  rewrite H5 in H2; try discriminate.
 split; intros.
 destruct H6 as (e0,H6); inversion_clear H6.
 compute in H7; destruct H7; subst.
 exists e'.
 apply P.MapsTo_eq with t0; auto with *.
 apply find_spec; auto.
 apply H3.
 exists e0; auto.
 inversion_clear H6.
 compute in H8; destruct H8; subst.
 assert (H8 : MapsTo t0 e'0 m'). { eapply P.MapsTo_eq; eauto. }
 apply find_spec in H8; trivial. congruence.
 apply H4 with k; auto.
Qed.

(** Specification of [equal] *)

Lemma equal_spec cmp m m' {Hm:Ok m}{Hm': Ok m'} :
  equal cmp m m' = true <-> Equivb cmp m m'.
Proof.
 unfold equal.
 split.
 - intros.
   destruct (andb_prop _ _ H); clear H.
   generalize (submap_2 Hm Hm' H0).
   generalize (submap_2 Hm' Hm H1).
   firstorder.
 - intuition.
   apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder.
Qed.
End Elt.
Section Elt2.
Variable elt elt' : Type.

(** * [map] and [mapi] *)

Definition map (f:elt -> elt') (m:t elt) : t elt' :=
  List.map (fun '(k,e) => (k,f e)) m.

Definition mapi (f: key -> elt -> elt') (m:t elt) : t elt' :=
  List.map (fun '(k,e) => (k,f k e)) m.

(** Specification of [map] *)

Lemma map_spec (f:elt->elt')(m:t elt) :
  bindings (map f m) = List.map (fun '(k,e) => (k,f e)) (bindings m).
Proof.
 reflexivity.
Qed.

Lemma map_InA (f:elt->elt')(m:t elt) x e :
 InA eqk (x,f e) (map f m) <-> InA eqk (x,e) m.
Proof.
 induction m as [|(k,v) m IH]; simpl; rewrite ?InA_nil, ?InA_cons;
  intuition.
Qed.

Global Instance map_ok (f:elt->elt') m (Hm : Ok m) : Ok (map f m).
Proof.
 induction m as [|(x,e) m IH]; simpl. red; constructor.
 inversion_clear Hm. constructor; autok. now rewrite map_InA.
Qed.

(** Specification of [mapi] *)

Lemma mapi_spec (f:key->elt->elt')(m:t elt) :
  bindings (mapi f m) = List.map (fun '(k,e) => (k,f k e)) (bindings m).
Proof.
 reflexivity.
Qed.

Global Instance mapi_ok (f: key->elt->elt') m (Hm:Ok m) : Ok (mapi f m).
Proof.
 induction m as [|(x,e) m IH]; simpl. red; constructor.
 inversion_clear Hm; auto.
 constructor; autok.
 contradict H. clear IH H0.
 induction m as [|(y,v) m IH]; simpl in *; inversion H; auto.
Qed.

End Elt2.

Lemma mapfst_InA {elt}(m:t elt) x :
 InA K.eq x (List.map fst m) <-> In x m.
Proof.
 induction m as [| (k,e) m IH]; simpl; auto.
 - split; inversion 1. inversion H0.
 - rewrite InA_cons, In_cons. simpl. now rewrite IH.
Qed.

Lemma mapfst_ok {elt}(m:t elt) :
 NoDupA K.eq (List.map fst m) <-> NoDupA eqk m.
Proof.
 induction m as [| (k,e) m IH]; simpl.
 - split; constructor.
 - split; inversion_clear 1; constructor; try apply IH; trivial.
   + contradict H0. rewrite mapfst_InA. eapply In_alt'; eauto.
   + rewrite mapfst_InA. contradict H0. now apply In_alt'.
Qed.

Lemma list_filter_ok f (m:list key) :
 NoDupA K.eq m -> NoDupA K.eq (List.filter f m).
Proof.
 induction 1; simpl.
 - constructor.
 - destruct (f x); trivial. constructor; trivial.
   contradict H. rewrite InA_alt in *. destruct H as (y,(Hy,H)).
   exists y; split; trivial. now rewrite filter_In in H.
Qed.

Lemma NoDupA_unique_repr (l:list key) x y :
 NoDupA K.eq l -> K.eq x y -> List.In x l -> List.In y l -> x = y.
Proof.
 intros H E Hx Hy.
 induction H; simpl in *.
 - inversion Hx.
 - intuition; subst; trivial.
   elim H. apply InA_alt. now exists y.
   elim H. apply InA_alt. now exists x.
Qed.

Section Elt3.

Variable elt elt' elt'' : Type.

Definition restrict (m:t elt)(k:key) :=
 match find k m with
 | None => true
 | Some _ => false
 end.

Definition domains (m:t elt)(m':t elt') :=
 List.map fst m ++ List.filter (restrict m) (List.map fst m').

Lemma domains_InA m m' (Hm : Ok m) x :
 InA K.eq x (domains m m') <-> In x m \/ In x m'.
Proof.
 unfold domains.
 assert (Proper (K.eq==>eq) (restrict m)).
 { intros k k' Hk. unfold restrict. now rewrite (find_eq Hm Hk). }
 rewrite InA_app_iff, filter_InA, !mapfst_InA; intuition.
 unfold restrict.
 destruct (find x m) eqn:F.
 - left. apply find_spec in F; trivial. now exists e.
 - now right.
Qed.

Lemma domains_ok m m' : NoDupA eqk m -> NoDupA eqk m' ->
 NoDupA K.eq (domains m m').
Proof.
 intros Hm Hm'. unfold domains.
 apply NoDupA_app; auto with *.
 - now apply mapfst_ok.
 - now apply list_filter_ok, mapfst_ok.
 - intros x.
   rewrite mapfst_InA. intros (e,H).
   apply find_spec in H; trivial.
   rewrite InA_alt. intros (y,(Hy,H')).
   rewrite (find_eq Hm Hy) in H.
   rewrite filter_In in H'. destruct H' as (_,H').
   unfold restrict in H'. now rewrite H in H'.
Qed.

Fixpoint fold_keys (f:key->option elt'') l :=
  match l with
    | nil => nil
    | k::l =>
      match f k with
        | Some e => (k,e)::fold_keys f l
        | None => fold_keys f l
      end
  end.

Lemma fold_keys_In f l x e :
  List.In (x,e) (fold_keys f l) <-> List.In x l /\ f x = Some e.
Proof.
 induction l as [|k l IH]; simpl.
 - intuition.
 - destruct (f k) eqn:F; simpl; rewrite IH; clear IH; intuition;
   try left; congruence.
Qed.

Lemma fold_keys_ok f l :
  NoDupA K.eq l -> Ok (fold_keys f l).
Proof.
 induction 1; simpl.
 - constructor.
 - destruct (f x); trivial.
   constructor; trivial. contradict H.
   apply InA_alt in H. destruct H as ((k,e'),(E,H)).
   rewrite fold_keys_In in H.
   apply InA_alt. exists k. now split.
Qed.

Variable f : key -> option elt -> option elt' -> option elt''.

Definition merge m m' : t elt'' :=
 fold_keys (fun k => f k (find k m) (find k m')) (domains m m').

Global Instance merge_ok m m' (Hm:Ok m)(Hm':Ok m') : Ok (merge m m').
Proof.
 now apply fold_keys_ok, domains_ok.
Qed.

Lemma merge_spec1 m m' x {Hm:Ok m}{Hm':Ok m'} :
  In x m \/ In x m' ->
  exists y:key, K.eq y x /\
                find x (merge m m') = f y (find x m) (find x m').
Proof.
 assert (Hmm' : Ok (merge m m')) by now apply merge_ok.
 rewrite <- domains_InA; trivial.
 rewrite InA_alt. intros (y,(Hy,H)).
 exists y; split; [easy|].
 rewrite (find_eq Hm Hy), (find_eq Hm' Hy).
 destruct (f y (find y m) (find y m')) eqn:F.
 - apply find_spec; trivial.
   red. apply InA_alt. exists (y,e). split. now split.
   unfold merge. apply fold_keys_In. now split.
 - destruct (find x (merge m m')) eqn:F'; trivial.
   rewrite <- F; clear F. symmetry.
   apply find_spec in F'; trivial.
   red in F'. rewrite InA_alt in F'.
   destruct F' as ((y',e'),(E,F')).
   unfold merge in F'; rewrite fold_keys_In in F'.
   destruct F' as (H',F').
   compute in E; destruct E as (Hy',<-).
   replace y with y'; trivial.
   apply (@NoDupA_unique_repr (domains m m')); auto.
   now apply domains_ok.
   now transitivity x.
Qed.

Lemma merge_spec2 m m' x {Hm:Ok m}{Hm':Ok m'} :
  In x (merge m m') -> In x m \/ In x m'.
Proof.
 rewrite <- domains_InA; trivial.
 intros (e,H). red in H. rewrite InA_alt in H. destruct H as ((k,e'),(E,H)).
 unfold merge in H; rewrite fold_keys_In in H. destruct H as (H,_).
 apply InA_alt. exists k. split; trivial. now destruct E.
Qed.

End Elt3.

Definition cardinal {elt} (m:t elt) := length m.
Lemma cardinal_spec {elt} (m:t elt) : cardinal m = length (bindings m).
Proof. reflexivity. Qed.

Definition MapsTo {elt} := @P.MapsTo elt.
Definition In {elt} := @P.In elt.

Instance MapsTo_compat {elt} :
  Proper (K.eq==>Logic.eq==>Logic.eq==>iff) (@MapsTo elt).
Proof.
 intros x x' Hx e e' <- m m' <-. unfold MapsTo. now rewrite Hx.
Qed.

Definition filter {elt} (f:key->elt->bool) :=
  List.filter (fun '(k,e) => f k e).

Definition partition {elt} (f:key->elt->bool) :=
  List.partition (fun '(k,e) => f k e).

Definition for_all {elt} (f:key->elt->bool) :=
  List.forallb (fun '(k,e) => f k e).

Definition exists_ {elt} (f:key->elt->bool) :=
  List.existsb (fun '(k,e) => f k e).

Lemma filter_spec {elt} (f:key->elt->bool) m `{!Ok m} :
 bindings (filter f m) = List.filter (fun '(k,e) => f k e) (bindings m).
Proof. reflexivity. Qed.

Instance filter_ok {elt} f (m:t elt) : Ok m -> Ok (filter f m).
Proof.
 induction 1; simpl.
 - constructor.
 - destruct x as (k,e).
   destruct (f k e); trivial. constructor; trivial.
   contradict H. rewrite InA_alt in *. destruct H as (y,(Hy,H)).
   exists y; split; trivial. unfold filter in *.
   now rewrite filter_In in H.
Qed.

Lemma partition_spec {elt} (f:key->elt->bool) m `{!Ok m} :
 prodmap (@bindings _) (partition f m) =
  List.partition (fun '(k,e) => f k e) (bindings m).
Proof. unfold bindings, partition. now destruct List.partition. Qed.

Lemma partition_fst {elt} f (m:t elt) : fst (partition f m) = filter f m.
Proof.
 induction m; simpl; auto.
 rewrite <- IHm. now destruct (partition f m), a, f.
Qed.

Lemma partition_snd {elt} f (m:t elt) :
  snd (partition f m) = filter (fun k e => negb (f k e)) m.
Proof.
 induction m; simpl; auto.
 rewrite <- IHm. now destruct (partition f m), a, f.
Qed.

Instance partition_ok1 {elt} f (m:t elt) : Ok m -> Ok (fst (partition f m)).
Proof.
 rewrite partition_fst; eauto with *.
Qed.

Instance partition_ok2 {elt} f (m:t elt) : Ok m -> Ok (snd (partition f m)).
Proof.
 rewrite partition_snd; eauto with *.
Qed.

Lemma for_all_spec {elt}(f:key->elt->bool) m :
 for_all f m = List.forallb (fun '(k,e) => f k e) (bindings m).
Proof. reflexivity. Qed.

Lemma exists_spec {elt}(f:key->elt->bool) m :
 exists_ f m = List.existsb (fun '(k,e) => f k e) (bindings m).
Proof. reflexivity. Qed.

End MakeRaw.

Module Make (K:DecidableType) <: Interface.WS K.
 Module Raw := MakeRaw K.
 Include Raw.WPack K Raw.
End Make.

author: xavierleroy

repo: canonical-binary-tries


text:
Require Import Eqdep Lia Framework FSParameters FileDiskLayer. (* LoggedDiskLayer TransactionCacheLayer TransactionalDiskLayer. *)
Require Import FileDiskNoninterference FileDiskRefinement.
Require Import ATCDLayer FileDisk.TransferProofs ATCD_Simulation ATCD_AOE.
Require Import Not_Init HSS ATCD_ORS ATCD_TS_Common ATCD_TS_Allocator ATCD_TS_Recovery.

Import FileDiskLayer.
Set Nested Proofs Allowed.

Opaque File.recover.
Lemma ATCD_TS_InodeAllocator_read:
forall n inum u u' txns1 txns2 hdr1 hdr2,
Termination_Sensitive u
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
 (@lift_L2 AuthenticationOperation _ TD _
    (Inode.InodeAllocator.read inum))))
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
 (@lift_L2 AuthenticationOperation _ TD _
    (Inode.InodeAllocator.read inum))))
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
 (Simulation.Definitions.compile
    FD.refinement
    (| Recover |))))
(refines_valid ATCD_Refinement
(refines_valid ATC_Refinement
 AD_valid_state))
 (fun s1 s2 =>
 refines_related ATCD_Refinement
 (fun s1 s2 => refines_related ATC_Refinement
  (fun s1 s2  => exists s1a s2a,
     File.files_inner_rep s1a (fst (snd (snd s1))) /\
     File.files_inner_rep s2a (fst (snd (snd s2))) /\
     FD_related_states u' None s1a s2a) s1 s2 /\
 (forall a,
  Transaction.get_first (fst (snd s1)) a = None <->
  Transaction.get_first (fst (snd s2)) a = None)) s1 s2 /\
  equivalent_for_recovery txns1 txns2 Log.Current_Part hdr1 hdr2 s1 s2 /\
  (forall a,
  fst (snd (snd s1)) a = None <->
  fst (snd (snd s2)) a = None) /\
  fst (snd (snd s1)) =
  Mem.list_upd_batch empty_mem (map Log.addr_list txns1)
    (map Log.data_blocks txns1) /\
  fst (snd (snd s2)) =
  Mem.list_upd_batch empty_mem (map Log.addr_list txns2)
    (map Log.data_blocks txns2))
(ATCD_reboot_list n).
Proof.
Transparent Inode.InodeAllocator.read.
unfold Inode.InodeAllocator.read; simpl; intros.
destruct (Compare_dec.lt_dec inum Inode.InodeAllocatorParams.num_of_blocks).
2:{
    simpl.
    eapply TS_eqv_impl.
    apply ATCD_TS_ret.
    simpl; intuition eauto.
}

simpl.
Admitted.

Lemma ATCD_TS_get_inode:
forall n inum u u' txns1 txns2 hdr1 hdr2,
Termination_Sensitive u
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
 (@lift_L2 AuthenticationOperation _ TD _
    (Inode.get_inode inum))))
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
 (@lift_L2 AuthenticationOperation _ TD _
    (Inode.get_inode inum))))
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
 (Simulation.Definitions.compile
    FD.refinement
    (| Recover |))))
(refines_valid ATCD_Refinement
(refines_valid ATC_Refinement
 AD_valid_state))
 (fun s1 s2 =>
 refines_related ATCD_Refinement
 (fun s1 s2 => refines_related ATC_Refinement
  (fun s1 s2  => exists s1a s2a,
     File.files_inner_rep s1a (fst (snd (snd s1))) /\
     File.files_inner_rep s2a (fst (snd (snd s2))) /\
     FD_related_states u' None s1a s2a) s1 s2 /\
 (forall a,
  Transaction.get_first (fst (snd s1)) a = None <->
  Transaction.get_first (fst (snd s2)) a = None)) s1 s2 /\
  equivalent_for_recovery txns1 txns2 Log.Current_Part hdr1 hdr2 s1 s2 /\
  (forall a,
  fst (snd (snd s1)) a = None <->
  fst (snd (snd s2)) a = None) /\
  fst (snd (snd s1)) =
  Mem.list_upd_batch empty_mem (map Log.addr_list txns1)
    (map Log.data_blocks txns1) /\
  fst (snd (snd s2)) =
  Mem.list_upd_batch empty_mem (map Log.addr_list txns2)
    (map Log.data_blocks txns2))
(ATCD_reboot_list n).
Proof.
Transparent Inode.get_inode.
simpl; intros.
eapply ATCD_TS_compositional.
intros; apply ATCD_TS_InodeAllocator_read.
intros; destruct r1, r2; eapply TS_eqv_impl;
try apply ATCD_TS_ret.
instantiate (5:= fun _ _ => _); simpl; eauto.
all: simpl; eauto.
intros; intuition eauto.
Opaque Inode.get_inode.
Admitted.

Lemma ATCD_TS_get_owner:
forall n inum u u' txns1 txns2 hdr1 hdr2,
Termination_Sensitive u
(Simulation.Definitions.compile
 ATCD_Refinement
(Simulation.Definitions.compile
 ATC_Refinement
(@lift_L2 AuthenticationOperation _ TD _
    (Inode.get_owner inum))))
    (Simulation.Definitions.compile
 ATCD_Refinement
(Simulation.Definitions.compile
 ATC_Refinement
(@lift_L2 AuthenticationOperation _ TD _
    (Inode.get_owner inum))))
    (Simulation.Definitions.compile
    ATCD_Refinement
(Simulation.Definitions.compile
 ATC_Refinement
 (Simulation.Definitions.compile
    FD.refinement
    (| Recover |))))
    (refines_valid ATCD_Refinement
(refines_valid ATC_Refinement
 AD_valid_state))
 (fun s1 s2 =>
 refines_related ATCD_Refinement
 (fun s1 s2 => refines_related ATC_Refinement
  (fun s1 s2  => exists s1a s2a,
     File.files_inner_rep s1a (fst (snd (snd s1))) /\
     File.files_inner_rep s2a (fst (snd (snd s2))) /\
     FD_related_states u' None s1a s2a) s1 s2 /\
 (forall a,
  Transaction.get_first (fst (snd s1)) a = None <->
  Transaction.get_first (fst (snd s2)) a = None)) s1 s2 /\
  equivalent_for_recovery txns1 txns2 Log.Current_Part hdr1 hdr2 s1 s2 /\
  (forall a,
  fst (snd (snd s1)) a = None <->
  fst (snd (snd s2)) a = None))
(ATCD_reboot_list n).
Proof.
Transparent Inode.get_owner.
simpl; intros.
eapply ATCD_TS_compositional.
intros; eapply TS_eqv_impl.
apply ATCD_TS_get_inode.
shelve.
intros; destruct r1, r2;
intros; eapply TS_eqv_impl;
try apply ATCD_TS_ret.
instantiate (5:= fun _ _ => equivalent_for_recovery txns1 txns2 Log.Current_Part hdr1 hdr2); simpl; eauto.
all: simpl; eauto.
intuition eauto.
Opaque Inode.get_owner.
Admitted.

Lemma ATCD_TS_get_block_number:
forall n inum u u' off txns1 txns2 hdr1 hdr2,
Termination_Sensitive u
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
(@lift_L2 AuthenticationOperation _ TD _
    (Inode.get_block_number inum off))))
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
(@lift_L2 AuthenticationOperation _ TD _
    (Inode.get_block_number inum off))))
(Simulation.Definitions.compile
 ATCD_Refinement
 (Simulation.Definitions.compile
 ATC_Refinement
 (Simulation.Definitions.compile
    FD.refinement
    (| Recover |))))
    (refines_valid ATCD_Refinement
(refines_valid ATC_Refinement
 AD_valid_state))
 (fun s1 s2 =>
 refines_related ATCD_Refinement
 (fun s1 s2 => refines_related ATC_Refinement
  (fun s1 s2  => exists s1a s2a,
     File.files_inner_rep s1a (fst (snd (snd s1))) /\
     File.files_inner_rep s2a (fst (snd (snd s2))) /\
     FD_related_states u' None s1a s2a) s1 s2 /\
 (forall a,
  Transaction.get_first (fst (snd s1)) a = None <->
  Transaction.get_first (fst (snd s2)) a = None)) s1 s2 /\
  equivalent_for_recovery txns1 txns2 Log.Current_Part hdr1 hdr2 s1 s2 /\
  (forall a,
  fst (snd (snd s1)) a = None <->
  fst (snd (snd s2)) a = None))
(ATCD_reboot_list n).
Proof.
Transparent Inode.get_block_number.
simpl; intros.
eapply ATCD_TS_compositional.
intros; eapply TS_eqv_impl; try apply ATCD_TS_get_inode.
shelve.
intros; destruct r1, r2;
eapply TS_eqv_impl; try apply ATCD_TS_ret.
instantiate (5:= fun _ _ => _); simpl; eauto.
all: simpl; eauto.
shelve.
Opaque Inode.get_block_number.
Admitted.

author: Atalay-Ileri

repo: ConFrm

save_path: github-repos/coq/Atalay-Ileri-ConFrm


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable wd_ : Universe -> Universe -> Prop.
Variable col_ : Universe -> Universe -> Universe -> Prop.

Variable col_swap1_1 : (forall A B C : Universe, (col_ A B C -> col_ B A C)).
Variable col_swap2_2 : (forall A B C : Universe, (col_ A B C -> col_ B C A)).
Variable col_triv_3 : (forall A B : Universe, col_ A B B).
Variable wd_swap_4 : (forall A B : Universe, (wd_ A B -> wd_ B A)).
Variable col_trans_5 : (forall P Q A B C : Universe, ((wd_ P Q /\ (col_ P Q A /\ (col_ P Q B /\ col_ P Q C))) -> col_ A B C)).

Theorem pipo_6 : (forall A B C G Aprime Aprimeprime Bprime Cprime Bprimeprime Bprimeprimeprime : Universe, ((wd_ Aprime Bprimeprime /\ (wd_ A B /\ (wd_ B C /\ (wd_ A C /\ (wd_ Bprime A /\ (wd_ Bprime C /\ (wd_ Aprime B /\ (wd_ Aprime C /\ (wd_ Cprime A /\ (wd_ Cprime B /\ (wd_ Aprimeprime Bprimeprime /\ (wd_ Aprime Bprimeprimeprime /\ (wd_ Aprime Bprime /\ (wd_ Bprime Bprimeprimeprime /\ (wd_ G Aprime /\ (wd_ G Aprimeprime /\ (wd_ G Bprimeprime /\ (wd_ Bprimeprime Bprimeprimeprime /\ (wd_ G Bprimeprimeprime /\ (wd_ Aprime Aprimeprime /\ (wd_ B G /\ (wd_ Bprimeprime B /\ (wd_ A G /\ (wd_ Aprimeprime A /\ (col_ Aprime Bprime Bprimeprimeprime /\ (col_ G Bprimeprime Bprimeprimeprime /\ (col_ Bprimeprime B G /\ (col_ Cprime A B /\ (col_ Bprime A C /\ (col_ G Aprime Aprimeprime /\ (col_ Aprimeprime A G /\ (col_ Aprime B C /\ col_ G Aprime Bprimeprime)))))))))))))))))))))))))))))))) -> col_ A B G)).
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus


text:
Require Export Bigop.

Definition nprod {L T : finType} {I : {set L}} {X : {set {set T}}} (g : I ⟶ X) :=
    [set f : I ⟶ ⊔ X | [forall i , (i ∈ I) ==> image f i ⊂ ⊔ image g i]].

Axiom choicep : forall {L T : finType} {I : {set L}} {X : {set {set T}}} (g : I ⟶ X),
    (forall i, i ∈ I -> image g i <> [set ∅]) -> nprod g <> ∅.

Theorem choice {T : finType} (X : {set {set T}}) :
   X <> ∅ -> ~ ∅ ∈ X -> (exists f : X ⟶ ⊔ X, forall x, x ∈ X -> image f x ⊂ x).
Proof.
    move /eqP /set0Pn => [x hx] H0.
    suff : exists f, f ∈ nprod (id X).
        move => [f].
        rewrite in_set => Hf.
        exists f.
        move => y Hy.
        move /forallP /(_ y) /implyP /(_ Hy) /subsetP in Hf.
        apply /subsetP => i.
        move /Hf /bigcupP => [y_ Hy_ iy]; move : Hy_.
        move /imageP => /=.
        rewrite in_set.
        move /andP => /= [_ /eqP] -> //.
    apply /set0Pn /eqP.
    apply  choicep.
    move => i Hi F.
    apply H0.
    suff : i = ∅.
        move <- => //.
    apply /set1P.
    rewrite -F.
    apply /imageP => /=.
    rewrite in_set.
    apply /andP; split => //.
    apply /setXP => //.
Qed.

Theorem surj_invr {T T' : finType} {A : {set T}} {B : {set T'}} (f : A ⟶ B) :
    surj f <-> exists g : B ⟶ A, f ○ g = id B.
Proof.
    split; rewrite /surj => /=.
    +   move => H.
        pose AA :=
            [set A : {set T} | [exists b, (b ∈ B) && (A == image (inv f) b)]].
        induction f as [Γ Hm_] => /=.
        induction Γ as [G Hf_] => /=.
        move : (map_mixin_elim Hm_) => Hm.
        move : (func_mixin_elim Hf_) => Hf.
        pose f := mkMap (mkFunc G Hf_) Hm_.
        simpl in AA.
        pose G' :=
            [set u in setX B AA | u.2 == image (inv (mkFunc G Hf_)) u.1].
        have fHG'_ : func_mixinb B AA G'.
            apply /forallP => u.
            apply /implyP; rewrite in_set.
            destruct u as [a b] => /=.
            move /andP => [HG _].
            move /setXP /andP : HG => //.
        pose fG' := mkFunc G' fHG'_.
        have mHG'_ : map_mixinb B AA fG'.
            apply /forallP => b.
            apply /implyP => Hb.
            apply /existsP.
            exists (image (inv (mkFunc G Hf_)) b).
            apply /andP; split.
            +   apply /eqP; apply extension; apply /subsetP => a.
                -   move /imageP; rewrite in_set => /=.
                    move /andP => [_ /eqP] ->; apply /set1P => //.
                -   move /set1P ->; apply /imageP; rewrite in_set => /=.
                    apply /andP; split => //.
                    apply /setXP; split => //.
                    rewrite in_set; apply /existsP; exists b.
                    apply /andP => //.
            +   apply /forallP => A_.
                apply /implyP; move /eqP => HA_.
                have : A_ ∈ image fG' b.
                    rewrite HA_; apply /set1P => //.
                move /imageP; rewrite in_set => /=.
                move /andP => [_].
                move /eqP => H0.
                apply /eqP; symmetry => //.

        pose g' := mkMap fG' mHG'_.
        move : (map_mixin_elim mHG'_ ) => mHG'.
        move : (func_mixin_elim fHG'_) => fHG'.
        have : nprod g' <> ∅.
            apply choicep => b Hb F.
            have : ∅ ∈ image g' b.
                rewrite F; apply /set1P => //.
            move /imageP => /=.
            rewrite in_set => /=; move /andP => [_ /eqP H1].
            rewrite -H in Hb.
            move /rangeP : Hb => [a].
            move /imageP.
            rewrite -in_inv => /=.
            rewrite -H1 in_set0 => //.
        move /eqP /set0Pn => [g Hg ].
        pose ids := [set u in setX (⊔ AA) A | u.1 == u.2 ].
        have  idfH : func_mixinb (⊔ AA) A ids.
            apply /forallP => u.
            induction u as [x y].
            apply /implyP; rewrite in_set.
            move /andP => /= [/setXP /andP Hxy _] //.
        pose idf := mkFunc ids idfH.
        have idmH : map_mixinb (⊔ AA) A idf.
            apply /forallP => a.
            apply /implyP.
            move /bigcupP => [A_ HA_ Ha].
            rewrite in_set in HA_.
            move /existsP : HA_ => [b /andP [Hb /eqP HA_]].
            rewrite HA_ in_inv in Ha.
            move /imageP : Ha => /= Hab.
            move : (Hf _ Hab) => /= [aA bB].
            apply /existsP; exists a.
            apply /andP; split.
            +   apply /eqP; apply extension; apply /subsetP => a_.
                -   move /imageP.
                    rewrite in_set => /=.
                    move /andP => [_ /eqP ->].
                    apply /set1P => //.
                -   move /set1P ->.
                    apply /imageP; rewrite in_set => //.
                    apply /andP; split => //.
                    apply /setXP; split => //.
                    apply /bigcupP.
                    exists (image (inv (mkFunc G Hf_)) b).
                    *   rewrite in_set.
                        apply /existsP; exists b; apply /andP => //.
                        rewrite in_inv; apply /imageP => //=.
            +   apply /forallP => a'.
                apply /implyP.
                move /eqP => Ha.
                suff : a' ∈ image idf a.
                    move /imageP; rewrite in_set.
                    move /andP => /= [_] //.
                rewrite Ha; apply /set1P => //.
        pose idm := mkMap idf idmH.
        exists (idm ○ g).
        rewrite in_set in Hg.
        move /forallP : Hg => Hg.
        apply map_extension => /=.
        apply extension; apply /subsetP => u; induction u as [b b']; rewrite !in_set => /=.
        -   move /existsP => [a /andP [Hba Hab']].
            rewrite in_set in Hba.
            move /existsP : Hba => /= [a' /andP [Hba' Haa]].
            rewrite in_set in Haa.
            move /andP : Haa => /= [_ /eqP aa]; subst a'.
            induction g as [h Hhm_ ].
            induction h as [F HFf_].
            move : (map_mixin_elim Hhm_) => Hhm.
            move : (func_mixin_elim HFf_) => HFf.
            simpl in Hba'.
            move : (HFf _ Hba') => /= [Hb _].
            move : (Hf _ Hab') => /= [_ Hb'].
            apply /andP; split => //.
            apply /andP; split => //.
            move : Hg; move /(_ b).
            move /implyP /(_ Hb) /subsetP => /= Hg.
            have : a ∈ image (mkFunc F HFf_) b.
                apply /imageP => //=.
            move /Hg /bigcupP => [A_ HA_].
            move /imageP : HA_ => /=.
            rewrite in_set; move /andP => /= [_ /eqP] ->.
            rewrite in_inv; move /imageP => /= Hab.
            apply /eqP.
            apply (map_theorem f a b b'); apply /imageP => //=.
        -   move /andP => [/andP [Hb _] /eqP bb]; subst b'.
            move : Hg; move /(_ b) /implyP /(_ Hb) /subsetP => Hg.
            induction g => /=.
            move : (map_mixin_elim axiom).
            move /(_ b Hb) => [a [gba unia]].
            have gb : a ∈ image sort b.
                rewrite gba; apply /set1P => //.
            move : (Hg _ gb ); move /bigcupP => [A_].
            move /imageP.
            rewrite in_set => /= /andP [_ /eqP] ->.
            rewrite in_inv; move /imageP => /= Hab.
            apply /existsP; exists a; apply /andP; split => //.
            rewrite in_set => /=.
            apply /existsP; exists a; apply /andP; split.
            *   apply /imageP => //.
            *   rewrite in_set => /=; apply /andP; split => //.
                move : (Hf _ Hab) => /= [Ha _].
                apply /setXP; split => //.
                apply /bigcupP.
                exists (image (inv f) b).
                +   rewrite in_set.
                    apply /existsP; exists b; apply /andP; split => //.
                +   rewrite in_inv; apply /imageP => //=.
    +   move => [g Hg].
        apply extension; apply /subsetP => b.
        move /rangeP => [a Hab].
        induction f as [F Hfm_].
        induction F as [Γ Hff_].
        move : (func_mixin_elim Hff_).
        move /(_ _ Hab) => /= [_] //.
    +   move => Hb.
        have : (b, b) ∈ id B.
            rewrite in_set; apply /andP; split => //.
            apply /setXP; split => //.
        rewrite -Hg.
        rewrite in_set => /=.
        move /existsP => [a /andP [_ Hab]].
        apply /rangeP; exists a => //.
Qed.

Theorem range_sub {T T' : finType} {A : {set T}} {B : {set T'}} (f : A ⟶ B) :
    range f ⊂ B.
Proof.
    apply /subsetP => b.
    move /rangeP => [a Hab].
    induction f.
    induction sort.
    move : (func_mixin_elim axiom0) => Hm.
    move : (Hm _ Hab) => [_] //.
Qed.

(* Theorem not_range0 {T T' : finType} {A : {set T}} {B : {set T'}} (f : A ⟶ B) :
    B <> ∅.
Proof.
    move => F.
    induction f.
    move : (map_mixin_elim axiom) => Hm.
    move : Hm.
    apply ex_not_not_all.
Search "not" "all".
    induction sort. *)

Theorem func00_mixin {T T' : finType} :
    func_mixinb (∅ : {set T}) (∅ : {set T'}) (∅ : {set T * T'}).
Proof.
    apply /forallP => a.
    apply /implyP.
    rewrite (in_set0 a) => //.
Qed.

Definition func00 {T T' : finType} := mkFunc (∅ : {set T * T'}) func00_mixin.

Theorem map00_mixin {T T' : finType}:
    map_mixinb (∅ : {set T}) (∅ : {set T'}) func00.
Proof.
    apply /forallP => a.
    apply /implyP.
    rewrite (in_set0 a) => //.
Qed.

Definition map00 {T T' : finType}:= mkMap func00 (@map00_mixin T T').

Theorem inj_invl {T T' : finType} {A : {set T}} {B : {set T'}} (f : A ⟶ B) :
    A <> ∅ -> inj f <-> exists g : B ⟶ A, g ○ f = id A.
Proof.
    induction f as [Gf Hfm_].
    induction Gf as [F Hff_].
    move : (func_mixin_elim Hff_) => Hff.
    move : (map_mixin_elim Hfm_) => Hfm.
    move => H0.
    split; rewrite /inj; first last.
    +   move => [g Hg] a a' Ha Ha' H.
        induction g as [Gg Hgm_].
        induction Gg as [G Hgf_].
        move : (func_mixin_elim Hgf_) => Hgf.
        move : (map_mixin_elim Hgm_) => Hgm.
        simpl.

        have : (a,a) ∈ id A.
            rewrite in_set; apply /andP; split => //.
            apply /setXP => //.
        rewrite -Hg in_set => /=.
        move /existsP => [b /andP [abF baG]].

        have : (a',a') ∈ id A.
            rewrite in_set; apply /andP; split => //.
            apply /setXP => //.
        rewrite -Hg in_set => /=.
        move /existsP => [b' /andP [abF' baG']].

        move : (Hfm _ Ha) => [b0 [Hb0 unib0]].
        move : (Hfm _ Ha') => [b0' [Hb0' unib0']].
        rewrite H in Hb0.
        rewrite Hb0' in Hb0.
        have bb : b0 = b0'.
            apply /set1P; rewrite Hb0; apply /set1P => //.
        subst b0'; clear Hb0.

        have bb : b = b0.
            apply /set1P; rewrite -Hb0'; rewrite -H; apply /imageP => //.
        subst b0.
        have bb : b' = b.
            apply /set1P; rewrite -Hb0'; apply /imageP => //.
        subst b'.

        apply (map_theorem (mkMap (mkFunc G Hgf_) Hgm_) b a a');
        apply /imageP => //.

    +   move => /= H.
        pose f := mkMap (mkFunc F Hff_) Hfm_.
        move /eqP /set0Pn : H0 => [a0 Ha0].
        pose G := inv_set f ∪ [set u | (u.1 ∈ B // range f)  && (u.2 == a0)] .
        have Hgf : func_mixinb B A G.
            apply /forallP => u; induction u as [b a].
            apply /implyP.
            case /setUP.
            -   move /inv_setP => /=.
                move /Hff => /= [Ha Hb].
                apply /andP => //.
            -   rewrite in_set => /=.
                move /andP; case.
                move /setDP => [Hb _].
                move /eqP ->.
                apply /andP => //.
        pose G_ := mkFunc G Hgf.
        have Hgm : map_mixinb B A G_.
            apply /forallP => b.
            apply /implyP => Hb.
            remember  (b ∈ range f).
            symmetry in Heqb0.
            destruct b0.
            -   move /rangeP : Heqb0 => [a Hab].
                apply /existsP; exists a.
                apply /andP; split.
                *   apply /eqP; setE a_.
                    +   move /imageP /setUP; case.
                        -   move /inv_setP => /= Hab_.
                            move : (Hff _ Hab) => /= [Ha _].
                            move : (Hff _ Hab_) => /= [Ha_ _].
                            move : (Hfm _ Ha) => [b0 [Hb0 _]].
                            have bb : b = b0.
                                apply /set1P; rewrite -Hb0; apply /imageP => //.
                            subst b0.
                            move : (Hfm _ Ha_) => [b0 [Hb0_ _]].
                            have bb : b = b0.
                                apply /set1P; rewrite -Hb0_; apply /imageP => //.
                            subst b0.
                            apply /set1P /H => //.
                            rewrite Hb0 Hb0_ => //.
                        -   rewrite in_set.
                            move /andP; case; move /setDP; case => /= _.
                            move /negP => Fb.
                            contradiction Fb.
                            apply /rangeP; exists a => //.
                    +   move /set1P ->.
                        apply /imageP; rewrite in_set => /=.
                        apply /orP; left.
                        apply /inv_setP => //=.
                *   move : (Hff _ Hab) => /= [Ha _].
                    apply /forallP => a_.
                    apply /implyP; move /eqP => HG.
                    have : a_ ∈ image G_ b.
                        rewrite HG; apply /set1P => //.
                    move /imageP; rewrite in_set.
                    move /orP; case.
                    -   move /inv_setP => /= Hab_.
                        move : (Hff _ Hab_ )  => /= [Ha_ _].
                        move : (Hfm _ Ha) => [b0 [Hb0 _]].
                            have bb : b = b0.
                                apply /set1P; rewrite -Hb0; apply /imageP => //.
                            subst b0.
                            move : (Hfm _ Ha_) => [b0 [Hb0_ _]].
                            have bb : b = b0.
                                apply /set1P; rewrite -Hb0_; apply /imageP => //.
                            subst b0.
                        apply /eqP /H => //.
                        rewrite Hb0 Hb0_ => //.
                    -   rewrite in_set => /=.
                        move /andP; case.
                        move /setDP => [_ ].
                        move /negP => Fb.
                        contradiction Fb.
                        apply /rangeP; exists a => //.
            -   apply /existsP; exists a0.
                have Fb : ~ b ∈ range f.
                    rewrite Heqb0 => //.
                apply /andP; split.
                +   apply /eqP; setE a_.
                    -   move /imageP; rewrite in_set => //.
                        move /orP; case.
                        *   move /inv_setP => /= Hab_.
                            contradiction Fb.
                            apply /rangeP; exists a_ => //.
                        *   rewrite in_set => /=.
                            move /andP; case => _.
                            move /eqP ->.
                            apply /set1P => //.
                    -   move /set1P ->.
                        apply /imageP.
                        rewrite in_set => /=.
                        apply /orP; right.
                        rewrite in_set => /=.
                        apply /andP; split => //.
                        *   apply /setDP; split => //.
                            rewrite Heqb0 => //.
                +   apply /forallP => a.
                    apply /implyP  => /eqP HG.
                    have : a ∈ image G_ b.
                        rewrite HG; apply /set1P => //.
                    move /imageP; rewrite in_set => //.
                    move /orP; case.
                    move /inv_setP => /= Hab.
                    contradiction Fb.
                    apply /rangeP; exists a => //.
                    rewrite in_set; move /andP => [_] /=.
                    move /eqP <- => //.
        pose g := mkMap G_ Hgm.

        exists g.
        apply map_extension.
        rename Hgf into Hgf_.
        rename Hgm into Hgm_.
        move : (func_mixin_elim Hgf_) => Hgf.
        move : (map_mixin_elim Hgm_) => Hgm.
        setE u; induction u as [ad ar].
        +   move /comp_setP => /= [b] [HF HG].
            move : (Hff _ HF) => /= [Had Hb].
            move : (Hgf _ HG) => /= [_ Har].
            apply /id_setP; split => /=.
            -   apply /setXP => //.
            -   move : HG.
                rewrite in_set => /=.
                move /orP; case.
                *   move /inv_setP => /= HF'.
                    apply H => //.
                    move : (Hfm _ Had) => [b0 [Hb0 _]].
                    have bb : b = b0.
                        apply /set1P; rewrite -Hb0; apply /imageP => //.
                    subst b0.
                    move : (Hfm _ Har) => [b0 [Hb0_ _]].
                    have bb : b = b0.
                        apply /set1P; rewrite -Hb0_; apply /imageP => //.
                    subst b0.
                    rewrite Hb0 Hb0_ => //.
                *   rewrite in_set => /=.
                    move /andP => [Hb_ _].
                    move /setDP : Hb_ => [_ ].
                    move /negP => Fb.
                    contradiction Fb.
                    apply /rangeP; exists ad => //.
        +   move /id_setP => /= [Ha aa].
            subst ar; rename ad into a.
            move /setXP : Ha => [Ha _].
            apply /comp_setP => /=.
            move : (Hfm _ Ha) => [b [Hb unib]].
            have Hab : (a,b) ∈ F.
                suff : b ∈ image (mkFunc F Hff_) a.
                    move /imageP => //.
                rewrite Hb; apply /set1P => //.
            exists b; split => //.
            rewrite in_set => /=.
            apply /orP; left.
            apply /inv_setP => //.
Qed.

author: gaxiiiiiiiiiiii

repo: SetTheory


text:
Require Import HoTT.

From GCTT Require Import
     conn_ptype finite_types monoids_and_groups delooping permutations sign fintype_monoidal.

(** Here we define the function [Bsign : FinType m -> FinType 2] induces by the homomorphism [sign : Hom (SymGrp m) (SymGrp 2)]  *)

Definition iso_path_finite_types (m : nat)
  : Isomorphism (SymGrp m) (loopGroup (Finite_Types m) (canon m)).
Proof.
  srapply Build_Grp_Iso'.
  - simpl. apply (equiv_path_finite_types m (canon m) (canon m)).
  - intros alpha beta. simpl.
    apply (path_finite_types_compose m (canon m) (canon m) (canon m) alpha beta).
Defined.

Definition equiv_functor_hom_fin (m n : nat)
  : Homomorphism (SymGrp m) (SymGrp n) <~> Homomorphism (loopGroup (pFin m) (canon m))
                                                        (loopGroup (pFin n) (canon n)).
Proof.
  apply equiv_functor_hom'; apply iso_path_finite_types.
Defined.

Definition deloop_fin (m n : nat)
  : Homomorphism (SymGrp m) (SymGrp n) -> pMap(pFin m) (pFin n).
Proof.
  intro f. apply (functor_deloop (pFin m) (pFin n)).
  apply (equiv_functor_hom_fin m n). exact f.
Defined.

Definition deloop_fin_canon (m n : nat) (f : Homomorphism (SymGrp m) (SymGrp n))
  : deloop_fin m n f (canon m) = canon n.
Proof.
  apply (point_eq (deloop_fin m n f)).
Defined.

Definition deloop_fin_loop (m n : nat) (f : Homomorphism (SymGrp m) (SymGrp n))
           (ω : canon m = canon m)
  : loops_functor (deloop_fin m n f) ω
    = (functor_hom
         (iso_inv (iso_path_finite_types m))
         (iso_path_finite_types n) f) ω.
Proof.
  apply functor_deloop_loop.
Defined.

Definition sgnhom (m : nat) : Homomorphism (SymGrp m) (SymGrp 2).
Proof.
  srapply @Build_GrpHom.
  + apply sign.
  + apply sgn_compose.
Defined.

Definition Bsign (m : nat) :=
  deloop_fin m 2 (sgnhom m).

Definition Bsign_uncurry : FinType -> Finite_Types 2.
Proof.
  intros [a A]. exact (Bsign a A).
Defined.

author: kalfsvag


text:
(** Adequacy of the bridge semantics w.r.t. standard semantics for
well-typed programs.
*)

(*
Author: Aslan Askarov
Created: 2016-07-27

- Note: that well-typedness is required may potentially be relaxed,
  but we leave that for future investigation.
 *)

Require Import Bool Arith List CpdtTactics SfLib LibTactics.
Require Import Coq.Program.Equality.
Require Import Omega.

Set Implicit Arguments.

Require Import Identifier Environment Imperative Types Augmented Bridge.
Require Import WellFormedness.
Require Import InductionPrinciple.
Require Import UtilTactics.
Require Import BridgeTactics.
Require Import BridgeProperties.

(** We start with a simple lemma stipulating that the augemented semantics is adequate *)
Lemma adequacy_of_event_steps:
  forall Γ pc c m cfg',
    wf_mem m Γ ->
    -{ Γ, pc ⊢ c }- ->
    〈c, m 〉 ⇒ cfg' ->
    exists ev, event_step Γ ev 〈c, m 〉 cfg'.
Proof.
  intros Γ pc c m [c' m']; intros.
  cmd_cases (dependent induction c) Case.
  Case "STOP".
  { invert_step. }
  Case "SKIP".
  { exists EmptyEvent.
    assert (c' = STOP /\ m' = m).
    {
      inverts H1.
      splits~.
    }
    super_destruct. subst.
    constructor; auto.
  }
  Case "::=".
  {
    inverts keep H1.
    inverts H0.
    exists (AssignmentEvent ℓ' i v).
    constructor~.
  }
  Case ";;".
  { assert (-{ Γ, pc ⊢ c1 }-) by
        (match goal with [ H:  -{ Γ, pc ⊢ c1;; c2 }- |- _ ] => inverts keep H end; auto).
    inverts H1;
      repeat match goal
           with
             | [ H:  〈 c1, m 〉 ⇒ 〈 ?c1', m' 〉|- _  ] =>
                  (specializes IHc1 m c1' m' H;
                   destruct IHc1 as [ev];
                   (exists ev);
                   constructor~ )
             |  [ H:  -{ Γ, pc ⊢ c1;; c' }- |- _ ] =>
                ( inverts H;
                  applys* wt_programs_are_not_stop
                )
           end.
  }
  Case "IFB".
  {
    exists EmptyEvent.
    assert (c' = c1 \/ c' = c2) as H_cmd
        by (inverts keep H1; tauto).
    match goal with
      | [ H:  -{ Γ, pc ⊢ IFB e THEN c1 ELSE c2 FI }- |- _ ]
        => inverts keep H
    end.
    assert (  -{ Γ, pc ⊢ c' }- )
      by ( destruct H_cmd; subst; applys* pc_lowering).

    assert ( m = m') by (inverts* H1); subst.
    constructor~ .
    applys* wt_programs_are_not_stop.
  }
  Case "WHILE".
  {
    exists EmptyEvent.
    inverts keep H1.
    constructor~ .
  }
Qed.

(* TODO: 2016-07-28: simplify the above lemma *)

Theorem bridge_adequacy:
  forall Γ (n:nat) c m m_end ,
    〈c, m 〉 ⇒/+ n +/ 〈STOP, m_end 〉 ->
    forall pc, -{ Γ, pc ⊢ c }-  ->
    wf_mem m Γ  ->
    (c = STOP \/
     exists ev n' cfg' k,
       〈 c, m 〉 ⇨+/(SL, Γ, ev, n') cfg' /\
       cfg' ⇒/+ k +/ 〈STOP, m_end 〉 /\ k < n).

Proof.
  intros Γ n.

  dependent induction n.
  (* n = 0 *)
  {
    left~.
    inverts H. auto.
  }

  (* inductive case *)
  {
    right; subst.
    inversion H.

    match goal with  [ H : 〈 c, m 〉 ⇒ ?y |- _ ] => destruct y as [c' m'] end; subst.
    match goal with [ H:  〈 c', m' 〉 ⇒/+ n +/ 〈 STOP, m_end 〉 |- _ ] => rename H into H_n end.
    match goal with [ H:  〈 c, m 〉 ⇒ 〈c', m' 〉 |- _ ] => rename H into H_step end.

    specialize (IHn c' m' m_end H_n pc).

    lets* (ev & H_ev) : adequacy_of_event_steps H_step.

    (* We define two auxiliary local propositions that consider the
       cases of a high and a low event respectively; these are then
       used in the case analysis afterwards *)

    assert ( low_event Γ Low ev ->
              exists ev0 n' cfg' k,
                〈 c, m 〉 ⇨+/(SL, Γ, ev0, n') cfg' /\ cfg' ⇒/+ k +/ 〈 STOP, m_end 〉/\ k < S n) as LemmaLowEvent.
    {
      intros H_low.
      inversion H_low.
      assert (ℓ' = Low) by
        ( destruct ℓ'; auto; try impossible_flows; subst ); subst.
      (exists   (AssignmentEvent Low x u) 0).
      forwards* (H_wf' & H_wt' ): preservation.
      compare c' STOP; intros;subst.
      * clear IHn.
        lets : multi_idx_stop_trivial H_n; subst.
        (exists*〈STOP, m_end 〉0).
        splits~ ; try omega.
        applys~ bridge_low_num.

      * specializes~ H_wt' __ .
        specializes~ H_n.
        exists 〈c', m' 〉.
        exists n.
        splits~ .
        applys* bridge_low_num.
    }

    assert ( high_event Γ Low ev ->
              exists ev0 n' cfg' k,
                〈 c, m 〉 ⇨+/(SL, Γ, ev0, n') cfg' /\ cfg' ⇒/+ k +/ 〈 STOP, m_end 〉/\ k < S n) as LemmaHighEvent.
    { clear LemmaLowEvent.
      intros H_high.
      compare c' STOP; intros; subst.
      - (exists ev 0 〈STOP, m' 〉 0).
        lets : multi_idx_stop_trivial H_n; subst.
        splits~ ; try omega.
        applys*  bridge_stop_num.

      - forwards*   (H_wf' & H_wt') : preservation.
        specializes~ H_wt'.
        specializes~ IHn.
        destruct* IHn as [? | ?IHH_multi].

        lets (?ev' & ?n' &  ?cfg' & k & ?H_bridge & ?H_tail & ?H_k ): IHH_multi.
        exists ev' (S n') cfg' k.
        splits~ ; try omega.
        applys* bridge_trans_num.
    }

    (* now we are ready to do the case analysis of the event, using the above assertions *)
    destruct ev.
    - (* Empty Event *)
      apply* LemmaHighEvent.
    - (* Assignment Event *)
      destruct l.
      + (* l is Low *)
        apply* LemmaLowEvent.
      + (* l is High *)
        applys* LemmaHighEvent.
  }
Qed.

author: aslanix

repo: SmallStepNI

save_path: github-repos/coq/aslanix-SmallStepNI


text:
(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Converted imports: *)

Require Coq.Init.Datatypes.
Require Coq.Program.Basics.
Require Data.Foldable.
Require Data.Functor.
Require Data.SemigroupInternal.
Require Data.Traversable.
Require GHC.Base.
Require GHC.Num.
Import Data.Functor.Notations.
Import GHC.Base.Notations.
Import GHC.Num.Notations.

(* Converted type declarations: *)

Inductive OrdList a : Type
  := | None : OrdList a
  |  One : a -> OrdList a
  |  Many : list a -> OrdList a
  |  Cons : a -> (OrdList a) -> OrdList a
  |  Snoc : (OrdList a) -> a -> OrdList a
  |  Two : (OrdList a) -> (OrdList a) -> OrdList a.

Arguments None {_}.

Arguments One {_} _.

Arguments Many {_} _.

Arguments Cons {_} _ _.

Arguments Snoc {_} _ _.

Arguments Two {_} _ _.

(* Converted value declarations: *)

(* Skipping all instances of class `Outputable.Outputable', including
   `OrdList.Outputable__OrdList' *)

Definition appOL {a} : OrdList a -> OrdList a -> OrdList a :=
  fun arg_0__ arg_1__ =>
    match arg_0__, arg_1__ with
    | None, b => b
    | a, None => a
    | One a, b => Cons a b
    | a, One b => Snoc a b
    | a, b => Two a b
    end.

Local Definition Semigroup__OrdList_op_zlzlzgzg__ {inst_a}
   : (OrdList inst_a) -> (OrdList inst_a) -> (OrdList inst_a) :=
  appOL.

Program Instance Semigroup__OrdList {a} : GHC.Base.Semigroup (OrdList a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__OrdList_op_zlzlzgzg__ |}.

Local Definition Monoid__OrdList_mappend {inst_a}
   : (OrdList inst_a) -> (OrdList inst_a) -> (OrdList inst_a) :=
  _GHC.Base.<<>>_.

Definition concatOL {a} : list (OrdList a) -> OrdList a :=
  fun aas => Data.Foldable.foldr appOL None aas.

Local Definition Monoid__OrdList_mconcat {inst_a}
   : list (OrdList inst_a) -> (OrdList inst_a) :=
  concatOL.

Definition nilOL {a} : OrdList a :=
  None.

Local Definition Monoid__OrdList_mempty {inst_a} : (OrdList inst_a) :=
  nilOL.

Program Instance Monoid__OrdList {a} : GHC.Base.Monoid (OrdList a) :=
  fun _ k__ =>
    k__ {| GHC.Base.mappend__ := Monoid__OrdList_mappend ;
           GHC.Base.mconcat__ := Monoid__OrdList_mconcat ;
           GHC.Base.mempty__ := Monoid__OrdList_mempty |}.

Fixpoint mapOL {a} {b} (arg_0__ : (a -> b)) (arg_1__ : OrdList a) : OrdList b
           := match arg_0__, arg_1__ with
              | _, None => None
              | f, One x => One (f x)
              | f, Cons x xs => Cons (f x) (mapOL f xs)
              | f, Snoc xs x => Snoc (mapOL f xs) (f x)
              | f, Two x y => Two (mapOL f x) (mapOL f y)
              | f, Many xs => Many (GHC.Base.map f xs)
              end.

Local Definition Functor__OrdList_fmap
   : forall {a} {b}, (a -> b) -> OrdList a -> OrdList b :=
  fun {a} {b} => mapOL.

Local Definition Functor__OrdList_op_zlzd__
   : forall {a} {b}, a -> OrdList b -> OrdList a :=
  fun {a} {b} => Functor__OrdList_fmap GHC.Base.∘ GHC.Base.const.

Program Instance Functor__OrdList : GHC.Base.Functor OrdList :=
  fun _ k__ =>
    k__ {| GHC.Base.fmap__ := fun {a} {b} => Functor__OrdList_fmap ;
           GHC.Base.op_zlzd____ := fun {a} {b} => Functor__OrdList_op_zlzd__ |}.

Fixpoint foldrOL {a} {b} (arg_0__ : (a -> b -> b)) (arg_1__ : b) (arg_2__
                   : OrdList a) : b
           := match arg_0__, arg_1__, arg_2__ with
              | _, z, None => z
              | k, z, One x => k x z
              | k, z, Cons x xs => k x (foldrOL k z xs)
              | k, z, Snoc xs x => foldrOL k (k x z) xs
              | k, z, Two b1 b2 => foldrOL k (foldrOL k z b2) b1
              | k, z, Many xs => Data.Foldable.foldr k z xs
              end.

Local Definition Foldable__OrdList_foldr
   : forall {a} {b}, (a -> b -> b) -> b -> OrdList a -> b :=
  fun {a} {b} => foldrOL.

Local Definition Foldable__OrdList_foldMap
   : forall {m} {a}, forall `{GHC.Base.Monoid m}, (a -> m) -> OrdList a -> m :=
  fun {m} {a} `{GHC.Base.Monoid m} =>
    fun f =>
      Foldable__OrdList_foldr (GHC.Base.mappend GHC.Base.∘ f) GHC.Base.mempty.

Local Definition Foldable__OrdList_fold
   : forall {m}, forall `{GHC.Base.Monoid m}, OrdList m -> m :=
  fun {m} `{GHC.Base.Monoid m} => Foldable__OrdList_foldMap GHC.Base.id.

Local Definition Foldable__OrdList_foldl
   : forall {b} {a}, (b -> a -> b) -> b -> OrdList a -> b :=
  fun {b} {a} =>
    fun f z t =>
      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
                                      (Foldable__OrdList_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
                                                                  (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
                                                                   GHC.Base.flip f)) t)) z.

Local Definition Foldable__OrdList_foldl'
   : forall {b} {a}, (b -> a -> b) -> b -> OrdList a -> b :=
  fun {b} {a} =>
    fun f z0 xs =>
      let f' := fun x k z => k (f z x) in
      Foldable__OrdList_foldr f' GHC.Base.id xs z0.

Local Definition Foldable__OrdList_foldr'
   : forall {a} {b}, (a -> b -> b) -> b -> OrdList a -> b :=
  fun {a} {b} =>
    fun f z0 xs =>
      let f' := fun k x z => k (f x z) in
      Foldable__OrdList_foldl f' GHC.Base.id xs z0.

Local Definition Foldable__OrdList_length
   : forall {a}, OrdList a -> GHC.Num.Int :=
  fun {a} =>
    Foldable__OrdList_foldl' (fun arg_0__ arg_1__ =>
                                match arg_0__, arg_1__ with
                                | c, _ => c GHC.Num.+ #1
                                end) #0.

Local Definition Foldable__OrdList_null : forall {a}, OrdList a -> bool :=
  fun {a} => Foldable__OrdList_foldr (fun arg_0__ arg_1__ => false) true.

Local Definition Foldable__OrdList_product
   : forall {a}, forall `{GHC.Num.Num a}, OrdList a -> a :=
  fun {a} `{GHC.Num.Num a} =>
    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
                               (Foldable__OrdList_foldMap Data.SemigroupInternal.Mk_Product).

Local Definition Foldable__OrdList_sum
   : forall {a}, forall `{GHC.Num.Num a}, OrdList a -> a :=
  fun {a} `{GHC.Num.Num a} =>
    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
                               (Foldable__OrdList_foldMap Data.SemigroupInternal.Mk_Sum).

Local Definition Foldable__OrdList_toList : forall {a}, OrdList a -> list a :=
  fun {a} =>
    fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__OrdList_foldr c n t)).

Program Instance Foldable__OrdList : Data.Foldable.Foldable OrdList :=
  fun _ k__ =>
    k__ {| Data.Foldable.fold__ := fun {m} `{GHC.Base.Monoid m} =>
             Foldable__OrdList_fold ;
           Data.Foldable.foldMap__ := fun {m} {a} `{GHC.Base.Monoid m} =>
             Foldable__OrdList_foldMap ;
           Data.Foldable.foldl__ := fun {b} {a} => Foldable__OrdList_foldl ;
           Data.Foldable.foldl'__ := fun {b} {a} => Foldable__OrdList_foldl' ;
           Data.Foldable.foldr__ := fun {a} {b} => Foldable__OrdList_foldr ;
           Data.Foldable.foldr'__ := fun {a} {b} => Foldable__OrdList_foldr' ;
           Data.Foldable.length__ := fun {a} => Foldable__OrdList_length ;
           Data.Foldable.null__ := fun {a} => Foldable__OrdList_null ;
           Data.Foldable.product__ := fun {a} `{GHC.Num.Num a} =>
             Foldable__OrdList_product ;
           Data.Foldable.sum__ := fun {a} `{GHC.Num.Num a} => Foldable__OrdList_sum ;
           Data.Foldable.toList__ := fun {a} => Foldable__OrdList_toList |}.

Definition fromOL {a} : OrdList a -> list a :=
  fun a =>
    let fix go arg_0__ arg_1__
              := match arg_0__, arg_1__ with
                 | None, acc => acc
                 | One a, acc => cons a acc
                 | Cons a b, acc => cons a (go b acc)
                 | Snoc a b, acc => go a (cons b acc)
                 | Two a b, acc => go a (go b acc)
                 | Many xs, acc => Coq.Init.Datatypes.app xs acc
                 end in
    go a nil.

Definition toOL {a} : list a -> OrdList a :=
  fun arg_0__ => match arg_0__ with | nil => None | xs => Many xs end.

Local Definition Traversable__OrdList_traverse
   : forall {f} {a} {b},
     forall `{GHC.Base.Applicative f}, (a -> f b) -> OrdList a -> f (OrdList b) :=
  fun {f} {a} {b} `{GHC.Base.Applicative f} =>
    fun f xs => toOL Data.Functor.<$> Data.Traversable.traverse f (fromOL xs).

Local Definition Traversable__OrdList_mapM
   : forall {m} {a} {b},
     forall `{GHC.Base.Monad m}, (a -> m b) -> OrdList a -> m (OrdList b) :=
  fun {m} {a} {b} `{GHC.Base.Monad m} => Traversable__OrdList_traverse.

Local Definition Traversable__OrdList_sequenceA
   : forall {f} {a},
     forall `{GHC.Base.Applicative f}, OrdList (f a) -> f (OrdList a) :=
  fun {f} {a} `{GHC.Base.Applicative f} =>
    Traversable__OrdList_traverse GHC.Base.id.

Local Definition Traversable__OrdList_sequence
   : forall {m} {a}, forall `{GHC.Base.Monad m}, OrdList (m a) -> m (OrdList a) :=
  fun {m} {a} `{GHC.Base.Monad m} => Traversable__OrdList_sequenceA.

Program Instance Traversable__OrdList : Data.Traversable.Traversable OrdList :=
  fun _ k__ =>
    k__ {| Data.Traversable.mapM__ := fun {m} {a} {b} `{GHC.Base.Monad m} =>
             Traversable__OrdList_mapM ;
           Data.Traversable.sequence__ := fun {m} {a} `{GHC.Base.Monad m} =>
             Traversable__OrdList_sequence ;
           Data.Traversable.sequenceA__ := fun {f} {a} `{GHC.Base.Applicative f} =>
             Traversable__OrdList_sequenceA ;
           Data.Traversable.traverse__ := fun {f} {a} {b} `{GHC.Base.Applicative f} =>
             Traversable__OrdList_traverse |}.

Definition unitOL {a} : a -> OrdList a :=
  fun as_ => One as_.

Definition snocOL {a} : OrdList a -> a -> OrdList a :=
  fun as_ b => Snoc as_ b.

Definition consOL {a} : a -> OrdList a -> OrdList a :=
  fun a bs => Cons a bs.

(* Skipping definition `OrdList.lastOL' *)

Definition isNilOL {a} : OrdList a -> bool :=
  fun arg_0__ => match arg_0__ with | None => true | _ => false end.

Fixpoint foldlOL {b} {a} (arg_0__ : (b -> a -> b)) (arg_1__ : b) (arg_2__
                   : OrdList a) : b
           := match arg_0__, arg_1__, arg_2__ with
              | _, z, None => z
              | k, z, One x => k z x
              | k, z, Cons x xs => foldlOL k (k z x) xs
              | k, z, Snoc xs x => k (foldlOL k z xs) x
              | k, z, Two b1 b2 => foldlOL k (foldlOL k z b1) b2
              | k, z, Many xs => Data.Foldable.foldl k z xs
              end.

(* External variables:
     bool cons false list nil true Coq.Init.Datatypes.app Coq.Program.Basics.compose
     Data.Foldable.Foldable Data.Foldable.foldMap__ Data.Foldable.fold__
     Data.Foldable.foldl Data.Foldable.foldl'__ Data.Foldable.foldl__
     Data.Foldable.foldr Data.Foldable.foldr'__ Data.Foldable.foldr__
     Data.Foldable.length__ Data.Foldable.null__ Data.Foldable.product__
     Data.Foldable.sum__ Data.Foldable.toList__ Data.Functor.op_zlzdzg__
     Data.SemigroupInternal.Mk_Dual Data.SemigroupInternal.Mk_Endo
     Data.SemigroupInternal.Mk_Product Data.SemigroupInternal.Mk_Sum
     Data.SemigroupInternal.appEndo Data.SemigroupInternal.getDual
     Data.SemigroupInternal.getProduct Data.SemigroupInternal.getSum
     Data.Traversable.Traversable Data.Traversable.mapM__
     Data.Traversable.sequenceA__ Data.Traversable.sequence__
     Data.Traversable.traverse Data.Traversable.traverse__ GHC.Base.Applicative
     GHC.Base.Functor GHC.Base.Monad GHC.Base.Monoid GHC.Base.Semigroup
     GHC.Base.build' GHC.Base.const GHC.Base.flip GHC.Base.fmap__ GHC.Base.id
     GHC.Base.map GHC.Base.mappend GHC.Base.mappend__ GHC.Base.mconcat__
     GHC.Base.mempty GHC.Base.mempty__ GHC.Base.op_z2218U__ GHC.Base.op_zlzd____
     GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlzlzgzg____ GHC.Num.Int GHC.Num.Num
     GHC.Num.fromInteger GHC.Num.op_zp__
*)

author: antalsz

repo: hs-to-coq

save_path: github-repos/coq/antalsz-hs-to-coq


text:
Ltac split_ n :=
  match constr:(n) with
  | O => fail
  | 1%nat => idtac
  | Datatypes.S ?x => split; [ | split_ x ]
  end.

Tactic Notation "split" := split.
Tactic Notation "split" constr(n) := split_ n.
Tactic Notation "split!" := repeat apply conj.

Tactic Notation "spec" hyp(H) :=
  match type of H with
    forall _ : ?a, _ =>
    let Ha := fresh in
    assert (Ha : a); [ | specialize (H Ha); clear Ha ]
  end.

Tactic Notation "spec" hyp(H) constr(t1) := specialize (H t1).
Tactic Notation "spec" hyp(H) constr(t1) constr(t2) := specialize (H t1 t2).
Tactic Notation "spec" hyp(H) constr(t1) constr(t2) constr(t3) := specialize (H t1 t2 t3).

Tactic Notation "spec" hyp(H) "by" tactic(t) :=
  spec H; [ now t | ].

Tactic Notation "apply" "!" constr(t) := repeat apply t.

Tactic Notation "apply" "?" constr(t) := try apply t.

From RelationAlgebra Require Import prop monoid kat relalg kat_tac.

Ltac destruct_rel :=
  repeat
    match goal with
    | |- _ ≡ _ => intros x y; split; intro
    | |- _ ≦ _ => intros x y ? || intros ? ? || intro
    | |- _ -> _ => intro
    | |- (!_) _ _ => intro
    | H : ?R° ?x ?y |- _ => change (R° x y) with (R y x) in H
    | H : (_ ⊓ _) _ _ |- _ => destruct H as [? ?]
    | H : (_ ⊓ _) _ |- _ => destruct H as [? ?]
    | H : (_ ⊔ _) _ _ |- _ => destruct H
    | H : (_ ⊔ _) _ |- _ => destruct H
    | H : ([_] ⋅ _) _ _ |- _ => destruct H as [? [<- ?] ?]
    | H : (1 ⋅ _) _ _ |- _ => destruct H as [? <- ?]
    | H : (_ ⋅ [_]) _ _ |- _ => destruct H as [? ? [-> ?]]
    | H : (_ ⋅ 1) _ _ |- _ => destruct H as [? ? ->]
    | H : (_ ⋅ _) _ _ |- _ => destruct H
    | H : [_] ?x ?x |- _ => destruct H as [_ H]
    | H : [_] _ _ |- _ => destruct H as [->]
    | H : 1 _ _ |- _ => destruct H
    end.

Tactic Notation "elim_trans" constr(r) :=
  let Heq := fresh "Heq" in
  assert (Heq : r ≡ r^+) by (now symmetry; apply itr_transitive);
  rewrite Heq in *;
  clear Heq.

Tactic Notation "elim_trans" :=
  match goal with
  | H : is_transitive ?r |- _ => elim_trans r; clear H
  | H : ?r ⋅ ?r ≦ ?r |- _ => elim_trans r; clear H
  end.

From Catincoq.lib Require Import proprel.

Lemma cnvtst {A} {E : set A} : [E]° ≡ [E].
Proof.
  intros a b; split; intros [-> Ha]; constructor; auto.
Qed.

Tactic Notation "elim_cnv" :=
  repeat (rewrite ?cnvtst, ?cnv1, ?cnv0, ?cnvstr, ?cnvitr,
          ?cnvtop, ?cnvcap, ?cnvdot, ?cnvpls, ?cnvneg).

Tactic Notation "elim_cnv" "in" hyp(H) :=
  repeat (rewrite ?cnvtst, ?cnv1, ?cnv0, ?cnvstr, ?cnvitr,
          ?cnvtop, ?cnvcap, ?cnvdot, ?cnvpls, ?cnvneg in H).

(** Help solve goals and generate constraints based on the "type" of
    some events i.e. the set to which it belongs, such as R, W, !W,
    etc. *)

Ltac types_ :=
  repeat
    match goal with
    | Hx : ?X |- ?X => assumption
    | Hx : (_ ⊓ _) _ |- _ => destruct Hx
    | Hx : ?X ?x, Hy : ?Y ?x, XY : ?X ⊓ ?Y ≦ bot |- _ =>
      eapply XY; split; eauto
    | H : (?r ⋅ [?Y]) ?x ?v |- ?Y ?v => destruct_rel; assumption
    | H : ([?X] ⋅ ?r ⋅ [?Y]) ?x ?v |- ?Y ?v => destruct_rel; assumption
    | H : ([?X] ⋅ ?r ⋅ [?Y]) ?v ?y |- ?X ?v => destruct_rel; assumption
    | H : ?r ?x ?v, H2 : ?r ≦ [?X] ⋅ ?r ⋅ [?Y] |- ?Y ?v =>
      assert (([X] ⋅ r ⋅ [Y]) x v) by apply H2, H;
      destruct_rel; assumption
    | H : ?r ?v ?y, H2 : ?r ≦ [?X] ⋅ ?r ⋅ [?Y] |- ?X ?v =>
      assert (([X] ⋅ r ⋅ [Y]) v y) by apply H2, H;
      destruct_rel; assumption
    | |- (_ ⊓ _) _ => split
    | |- (!_) _ => try solve [intro; types_]
    | H : ?X ≦ ?Y, H' : ?X ?x |- ?Y ?x => apply H, H'
    | H : ?X ≦ ?Y |- ?Y ?x => try solve [apply H; types_]
    | |- top _ => constructor
    end.

Tactic Notation "types" := types_.

Tactic Notation "types" var(v) :=
  match goal with
  | H : ?r ?x v, H2 : ?r ≦ [?X] ⋅ ?r ⋅ [?Y] |- _ =>
    assert (Y v) by types
  | H : ?r v ?y, H2 : ?r ≦ [?X] ⋅ ?r ⋅ [?Y] |- _ =>
    assert (X v) by types
  end.

(** Somewhat dual to destruct_rel: helps solve goals of the form
    [(some relation) x y] *)

Ltac relate :=
  repeat
    (match goal with
     | |- (_ ⋅ [_]) ?x ?y => exists y; [ | split; auto ]
     | |- ([_] ⋅ [_] ⋅ _) ?x ?y => exists x
     | |- ([_] ⋅ [_] ⋅ [_] ⋅ _) ?x ?y => exists x
     | |- ([_] ⋅ _) ?x ?y => exists x; [ split; auto | ]
     | |- (_ ⊓ _) ?x ?y => split; auto
     | |- [_] ?x ?y => split; [ reflexivity | ]
     | |- 1 ?x ?y => reflexivity
     | |- top ?x ?y => constructor
     | |- ?R° ?x ?y => change (R y x)
     | |- _ => idtac
     end; types; try assumption).

(** [rel t], on a goal of the form [r x y], applies tactic [t] on
    relation [r], in a way that allows rewriting. [t] is typically of
    the form [rewrite e] (if e is of the form [_ ≡ _]) or of the form
    [rewrite <-e] (if e is of the form [_ ≦ _]) *)

Tactic Notation "rel" tactic(t) :=
  match goal with
    x : ?A, y : ?A |- ?r ?x ?y =>
    let s := fresh "s" in
    let H := fresh "H" in
    evar (s : relation A);
    assert (H : s ≦ r);
    [ t; unfold s; reflexivity
    | apply H; unfold s; clear s H ]
  end.

Example rel_example {A} (r : relation A) a b c : r a b -> r b c -> r^+ a c.
Proof.
  intros ab bc.
  rel rewrite <-itr_trans.
  rel rewrite <-itr_ext.
  eexists; eauto.
Qed.

(** [in H rel t] is similar to [rel t] but applies [t] on the relation
    [r] where [H] is an hypothesis of the form [r x y] *)

Tactic Notation "in" hyp(H) "rel" tactic(t) :=
  match type of H with
  | ?r ?x ?y =>
    let A := type of x in
    let s := fresh "s" in
    let L := fresh "L" in
    evar (s : relation A);
    assert (L : r ≦ s);
    [ unfold s; t; reflexivity
    | subst s; try (apply L in H; clear L) ];
    idtac
  end.

(* alternative syntax [rel t in H]: better indentation, but requires
   parentheses in [t] when [t] is e.g. [rewrite _] *)

Tactic Notation "rel" tactic(t) "in" hyp(H) := in H rel t.

Example in_rel_example {A} (r : relation A) a b c : r a b -> r b c -> r^+ a c.
Proof.
  intros ab bc.
  in ab rel rewrite (itr_ext r).
  rel (rewrite (itr_ext r)) in bc. (* alternative syntax *)
  rel rewrite <-itr_trans.
  eexists; eauto.
Qed.

author: jmadiot

repo: cats

save_path: github-repos/coq/jmadiot-cats