Merge pull request #6 from coq-community/compat-8.17

Compatibility with 8.17 and beyond
coq-community · Oct 25, 2022 · 5e3d544 · 5e3d544
2 parents 00611ae + ce40f18
commit 5e3d544
Show file tree

Hide file tree

Showing 17 changed files with 233 additions and 228 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,10 +17,10 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'coqorg/coq:dev'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'
           - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.13'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

diff --git a/AVL.v b/AVL.v
@@ -380,7 +380,7 @@ Implicit Types m r : t elt.
 
 (** * Helper functions *)
 
-Global Instance create_ok l x e r `{!Ok l, !Ok r} :
+#[export] Instance create_ok l x e r `{!Ok l, !Ok r} :
  l < x -> x < r -> Ok (create l x e r).
 Proof.
  unfold create; autok.
@@ -398,11 +398,11 @@ Proof.
  apply bindings_node.
 Qed.
 
-Global Instance bal_ok l x e r `{!Ok l, !Ok r} :
+#[export] Instance bal_ok l x e r `{!Ok l, !Ok r} :
  l < x -> x < r -> Ok (bal l x e r).
 Proof.
  functional induction (bal l x e r); intros; cleanf; invok; invlt;
- repeat apply create_ok; rewrite ?above_node, ?below_node; intuition;
+ repeat apply create_ok; rewrite ?above_node, ?below_node; intuition (auto with map);
  intro; rewrite create_in; intuition; order.
 Qed.
 
@@ -441,7 +441,7 @@ Proof.
  unfold singleton. now rewrite bindings_node.
 Qed.
 
-Global Instance singleton_ok x (e:elt) : Ok (singleton x e).
+#[export] Instance singleton_ok x (e:elt) : Ok (singleton x e).
 Proof.
  unfold singleton. autok.
 Qed.
@@ -466,7 +466,7 @@ Proof.
 Qed.
 Local Hint Resolve add_lt add_gt : map.
 
-Global Instance add_ok m x e `{!Ok m} : Ok (add x e m).
+#[export] Instance add_ok m x e `{!Ok m} : Ok (add x e m).
 Proof.
  functional induction (add x e m); intros; cleanf; invok; autok.
 Qed.
@@ -580,7 +580,7 @@ Proof.
  intros z. rewrite bal_in. intuition; order.
 Qed.
 
-Global Instance remove_min_ok m m' p `{!Ok m} : RemoveMin m (m',p) -> Ok m'.
+#[export] Instance remove_min_ok m m' p `{!Ok m} : RemoveMin m (m',p) -> Ok m'.
 Proof.
  revert m'.
  induction m as [|h l IH x e r _]; [destruct 1|].
@@ -647,7 +647,7 @@ Proof.
  unfold In. setoid_rewrite append_mapsto. firstorder.
 Qed.
 
-Global Instance append_ok m1 m2 `{!Ok m1, !Ok m2} : m1 < m2 ->
+#[export] Instance append_ok m1 m2 `{!Ok m1, !Ok m2} : m1 < m2 ->
  Ok (append m1 m2).
 Proof.
  functional induction (append m1 m2); intros B12; trivial.
@@ -677,15 +677,15 @@ Proof.
 Qed.
 Local Hint Resolve remove_gt remove_lt : map.
 
-Global Instance remove_ok m x `{!Ok m} : Ok (remove x m).
+#[export] Instance remove_ok m x `{!Ok m} : Ok (remove x m).
 Proof.
  functional induction (remove x m); simpl; intros; cleanf; invok; autok.
  apply append_ok; eauto using between.
 Qed.
 
 Lemma remove_spec1 m x `{!Ok m} : find x (remove x m) = None.
 Proof.
- intros. apply not_find_iff; autok. rewrite remove_in; intuition.
+ intros. apply not_find_iff; autok. rewrite remove_in; intuition (auto with map).
 Qed.
 
 Lemma remove_spec2 m x y `{!Ok m} : ~ x == y ->
@@ -712,7 +712,7 @@ Proof.
  - apply create_in.
 Qed.
 
-Global Instance join_ok l x d r :
+#[export] Instance join_ok l x d r :
  Ok (create l x d r) -> Ok (join l x d r).
 Proof.
   join_tac l x d r; unfold create in *; invok; invok; invlt; autok.
@@ -827,14 +827,16 @@ Proof.
 Qed.
 Local Hint Resolve split_lt_l split_lt_r split_gt_l split_gt_r : map.
 
