Closed some admits

multris/channel/proto_model.v

@@ -148,117 +148,72 @@ Qed.
 (* TODO: This is FALSE *)
 Lemma proto_ind {V} `{!Cofe PROPn, !Cofe PROP} (P : proto V PROPn PROP → Prop) :
   Proper ((≡) ==> impl) P →
-  P proto_end → (∀ i x p, p ≡ [] → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
-(* Proof. *)
-(* (* Should hold in the same way map_ind holds *) *)
-(* Lemma proto_ind {V} `{!Cofe PROPn, !Cofe PROP} (P : proto V PROPn PROP → Prop) : *)
-(*   Proper ((≡) ==> impl) P → *)
-(*   P proto_end → (∀ i x p, p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m. *)
-(* Proof. *)
-(*   intros HP ? Hins m. *)
-(*   induction (map_wf m) as [m _ IH]. *)
-(*   destruct (map_choose_or_empty m) as [(i&x&?)| H']. *)
-(*   { *)
-(*     assert (m ≡ proto_union (proto_message i (λ v, x v ◎ laterO_map proto_unfold)) (delete i m)) as Heq. *)
-(*     { *)
-(*       rewrite /proto_message /proto_union. *)
-(*       rewrite -insert_union_singleton_l. *)
-(*       intros i'. *)
-(*       (* TODO: Simplify *) *)
-(*       destruct (decide (i=i')) as [->|]. *)
-(*       { rewrite H0. rewrite lookup_insert. f_equiv. *)
-(*         intros v. *)
-(*         intros x''. *)
-(*         simpl. *)
-(*         rewrite -later_map_compose. *)
-(*         simpl. f_equiv. *)
-(*         destruct x''. *)
-(*         rewrite later_map_Next. f_equiv. *)
-(*         simpl. rewrite proto_unfold_fold. done. } *)
-(*       rewrite lookup_insert_ne; [|done]. *)
-(*       by rewrite lookup_delete_ne. } *)
-(*     rewrite Heq. *)
-(*     apply Hins. *)
-(*     { by rewrite lookup_delete. } *)
-(*     eapply IH. by apply: delete_subset. *)
-(*   } *)
-(*   rewrite /proto_end in H. *)
-(*   by rewrite -H' in H. *)
-(* Qed. *)
-Admitted.
+  P proto_end → (∀ i x p, P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
+Proof.
+  intros.
+  induction m; [done|].
+  destruct a.
+  apply (H1 o (λ v, o0 v ◎ laterO_map proto_unfold) _) in IHm.
+  simpl in *.
+  assert (o0 ≡ λ v : V, o0 v ◎ laterO_map proto_unfold ◎ laterO_map proto_fold).
+  { intros v m'. simpl. rewrite -later_map_compose. f_equiv.
+    destruct m'. rewrite later_map_Next. simpl. rewrite proto_unfold_fold. done. }
+  rewrite H2. done.
+Qed.
 
 Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
   p ≡ proto_end ∨ ∃ a m p', p ≡ proto_union (proto_message a m) p'.
-Proof. Admitted.
-(*   destruct (proto_unfold p) as [[a m]|] eqn:E; simpl in *; last first. *)
-(*   - left. by rewrite -(proto_fold_unfold p) E. *)
-(*   - right. exists a, m. by rewrite /proto_message -E proto_fold_unfold. *)
-(* Qed. *)
+Proof.
+  destruct p as [|[a m] p'] eqn:E; simpl in *.
+  - left. done.
+  - right. exists a, (λ v, m v ◎ laterO_map proto_unfold), p'.
+  f_equiv. f_equiv.
+  intros v m'. simpl. rewrite -later_map_compose. f_equiv.
+  destruct m'. rewrite later_map_Next. simpl. rewrite proto_unfold_fold. done.
+Qed.
 Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
   Inhabited (proto V PROPn PROP) := populate proto_end.
 
 Lemma proto_message_equivI {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
   ⊣⊢@{iProp Σ} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
-Proof. Admitted.
-(*   rewrite /proto_message list_equivI /=. *)
-(*   iSplit. *)
-(*   { destruct (decide (a1=a2)) as [->|Hne]; last first. *)
-(*     { iIntros "H". iSpecialize ("H" $! 0). simpl. *)
-(*       rewrite option_equivI. rewrite prod_equivI. simpl. } *)
-(*     iIntros "H". iSpecialize ("H" $! a2). *)
-(*     rewrite !lookup_insert option_equivI. *)
-(*     iSplit; [done|]. *)
-(*     iIntros (v p). rewrite discrete_fun_equivI. *)
-(*     iSpecialize ("H" $! v). *)
-(*     rewrite ofe_morO_equivI=> /=. *)
-(*     iSpecialize ("H" $! (laterO_map proto_unfold p)). *)
-(*     assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as <-; last by done. *)
-(*     rewrite -later_map_compose. rewrite -(later_map_id p). *)
-(*     apply later_map_ext=> p' /=. by rewrite proto_fold_unfold. } *)
-(*   iIntros "[%Heq H2]" (i). rewrite Heq. *)
-(*   destruct (decide (a2 = i)) as [->|Hneq]; [|by rewrite !lookup_insert_ne]. *)
-(*   rewrite !lookup_insert option_equivI discrete_fun_equivI. *)
-(*   iIntros (v). rewrite ofe_morO_equivI. by iIntros (p). *)
-(* Qed. *)
+Proof.
+  rewrite /proto_message list_equivI /=.
+  iSplit.
+  { iIntros "H".
+    iSpecialize ("H" $! 0).
+    simpl.
+    rewrite option_equivI.
+    rewrite prod_equivI.
+    simpl.
+    iDestruct "H" as "[%Haeq H]".
+    iSplit; [done|].
+    iIntros (v p). rewrite discrete_fun_equivI.    
+    iSpecialize ("H" $! v).
+    rewrite ofe_morO_equivI=> /=.
+    iSpecialize ("H" $! (laterO_map proto_unfold p)).
+    assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as <-; last by done.
+    rewrite -later_map_compose. rewrite -(later_map_id p).
+    apply later_map_ext=> p' /=. by rewrite proto_fold_unfold. }
+  iIntros "[%Heq H2]" (i). rewrite Heq.
+  destruct i; [|done]. simpl. 
+  rewrite option_equivI. rewrite prod_equivI. simpl.
+  iSplit; [done|].
+  rewrite discrete_fun_equivI.
+  iIntros (v). rewrite ofe_morO_equivI. by iIntros (p).
+Qed.
 Lemma proto_message_end_equivI  {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{iProp Σ} False.
-Proof. Admitted.
-(*   rewrite /proto_message /proto_end. rewrite gmap_equivI. *)
-(*   iIntros "H". iSpecialize ("H" $! a). rewrite lookup_insert. rewrite lookup_empty. *)
-(*   by rewrite option_equivI. *)
-(* Qed. *)
+Proof.
+  rewrite /proto_message /proto_end. rewrite list_equivI.
+  iIntros "H". iSpecialize ("H" $! 0). simpl.
+  by rewrite option_equivI.
+Qed.
 Lemma proto_end_message_equivI {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{iProp Σ} False.
 Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
 
-(* Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A} *)
-(*     (x : A) (f : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) *)
-(*     (p : proto V PROPn PROP) : A := *)
-(*   match p with *)
-(*   | [] => x *)
-(*   | p' => fold_left (λ acc am, f acc am.1 (λ v, am.2 v ◎ laterO_map proto_unfold)) p' x *)
-(*   end. *)
-
-(* Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe} *)
-(*     (x : A) (f1 f2 : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n : *)
-(*   (∀ x a m1 m2, (∀ v, m1 v ≡{n}≡ m2 v) → f1 x a m1 ≡{n}≡ f2 x a m2) → *)
-(*   p1 ≡{n}≡ p2 → *)
-(*   proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2. *)
-(* Proof. Admitted. *)
-
 (** Functor *)
-(* Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} *)
-(*     (g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) : *)
-(*   proto V PROPn PROP -n> proto V PROPn' PROP' := λne p, *)
-(*     proto_elim proto_end (λ acc a m, proto_union acc $ proto_message a (λ v, g ◎ m v ◎ laterO_map rec)) p. *)
-(* Next Obligation. *)
-(*   intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp. *)
-(*   apply proto_elim_ne. *)
-(*   - intros. repeat f_equiv. done. *)
-(*   - done. *)
-(* Qed. *)
-
 Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (f : action → action) (g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
   proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
@@ -273,7 +228,15 @@ Qed.
 Global Instance proto_map_aux_contractive {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} f (g : PROP -n> PROP') :
   Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') f g).
-Proof. Admitted.
+Proof.
+  intros n rec1 rec2 Hrec p. simpl.
+  apply: (list_fmap_ne n _ _ _ p); [|done].
+  intros [a1 m1] [a2 m2] Hm=> /=. apply pair_ne.
+  - f_equiv. by inversion Hm.
+  - inversion Hm. intros v m. simpl. do 2 f_equiv; [done|].
+    do 1 f_equiv.
+    apply Next_contractive; by dist_later_intro as n' Hn'.
+Qed.
 
 Definition proto_map_aux_2 {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
@@ -346,8 +309,7 @@ Proof.
   pattern p. apply proto_ind.
   { intros p1 p2 Hp H'. rewrite -Hp. done. }
   { rewrite !proto_map_end. done. }
-  intros a m p' Hp Hp'.
-  clear Hp.                     (* Make sure we dont abuse false assumption *)
+  intros a m p' Hp'.
   rewrite !proto_map_union.
   apply proto_union_ne; [|done].
   { rewrite !proto_map_message /=.
@@ -371,8 +333,7 @@ Proof.
   apply proto_ind.
   { intros p1 p2 Hp H'. rewrite -Hp. done. }
   { rewrite !proto_map_end. done. }
-  intros a m p' Hp Hp'.
-  clear Hp.                     (* Make sure we dont use false assumption *)
+  intros a m p' Hp'.
   rewrite proto_map_union. f_equiv.
   { rewrite !proto_map_message /=. apply proto_message_ne=> // v p'' /=. f_equiv.
     apply Next_contractive; dist_later_intro as n' Hn'; auto. }
@@ -392,8 +353,7 @@ Proof.
   pattern p. apply proto_ind.
   { intros p1 p2 Hp H'. rewrite -Hp. done. }
   { rewrite !proto_map_end. done. }
-  intros a m p' Hp Hp'.
-  clear Hp.                     (* Make sure we dont use false assumption *)
+  intros a m p' Hp'.
   rewrite !proto_map_union. f_equiv.
   { rewrite !proto_map_message /=. apply proto_message_ne=> // v p'' /=. do 3 f_equiv.
     apply Next_contractive; dist_later_intro as n' Hn'; auto. }