Automate typing derivations

..by introducing a hint database for typeability

F_mu_ref_conc/examples/counter.v

@@ -33,15 +33,17 @@ Section CG_Counter.
 
   Notation D := (prodC valC valC -n> iProp Σ).
   Implicit Types Δ : listC D.
-
+  
   (* Coarse-grained increment *)
   Lemma CG_increment_type Γ :
     typed Γ CG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
   Proof.    
     unfold CG_increment. unlock.
-    repeat econstructor; eauto; cbn; seq_map_lookup.
+    eauto 10 with typeable.    
   Qed.
 
+  Hint Resolve CG_increment_type : typeable.
+  
   Lemma steps_CG_increment E ρ j K x n:
     nclose specN ⊆ E →
     spec_ctx ρ -∗ x ↦ₛ (#nv n)
@@ -83,14 +85,11 @@ Section CG_Counter.
     typed Γ CG_locked_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
   Proof.
     unfold CG_locked_increment. unlock.
-    repeat econstructor; eauto;
-    try (eapply with_lock_type); auto using CG_increment_type.
-    - cbn. rewrite lookup_insert_ne; eauto. rewrite lookup_insert_ne; eauto.
-      apply lookup_insert.
-    - cbn. apply lookup_insert.
-    - cbn. apply lookup_insert.
+    eauto 25 with typeable.
   Qed.
 
+  Hint Resolve CG_locked_increment_type : typeable.
+
   Lemma steps_CG_locked_increment E ρ j K x n l :
     nclose specN ⊆ E →
     spec_ctx ρ -∗ x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false)
@@ -137,11 +136,11 @@ Section CG_Counter.
     typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
   Proof.
     unfold counter_read. unlock.
-    repeat econstructor.
-    cbn. rewrite lookup_insert_ne; auto.
-    apply lookup_insert.
+    eauto 10 with typeable.
   Qed.
 
+  Hint Resolve counter_read_type : typeable.
+
   Lemma steps_counter_read E ρ j K x n :
     nclose specN ⊆ E →
     spec_ctx ρ -∗ x ↦ₛ (#nv n)
@@ -164,34 +163,30 @@ Section CG_Counter.
               (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)))).
   Proof.
     unfold CG_counter_body. unlock.
-    repeat econstructor;
-      eauto using CG_locked_increment_type, counter_read_type.
-    - cbn. rewrite lookup_insert_ne; auto.
-      apply lookup_insert.
-    - cbn. apply lookup_insert.
-    - cbn. rewrite lookup_insert_ne; auto.
-      apply lookup_insert.
+    eauto 15 with typeable.
   Qed.
 
+  Hint Resolve CG_counter_body_type : typeable.
+
   Lemma CG_counter_type Γ :
     typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
   Proof.
-    econstructor; eauto using newlock_type.
-    do 2 econstructor; [|do 2 constructor].
-    repeat econstructor; eauto. apply CG_counter_body_type; by constructor.
-    - apply lookup_insert.
-    - cbn. rewrite lookup_insert_ne; auto.
-      apply lookup_insert.
+    unfold CG_counter.
+    eauto 15 with typeable.
   Qed.
 
+  Hint Resolve CG_counter_type : typeable.
+
   (* Fine-grained increment *)
   Lemma FG_increment_type Γ :
     typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
   Proof.
     unfold FG_increment. unlock.
-    repeat (econstructor; eauto using EqTNat); cbn; try by seq_map_lookup.
+    eauto 20 with typeable.
   Qed.
 