-Global Instance split_ok_l m x `{!Ok m} : Ok (split x m)#l.
+#[export] Instance split_ok_l m x `{!Ok m} : Ok (split x m)#l.
 Proof.
-  functional induction (split x m); intros; cleansplit; intuition.
+  functional induction (split x m); intros; cleansplit;
+   intuition (auto with map typeclass_instances).
 Qed.
 
-Global Instance split_ok_r m x `{!Ok m} : Ok (split x m)#r.
+#[export] Instance split_ok_r m x `{!Ok m} : Ok (split x m)#r.
 Proof.
-  functional induction (split x m); intros; cleansplit; intuition.
+  functional induction (split x m); intros; cleansplit;
+   intuition (auto with map typeclass_instances).
 Qed.
 
 Lemma split_find m x y `{!Ok m} :
@@ -865,7 +867,7 @@ Proof.
    rewrite join_in, (remove_min_in R); simpl; intuition.
 Qed.
 
-Global Instance concat_ok m1 m2 `{!Ok m1, !Ok m2} : m1 < m2 ->
+#[export] Instance concat_ok m1 m2 `{!Ok m1, !Ok m2} : m1 < m2 ->
  Ok (concat m1 m2).
 Proof.
   functional induction (concat m1 m2); intros LT; auto;
@@ -922,7 +924,7 @@ Proof.
  case (f y d); rewrite ?join_in, ?concat_in; intuition_in.
 Qed.
 
-Global Instance filter_ok f (m:t elt) `(!Ok m) : Ok (filter f m).
+#[export] Instance filter_ok f (m:t elt) `(!Ok m) : Ok (filter f m).
 Proof.
  induction m as [|h l IHl x e r IHr]; simpl; autok.
  invok. case (f x e).
@@ -961,12 +963,12 @@ Proof.
  now destruct (partition f l), (partition f r), f.
 Qed.
 
-Instance partition_ok1 f (m:t elt) : Ok m -> Ok (fst (partition f m)).
+#[export] Instance partition_ok1 f (m:t elt) : Ok m -> Ok (fst (partition f m)).
 Proof.
  rewrite partition_fst; eauto with *.
 Qed.
 
-Instance partition_ok2 f (m:t elt) : Ok m -> Ok (snd (partition f m)).
+#[export] Instance partition_ok2 f (m:t elt) : Ok m -> Ok (snd (partition f m)).
 Proof.
  rewrite partition_snd; eauto with *.
 Qed.
@@ -1015,7 +1017,7 @@ Proof.
 Qed.
 Local Hint Resolve mapo_lt mapo_gt : map.
 
-Global Instance mapo_ok m `{!Ok m} : Ok (mapo f m).
+#[export] Instance mapo_ok m `{!Ok m} : Ok (mapo f m).
 Proof.
 functional induction (mapo f m); simpl; autok; invok.
 - apply join_ok, create_ok; autok.
@@ -1110,11 +1112,11 @@ Qed.
 Local Hint Resolve gmerge_lt gmerge_gt : map.
 Local Hint Resolve split_ok_l split_ok_r split_lt_l split_gt_r : map.
 
