improved auto goal selection (MetaCoq#737)

JasonGross · Jul 18, 2022 · 3a4214b · 3a4214b
1 parent bc3a9a8
commit 3a4214b
Show file tree

Hide file tree

Showing 16 changed files with 21 additions and 21 deletions.
diff --git a/pcuic/theories/Conversion/PCUICInstConv.v b/pcuic/theories/Conversion/PCUICInstConv.v
@@ -73,7 +73,7 @@ Qed.
 
 Lemma inst_mkApps f l σ : (mkApps f l).[σ] = mkApps f.[σ] (map (inst σ) l).
 Proof.
-  induction l in f |- *; simpl; auto. rewrite IHl.
+  induction l in f |- *; simpl; [auto|]. rewrite IHl.
   now autorewrite with sigma.
 Qed.
 #[global]

diff --git a/pcuic/theories/PCUICConfluence.v b/pcuic/theories/PCUICConfluence.v
@@ -3035,7 +3035,7 @@ Section RedConfluence.
     move=> [[Γ hΓ] [t ht]] [[Δ hΔ] [u hu]] [redt redctx].
     eapply clos_rt_rt1n_iff in redt. cbn in *.
     induction redt in ht, hu |- *.
-    induction redctx in hΓ, hΔ, ht, hu |- *; try solve [constructor; eauto].
+    induction redctx in hΓ, hΔ, ht, hu |- *.
     - econstructor 2; simpl; apply reflexivity.
     - pose proof hΔ. rewrite on_free_vars_ctx_snoc in H.
       move/andP: H => [] hΔ' Hd'.

diff --git a/pcuic/theories/PCUICContexts.v b/pcuic/theories/PCUICContexts.v
@@ -743,7 +743,7 @@ Lemma eq_names_subst_context nas Γ s k :
   eq_names nas (subst_context s k Γ).
 Proof.
   induction 1.
-  * cbn; auto. constructor.
+  * cbn. constructor.
   * rewrite subst_context_snoc. constructor; auto.
 Qed.
 

diff --git a/pcuic/theories/PCUICCumulProp.v b/pcuic/theories/PCUICCumulProp.v
@@ -875,7 +875,7 @@ Lemma R_eq_univ_prop_consistent_instances Σ univs u u' :
 Proof using Type.
   intros wfΣ cu cu'.
   destruct univs; simpl in *.
-  - destruct u, u' => /= //. red.
+  - destruct u, u' => /=; [|done..]. red.
     simpl. constructor.
   - intuition.
     eapply Forall2_map.

diff --git a/pcuic/theories/PCUICExpandLetsCorrectness.v b/pcuic/theories/PCUICExpandLetsCorrectness.v
@@ -1185,7 +1185,7 @@ Require Import PCUICSpine.
 Lemma trans_reln l p Γ : map trans (SE.reln l p Γ) = 
   reln (map trans l) p (trans_local Γ).
 Proof.
-  induction Γ as [|[na [b|] ty] Γ] in l, p |- *; simpl; auto.
+  induction Γ as [|[na [b|] ty] Γ] in l, p |- *; simpl; [auto..|].
   now rewrite IHΓ.
 Qed.
 
@@ -1884,9 +1884,9 @@ Proof.
     try solve [econstructor; eauto].
 
   - simpl. tofvs.
-    rewrite (trans_subst_ctx Γ) /=; pcuic. eapply red1_red; constructor.
+    rewrite (trans_subst_ctx Γ) /=; [pcuic..|]. eapply red1_red; constructor.
 
-  - destruct wt. tofvs. rewrite (trans_subst_ctx Γ); pcuic. repeat constructor.
+  - destruct wt. tofvs. rewrite (trans_subst_ctx Γ); [pcuic..|]. repeat constructor.
 
   - destruct nth_error eqn:Heq => //. simpl in H. noconf H.
     simpl. destruct c; noconf H => //.

diff --git a/pcuic/theories/PCUICInductives.v b/pcuic/theories/PCUICInductives.v
@@ -390,7 +390,7 @@ Lemma projs_inst_skipn {ind pars arg t} n :
 Proof.
   induction arg in n |- *; simpl; auto.
   - now rewrite skipn_nil.
-  - destruct n as [|n']; [rewrite skipn_0|rewrite skipn_S] => //.
+  - destruct n as [|n']; [rewrite skipn_0|rewrite skipn_S]; [done|].
     rewrite IHarg /= //.
 Qed.
 

diff --git a/pcuic/theories/PCUICToTemplateCorrectness.v b/pcuic/theories/PCUICToTemplateCorrectness.v
@@ -940,7 +940,7 @@ Qed.
 Lemma trans_reln l p Γ : map trans (SE.reln l p Γ) = 
   reln (map trans l) p (trans_local Γ).
 Proof.
-  induction Γ as [|[na [b|] ty] Γ] in l, p |- *; simpl; auto.
+  induction Γ as [|[na [b|] ty] Γ] in l, p |- *; simpl; [auto..|].
   now rewrite IHΓ.
 Qed.
 

diff --git a/pcuic/theories/PCUICValidity.v b/pcuic/theories/PCUICValidity.v
@@ -176,7 +176,7 @@ Section Validity.
   Proof using Type.
     intros. eapply All2_map_right in X.
     depind X.
-    * destruct Γ => //. constructor.
+    * destruct Γ; [|done]. constructor.
     * destruct Γ => //.
       rewrite /expand_lets_ctx /expand_lets_k_ctx /=
         !lift_context_snoc; simpl.

diff --git a/pcuic/theories/PCUICWfUniverses.v b/pcuic/theories/PCUICWfUniverses.v
@@ -672,7 +672,7 @@ Qed.
   Lemma wf_abstract_instance Σ decl :
     wf_universe_instance (Σ, decl) (abstract_instance decl).
   Proof using Type.
-    destruct decl as [|[u cst]]=> /= //.
+    destruct decl as [|[u cst]]=> /=.
     red. constructor.
     rewrite /UContext.instance /AUContext.repr /=.
     rewrite mapi_unfold.

diff --git a/pcuic/theories/TemplateToPCUICCorrectness.v b/pcuic/theories/TemplateToPCUICCorrectness.v
@@ -562,7 +562,7 @@ Lemma trans_it_mkProd_or_LetIn ctx t :
   it_mkProd_or_LetIn (map trans_decl ctx) (trans t).
 Proof.
   induction ctx in t |- *; simpl; auto.
-  destruct a as [na [body|] ty]; simpl; auto.
+  destruct a as [na [body|] ty]; simpl.
   now rewrite IHctx.
   now rewrite IHctx.
 Qed.
@@ -572,7 +572,7 @@ Lemma trans_it_mkLambda_or_LetIn ctx t :
   it_mkLambda_or_LetIn (map trans_decl ctx) (trans t).
 Proof.
   induction ctx in t |- *; simpl; auto.
-  destruct a as [na [body|] ty]; simpl; auto.
+  destruct a as [na [body|] ty]; simpl.
   now rewrite IHctx.
   now rewrite IHctx.
 Qed.
@@ -638,7 +638,7 @@ Proof. simpl. reflexivity. Qed.
 Lemma trans_reln l p Γ : map trans (Ast.Env.reln l p Γ) = 
   reln (map trans l) p (trans_local Γ).
 Proof.
-  induction Γ as [|[na [b|] ty] Γ] in l, p |- *; simpl; auto.
+  induction Γ as [|[na [b|] ty] Γ] in l, p |- *; simpl; [auto..|].
   now rewrite IHΓ.
 Qed.
 

diff --git a/pcuic/theories/TemplateToPCUICWcbvEval.v b/pcuic/theories/TemplateToPCUICWcbvEval.v
@@ -116,7 +116,7 @@ Qed.
 Lemma csubst_mkApps a k f l : 
   csubst a k (mkApps f l) = mkApps (csubst a k f) (map (csubst a k) l).
 Proof.
-  induction l in f |- *; cbn; auto.
+  induction l in f |- *; cbn; [auto|].
   rewrite IHl.
   now cbn.
 Qed.

diff --git a/pcuic/theories/Typing/PCUICUnivSubstitutionTyp.v b/pcuic/theories/Typing/PCUICUnivSubstitutionTyp.v
@@ -300,7 +300,7 @@ Proof using Type.
       rewrite case_branch_type_fst.
       rewrite - !subst_instance_case_branch_context - !subst_instance_app_ctx.
       rewrite -subst_instance_case_predicate_context subst_instance_case_branch_type.
-      repeat split; auto.
+      repeat split; [auto..| |].
       * specialize (ihbod i univs wfext cu).
         cbn. eapply ihbod.
       * specialize (ihbty i univs wfext cu).

diff --git a/pcuic/theories/utils/PCUICAstUtils.v b/pcuic/theories/utils/PCUICAstUtils.v
@@ -150,7 +150,7 @@ Qed.
 
 Lemma mkApps_app f l l' : mkApps f (l ++ l') = mkApps (mkApps f l) l'.
 Proof.
-  induction l in f, l' |- *; destruct l'; simpl; rewrite ?app_nil_r; auto.
+  induction l in f, l' |- *; destruct l'; simpl; rewrite ?app_nil_r; [auto..|].
   rewrite IHl //.
 Qed.
 

diff --git a/safechecker/theories/PCUICEqualityDec.v b/safechecker/theories/PCUICEqualityDec.v
@@ -906,7 +906,7 @@ Proof.
   - apply forallb_All in wt; eapply All_mix in wt; try exact X; eapply All_All2 ; try exact wt;
     intros ? [? ?]; eauto.
   - revert s wt; move => ? /wf_universe_reflect ?; eauto.
-  - apply forallb_All in wt. apply All2_Forall2. induction u; eauto; cbn.
+  - apply forallb_All in wt. apply All2_Forall2. induction u; cbn.
     + eapply All2_nil.
     + cbn in wt. inversion wt; subst.  eapply All2_cons; eauto.
     clear -a H0 hRe; revert a H0; move => ? /wf_universe_reflect ?; eauto.

diff --git a/template-coq/theories/EnvMap.v b/template-coq/theories/EnvMap.v
@@ -183,7 +183,7 @@ Module EnvMap.
   Proof using Type.
     intros wf eq k. red in eq.
     move: eq.
-    induction g in e, k, wf |- *; auto.
+    induction g in e, k, wf |- *.
     - simpl. intros eq.
       unfold lookup.
       rewrite -KernameMapFact.F.not_find_in_iff.

diff --git a/template-coq/theories/utils/All_Forall.v b/template-coq/theories/utils/All_Forall.v
@@ -1160,7 +1160,7 @@ Proof.
   destruct n; simpl.
   - intros [= ->]. exists hd'; rewrite Nat.add_0_r; intuition auto.
   - exists t. intuition auto.
-  - destruct n; simpl; rewrite ?Nat.add_succ_r /=; auto.
+  - destruct n; simpl; rewrite ?Nat.add_succ_r /=.
     intros [= ->]. exists t; intuition auto.
     apply IHX.
 Qed.
@@ -3454,7 +3454,7 @@ Lemma All2_map2_left {A B C D} {P : A -> A -> Type} Q (R : B -> D -> Type) {f :
 Proof.
   intros hb ha hlen hPQ.
   induction ha in l, l''', hlen, hb |- *; simpl; try constructor; auto.
-  - destruct l => //. simpl. constructor.
+  - destruct l; simpl; constructor.
   - destruct l => //.
     noconf hlen. depelim hb.
     specialize (IHha _ _ hb H).