Tactic for solving contractiveness of protocols.

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]).

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 :

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).