Commit ead22267 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Bump Coq, Iris & TLC.

parent 6f129507
......@@ -10,7 +10,7 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq" { (>= "8.14" & < "8.15~") | (= "dev") }
"coq-iris" { (= "dev.2021-12-09.1.f52f9f6a") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
"coq-tlc" { (= "20210316") }
]
......@@ -226,7 +226,7 @@ Section ThunkProofs.
eapply to_agree_op_valid_L, (proj1 (Cinr_valid (A:=unitR) _)). by rewrite Cinr_op.
Qed.
Instance Thunk'_persistent p t γv n R φ d :
Local Instance Thunk'_persistent p t γv n R φ d :
Persistent (Thunk' p t γv n R φ d).
Proof.
revert n φ. induction d ; exact _.
......
......@@ -414,7 +414,7 @@ Notation "'tickmatch:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
Typeclass instance for the proofmode
*)
Instance AsRecV_translationV `{Tick} v f x e :
Global Instance AsRecV_translationV `{Tick} v f x e :
AsRecV v f x e
AsRecV « v » f x « e ».
Proof. by intros ->. Qed.
......
......@@ -10,7 +10,7 @@ Class heapGpreS Σ := HeapGpreS {
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapGpreS Σ.
Global Instance subG_heapPreG {Σ} : subG heapΣ Σ heapGpreS Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapGpreS Σ} s e σ φ :
......
......@@ -59,7 +59,7 @@ Next Obligation.
split; unfold min_mach_int; lia.
Qed.
Instance mach_int_dec_eq :
Global Instance mach_int_dec_eq :
EqDecision mach_int.
Proof. apply sig_eq_dec; by apply _. Qed.
......@@ -87,10 +87,10 @@ Bind Scope binder_scope with binder.
Definition cons_binder (mx : binder) (X : list string) : list string :=
match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_eq_dec_eq : EqDecision binder.
Global Instance binder_eq_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
Instance set_unfold_cons_binder x mx X P :
Global Instance set_unfold_cons_binder x mx X P :
SetUnfold (x X) P SetUnfold (x mx :b: X) (BNamed x = mx P).
Proof.
constructor. rewrite -(set_unfold (x X) P).
......
......@@ -13,7 +13,7 @@ Class heapGS Σ := HeapGS {
heapG_gen_heapG :> gen_heapGS loc val Σ
}.
Instance heapG_irisG `{heapGS Σ} : irisGS heap_lang Σ := {
Global Instance heapG_irisG `{heapGS Σ} : irisGS heap_lang Σ := {
iris_invGS := heapG_invG;
state_interp σ _ κs _ := gen_heap_interp σ;
num_laters_per_step _ := 0%nat;
......
......@@ -109,8 +109,8 @@ Record Inv D F K R V : Prop := {
Inv_data : forall x, V x = V (R x)
}.
Hint Resolve is_rdsf_is_dsf : core.
Hint Resolve Inv_rdsf Inv_incl Inv_data : core.
Local Hint Resolve is_rdsf_is_dsf : core.
Local Hint Resolve Inv_rdsf Inv_incl Inv_data : core.
(* Throughout, we instantiate the parameter [r] of Alstrup et al.'s proof
with the value 1. Thus, we write just [Phi] for [Phi 1]. *)
......@@ -803,7 +803,7 @@ Proof using.
assert (z' = R y). { symmetry. eapply is_repr_incl_R; eauto. } subst z'.
forwards IH' : IH HI HM HB'; [math|done|].
iCombine "TCd TC" as "TC".
math_rewrite (11 * S d' + 6 = 11 * d' + 11 + 6)%nat ; first by lia.
math_rewrite (11 * S d' + 6 = 11 * d' + 11 + 6)%nat.
iDestruct "TC" as "[TCd TC]".
wp_apply (IH' with "[//] [$HM $TCd]").
iIntros (M') "[HM' hM']". iDestruct "hM'" as %HM'. wp_tick_let.
......@@ -852,8 +852,7 @@ Theorem get_spec : forall D R V x, x \in D ->
{{{ RET V x; UF D R V }}}.
Proof using.
introv Dx. iIntros "#?" (Φ) "!# [UF TC] HΦ".
math_rewrite (22 * alpha (card D) + 57 = 22 * alpha (card D) + 44 + 13)%nat ;
first by lia.
math_rewrite (22 * alpha (card D) + 57 = 22 * alpha (card D) + 44 + 13)%nat.
iDestruct "TC" as "[TC1 TC2]".
wp_tick_rec.
wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.
......@@ -885,8 +884,7 @@ Theorem set_spec : forall D R V x v,
{{{ RET #(); UF D R (update1 V R x «v»%V) }}}.
Proof using.
introv Dx. iIntros "#?" (Φ) "!# [UF TC] HΦ".
math_rewrite (22 * alpha (card D) + 62 = 22 * alpha (card D) + 44 + 18)%nat ;
first by lia.
math_rewrite (22 * alpha (card D) + 62 = 22 * alpha (card D) + 44 + 18)%nat.
iDestruct "TC" as "[TC1 TC2]".
wp_tick_rec. wp_tick_let. wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.
iIntros "UF". wp_tick_let. iDestruct "UF" as (F K M HI HM) "[HM TC]".
......@@ -919,8 +917,7 @@ Theorem eq_spec : forall D R V x y,
Proof using.
introv Dx Dy. iIntros "#?" (Φ) "!# [UF TC] HΦ".
math_rewrite (44 * alpha (card D) + 92 =
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 4)%nat ;
first by lia.
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 4)%nat.
iDestruct "TC" as "[[TC1 TC2] TC3]".
wp_tick_rec. wp_tick_let.
wp_apply (find_spec with "[//] [$TC1 $UF]")=>//. iIntros "UF".
......@@ -1075,8 +1072,7 @@ Theorem union_spec : forall D R V x y,
Proof using.
introv Hnmax Dx Dy.
math_rewrite (44 * alpha (card D) + 152 =
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 61 + 3)%nat ;
first by lia.
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 61 + 3)%nat.
iIntros "#?" (Φ) "!# [UF [[[TC1 TC2] TC3] TC4]] HΦ".
wp_tick_rec. wp_tick_let.
wp_apply (find_spec with "[//] [$TC1 $UF]")=>//. iIntros "UF".
......
......@@ -173,7 +173,7 @@ Proof using.
eauto using A_monotonic.
Qed.
Hint Resolve Akx_monotonic_in_k : monotonic typeclass_instances.
Global Hint Resolve Akx_monotonic_in_k : monotonic typeclass_instances.
(* Example. *)
......@@ -222,7 +222,7 @@ Proof using.
preserves_inflationary_Astep, preserves_monotonic_Astep.
Qed.
Hint Resolve Akx_monotonic_in_x Akx_monotonic_in_k : monotonic typeclass_instances.
Global Hint Resolve Akx_monotonic_in_x Akx_monotonic_in_k : monotonic typeclass_instances.
(* Example. *)
......@@ -375,7 +375,7 @@ Proof using.
eauto with monotonic.
Qed.
Hint Resolve Akx_tends_to_infinity_along_k : monotonic typeclass_instances.
Global Hint Resolve Akx_tends_to_infinity_along_k : monotonic typeclass_instances.
(* exploited in [InverseAckermann.v] *)
(* -------------------------------------------------------------------------- *)
......@@ -437,7 +437,7 @@ Proof using.
lia.
Qed.
Hint Resolve Akx_strictly_monotonic_in_k : monotonic typeclass_instances.
Global Hint Resolve Akx_strictly_monotonic_in_k : monotonic typeclass_instances.
(* -------------------------------------------------------------------------- *)
......
......@@ -12,7 +12,7 @@ From iris_time.union_find.math Require Import LibNatExtra Filter.
Definition towards_infinity (F : nat -> Prop) :=
exists m, forall n, m <= n -> F n.
Instance filter_towards_infinity : Filter towards_infinity.
Global Instance filter_towards_infinity : Filter towards_infinity.
Proof.
unfold towards_infinity. econstructor.
(* There exists an element in this filter, namely the universe, [le 0]. *)
......@@ -33,7 +33,7 @@ Proof.
unfold towards_infinity. eauto.
Qed.
Hint Resolve towards_infinity_le : filter.
Global Hint Resolve towards_infinity_le : filter.
(* The statement that [f x] tends towards infinity as [x] tends
towards infinity can be stated in its usual concrete form or
......
......@@ -20,7 +20,7 @@ Proof using.
eauto 8 with monotonic typeclass_instances.
Qed.
Hint Resolve alpha_monotonic : monotonic typeclass_instances.
Global Hint Resolve alpha_monotonic : monotonic typeclass_instances.
(* -------------------------------------------------------------------------- *)
......
......@@ -398,4 +398,4 @@ Qed.
End Inverse.
Hint Resolve alphaf_monotonic betaf_monotonic : monotonic typeclass_instances.
Global Hint Resolve alphaf_monotonic betaf_monotonic : monotonic typeclass_instances.
......@@ -59,7 +59,7 @@ Definition pointwise A B (okA : A -> Prop) (leB : B -> B -> Prop) (f g : A -> B)
(* TEMPORARY maybe this should be the *definition* of [monotonic] *)
Program Instance monotonic_Proper
Global Program Instance monotonic_Proper
A B (leA : A -> A -> Prop) (leB : B -> B -> Prop) (f : A -> B) :
monotonic leA leB f -> Proper (leA ++> leB) f.
......@@ -105,13 +105,13 @@ Qed.
ordering relation that appears in the premise can help apply
[lia] to the premise. *)
Hint Resolve (@use_monotonic nat le nat le) (@use_monotonic nat lt nat lt)
Global Hint Resolve (@use_monotonic nat le nat le) (@use_monotonic nat lt nat lt)
: monotonic typeclass_instances.
Hint Resolve (@use_monotonic_2 nat le nat le) (@use_monotonic_2 nat lt nat lt)
Global Hint Resolve (@use_monotonic_2 nat le nat le) (@use_monotonic_2 nat lt nat lt)
: monotonic typeclass_instances.
Hint Resolve (@use_inverse_monotonic nat le nat le)
Global Hint Resolve (@use_inverse_monotonic nat le nat le)
(@use_inverse_monotonic nat lt nat lt) : monotonic typeclass_instances.
(* -------------------------------------------------------------------------- *)
......@@ -180,7 +180,7 @@ Proof using.
{ assert (f x1 < f x2). eapply h; lia. lia. }
Qed.
Hint Resolve monotonic_lt_lt_implies_inverse_monotonic_le_le
Global Hint Resolve monotonic_lt_lt_implies_inverse_monotonic_le_le
monotonic_lt_lt_implies_monotonic_le_le : monotonic typeclass_instances.
Goal
......@@ -204,5 +204,5 @@ Proof using.
intros f ? x y ?. prove_lt_lt_by_contraposition. eauto.
Qed.
Hint Resolve monotonic_le_le_implies_inverse_monotonic_lt_lt :
Global Hint Resolve monotonic_le_le_implies_inverse_monotonic_lt_lt :
monotonic typeclass_instances.
......@@ -50,7 +50,7 @@ Qed.
(* Make [lia] a hint. *)
Hint Extern 1 => lia : lia.
Global Hint Extern 1 => lia : lia.
(* ---------------------------------------------------------------------------- *)
......@@ -122,7 +122,7 @@ Lemma mult_positive:
0 < m * n.
Proof using. lia. Qed.
Hint Resolve mult_positive : positive.
Global Hint Resolve mult_positive : positive.
Lemma mult_magnifies_left:
forall m n,
......@@ -305,9 +305,9 @@ Proof using.
intros m n. div2. lia.
Qed.
Hint Resolve prove_lt_div2_zero : positive.
Global Hint Resolve prove_lt_div2_zero : positive.
Hint Resolve prove_div2_le use_div2_plus1_le use_div2_le prove_le_div2
Global Hint Resolve prove_div2_le use_div2_plus1_le use_div2_le prove_le_div2
use_le_div2 prove_div2_lt use_div2_lt prove_lt_div2 use_lt_div2 :
div2.
......@@ -332,7 +332,7 @@ Proof using.
eauto using mult_positive.
Qed.
Hint Resolve power_positive : positive.
Global Hint Resolve power_positive : positive.
Lemma power_plus:
forall k1 k2 n,
......@@ -410,7 +410,7 @@ Proof using.
eapply f. lia. } (* ouf *)
Qed.
Hint Resolve power_monotonic_in_k power_strictly_monotonic_in_k
Global Hint Resolve power_monotonic_in_k power_strictly_monotonic_in_k
power_strictly_monotonic_in_n : monotonic typeclass_instances.
Lemma power_monotonic_in_n:
......@@ -422,7 +422,7 @@ Proof using.
{ eauto with monotonic lia. }
Qed.
Hint Resolve power_monotonic_in_n : monotonic typeclass_instances.
Global Hint Resolve power_monotonic_in_n : monotonic typeclass_instances.
(* TEMPORARY maybe explicitly use [inverse_monotonic] in lemmas below *)
......@@ -593,7 +593,7 @@ Proof using.
eapply power_strictly_inverse_monotonic_in_k_variant with (n := 2); simpl; lia.
Qed.
Hint Resolve log2_monotonic : monotonic typeclass_instances.
Global Hint Resolve log2_monotonic : monotonic typeclass_instances.
(* A collection of lemmas involving [log2] and ordering. *)
......@@ -631,7 +631,7 @@ Proof using.
eauto using Nat.le_lt_trans, pow_log2.
Qed.
Hint Resolve prove_le_log2 prove_log2_le prove_log2_lt : log2.
Global Hint Resolve prove_le_log2 prove_log2_le prove_log2_lt : log2.
(* An upper bound on [log2 n]. *)
......
......@@ -16,7 +16,7 @@ Ltac lia_rewrite P :=
(* Addition is covariant in both arguments. *)
Program Instance proper_plus: Proper (le ++> le ++> le) plus.
Global Program Instance proper_plus: Proper (le ++> le ++> le) plus.
Next Obligation.
intros x1 y1 h1 x2 y2 h2. lia.
Qed.
......@@ -24,14 +24,14 @@ Qed.
(* Subtraction is covariant in its first argument and contravariant in
its second argument. *)
Program Instance proper_minus: Proper (le ++> le --> le) minus.
Global Program Instance proper_minus: Proper (le ++> le --> le) minus.
Next Obligation.
unfold flip. intros x1 y1 h1 x2 y2 h2. lia.
Qed.
(* Multiplication is covariant in both arguments. *)
Program Instance proper_mult: Proper (le ++> le ++> le) mult.
Global Program Instance proper_mult: Proper (le ++> le ++> le) mult.
Next Obligation.
intros x1 y1 h1 x2 y2 h2.
rewrite Mult.mult_le_compat_l, Mult.mult_le_compat_r by eauto.
......@@ -40,14 +40,14 @@ Qed.
(* Maximum is covariant in both arguments. *)
Program Instance proper_max: Proper (le ++> le ++> le) max.
Global Program Instance proper_max: Proper (le ++> le ++> le) max.
Next Obligation.
intros x1 y1 h1 x2 y2 h2. do 2 max_case; lia.
Qed.
(* Strict ordering implies lax ordering. *)
Program Instance subrelation_lt_le: subrelation lt le.
Global Program Instance subrelation_lt_le: subrelation lt le.
Next Obligation.
intros x y h. lia.
Qed.
......@@ -66,7 +66,7 @@ Qed.
(* The lemma [eq_subrelation] is proved somewhere in the standard library,
but is not added to the type class database (why?). *)
Program Instance Eq_subrelation A (R : relation A) `{Reflexive A R} :
Global Program Instance Eq_subrelation A (R : relation A) `{Reflexive A R} :
subrelation eq R.
Next Obligation.
intros. eapply eq_subrelation; eauto.
......@@ -75,7 +75,7 @@ Qed.
(* The pointwise extension of a relation [R] is reflexive, symmetric, and
transitive, if [R] is. *)
Program Instance pointwise_relation_reflexive
Global Program Instance pointwise_relation_reflexive
A B (R : relation B) `{Reflexive B R} : Reflexive (pointwise_relation A R).
Next Obligation.
intro. reflexivity.
......@@ -87,7 +87,7 @@ Next Obligation.
repeat intro. eauto.
Qed.
Program Instance pointwise_relation_transitive
Global Program Instance pointwise_relation_transitive
A B (R : relation B) `{Transitive B R} : Transitive (pointwise_relation A R).
Next Obligation.
repeat intro. transitivity (y a); eauto.
......@@ -131,13 +131,13 @@ Abort. (* OK *) (* TEMPORARY *)
(* Rewriting lists up to permutations. *)
Program Instance app_permutation (A : Type) :
Global Program Instance app_permutation (A : Type) :
Proper (@Permutation A ++> @Permutation A ++> @Permutation A) (@app A).
Next Obligation.
repeat intro. eauto using Permutation_app.
Qed.
Program Instance map_permutation (A B : Type) (f : A -> B) :
Global Program Instance map_permutation (A B : Type) (f : A -> B) :
Proper (@Permutation A ++> @Permutation B) (@map A B f).
Next Obligation.
repeat intro. eauto using Permutation_map.
......
......@@ -57,7 +57,7 @@ Qed.
(* LibTactics local extension. *)
Hint Extern 1 (_ = _) => congruence : congruence.
Global Hint Extern 1 (_ = _) => congruence : congruence.
(* FRANCOIS: this should only be used for terminal goals *)
Ltac unpack := jauto_set_hyps; intros.
......@@ -102,7 +102,7 @@ Ltac exploit_functional F :=
(* Some lemmas that prove membership in a relation. *)
Hint Resolve union_l union_r prove_per_single : relations.
Global Hint Resolve union_l union_r prove_per_single : relations.
......@@ -112,7 +112,7 @@ Lemma tclosure_intro_right:
forall (A : Type) (R : binary A) y x z,
rtclosure R x y -> R y z -> tclosure R x z.
Proof using.
Hint Constructors tclosure : core.
Local Hint Constructors tclosure : core.
introv M N. induction M using rtclosure_ind_l; autos*.
Qed.
......@@ -142,7 +142,7 @@ Inductive kpath : nat -> binary A :=
forall y x z k,
R x y -> kpath k y z -> kpath (S k) x z.
Hint Constructors kpath : kpath.
Local Hint Constructors kpath : kpath.
Lemma kpath_rtclosure:
forall k x y,
......@@ -174,7 +174,7 @@ Qed.
End Closures.
Hint Resolve kpath_rtclosure : rtclosure.
Global Hint Resolve kpath_rtclosure : rtclosure.
From TLC Require Import LibList.
......@@ -281,7 +281,7 @@ Qed.
Lemma le_refl : refl Peano.le.
Proof using. intros_all; lia. Qed.
Hint Resolve le_refl : core.
Global Hint Resolve le_refl : core.
......@@ -312,7 +312,7 @@ Definition mmax `{Inhab A} (le:binary A) (P:A->Prop) :=
Lemma mmax_equiv : @mmax = @LibMin.mmax.
Proof using.
extens. intros. unfold mmax. rewrite~ <- mmax_inverse.
extens. intros. unfold mmax. rewrite <- mmax_inverse. reflexivity.
Qed.
Definition MMax `{Inhab A} `{Le A} := mmax le.
......@@ -334,7 +334,7 @@ Proof using. intros. apply notin_eq. Qed.
End Autorewrite.
Hint Rewrite notin_eq' : set_norm.
Global Hint Rewrite notin_eq' : set_norm.
(* ------------------------------------------------------------------------- *)
......@@ -405,7 +405,7 @@ Proof using. set_prove. Qed.
(* ------------------------------------------------------------------------- *)
Hint Rewrite disjoint_single_left_eq disjoint_single_right_eq subset_single_eq
Global Hint Rewrite disjoint_single_left_eq disjoint_single_right_eq subset_single_eq
@notin_eq @in_empty_eq @in_single_eq @in_union_eq @in_inter_eq @in_remove_eq : rew_set.
Tactic Notation "rew_set" "in" "*" :=
......@@ -414,19 +414,19 @@ Tactic Notation "rew_set" "in" "*" :=
(* ------------------------------------------------------------------------- *)
Program Instance Reflexive_incl A :
Global Program Instance Reflexive_incl A :
Reflexive (@LibContainer.incl _ (incl_inst A)).
Next Obligation.
eapply incl_refl; eauto.
Qed.
Program Instance Transitive_incl A :
Global Program Instance Transitive_incl A :
Transitive (@LibContainer.incl _ (incl_inst A)).
Next Obligation.
eapply incl_trans; eauto. typeclass.
Qed.
Program Instance Proper_inter_incl (A : Type) :
Global Program Instance Proper_inter_incl (A : Type) :
Proper (@LibContainer.incl _ (incl_inst A) ++>
@LibContainer.incl _ (incl_inst A) ++>
@LibContainer.incl _ (incl_inst A))
......@@ -560,7 +560,7 @@ Proof.
rew_set in *.
Qed.
Hint Resolve use_confined_left use_confined_right confined_union
Global Hint Resolve use_confined_left use_confined_right confined_union
confined_per_single confined_stclosure : confined.
Definition confine (A : Type) (D : set A) (F : binary A) : binary A :=
......@@ -621,7 +621,7 @@ Proof using.
unfold rel_incl, confine. intuition eauto.
Qed.
Hint Resolve confined_confine incl_confine : confined.
Global Hint Resolve confined_confine incl_confine : confined.
(* ------------------------------------------------------------------------- *)
......@@ -658,7 +658,7 @@ Proof using.
forwards: h. eauto. tauto.
Qed.
Hint Resolve use_sticky_left use_sticky_right : sticky.
Global Hint Resolve use_sticky_left use_sticky_right : sticky.
Lemma sticky_per_single:
forall (A : Type) (D : set A) x y,
......@@ -687,7 +687,7 @@ Proof using.
unfold sticky. induction 2. eauto. tauto. tauto.
Qed.
Hint Resolve sticky_per_single sticky_union sticky_stclosure : sticky.
Global Hint Resolve sticky_per_single sticky_union sticky_stclosure : sticky.
Lemma confine_stclosure:
forall (A : Type) (D : set A) (R : binary A),
......@@ -734,4 +734,4 @@ Qed.
(* ------------------------------------------------------------------------- *)
Hint Resolve tclosure_of_rtclosure_r : tclosure.
Global Hint Resolve tclosure_of_rtclosure_r : tclosure.
......@@ -79,9 +79,9 @@ Definition is_dsf_confined := proj31 is_dsf_F.
Definition is_dsf_functional := proj32 is_dsf_F.
Definition is_dsf_defined_is_repr := proj33 is_dsf_F.
Hint Resolve is_dsf_confined : confined.
Local Hint Resolve is_dsf_confined : confined.
Hint Resolve is_dsf_functional : functional.
Local Hint Resolve is_dsf_functional : functional.
(* -------------------------------------------------------------------------- *)
......@@ -153,7 +153,7 @@ Proof using is_dsf_F.
exploit_functional F; eauto.
Qed.
Hint Resolve functional_is_repr : functional.
Local Hint Resolve functional_is_repr : functional.
(* Two equivalent vertices must have the same representative. *)
......@@ -327,7 +327,7 @@ Proof using is_dsf_F.
tauto.
Qed.
Hint Resolve sticky_path sticky_is_repr sticky_is_equiv : sticky.
Local Hint Resolve sticky_path sticky_is_repr sticky_is_equiv : sticky.
Lemma is_equiv_in_D_direct:
forall x y,
......@@ -371,7 +371,7 @@ Lemma one_step_in_a_cycle:
Proof using is_dsf_F.
induction 1 using tclosure_ind_l; intros; subst; exploit_functional F.
applys~ tclosure_once.
eauto using tclosure_intro_right.
eauto using tclosure_intro_right, rtclosure_of_tclosure.
Qed.
(* Thus, a path cannot leave a cycle. *)
......@@ -749,23 +749,23 @@ Qed.
End DisjointSetForest.
Hint Resolve sticky_path sticky_is_repr sticky_is_equiv : sticky.
Global Hint Resolve sticky_path sticky_is_repr sticky_is_equiv : sticky.