+  Hint Resolve FG_increment_type : typeable.
+
   Lemma bin_log_FG_increment_l Γ K E x n t τ :
     x ↦ᵢ (#nv n) -∗
     (x ↦ᵢ (#nv (S n)) -∗ {E,E;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ) -∗
@@ -269,18 +264,19 @@ Section CG_Counter.
             (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
   Proof.
     unfold FG_counter_body. unlock.
-    repeat econstructor; eauto; cbn; seq_map_lookup.
-    - apply FG_increment_type; trivial.
-    - apply counter_read_type; trivial.
+    eauto 15 with typeable.
   Qed.
 
+  Hint Resolve FG_counter_body_type : typeable.
+  
   Lemma FG_counter_type Γ :
     typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
   Proof.
-    econstructor; eauto using newlock_type, typed.
-    apply FG_counter_body_type; by constructor.
+    unfold FG_counter.
+    eauto 15 with typeable.
   Qed.
 
+  Hint Resolve FG_counter_type : typeable.
 
   Definition counterN : namespace := nroot .@ "counter".
 

F_mu_ref_conc/examples/lock.v

@@ -25,48 +25,32 @@ Proof. rewrite /newlock. solve_closed. Qed.
 
 Definition LockType := Tref TBool.
 
+Hint Unfold LockType : typeable.
+
 Lemma newlock_type Γ : typed Γ newlock LockType.
-Proof. repeat constructor. Qed.
+Proof. eauto with typeable. Qed.
 
 Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
-Proof.
-  do 3 econstructor; eauto using EqTBool; repeat constructor.
-  - by rewrite lookup_insert.
-  - rewrite lookup_insert_ne; eauto. by rewrite lookup_insert.
-  - by rewrite lookup_insert.
-Qed.
+Proof. unfold acquire. eauto 10 with typeable. Qed.
 
 Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
-Proof. repeat econstructor. by rewrite lookup_insert. Qed.
+Proof. unfold release. eauto with typeable. Qed.
 
 Opaque acquire.
 Opaque release.
 
-(* TODO: this lemma is not true without the assumption
-   that x is not in Γ *)
-Lemma context_weaken_insert Γ x τ' e τ :
-  Γ !! x = None →
-  Γ ⊢ₜ e : τ →
-  <[x:=τ']>Γ ⊢ₜ e : τ.
-Proof.
-  intros Hx. eapply context_gen_weakening; eauto.
-  by apply insert_subseteq.
-Qed.
-
-Ltac seq_map_lookup :=
-  repeat lazymatch goal with
-  | [ |- <[?x:=_]>_ !! ?x = Some _ ] => rewrite lookup_insert; eauto
-  | [ |- <[?x:=_]>_ !! ?l = Some _ ] => rewrite lookup_insert_ne; eauto
-  end.
+Hint Resolve newlock_type : typeable.
+Hint Resolve release_type : typeable.
+Hint Resolve acquire_type : typeable.
 
 Lemma with_lock_type Γ τ τ' :
   typed Γ with_lock (TArrow (TArrow τ τ') (TArrow LockType (TArrow τ τ'))).
 Proof.
-  unfold with_lock. unlock.
-  do 3 (econstructor; eauto). cbn.
-  repeat (econstructor; eauto using release_type, acquire_type; cbn); seq_map_lookup.
+  unfold with_lock. unlock. eauto 25 with typeable.
 Qed.
 
+Hint Resolve with_lock_type : typeable.
+
 Section proof.
   Context `{cfgSG Σ}.
   Context `{heapIG Σ}.

F_mu_ref_conc/typing.v

@@ -79,6 +79,37 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
      Γ ⊢ₜ CAS e1 e2 e3 : TBool
 where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
 
+(** A hint db for the typing information *)
+
+Create HintDb typeable.
+
+Hint Constructors typed : typeable.
+
+(** we need to replace some of the constructors with lemmas better suitable for search *)
+Lemma TCAS' Γ e1 e2 e3 τ :
+  Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
+  EqType τ → 
+  Γ ⊢ₜ CAS e1 e2 e3 : TBool.
+Proof. eauto using TCAS. Qed.
+
+Hint Resolve TCAS' : typeable.
+Remove Hints TCAS : typeable.
+
+Lemma BINOP' Γ op e1 e2 τ :
+  Γ ⊢ₜ e1 : TNat →
+  Γ ⊢ₜ e2 : TNat → 
+  τ = binop_res_type op →
+  Γ ⊢ₜ BinOp op e1 e2 : τ.
+Proof. intros. subst τ. by econstructor. Qed.
+
+Hint Resolve BINOP' : typeable.
+Remove Hints BinOp_typed : typeable.
+
+Hint Constructors EqType : typeable.
+
+Hint Extern 10 (<[_:=_]>_ !! _ = Some _) => eapply lookup_insert : typeable.
+Hint Extern 20 (<[_:=_]>_ !! _ = Some _) => rewrite lookup_insert_ne; last done : typeable.
+
 (** Environment substitution and closedness *)
 Definition env_subst := subst_p. 
 
@@ -106,15 +137,12 @@ Proof.
   - case_bool_decide; auto.
     apply H0. 
     rewrite elem_of_dom. by exists τ.
-  - destruct f, x; eauto; simpl.
-    rewrite -(dom_insert _ _ τ1). eauto.
-    rewrite -(dom_insert _ _ (TArrow τ1 τ2)). eauto.    
-    rewrite -(dom_insert _ s (TArrow τ1 τ2)). 
-    rewrite -(dom_insert _ s0 τ1). 
-    eauto.
+  - revert IHtyped.
+    rewrite !dom_insert_binder.
+    destruct f, x; cbn-[union];
+    rewrite ?(left_id ∅ union); eauto.
   - rewrite -dom_fmap. eassumption.
-  - apply andb_prop_intro; split; auto.
-    rewrite -dom_fmap. eauto.
+  - split_and?; [ | rewrite -dom_fmap ]; eauto.
 Qed.
 
 (** Weakening *)
@@ -124,14 +152,12 @@ Lemma context_gen_weakening Γ Δ e τ :
   Δ ⊢ₜ e : τ.
 Proof.
   intros Hsub Ht. revert Hsub. generalize dependent Δ.
-  induction Ht => Δ Hsub; subst; eauto using typed.
-  - econstructor.
-    eapply lookup_weaken; eauto.
-  - econstructor. eapply IHHt.
+  induction Ht => Δ Hsub; subst; eauto with typeable.
+  - econstructor. by eapply lookup_weaken.
+  - econstructor. eapply IHHt.    
     destruct f, x; cbn; eauto;
     repeat eapply insert_mono; done.
-  - econstructor.
-    eapply IHHt.
+  - econstructor. eapply IHHt.
     by apply map_fmap_mono.
   - econstructor.
     * by eapply IHHt1.