Skip to content

Commit 5d79bbc

Browse files
mattam82mattam82
authored
Merge pull request MetaRocq#837 from JasonGross/coq-8.16+dec
Add some utility tactics and decidability properties
2 parents f744ab6 + 850a39b commit 5d79bbc

18 files changed

+804
-11
lines changed

‎common/_CoqProject.in

+1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ theories/uGraph.v
55
theories/config.v
66
theories/Kernames.v
77
theories/Universes.v
8+
theories/UniversesDec.v
89
theories/BasicAst.v
910
theories/Environment.v
1011
theories/Reflect.v

‎common/theories/EnvironmentTyping.v

+13
Original file line numberDiff line numberDiff line change
@@ -285,6 +285,19 @@ Module Lookup (T : Term) (E : EnvironmentSig T).
285285
(fun u => forall l, LevelExprSet.In l u -> LevelSet.In (LevelExpr.get_level l) (global_ext_levels Σ))
286286
True s.
287287

288+
Definition wf_universe_dec Σ s : {@wf_universe Σ s} + {~@wf_universe Σ s}.
289+
Proof.
290+
destruct s; try (left; exact I).
291+
cbv [wf_universe Universe.on_sort LevelExprSet.In LevelExprSet.this t_set].
292+
destruct t as [[t _] _].
293+
induction t as [|t ts [IHt|IHt]]; [ left | | right ].
294+
{ inversion 1. }
295+
{ destruct (LevelSetProp.In_dec (LevelExpr.get_level t) (global_ext_levels Σ)) as [H|H]; [ left | right ].
296+
{ inversion 1; subst; auto. }
297+
{ intro H'; apply H, H'; now constructor. } }
298+
{ intro H; apply IHt; intros; apply H; now constructor. }
299+
Defined.
300+
288301
Lemma declared_ind_declared_constructors `{cf : checker_flags} {Σ ind mib oib} :
289302
declared_inductive Σ ind mib oib ->
290303
Alli (fun i => declared_constructor Σ (ind, i) mib oib) 0 (ind_ctors oib).

‎common/theories/UniversesDec.v

+203
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,203 @@
1+
From MetaCoq.Utils Require Import MCList MCOption MCUtils.
2+
From MetaCoq.Common Require Import uGraph.
3+
From MetaCoq.Common Require Import Universes.
4+
Import wGraph.
5+
6+
Definition levels_of_cs (cstr : ConstraintSet.t) : LevelSet.t
7+
:= ConstraintSet.fold (fun '(l1, _, l2) acc => LevelSet.add l1 (LevelSet.add l2 acc)) cstr (LevelSet.singleton Level.lzero).
8+
Lemma levels_of_cs_spec cstr (lvls := levels_of_cs cstr)
9+
: uGraph.global_uctx_invariants (lvls, cstr).
10+
Proof.
11+
subst lvls; cbv [levels_of_cs].
12+
cbv [uGraph.global_uctx_invariants uGraph.uctx_invariants ConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
13+
repeat first [ apply conj
14+
| progress intros
15+
| progress destruct ?
16+
| match goal with
17+
| [ |- ?x \/ ?y ]
18+
=> first [ lazymatch x with context[LevelSet.In ?l (LevelSet.singleton ?l)] => idtac end;
19+
left
20+
| lazymatch y with context[LevelSet.In ?l (LevelSet.singleton ?l)] => idtac end;
21+
right ]
22+
| [ H : ConstraintSet.In ?l ?c |- ?x \/ ?y ]
23+
=> first [ lazymatch x with context[LevelSet.In _ (ConstraintSet.fold _ c _)] => idtac end;
24+
left
25+
| lazymatch y with context[LevelSet.In _ (ConstraintSet.fold _ c _)] => idtac end;
26+
right ]
27+
end
28+
| rewrite !LevelSet.union_spec
29+
| progress rewrite <- ?ConstraintSet.elements_spec1, ?InA_In_eq in *
30+
| rewrite ConstraintSetProp.fold_spec_right ].
31+
all: lazymatch goal with
32+
| [ |- LevelSet.In Level.lzero (List.fold_right ?f ?init ?ls) ]
33+
=> first [ LevelSetDecide.fsetdec
34+
| cut (LevelSet.In Level.lzero init);
35+
[ generalize init; induction ls; intros; cbn in *
36+
| LevelSetDecide.fsetdec ] ]
37+
| [ H : List.In ?v ?ls |- LevelSet.In ?v' (List.fold_right ?f ?init (List.rev ?ls)) ]
38+
=> rewrite List.in_rev in H;
39+
let ls' := fresh "ls" in
40+
set (ls' := List.rev ls);
41+
change (List.In v ls') in H;
42+
change (LevelSet.In v' (List.fold_right f init ls'));
43+
generalize init; induction ls'; cbn in *
44+
end.
45+
all: repeat first [ exfalso; assumption
46+
| progress destruct_head'_or
47+
| progress subst
48+
| progress intros
49+
| progress destruct ?
50+
| rewrite !LevelSetFact.add_iff
51+
| solve [ auto ] ].
52+
Qed.
53+
54+
Definition consistent_dec ctrs : {@consistent ctrs} + {~@consistent ctrs}.
55+
Proof.
56+
pose proof (@uGraph.is_consistent_spec config.default_checker_flags (levels_of_cs ctrs, ctrs) (levels_of_cs_spec ctrs)) as H.
57+
destruct uGraph.is_consistent; [ left; apply H | right; intro H'; apply H in H' ]; auto.
58+
Defined.
59+
60+
Definition levels_of_cs2 (cs1 cs2 : ConstraintSet.t) : LevelSet.t
61+
:= LevelSet.union (levels_of_cs cs1) (levels_of_cs cs2).
62+
Lemma levels_of_cs2_spec cs1 cs2 (lvls := levels_of_cs2 cs1 cs2)
63+
: uGraph.global_uctx_invariants (lvls, cs1)
64+
/\ uGraph.global_uctx_invariants (lvls, cs2).
65+
Proof.
66+
split; apply global_uctx_invariants_union_or; constructor; apply levels_of_cs_spec.
67+
Qed.
68+
69+
Definition levels_of_cscs (cs : ContextSet.t) (cstr : ConstraintSet.t) : LevelSet.t
70+
:= LevelSet.union (ContextSet.levels cs) (levels_of_cs2 cstr (ContextSet.constraints cs)).
71+
Lemma levels_of_cscs_spec cs cstr (lvls := levels_of_cscs cs cstr)
72+
: uGraph.global_uctx_invariants (lvls, ContextSet.constraints cs)
73+
/\ uGraph.global_uctx_invariants (lvls, cstr).
74+
Proof.
75+
generalize (levels_of_cs2_spec cstr (ContextSet.constraints cs)).
76+
split; apply global_uctx_invariants_union_or; constructor; apply levels_of_cs2_spec.
77+
Qed.
78+
79+
Definition levels_of_algexpr (u : LevelAlgExpr.t) : VSet.t
80+
:= LevelExprSet.fold
81+
(fun gc acc => match LevelExpr.get_noprop gc with
82+
| Some l => VSet.add l acc
83+
| None => acc
84+
end)
85+
u
86+
VSet.empty.
87+
Lemma levels_of_algexpr_spec u cstr (lvls := levels_of_algexpr u)
88+
: gc_levels_declared (lvls, cstr) u.
89+
Proof.
90+
subst lvls; cbv [levels_of_algexpr gc_levels_declared gc_expr_declared on_Some_or_None LevelExpr.get_noprop]; cbn [fst snd].
91+
cbv [LevelExprSet.For_all]; cbn [fst snd].
92+
repeat first [ apply conj
93+
| progress intros
94+
| progress destruct ?
95+
| exact I
96+
| progress rewrite <- ?LevelExprSet.elements_spec1, ?InA_In_eq in *
97+
| rewrite LevelExprSetProp.fold_spec_right ].
98+
all: lazymatch goal with
99+
| [ H : List.In ?v ?ls |- VSet.In ?v' (List.fold_right ?f ?init (List.rev ?ls)) ]
100+
=> rewrite List.in_rev in H;
101+
let ls' := fresh "ls" in
102+
set (ls' := List.rev ls);
103+
change (List.In v ls') in H;
104+
change (VSet.In v' (List.fold_right f init ls'));
105+
generalize init; induction ls'; cbn in *
106+
end.
107+
all: repeat first [ exfalso; assumption
108+
| progress destruct_head'_or
109+
| progress subst
110+
| progress intros
111+
| progress destruct ?
112+
| rewrite !VSetFact.add_iff
113+
| solve [ auto ] ].
114+
Qed.
115+
116+
Definition leq0_levelalg_n_dec n ϕ u u' : {@leq0_levelalg_n (uGraph.Z_of_bool n) ϕ u u'} + {~@leq0_levelalg_n (uGraph.Z_of_bool n) ϕ u u'}.
117+
Proof.
118+
pose proof (@uGraph.gc_leq0_levelalg_n_iff config.default_checker_flags (uGraph.Z_of_bool n) ϕ u u') as H.
119+
pose proof (@uGraph.gc_consistent_iff config.default_checker_flags ϕ).
120+
cbv [on_Some on_Some_or_None] in *.
121+
destruct gc_of_constraints eqn:?.
122+
all: try solve [ left; cbv [consistent] in *; hnf; intros; exfalso; intuition eauto ].
123+
pose proof (fun G cstr => @uGraph.leqb_levelalg_n_spec G (LevelSet.union (levels_of_cs ϕ) (LevelSet.union (levels_of_algexpr u) (levels_of_algexpr u')), cstr)).
124+
pose proof (fun x y => @gc_of_constraints_of_uctx config.default_checker_flags (x, y)) as H'.
125+
pose proof (@is_consistent_spec config.default_checker_flags (levels_of_cs ϕ, ϕ)).
126+
specialize_under_binders_by eapply gc_levels_declared_union_or.
127+
specialize_under_binders_by eapply global_gc_uctx_invariants_union_or.
128+
specialize_under_binders_by (constructor; eapply gc_of_uctx_invariants).
129+
cbn [fst snd] in *.
130+
specialize_under_binders_by eapply H'.
131+
specialize_under_binders_by eassumption.
132+
specialize_under_binders_by eapply levels_of_cs_spec.
133+
specialize_under_binders_by reflexivity.
134+
destruct is_consistent;
135+
[ | left; now cbv [leq0_levelalg_n consistent] in *; intros; exfalso; intuition eauto ].
136+
specialize_by intuition eauto.
137+
let H := match goal with H : forall (b : bool), _ |- _ => H end in
138+
specialize (H n u u').
139+
specialize_under_binders_by (constructor; eapply gc_levels_declared_union_or; constructor; eapply levels_of_algexpr_spec).
140+
match goal with H : is_true ?b <-> ?x, H' : ?y <-> ?x |- {?y} + {_} => destruct b eqn:?; [ left | right ] end.
141+
all: intuition.
142+
Defined.
143+
144+
Definition leq_levelalg_n_dec cf n ϕ u u' : {@leq_levelalg_n cf (uGraph.Z_of_bool n) ϕ u u'} + {~@leq_levelalg_n cf (uGraph.Z_of_bool n) ϕ u u'}.
145+
Proof.
146+
cbv [leq_levelalg_n]; destruct (@leq0_levelalg_n_dec n ϕ u u'); destruct ?; auto.
147+
Defined.
148+
149+
Definition eq0_levelalg_dec ϕ u u' : {@eq0_levelalg ϕ u u'} + {~@eq0_levelalg ϕ u u'}.
150+
Proof.
151+
pose proof (@eq0_leq0_levelalg ϕ u u') as H.
152+
destruct (@leq0_levelalg_n_dec false ϕ u u'), (@leq0_levelalg_n_dec false ϕ u' u); constructor; destruct H; split_and; now auto.
153+
Defined.
154+
155+
Definition eq_levelalg_dec {cf ϕ} u u' : {@eq_levelalg cf ϕ u u'} + {~@eq_levelalg cf ϕ u u'}.
156+
Proof.
157+
cbv [eq_levelalg]; destruct ?; auto using eq0_levelalg_dec.
158+
Defined.
159+
160+
Definition eq_universe__dec {CS eq_levelalg ϕ}
161+
(eq_levelalg_dec : forall u u', {@eq_levelalg ϕ u u'} + {~@eq_levelalg ϕ u u'})
162+
s s'
163+
: {@eq_universe_ CS eq_levelalg ϕ s s'} + {~@eq_universe_ CS eq_levelalg ϕ s s'}.
164+
Proof.
165+
cbv [eq_universe_]; repeat destruct ?; auto.
166+
Defined.
167+
168+
Definition eq_universe_dec {cf ϕ} s s' : {@eq_universe cf ϕ s s'} + {~@eq_universe cf ϕ s s'} := eq_universe__dec eq_levelalg_dec _ _.
169+
170+
Definition valid_constraints_dec cf ϕ cstrs : {@valid_constraints cf ϕ cstrs} + {~@valid_constraints cf ϕ cstrs}.
171+
Proof.
172+
pose proof (fun G a b c => uGraph.check_constraints_spec (uGraph.make_graph G) (levels_of_cs2 ϕ cstrs, ϕ) a b c cstrs) as H1.
173+
pose proof (fun G a b c => uGraph.check_constraints_complete (uGraph.make_graph G) (levels_of_cs2 ϕ cstrs, ϕ) a b c cstrs) as H2.
174+
pose proof (levels_of_cs2_spec ϕ cstrs).
175+
cbn [fst snd] in *.
176+
destruct (consistent_dec ϕ); [ | now left; cbv [valid_constraints valid_constraints0 consistent not] in *; destruct ?; intros; eauto; exfalso; eauto ].
177+
destruct_head'_and.
178+
specialize_under_binders_by assumption.
179+
cbv [uGraph.is_graph_of_uctx MCOption.on_Some] in *.
180+
cbv [valid_constraints] in *; repeat destruct ?; auto.
181+
{ specialize_under_binders_by reflexivity.
182+
destruct uGraph.check_constraints_gen; specialize_by reflexivity; auto. }
183+
{ rewrite uGraph.gc_consistent_iff in *.
184+
cbv [uGraph.gc_of_uctx monad_utils.bind monad_utils.ret monad_utils.option_monad MCOption.on_Some] in *; cbn [fst snd] in *.
185+
destruct ?.
186+
all: try congruence.
187+
all: exfalso; assumption. }
188+
Defined.
189+
190+
Definition valid_constraints0_dec ϕ ctrs : {@valid_constraints0 ϕ ctrs} + {~@valid_constraints0 ϕ ctrs}
191+
:= @valid_constraints_dec config.default_checker_flags ϕ ctrs.
192+
193+
Definition is_lSet_dec cf ϕ s : {@is_lSet cf ϕ s} + {~@is_lSet cf ϕ s}.
194+
Proof.
195+
apply eq_universe_dec.
196+
Defined.
197+
198+
Definition is_allowed_elimination_dec cf ϕ allowed u : {@is_allowed_elimination cf ϕ allowed u} + {~@is_allowed_elimination cf ϕ allowed u}.
199+
Proof.
200+
cbv [is_allowed_elimination is_true]; destruct ?; auto;
201+
try solve [ repeat decide equality ].
202+
destruct (@is_lSet_dec cf ϕ u), is_propositional; intuition auto.
203+
Defined.

‎common/theories/uGraph.v

+64-11
Original file line numberDiff line numberDiff line change
@@ -1429,7 +1429,7 @@ Section CheckLeq.
14291429
gc_expr_declared e' ->
14301430
leqb_expr_n_gen leqb_level_n_gen lt e e' ->
14311431
gc_leq0_levelalg_n lt uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
1432-
Proof.
1432+
Proof using Type.
14331433
unfold leqb_expr_n.
14341434
destruct e as [l k], e' as [l' k'];
14351435
try (cbn in *; discriminate);
@@ -1449,7 +1449,7 @@ Section CheckLeq.
14491449
(HHl' : gc_expr_declared e')
14501450
: leqb_expr_n_gen leqb_level_n_gen ⎩ n ⎭ e e'
14511451
<-> gc_leq0_levelalg_n ⎩ n ⎭ uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
1452-
Proof.
1452+
Proof using HC.
14531453
split; [apply (leqb_expr_n_spec0_gen _ leqb_correct)|]; try assumption.
14541454
destruct e as [l k] eqn:eqe, e' as [l' k'] eqn:eqe'; cbn; intro H;
14551455
destruct HC as [v0 Hv0]; pose proof (H v0 Hv0) as H0; cbn in H0.
@@ -1471,7 +1471,7 @@ Section CheckLeq.
14711471
n e1 u
14721472
: gc_expr_declared e1 -> gc_levels_declared u -> leqb_expr_univ_n_gen leqb_level_n_gen n e1 u
14731473
-> gc_leq0_levelalg_n n uctx.2 (LevelAlgExpr.make e1) u.
1474-
Proof.
1474+
Proof using Type.
14751475
unfold leqb_expr_univ_n_gen; intros He1 Hu H.
14761476
unfold_univ_rel0.
14771477
rewrite val_fold_right.
@@ -1565,7 +1565,7 @@ Section CheckLeq.
15651565
gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e) u ->
15661566
exists (e' : LevelExpr.t), LevelExprSet.In e' u
15671567
/\ gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
1568-
Proof.
1568+
Proof using HC HG Huctx.
15691569
intros Hl Hu H.
15701570
assert (HG1 : invariants G) by (rewrite HG; exact _).
15711571
assert (HG2 : acyclic_no_loop G) by (rewrite HG; exact _).
@@ -1855,7 +1855,7 @@ Section CheckLeq.
18551855
(Hu : gc_levels_declared u)
18561856
: leqb_expr_univ_n_gen leqb_level_n_gen ⎩ lt ⎭ e1 u
18571857
<-> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e1) u.
1858-
Proof.
1858+
Proof using HC HG Huctx.
18591859
split; [eapply leqb_expr_univ_n_spec0_gen; eauto|].
18601860
unfold leqb_expr_univ_n_gen; intro HH.
18611861
case_eq (LevelAlgExpr.exprs u). intros e u' ee.
@@ -1889,7 +1889,7 @@ Section CheckLeq.
18891889
(Hu1 : gc_levels_declared u1)
18901890
(Hu2 : gc_levels_declared u2)
18911891
: leqb_levelalg_n_gen leqb_level_n_gen lt u1 u2 -> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 u1 u2.
1892-
Proof.
1892+
Proof using Type.
18931893
unfold leqb_levelalg_n_gen. intros H.
18941894
unfold_univ_rel0.
18951895
unfold val, LevelAlgExpr.Evaluable.
@@ -1921,7 +1921,7 @@ Section CheckLeq.
19211921
(Hu2 : gc_levels_declared l2)
19221922
: leqb_levelalg_n_gen leqb_level_n_gen lt l1 l2
19231923
<-> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 l1 l2.
1924-
Proof.
1924+
Proof using HC HG Huctx.
19251925
split; [eapply leqb_levelalg_n_spec0_gen; eauto |].
19261926
unfold leqb_levelalg_n_gen; intro HH.
19271927
unfold LevelAlgExpr.exprs.
@@ -1949,7 +1949,7 @@ Section CheckLeq.
19491949
(Hu1 : gc_levels_declared u1)
19501950
(Hu2 : gc_levels_declared u2)
19511951
: check_leqb_levelalg_gen leqb_level_n_gen u1 u2 <-> gc_leq_levelalg uctx.2 u1 u2.
1952-
Proof.
1952+
Proof using HC HG Huctx.
19531953
unfold check_leqb_levelalg_gen,
19541954
gc_leq_levelalg, gc_leq_levelalg_n,
19551955
leqb_levelalg_n_gen, gc_leq0_levelalg_n.
@@ -1975,7 +1975,7 @@ Section CheckLeq.
19751975
(Hu1 : gc_levels_declared l1)
19761976
(Hu2 : gc_levels_declared l2)
19771977
: check_eqb_levelalg_gen leqb_level_n_gen l1 l2 <-> gc_eq_levelalg uctx.2 l1 l2.
1978-
Proof.
1978+
Proof using HC HG Huctx.
19791979
unfold check_eqb_levelalg_gen, gc_eq_levelalg.
19801980
destruct check_univs; [|split; trivial].
19811981
split; cbn.
@@ -2024,7 +2024,7 @@ Section CheckLeq.
20242024
(Hu1 : gc_levels_declared' uctx.1 gc)
20252025
: check_gc_constraint_gen leqb_level_n_gen gc
20262026
-> if check_univs then forall v, gc_satisfies v uctx.2 -> gc_satisfies0 v gc else True.
2027-
Proof.
2027+
Proof using Huctx.
20282028
unfold check_gc_constraint_gen.
20292029
destruct check_univs; [cbn|trivial].
20302030
destruct gc as [l z l'|k l|k n|l k|n k].
@@ -2056,7 +2056,7 @@ Section CheckLeq.
20562056
ctrs (Hu1 : gcs_levels_declared uctx.1 ctrs)
20572057
: check_gc_constraints_gen leqb_level_n_gen ctrs
20582058
-> if check_univs then forall v, gc_satisfies v uctx.2 -> gc_satisfies v ctrs else True.
2059-
Proof.
2059+
Proof using Huctx.
20602060
rewrite /gcs_levels_declared in Hu1. pose proof check_gc_constraint_spec_gen as XX.
20612061
unfold check_gc_constraints_gen. destruct check_univs; [cbn|trivial].
20622062
intros HH v Hv.
@@ -3252,3 +3252,56 @@ Proof.
32523252
unfold is_consistent. by move=> /on_SomeP [? [-> <-]].
32533253
Qed.
32543254

3255+
From MetaCoq.Utils Require Import MCUtils.
3256+
3257+
Lemma global_uctx_invariants_union_or lvls1 lvls2 cs
3258+
: global_uctx_invariants (lvls1, cs) \/ global_uctx_invariants (lvls2, cs)
3259+
-> global_uctx_invariants (LevelSet.union lvls1 lvls2, cs).
3260+
Proof.
3261+
cbv [global_uctx_invariants uctx_invariants ConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
3262+
repeat first [ apply conj
3263+
| progress intros
3264+
| progress cbv beta iota in *
3265+
| progress destruct ?
3266+
| progress destruct_head'_and
3267+
| progress destruct_head'_or
3268+
| progress split_and
3269+
| rewrite !LevelSet.union_spec
3270+
| progress specialize_dep_under_binders_by eapply pair
3271+
| solve [ eauto ] ].
3272+
Qed.
3273+
3274+
Lemma global_gc_uctx_invariants_union_or lvls1 lvls2 cs
3275+
: global_gc_uctx_invariants (lvls1, cs) \/ global_gc_uctx_invariants (lvls2, cs)
3276+
-> global_gc_uctx_invariants (VSet.union lvls1 lvls2, cs).
3277+
Proof.
3278+
cbv [global_gc_uctx_invariants uctx_invariants GoodConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
3279+
repeat first [ apply conj
3280+
| progress intros
3281+
| progress cbv beta iota in *
3282+
| progress subst
3283+
| progress destruct ?
3284+
| progress destruct_head'_and
3285+
| progress destruct_head'_or
3286+
| progress split_and
3287+
| rewrite !VSet.union_spec
3288+
| progress specialize_dep_under_binders_by eassumption
3289+
| solve [ eauto ] ].
3290+
Qed.
3291+
3292+
Lemma gc_levels_declared_union_or lvls1 lvls2 cstr u
3293+
: gc_levels_declared (lvls1, cstr) u \/ gc_levels_declared (lvls2, cstr) u
3294+
-> gc_levels_declared (VSet.union lvls1 lvls2, cstr) u.
3295+
Proof.
3296+
cbv [gc_levels_declared LevelExprSet.For_all gc_expr_declared on_Some_or_None LevelExpr.get_noprop]; cbn [fst].
3297+
repeat first [ apply conj
3298+
| progress intros
3299+
| progress cbv beta iota in *
3300+
| progress destruct ?
3301+
| progress destruct_head'_and
3302+
| progress destruct_head'_or
3303+
| progress split_and
3304+
| rewrite !VSet.union_spec
3305+
| progress specialize_dep_under_binders_by eassumption
3306+
| solve [ eauto ] ].
3307+
Qed.

0 commit comments

Comments
 (0)