-Global Instance gmerge_ok m m' `{!Ok m, !Ok m'} : Ok (gmerge m m').
+#[export] Instance gmerge_ok m m' `{!Ok m, !Ok m'} : Ok (gmerge m m').
 Proof.
   functional induction (gmerge m m'); auto; factornode m2; invok;
   (apply join_ok, create_ok || apply concat_ok);
-  revert IHt2 IHt0; cleansplit; intuition.
+  revert IHt2 IHt0; cleansplit; intuition (auto with map).
   apply between with x1; autom.
 Qed.
 
@@ -1186,7 +1188,7 @@ Section Merge.
 Variable elt elt' elt'' : Type.
 Variable f : key -> option elt -> option elt' -> option elt''.
 
-Global Instance merge_ok m m' `{!Ok m, !Ok m'} : Ok (merge f m m').
+#[export] Instance merge_ok m m' `{!Ok m, !Ok m'} : Ok (merge f m m').
 Proof.
 unfold merge; intros.
 apply gmerge_ok with f;

diff --git a/AVLproofs.v b/AVLproofs.v
@@ -46,7 +46,7 @@ Inductive avl elt : tree elt -> Prop :=
 
 Class Avl elt (t:tree elt) : Prop := mkAvl : avl t.
 
-Instance avl_Avl elt (s:tree elt) (Hs : avl s) : Avl s := Hs.
+#[export] Instance avl_Avl elt (s:tree elt) (Hs : avl s) : Avl s := Hs.
 
 (** * Automation and dedicated tactics *)
 
@@ -289,14 +289,14 @@ Local Hint Resolve avl_node : map.
 
 (** empty *)
 
-Instance empty_avl : Avl (empty elt).
+#[export] Instance empty_avl : Avl (empty elt).
 Proof.
  autok.
 Qed.
 
 (** singleton *)
 
-Instance singleton_avl x e : Avl (singleton x e).
+#[export] Instance singleton_avl x e : Avl (singleton x e).
 Proof.
  unfold singleton. constructor; autom; simpl; lia_max.
 Qed.
@@ -370,7 +370,7 @@ Proof.
  induct s; inv_avl.
  - intuition; try constructor; simpl; autom; lia_max.
  - (* Eq *)
-   simpl. intuition; lia_max.
+   simpl. intuition (auto with map typeclass_instances); lia_max.
  - (* Lt *)
    destruct (IHl x e); trivial.
    split.
@@ -383,7 +383,7 @@ Proof.
    * lia_bal.
 Qed.
 
-Instance add_avl s x e `{!Avl s} : Avl (add x e s).
+#[export] Instance add_avl s x e `{!Avl s} : Avl (add x e s).
 Proof.
  now destruct (@add_avl_1 s x e).
 Qed.
@@ -439,7 +439,7 @@ Proof.
    * rewrite create_height; trivial; lia_max.
 Qed.
 
-Instance join_avl l x e r `{!Avl l, !Avl r} : Avl (join l x e r).
+#[export] Instance join_avl l x e r `{!Avl l, !Avl r} : Avl (join l x e r).
 Proof.
  now destruct (@join_avl_1 l x e r).
 Qed.
@@ -460,7 +460,7 @@ Proof.
    * lia_bal.
 Qed.
 
-Instance remove_min_avl l x e r h `{!Avl (Node h l x e r)} :
+#[export] Instance remove_min_avl l x e r h `{!Avl (Node h l x e r)} :
   Avl (remove_min l x e r)#1.
 Proof.
  now destruct (@remove_min_avl_1 l x e r h).
@@ -497,7 +497,7 @@ Lemma remove_avl_1 : forall s x `{!Avl s},
  Avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
 Proof.
  induct s; inv_avl.
- - intuition; lia_max.
+ - intuition (auto with map typeclass_instances); lia_max.
  - (* Eq *)
    generalize (@append_avl_1 l r).
    intuition lia_max.
@@ -513,14 +513,14 @@ Proof.
    * lia_bal.
 Qed.
 
-Instance remove_avl s x `{!Avl s} : Avl (remove x s).
+#[export] Instance remove_avl s x `{!Avl s} : Avl (remove x s).
 Proof.
  now destruct (@remove_avl_1 s x).
 Qed.
 
 (** concat *)
 
-Instance concat_avl s1 s2 `{!Avl s1, !Avl s2} : Avl (concat s1 s2).
+#[export] Instance concat_avl s1 s2 `{!Avl s1, !Avl s2} : Avl (concat s1 s2).
 Proof.
  functional induction (concat s1 s2); auto.
  apply join_avl; auto.
@@ -534,27 +534,27 @@ Lemma split_avl : forall s x `{!Avl s},
 Proof.
  intros s x. functional induction (split x s); simpl; auto.
  - intros. inv_avl; auto.
- - mysubst; simpl in *; inversion_clear 1; intuition.
- - mysubst; simpl in *; inversion_clear 1; intuition.
+ - mysubst; simpl in *; inversion_clear 1; intuition (auto with map typeclass_instances).
+ - mysubst; simpl in *; inversion_clear 1; intuition (auto with map typeclass_instances).
 Qed.
 
 (** filter *)
 
-Instance filter_avl (f:key->elt->bool) m `{!Avl m} : Avl (filter f m).
+#[export] Instance filter_avl (f:key->elt->bool) m `{!Avl m} : Avl (filter f m).
 Proof.
  induction m; simpl; auto. inv_avl.
  destruct f; [apply join_avl | apply concat_avl ]; auto.
 Qed.
 
-Instance partition_avl1 (f:key->elt->bool) m `{!Avl m} :
+#[export] Instance partition_avl1 (f:key->elt->bool) m `{!Avl m} :
  Avl (fst (partition f m)).
 Proof.
  induction m; simpl; auto. inv_avl.
  destruct partition, partition, f; simpl in *;
  [apply join_avl | apply concat_avl]; auto.
 Qed.
 
-Instance partition_avl2 (f:key->elt->bool) m `{!Avl m} :
+#[export] Instance partition_avl2 (f:key->elt->bool) m `{!Avl m} :
  Avl (snd (partition f m)).
 Proof.
  induction m; simpl; auto. inv_avl.
@@ -569,9 +569,9 @@ Proof.
  induction m; simpl; auto.
 Qed.
 
-Instance map_avl {elt elt'}(f:elt->elt') m `(!Avl m) : Avl (map f m).
+#[export] Instance map_avl {elt elt'}(f:elt->elt') m `(!Avl m) : Avl (map f m).
 Proof.
- induction m; simpl; inv_avl; intuition.
+ induction m; simpl; inv_avl; intuition (auto with map typeclass_instances).
  constructor; intuition; rewrite ?map_height; auto.
 Qed.
 
@@ -581,16 +581,16 @@ Proof.
  induction m; simpl; auto.
 Qed.
 
-Instance mapi_avl {elt elt'}(f:key->elt->elt') m `(!Avl m) : Avl (mapi f m).
+#[export] Instance mapi_avl {elt elt'}(f:key->elt->elt') m `(!Avl m) : Avl (mapi f m).
 Proof.
- induction m; simpl; inv_avl; intuition.
+ induction m; simpl; inv_avl; intuition (auto with map typeclass_instances).
  constructor; intuition; rewrite ?mapi_height; auto.
 Qed.
 
-Instance mapo_avl {elt elt'}(f:key->elt->option elt') m `{!Avl m} :
+#[export] Instance mapo_avl {elt elt'}(f:key->elt->option elt') m `{!Avl m} :
   Avl (mapo f m).
 Proof.
- induction m; simpl; inv_avl; intuition.
+ induction m; simpl; inv_avl; intuition (auto with map typeclass_instances).
  destruct f.
  - apply join_avl; auto.
  - apply concat_avl; auto.
@@ -604,7 +604,7 @@ Variable mapr : t elt' -> t elt''.
 Hypothesis mapl_avl : forall m, Avl m -> Avl (mapl m).
 Hypothesis mapr_avl : forall m', Avl m' -> Avl (mapr m').
 
-Instance gmerge_avl m m' `{!Avl m, !Avl m'} :
+#[export] Instance gmerge_avl m m' `{!Avl m, !Avl m'} :
   Avl (gmerge f mapl mapr m m').
 Proof.
   functional induction (gmerge f mapl mapr m m');
@@ -614,7 +614,7 @@ Proof.
 Qed.
 End Gmerge.
 
-Instance merge_avl {elt elt' elt''}
+#[export] Instance merge_avl {elt elt' elt''}
  (f:key -> option elt -> option elt' -> option elt'') m m'
  `(!Avl m, !Avl m') :
    Avl (merge f m m').

diff --git a/Comparisons.v b/Comparisons.v
@@ -94,7 +94,7 @@ Proof.
    + rewrite tra; eauto. easy.
 Qed.
 
-Global Instance pair_compare_st :
+#[export] Instance pair_compare_st :
   SymTrans cmpA -> SymTrans cmpB -> SymTrans pair_compare.
 Proof.
  constructor.
@@ -145,7 +145,7 @@ Proof.
  - intros <- _. rewrite tra; eauto. easy.
 Qed.
 
-Global Instance list_compare_st : SymTrans cmp -> SymTrans list_compare.
+#[export] Instance list_compare_st : SymTrans cmp -> SymTrans list_compare.
 Proof.
  constructor. apply list_compare_sym, sym. now apply list_compare_trans.
 Qed.
@@ -225,7 +225,7 @@ Fixpoint list_ecompare (l1 l2 : list A) : comparison*flag :=
  induction u; destruct u'; intros GT LT; cbn; auto.
  - destruct v; simpl in *; auto. rewrite GT; auto.
  - destruct v'; simpl in *; auto. rewrite LT; auto.
- - case cmp; intuition.
+ - case cmp; intuition (auto with datatypes).
  Qed.
 
 End ListExtComp.