From 2c2ed9336c2d0ce10ce72d59689db457b36ff736 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 30 Jun 2019 11:52:46 +0200
Subject: [PATCH] Tactic for solving contractiveness of protocols.

---
 theories/channel/proto_channel.v   | 14 ++++++++++++++
 theories/examples/list_sort_elem.v | 10 ++--------
 theories/examples/loop_sort.v      |  5 +----
 3 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 18501ad..b2e01fa 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -803,3 +803,17 @@ Section proto.
     iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
   Qed.
 End proto.
+
+Ltac f_proto_contractive :=
+  match goal with
+  | _ => apply iProto_branch_contractive
+  | _ => apply iProto_message_contractive; simpl; intros; [reflexivity|..]
+  | H : _ ≡{?n}≡ _ |- _ ≡{?n'}≡ _ => apply (dist_le n); [apply H|lia]
+  end;
+  try match goal with
+  | |- @dist_later ?A _ ?n ?x ?y =>
+         destruct n as [|n]; simpl in *; [exact Logic.I|change (@dist A _ n x y)]
+  end.
+
+Ltac solve_proto_contractive :=
+  solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]).
diff --git a/theories/examples/list_sort_elem.v b/theories/examples/list_sort_elem.v
index ca6ddf8..3967fd5 100644
--- a/theories/examples/list_sort_elem.v
+++ b/theories/examples/list_sort_elem.v
@@ -57,10 +57,7 @@ Section list_sort_elem.
      <&{⌜ ys ≡ₚ xs ⌝}> END)%proto.
 
   Instance tail_protocol_aux_contractive xs : Contractive (tail_protocol_aux xs).
-  Proof.
-    intros n p p' Hp ys. apply iProto_branch_ne=> //=.
-    apply iProto_message_contractive=> x //=. destruct n as [|n]=> //=.
-  Qed.
+  Proof. solve_proto_contractive. Qed.
   Definition tail_protocol (xs : list (A * val)) : list (A * val) → iProto Σ :=
     fixpoint (tail_protocol_aux xs).
   Global Instance tail_protocol_unfold xs ys :
@@ -73,10 +70,7 @@ Section list_sort_elem.
      <+> tail_protocol xs [])%proto.
 
   Instance head_protocol_aux_contractive : Contractive head_protocol_aux.
-  Proof.
-    intros n p p' Hp xs. apply iProto_branch_ne=> //=.
-    apply iProto_message_contractive=> //= x. destruct n as [|n]=> //=.
-  Qed.
+  Proof. solve_proto_contractive. Qed.
 
   Definition head_protocol : list (A * val) → iProto Σ := fixpoint head_protocol_aux.
   Global Instance head_protocol_unfold xs :
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
index 4c6dc44..ff403fb 100644
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -20,10 +20,7 @@ Section loop_sort.
     ((sort_protocol <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec @ N }}; rec) <+> END))%proto.
 
   Instance loop_sort_protocol_aux_contractive : Contractive loop_sort_protocol_aux.
-  Proof.
-    intros n p p' Hp. rewrite /loop_sort_protocol_aux.
-    f_contractive; f_equiv=> //. apply iProto_message_ne=> c /=; by repeat f_equiv.
-  Qed.
+  Proof. solve_proto_contractive. Qed.
   Definition loop_sort_protocol : iProto Σ := fixpoint loop_sort_protocol_aux.
   Global Instance loop_sort_protocol_unfold :
     ProtoUnfold loop_sort_protocol (loop_sort_protocol_aux loop_sort_protocol).
-- 
GitLab