From cd8e839e8af67a6a499ff260cfe93bdfca54bb48 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 11 Feb 2023 15:00:42 -0800
Subject: [PATCH 1/2] Add some utility tactics

I used these for proving some decidability properties and for defining
Gallina quotation functions.
---
 utils/_CoqProject                             |  13 +++
 utils/theories/MCTactics/DestructHead.v       |  88 ++++++++++++++
 utils/theories/MCTactics/DestructHyps.v       |  46 ++++++++
 utils/theories/MCTactics/FindHyp.v            |  31 +++++
 .../theories/MCTactics/GeneralizeOverHoles.v  |   7 ++
 utils/theories/MCTactics/Head.v               |   8 ++
 .../theories/MCTactics/InHypUnderBindersDo.v  | 104 +++++++++++++++++
 utils/theories/MCTactics/SpecializeAllWays.v  |   7 ++
 utils/theories/MCTactics/SpecializeBy.v       |  36 ++++++
 .../MCTactics/SpecializeUnderBindersBy.v      | 109 ++++++++++++++++++
 utils/theories/MCTactics/SplitInContext.v     |  32 +++++
 utils/theories/MCTactics/UniquePose.v         |  29 +++++
 utils/theories/MCTactics/Zeta1.v              |   4 +
 utils/theories/MCUtils.v                      |   9 ++
 14 files changed, 523 insertions(+)
 create mode 100644 utils/theories/MCTactics/DestructHead.v
 create mode 100644 utils/theories/MCTactics/DestructHyps.v
 create mode 100644 utils/theories/MCTactics/FindHyp.v
 create mode 100644 utils/theories/MCTactics/GeneralizeOverHoles.v
 create mode 100644 utils/theories/MCTactics/Head.v
 create mode 100644 utils/theories/MCTactics/InHypUnderBindersDo.v
 create mode 100644 utils/theories/MCTactics/SpecializeAllWays.v
 create mode 100644 utils/theories/MCTactics/SpecializeBy.v
 create mode 100644 utils/theories/MCTactics/SpecializeUnderBindersBy.v
 create mode 100644 utils/theories/MCTactics/SplitInContext.v
 create mode 100644 utils/theories/MCTactics/UniquePose.v
 create mode 100644 utils/theories/MCTactics/Zeta1.v

diff --git a/utils/_CoqProject b/utils/_CoqProject
index 142f6acc0..7e1069665 100644
--- a/utils/_CoqProject
+++ b/utils/_CoqProject
@@ -30,3 +30,16 @@ theories/ReflectEq.v
 theories/monad_utils.v
 theories/utils.v
 
+# extra tactics
+theories/MCTactics/DestructHead.v
+theories/MCTactics/DestructHyps.v
+theories/MCTactics/FindHyp.v
+theories/MCTactics/GeneralizeOverHoles.v
+theories/MCTactics/Head.v
+theories/MCTactics/InHypUnderBindersDo.v
+theories/MCTactics/SpecializeAllWays.v
+theories/MCTactics/SpecializeBy.v
+theories/MCTactics/SpecializeUnderBindersBy.v
+theories/MCTactics/SplitInContext.v
+theories/MCTactics/UniquePose.v
+theories/MCTactics/Zeta1.v
diff --git a/utils/theories/MCTactics/DestructHead.v b/utils/theories/MCTactics/DestructHead.v
new file mode 100644
index 000000000..5424dba37
--- /dev/null
+++ b/utils/theories/MCTactics/DestructHead.v
@@ -0,0 +1,88 @@
+Require Import MetaCoq.Utils.MCTactics.Head.
+Require Import MetaCoq.Utils.MCTactics.DestructHyps.
+
+Ltac destruct_head_matcher T HT :=
+  match head HT with
+  | T => idtac
+  end.
+Ltac destruct_head T := destruct_all_matches ltac:(destruct_head_matcher T).
+Ltac destruct_one_head T := destruct_one_match ltac:(destruct_head_matcher T).
+Ltac destruct_head' T := destruct_all_matches' ltac:(destruct_head_matcher T).
+
+Ltac inversion_head T := inversion_all_matches ltac:(destruct_head_matcher T).
+Ltac inversion_one_head T := inversion_one_match ltac:(destruct_head_matcher T).
+Ltac inversion_head' T := inversion_all_matches' ltac:(destruct_head_matcher T).
+
+
+Ltac head_hnf_matcher T HT :=
+  match head_hnf HT with
+  | T => idtac
+  end.
+Ltac destruct_head_hnf T := destruct_all_matches ltac:(head_hnf_matcher T).
+Ltac destruct_one_head_hnf T := destruct_one_match ltac:(head_hnf_matcher T).
+Ltac destruct_head_hnf' T := destruct_all_matches' ltac:(head_hnf_matcher T).
+
+Ltac inversion_head_hnf T := inversion_all_matches ltac:(head_hnf_matcher T).
+Ltac inversion_one_head_hnf T := inversion_one_match ltac:(head_hnf_matcher T).
+Ltac inversion_head_hnf' T := inversion_all_matches' ltac:(head_hnf_matcher T).
+
+(** Faster versions for some common connectives *)
+Ltac destruct_one_head'_ex := match goal with H : ex _ |- _ => destruct H end.
+Ltac destruct_one_head_ex := destruct_one_head'_ex; simpl in *.
+Ltac destruct_head'_ex := repeat destruct_one_head'_ex.
+Ltac destruct_head_ex := repeat destruct_one_head_ex.
+
+Ltac destruct_one_head'_sig := match goal with H : sig _ |- _ => destruct H end.
+Ltac destruct_one_head_sig := destruct_one_head'_sig; simpl in *.
+Ltac destruct_head'_sig := repeat destruct_one_head'_sig.
+Ltac destruct_head_sig := repeat destruct_one_head_sig.
+
+Ltac destruct_one_head'_sigT := match goal with H : sigT _ |- _ => destruct H end.
+Ltac destruct_one_head_sigT := destruct_one_head'_sigT; simpl in *.
+Ltac destruct_head'_sigT := repeat destruct_one_head'_sigT.
+Ltac destruct_head_sigT := repeat destruct_one_head_sigT.
+
+Ltac destruct_one_head'_prod := match goal with H : prod _ _ |- _ => destruct H end.
+Ltac destruct_one_head_prod := destruct_one_head'_prod; simpl in *.
+Ltac destruct_head'_prod := repeat destruct_one_head'_prod.
+Ltac destruct_head_prod := repeat destruct_one_head_prod.
+
+Ltac destruct_one_head'_and := match goal with H : and _ _ |- _ => destruct H end.
+Ltac destruct_one_head_and := destruct_one_head'_and; simpl in *.
+Ltac destruct_head'_and := repeat destruct_one_head'_and.
+Ltac destruct_head_and := repeat destruct_one_head_and.
+
+Ltac destruct_one_head'_or := match goal with H : or _ _ |- _ => destruct H end.
+Ltac destruct_one_head_or := destruct_one_head'_or; simpl in *.
+Ltac destruct_head'_or := repeat destruct_one_head'_or.
+Ltac destruct_head_or := repeat destruct_one_head_or.
+
+Ltac destruct_one_head'_sum := match goal with H : sum _ _ |- _ => destruct H end.
+Ltac destruct_one_head_sum := destruct_one_head'_sum; simpl in *.
+Ltac destruct_head'_sum := repeat destruct_one_head'_sum.
+Ltac destruct_head_sum := repeat destruct_one_head_sum.
+
+Ltac destruct_one_head'_unit := match goal with H : unit |- _ => clear H || destruct H end.
+Ltac destruct_one_head_unit := destruct_one_head'_unit; simpl in *.
+Ltac destruct_head'_unit := repeat destruct_one_head'_unit.
+Ltac destruct_head_unit := repeat destruct_one_head_unit.
+
+Ltac destruct_one_head'_True := match goal with H : True |- _ => clear H || destruct H end.
+Ltac destruct_one_head_True := destruct_one_head'_True; simpl in *.
+Ltac destruct_head'_True := repeat destruct_one_head'_True.
+Ltac destruct_head_True := repeat destruct_one_head_True.
+
+Ltac destruct_one_head'_bool := match goal with H : bool |- _ => clear H || destruct H end.
+Ltac destruct_one_head_bool := destruct_one_head'_bool; simpl in *.
+Ltac destruct_head'_bool := repeat destruct_one_head'_bool.
+Ltac destruct_head_bool := repeat destruct_one_head_bool.
+
+Ltac destruct_one_head'_False := match goal with H : False |- _ => destruct H end.
+Ltac destruct_one_head_False := destruct_one_head'_False; simpl in *.
+Ltac destruct_head'_False := repeat destruct_one_head'_False.
+Ltac destruct_head_False := repeat destruct_one_head_False.
+
+Ltac destruct_one_head'_Empty_set := match goal with H : Empty_set |- _ => destruct H end.
+Ltac destruct_one_head_Empty_set := destruct_one_head'_Empty_set; simpl in *.
+Ltac destruct_head'_Empty_set := repeat destruct_one_head'_Empty_set.
+Ltac destruct_head_Empty_set := repeat destruct_one_head_Empty_set.
diff --git a/utils/theories/MCTactics/DestructHyps.v b/utils/theories/MCTactics/DestructHyps.v
new file mode 100644
index 000000000..7b647e0b7
--- /dev/null
+++ b/utils/theories/MCTactics/DestructHyps.v
@@ -0,0 +1,46 @@
+(** given a [matcher] that succeeds on some hypotheses and fails on
+    others, destruct any matching hypotheses, and then execute [tac]
+    after each [destruct].
+
+    The [tac] part exists so that you can, e.g., [simpl in *], to
+    speed things up. *)
+Ltac do_one_match_then matcher do_tac tac :=
+  idtac;
+  match goal with
+  | [ H : ?T |- _ ]
+    => matcher T; do_tac H;
+       try match type of H with
+           | T => clear H
+           end;
+       tac
+  end.
+
+Ltac do_all_matches_then matcher do_tac tac :=
+  repeat do_one_match_then matcher do_tac tac.
+
+Ltac destruct_all_matches_then matcher tac :=
+  do_all_matches_then matcher ltac:(fun H => destruct H) tac.
+Ltac destruct_one_match_then matcher tac :=
+  do_one_match_then matcher ltac:(fun H => destruct H) tac.
+
+Ltac inversion_all_matches_then matcher tac :=
+  do_all_matches_then matcher ltac:(fun H => inversion H; subst) tac.
+Ltac inversion_one_match_then matcher tac :=
+  do_one_match_then matcher ltac:(fun H => inversion H; subst) tac.
+
+Ltac destruct_all_matches matcher :=
+  destruct_all_matches_then matcher ltac:( simpl in * ).
+Ltac destruct_one_match matcher := destruct_one_match_then matcher ltac:( simpl in * ).
+Ltac destruct_all_matches' matcher := destruct_all_matches_then matcher idtac.
+
+Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:( simpl in * ).
+Ltac inversion_one_match matcher := inversion_one_match_then matcher ltac:( simpl in * ).
+Ltac inversion_all_matches' matcher := inversion_all_matches_then matcher idtac.
+
+(* matches anything whose type has a [T] in it *)
+Ltac destruct_type_matcher T HT :=
+  match HT with
+  | context[T] => idtac
+  end.
+Ltac destruct_type T := destruct_all_matches ltac:(destruct_type_matcher T).
+Ltac destruct_type' T := destruct_all_matches' ltac:(destruct_type_matcher T).
diff --git a/utils/theories/MCTactics/FindHyp.v b/utils/theories/MCTactics/FindHyp.v
new file mode 100644
index 000000000..639f3d358
--- /dev/null
+++ b/utils/theories/MCTactics/FindHyp.v
@@ -0,0 +1,31 @@
+Ltac find_hyp_eq a b := match goal with _ => constr_eq_nounivs a b end.
+(* Work around https://github.com/coq/coq/issues/15554 *)
+Ltac find_hyp T :=
+  lazymatch T with
+  | T
+    => (* we're not in https://github.com/coq/coq/issues/15554 *)
+      multimatch goal with
+      | [ H : T |- _ ] => H
+      end
+  | _
+    => (* https://github.com/coq/coq/issues/15554 *)
+      multimatch goal with
+      | [ H : ?T' |- _ ] => let __ := find_hyp_eq T T' in
+                            H
+      end
+  end.
+
+Ltac find_hyp_with_body body :=
+  lazymatch body with
+  | body
+    => (* we're not in https://github.com/coq/coq/issues/15554 *)
+      multimatch goal with
+      | [ H := body |- _ ] => H
+      end
+  | _
+    => (* https://github.com/coq/coq/issues/15554 *)
+      multimatch goal with
+      | [ H := ?body' |- _ ] => let __ := find_hyp_eq body body' in
+                                H
+      end
+  end.
diff --git a/utils/theories/MCTactics/GeneralizeOverHoles.v b/utils/theories/MCTactics/GeneralizeOverHoles.v
new file mode 100644
index 000000000..2ee552979
--- /dev/null
+++ b/utils/theories/MCTactics/GeneralizeOverHoles.v
@@ -0,0 +1,7 @@
+Require Import MetaCoq.Utils.MCTactics.Zeta1.
+Require Import Coq.ssr.ssreflect.
+
+Ltac generalize_over_holes tac :=
+  zeta1 (ltac:(let H := fresh in
+               (pose H := ltac:(let v := tac () in refine v));
+               exact H)).
diff --git a/utils/theories/MCTactics/Head.v b/utils/theories/MCTactics/Head.v
new file mode 100644
index 000000000..be01c3a17
--- /dev/null
+++ b/utils/theories/MCTactics/Head.v
@@ -0,0 +1,8 @@
+(** find the head of the given expression *)
+Ltac head expr :=
+  match expr with
+  | ?f _ => head f
+  | _ => expr
+  end.
+
+Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'.
diff --git a/utils/theories/MCTactics/InHypUnderBindersDo.v b/utils/theories/MCTactics/InHypUnderBindersDo.v
new file mode 100644
index 000000000..d53adc674
--- /dev/null
+++ b/utils/theories/MCTactics/InHypUnderBindersDo.v
@@ -0,0 +1,104 @@
+Require Import MetaCoq.Utils.MCTactics.SpecializeBy.
+Require Import MetaCoq.Utils.MCTactics.GeneralizeOverHoles.
+Require Import MetaCoq.Utils.MCTactics.UniquePose.
+
+Ltac guarded_in_hyp_term_under_binders_do' guard_tac H tac :=
+  let is_transparent := match goal with
+                        | _ => let __ := (eval cbv delta [H] in H) in
+                               constr:(true)
+                        | _ => constr:(false)
+                        end in
+  let __ := lazymatch goal with _ => guard_tac H end in
+  match goal with
+  | _ => let __ := lazymatch goal with _ => progress tac H end in
+         H
+  | _ => let __ := lazymatch is_transparent with
+                   | true => let H' := fresh in
+                             rename H into H';
+                             let v := open_constr:(_) in
+                             pose (H' v) as H;
+                             subst H'
+                   | false
+                     => (* kludge for old Coq *)
+                       (*let v := open_constr:(_) in*)
+                       let t := open_constr:(_) in
+                       let v := fresh in
+                       evar (v : t);
+                       specialize (H v);
+                       subst v
+                   end in
+         guarded_in_hyp_term_under_binders_do' guard_tac H tac
+  end.
+
+Ltac guarded_in_hyp_term_under_binders_do guard_tac H tac :=
+  generalize_over_holes ltac:(fun _ => guarded_in_hyp_term_under_binders_do' guard_tac H tac).
+
+Ltac guarded_in_hyp_gen_hyp_under_binders_do all_ways guard_tac H tac :=
+  idtac;
+  let is_transparent := match goal with
+                        | _ => let __ := (eval cbv delta [H] in H) in
+                               constr:(true)
+                        | _ => constr:(false)
+                        end in
+  lazymatch constr:((all_ways, is_transparent)) with
+  | (false, true)
+    => let H' := fresh in
+       rename H into H';
+       let H'' := guarded_in_hyp_term_under_binders_do guard_tac H' tac in
+       pose H'' as H;
+       subst H'
+  | (true, true)
+    => let H := guarded_in_hyp_term_under_binders_do guard_tac H tac in
+       unique pose H
+  | (false, false)
+    => let H' := fresh in
+       rename H into H';
+       let H'' := guarded_in_hyp_term_under_binders_do guard_tac H' tac in
+       pose proof H'' as H;
+       clear H'
+  | (true, false)
+    => let H := guarded_in_hyp_term_under_binders_do guard_tac H tac in
+       unique pose proof H
+  end.
+
+Ltac guarded_in_hyp_hyp_under_binders_do guard_tac H tac :=
+  guarded_in_hyp_gen_hyp_under_binders_do false guard_tac H tac.
+Ltac guarded_in_hyp_hyp_all_ways_under_binders_do guard_tac H tac :=
+  guarded_in_hyp_gen_hyp_under_binders_do true guard_tac H tac.
+
+Ltac guard_noop H := idtac.
+
+Ltac guarded_in_hyp_gen_under_binders_do' all_ways tac guard_tac :=
+  idtac;
+  match goal with
+  | [ H : _ |- _ ]
+    => guard_tac H;
+       guarded_in_hyp_gen_hyp_under_binders_do all_ways guard_noop H tac
+  end.
+
+Ltac guarded_in_hyp_under_binders_do' tac guard_tac :=
+  guarded_in_hyp_gen_under_binders_do' false tac guard_tac.
+
+Ltac in_hyp_gen_under_binders_do' all_ways tac := guarded_in_hyp_gen_under_binders_do' all_ways tac ltac:(fun _ => idtac).
+
+Ltac in_hyp_under_binders_do' tac := in_hyp_gen_under_binders_do' false tac.
+
+Ltac guarded_in_hyp_gen_under_binders_do all_ways tac guard_tac := repeat guarded_in_hyp_gen_under_binders_do' all_ways tac guard_tac.
+
+Ltac guarded_in_hyp_under_binders_do tac guard_tac := guarded_in_hyp_gen_under_binders_do false tac guard_tac.
+
+Ltac guarded_in_hyp_all_ways_under_binders_do tac guard_tac := guarded_in_hyp_gen_under_binders_do true tac guard_tac.
+
+Ltac in_hyp_gen_under_binders_do all_ways tac := repeat in_hyp_gen_under_binders_do' all_ways tac.
+
+Ltac in_hyp_under_binders_do tac := in_hyp_gen_under_binders_do false tac.
+
+Ltac in_hyp_all_ways_under_binders_do tac := in_hyp_gen_under_binders_do true tac.
+
+(** [in_hyp_under_binders_do auto] should not mean [in_hyp_under_binders_do ( auto
+    with * )]!!!!!!! (see
+    https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
+    flaw. *)
+Tactic Notation "in_hyp_under_binders_do" tactic3(tac) := in_hyp_under_binders_do tac.
+
+Tactic Notation "in_hyp_all_ways_under_binders_do" tactic3(tac) := in_hyp_all_ways_under_binders_do tac.
diff --git a/utils/theories/MCTactics/SpecializeAllWays.v b/utils/theories/MCTactics/SpecializeAllWays.v
new file mode 100644
index 000000000..fbbbac3a1
--- /dev/null
+++ b/utils/theories/MCTactics/SpecializeAllWays.v
@@ -0,0 +1,7 @@
+Require Export MetaCoq.Utils.MCTactics.UniquePose.
+
+Ltac specialize_all_ways :=
+  repeat match goal with
+         | [ H : ?A, H' : forall a : ?A, _ |- _ ]
+           => unique pose proof (H' H)
+         end.
diff --git a/utils/theories/MCTactics/SpecializeBy.v b/utils/theories/MCTactics/SpecializeBy.v
new file mode 100644
index 000000000..37dcd83a3
--- /dev/null
+++ b/utils/theories/MCTactics/SpecializeBy.v
@@ -0,0 +1,36 @@
+Ltac transparent_specialize_one H arg :=
+  first [ let test := eval unfold H in H in idtac;
+          let H' := fresh in rename H into H'; pose (H' arg) as H; subst H'
+         | specialize (H arg) ].
+
+(** try to specialize all non-dependent hypotheses using [tac], maintaining transparency *)
+Ltac guarded_specialize_by' tac guard_tac :=
+  idtac;
+  match goal with
+  | [ H : ?A -> ?B |- _ ]
+    => guard_tac H;
+       let H' := fresh in
+       assert (H' : A) by tac;
+       transparent_specialize_one H H';
+       try clear H' (* if [H] was transparent, [H'] will remain *)
+  end.
+Ltac specialize_by' tac := guarded_specialize_by' tac ltac:(fun _ => idtac).
+
+Ltac specialize_by tac := repeat specialize_by' tac.
+
+(** [specialize_by auto] should not mean [specialize_by ( auto
+    with * )]!!!!!!! (see
+    https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
+    flaw. *)
+Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac.
+
+(** A marginally faster version of [specialize_by assumption] *)
+Ltac specialize_by_assumption :=
+  repeat match goal with
+         | [ H : ?T, H' : (?T -> ?U)%type |- _ ]
+           => lazymatch goal with
+              | [ _ : context[H'] |- _ ] => fail
+              | [ |- context[H'] ] => fail
+              | _ => specialize (H' H)
+              end
+         end.
diff --git a/utils/theories/MCTactics/SpecializeUnderBindersBy.v b/utils/theories/MCTactics/SpecializeUnderBindersBy.v
new file mode 100644
index 000000000..9b701dde5
--- /dev/null
+++ b/utils/theories/MCTactics/SpecializeUnderBindersBy.v
@@ -0,0 +1,109 @@
+Require Import MetaCoq.Utils.MCTactics.SpecializeBy.
+Require Import MetaCoq.Utils.MCTactics.UniquePose.
+Require Import MetaCoq.Utils.MCTactics.GeneralizeOverHoles.
+
+Ltac guarded_specialize_term_under_binders_by' guard_tac H tac :=
+  lazymatch type of H with
+  | forall a, _
+    => match goal with
+       | _ => let __ := lazymatch goal with _ => guard_tac H end in
+              open_constr:(H ltac:(progress tac))
+       | _ => let H := open_constr:(H _) in
+              guarded_specialize_term_under_binders_by' guard_tac H tac
+       end
+  end.
+
+Ltac guarded_specialize_term_under_binders_by guard_tac H tac :=
+  generalize_over_holes ltac:(fun _ => guarded_specialize_term_under_binders_by' guard_tac H tac).
+
+Ltac guarded_specialize_gen_hyp_under_binders_by all_ways guard_tac H tac :=
+  idtac;
+  let is_transparent := match goal with
+                        | _ => let __ := (eval cbv delta [H] in H) in
+                               constr:(true)
+                        | _ => constr:(false)
+                        end in
+  lazymatch constr:((all_ways, is_transparent)) with
+  | (false, true)
+    => let H' := fresh in
+       rename H into H';
+       let H'' := guarded_specialize_term_under_binders_by guard_tac H' tac in
+       pose H'' as H;
+       subst H'
+  | (true, true)
+    => let H := guarded_specialize_term_under_binders_by guard_tac H tac in
+       unique pose H
+  | (false, false)
+    => let H := guarded_specialize_term_under_binders_by guard_tac H tac in
+       specialize H
+  | (true, false)
+    => let H := guarded_specialize_term_under_binders_by guard_tac H tac in
+       unique pose proof H
+  end.
+
+Ltac guarded_specialize_hyp_under_binders_by guard_tac H tac :=
+  guarded_specialize_gen_hyp_under_binders_by false guard_tac H tac.
+Ltac guarded_specialize_hyp_all_ways_under_binders_by guard_tac H tac :=
+  guarded_specialize_gen_hyp_under_binders_by true guard_tac H tac.
+
+Ltac guard_noop H := idtac.
+
+Ltac guard_nondep H :=
+  lazymatch type of H with
+  | ?A -> ?B => idtac
+  end.
+
+(** try to specialize all non-dependent hypotheses using [tac] at any point under their binders, maintaining transparency *)
+Ltac guarded_specialize_gen_under_binders_by' all_ways tac guard_tac :=
+  idtac;
+  match goal with
+  | [ H : _ |- _ ]
+    => guard_tac H;
+       guarded_specialize_gen_hyp_under_binders_by all_ways guard_nondep H tac
+  end.
+Ltac guarded_specialize_gen_dep_under_binders_by' all_ways tac guard_tac :=
+  idtac;
+  match goal with
+  | [ H : _ |- _ ]
+    => guard_tac H;
+       guarded_specialize_gen_hyp_under_binders_by all_ways guard_noop H tac
+  end.
+
+Ltac guarded_specialize_under_binders_by' tac guard_tac :=
+  guarded_specialize_gen_under_binders_by' false tac guard_tac.
+Ltac guarded_specialize_dep_under_binders_by' tac guard_tac :=
+  guarded_specialize_gen_dep_under_binders_by' false tac guard_tac.
+
+Ltac specialize_gen_under_binders_by' all_ways tac := guarded_specialize_gen_under_binders_by' all_ways tac ltac:(fun _ => idtac).
+Ltac specialize_gen_dep_under_binders_by' all_ways tac := guarded_specialize_gen_dep_under_binders_by' all_ways tac ltac:(fun _ => idtac).
+
+Ltac specialize_under_binders_by' tac := specialize_gen_under_binders_by' false tac.
+Ltac specialize_dep_under_binders_by' tac := specialize_gen_dep_under_binders_by' false tac.
+
+Ltac guarded_specialize_gen_under_binders_by all_ways tac guard_tac := repeat guarded_specialize_gen_under_binders_by' all_ways tac guard_tac.
+Ltac guarded_specialize_gen_dep_under_binders_by all_ways tac guard_tac := repeat guarded_specialize_gen_dep_under_binders_by' all_ways tac guard_tac.
+
+Ltac guarded_specialize_under_binders_by tac guard_tac := guarded_specialize_gen_under_binders_by false tac guard_tac.
+Ltac guarded_specialize_dep_under_binders_by tac guard_tac := guarded_specialize_gen_dep_under_binders_by false tac guard_tac.
+
+Ltac guarded_specialize_all_ways_under_binders_by tac guard_tac := guarded_specialize_gen_under_binders_by true tac guard_tac.
+Ltac guarded_specialize_all_ways_dep_under_binders_by tac guard_tac := guarded_specialize_gen_dep_under_binders_by true tac guard_tac.
+
+Ltac specialize_gen_under_binders_by all_ways tac := repeat specialize_gen_under_binders_by' all_ways tac.
+Ltac specialize_gen_dep_under_binders_by all_ways tac := repeat specialize_gen_dep_under_binders_by' all_ways tac.
+
+Ltac specialize_under_binders_by tac := specialize_gen_under_binders_by false tac.
+Ltac specialize_dep_under_binders_by tac := specialize_gen_dep_under_binders_by false tac.
+
+Ltac specialize_all_ways_under_binders_by tac := specialize_gen_under_binders_by true tac.
+Ltac specialize_all_ways_dep_under_binders_by tac := specialize_gen_dep_under_binders_by true tac.
+
+(** [specialize_under_binders_by auto] should not mean [specialize_under_binders_by ( auto
+    with * )]!!!!!!! (see
+    https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
+    flaw. *)
+Tactic Notation "specialize_under_binders_by" tactic3(tac) := specialize_under_binders_by tac.
+Tactic Notation "specialize_dep_under_binders_by" tactic3(tac) := specialize_dep_under_binders_by tac.
+
+Tactic Notation "specialize_all_ways_under_binders_by" tactic3(tac) := specialize_all_ways_under_binders_by tac.
+Tactic Notation "specialize_all_ways_dep_under_binders_by" tactic3(tac) := specialize_all_ways_dep_under_binders_by tac.
diff --git a/utils/theories/MCTactics/SplitInContext.v b/utils/theories/MCTactics/SplitInContext.v
new file mode 100644
index 000000000..801dab117
--- /dev/null
+++ b/utils/theories/MCTactics/SplitInContext.v
@@ -0,0 +1,32 @@
+(* Coq's build in tactics don't work so well with things like [iff]
+   so split them up into multiple hypotheses *)
+Ltac split_in_context_by ident funl funr tac :=
+  repeat match goal with
+         | [ H : context p [ident] |- _ ] =>
+           let H0 := context p[funl] in
+           let H1 := context p[funr] in
+           let H0' := (eval cbv beta in H0) in
+           let H1' := (eval cbv beta in H1) in
+           assert H0' by (tac H);
+           assert H1' by (tac H);
+           clear H
+         end.
+Ltac split_in_context ident funl funr :=
+  split_in_context_by ident funl funr ltac:(fun H => apply H).
+
+Ltac split_iff := split_in_context iff (fun a b : Prop => a -> b) (fun a b : Prop => b -> a).
+
+Ltac split_contravariant_or := split_in_context_by or (fun A B : Prop => A) (fun A B : Prop => B) ltac:(fun H => intros; eauto 100 using H, or_introl, or_intror, ex_intro, exist, existT with nocore).
+
+Ltac split_and' :=
+  repeat match goal with
+         | [ H : ?a /\ ?b |- _ ] => let H0 := fresh in let H1 := fresh in
+                                                       assert (H0 := proj1 H); assert (H1 := proj2 H); clear H
+         end.
+Ltac split_prod' :=
+  repeat match goal with
+         | [ H : prod ?a ?b |- _ ] => let H0 := fresh in let H1 := fresh in
+                                                         assert (H0 := fst H); assert (H1 := snd H); clear H
+         end.
+Ltac split_and := split_and'; split_in_context and (fun a b : Type => a) (fun a b : Type => b).
+Ltac split_prod := split_and'; split_in_context prod (fun a b : Type => a) (fun a b : Type => b).
diff --git a/utils/theories/MCTactics/UniquePose.v b/utils/theories/MCTactics/UniquePose.v
new file mode 100644
index 000000000..1c1342bef
--- /dev/null
+++ b/utils/theories/MCTactics/UniquePose.v
@@ -0,0 +1,29 @@
+Require Import MetaCoq.Utils.MCTactics.FindHyp.
+
+(** [pose proof defn], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "pose" "proof" constr(defn) :=
+  let T := type of defn in
+  tryif let H := find_hyp T in fail 2 "Already a hypothesis" H "of type" T
+  then fail
+  else pose proof defn.
+
+(** [pose defn], but only if that hypothesis doesn't exist *)
+Tactic Notation "unique" "pose" constr(defn) :=
+  tryif let H := find_hyp_with_body defn in fail 2 "Already a hypothesis" H "with body" defn
+  then fail
+  else pose defn.
+
+(** [assert T], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) :=
+  tryif let H := find_hyp T in fail 2 "Already a hypothesis" H "of type" T
+  then fail
+  else assert T.
+
+(** [assert T], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) "by" tactic3(tac) :=
+  tryif let H := find_hyp T in fail 2 "Already a hypothesis" H "of type" T
+  then fail
+  else assert T by tac.
diff --git a/utils/theories/MCTactics/Zeta1.v b/utils/theories/MCTactics/Zeta1.v
new file mode 100644
index 000000000..4a881740d
--- /dev/null
+++ b/utils/theories/MCTactics/Zeta1.v
@@ -0,0 +1,4 @@
+Ltac zeta1 x :=
+  lazymatch x with
+  | let a := ?b in ?f => constr:(match b with a => f end)
+  end.
diff --git a/utils/theories/MCUtils.v b/utils/theories/MCUtils.v
index a7557a3fc..e71c20c57 100644
--- a/utils/theories/MCUtils.v
+++ b/utils/theories/MCUtils.v
@@ -12,6 +12,15 @@ Require Export MCPrelude
         MCSquash
         MCRelations
         MCString
+        MCTactics.InHypUnderBindersDo
+        MCTactics.SpecializeUnderBindersBy
+        MCTactics.Zeta1
+        MCTactics.DestructHead
+        MCTactics.SpecializeAllWays
+        MCTactics.SplitInContext
+        MCTactics.Head
+        MCTactics.SpecializeBy
+        MCTactics.UniquePose
         ReflectEq
         bytestring
 .

From 850a39b32e8581a3b979421b3bd14379419c2dfe Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 11 Feb 2023 18:19:59 -0800
Subject: [PATCH 2/2] Add some decision procedures

---
 common/_CoqProject.in               |   1 +
 common/theories/EnvironmentTyping.v |  13 ++
 common/theories/UniversesDec.v      | 203 ++++++++++++++++++++++++++++
 common/theories/uGraph.v            |  75 ++++++++--
 4 files changed, 281 insertions(+), 11 deletions(-)
 create mode 100644 common/theories/UniversesDec.v

diff --git a/common/_CoqProject.in b/common/_CoqProject.in
index 66dfd7215..45bccac4f 100644
--- a/common/_CoqProject.in
+++ b/common/_CoqProject.in
@@ -5,6 +5,7 @@ theories/uGraph.v
 theories/config.v
 theories/Kernames.v
 theories/Universes.v
+theories/UniversesDec.v
 theories/BasicAst.v
 theories/Environment.v
 theories/Reflect.v
diff --git a/common/theories/EnvironmentTyping.v b/common/theories/EnvironmentTyping.v
index 687c0cbd5..222105480 100644
--- a/common/theories/EnvironmentTyping.v
+++ b/common/theories/EnvironmentTyping.v
@@ -284,6 +284,19 @@ Module Lookup (T : Term) (E : EnvironmentSig T).
       (fun u => forall l, LevelExprSet.In l u -> LevelSet.In (LevelExpr.get_level l) (global_ext_levels Σ))
       True s.
 
+  Definition wf_universe_dec Σ s : {@wf_universe Σ s} + {~@wf_universe Σ s}.
+  Proof.
+    destruct s; try (left; exact I).
+    cbv [wf_universe Universe.on_sort LevelExprSet.In LevelExprSet.this t_set].
+    destruct t as [[t _] _].
+    induction t as [|t ts [IHt|IHt]]; [ left | | right ].
+    { inversion 1. }
+    { destruct (LevelSetProp.In_dec (LevelExpr.get_level t) (global_ext_levels Σ)) as [H|H]; [ left | right ].
+      { inversion 1; subst; auto. }
+      { intro H'; apply H, H'; now constructor. } }
+    { intro H; apply IHt; intros; apply H; now constructor. }
+  Defined.
+
   Lemma declared_ind_declared_constructors `{cf : checker_flags} {Σ ind mib oib} :
     declared_inductive Σ ind mib oib ->
     Alli (fun i => declared_constructor Σ (ind, i) mib oib) 0 (ind_ctors oib).
diff --git a/common/theories/UniversesDec.v b/common/theories/UniversesDec.v
new file mode 100644
index 000000000..bae647212
--- /dev/null
+++ b/common/theories/UniversesDec.v
@@ -0,0 +1,203 @@
+From MetaCoq.Utils Require Import MCList MCOption MCUtils.
+From MetaCoq.Common Require Import uGraph.
+From MetaCoq.Common Require Import Universes.
+Import wGraph.
+
+Definition levels_of_cs (cstr : ConstraintSet.t) : LevelSet.t
+  := ConstraintSet.fold (fun '(l1, _, l2) acc => LevelSet.add l1 (LevelSet.add l2 acc)) cstr (LevelSet.singleton Level.lzero).
+Lemma levels_of_cs_spec cstr (lvls := levels_of_cs cstr)
+  : uGraph.global_uctx_invariants (lvls, cstr).
+Proof.
+  subst lvls; cbv [levels_of_cs].
+  cbv [uGraph.global_uctx_invariants uGraph.uctx_invariants ConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
+  repeat first [ apply conj
+               | progress intros
+               | progress destruct ?
+               | match goal with
+                 | [ |- ?x \/ ?y ]
+                   => first [ lazymatch x with context[LevelSet.In ?l (LevelSet.singleton ?l)] => idtac end;
+                              left
+                            | lazymatch y with context[LevelSet.In ?l (LevelSet.singleton ?l)] => idtac end;
+                              right ]
+                 | [ H : ConstraintSet.In ?l ?c |- ?x \/ ?y ]
+                   => first [ lazymatch x with context[LevelSet.In _ (ConstraintSet.fold _ c _)] => idtac end;
+                              left
+                            | lazymatch y with context[LevelSet.In _ (ConstraintSet.fold _ c _)] => idtac end;
+                              right ]
+                 end
+               | rewrite !LevelSet.union_spec
+               | progress rewrite <- ?ConstraintSet.elements_spec1, ?InA_In_eq in *
+               | rewrite ConstraintSetProp.fold_spec_right ].
+  all: lazymatch goal with
+       | [ |- LevelSet.In Level.lzero (List.fold_right ?f ?init ?ls) ]
+         => first [ LevelSetDecide.fsetdec
+                  | cut (LevelSet.In Level.lzero init);
+                    [ generalize init; induction ls; intros; cbn in *
+                    | LevelSetDecide.fsetdec ] ]
+       | [ H : List.In ?v ?ls |- LevelSet.In ?v' (List.fold_right ?f ?init (List.rev ?ls)) ]
+         => rewrite List.in_rev in H;
+            let ls' := fresh "ls" in
+            set (ls' := List.rev ls);
+            change (List.In v ls') in H;
+            change (LevelSet.In v' (List.fold_right f init ls'));
+            generalize init; induction ls'; cbn in *
+       end.
+  all: repeat first [ exfalso; assumption
+                    | progress destruct_head'_or
+                    | progress subst
+                    | progress intros
+                    | progress destruct ?
+                    | rewrite !LevelSetFact.add_iff
+                    | solve [ auto ] ].
+Qed.
+
+Definition consistent_dec ctrs : {@consistent ctrs} + {~@consistent ctrs}.
+Proof.
+  pose proof (@uGraph.is_consistent_spec config.default_checker_flags (levels_of_cs ctrs, ctrs) (levels_of_cs_spec ctrs)) as H.
+  destruct uGraph.is_consistent; [ left; apply H | right; intro H'; apply H in H' ]; auto.
+Defined.
+
+Definition levels_of_cs2 (cs1 cs2 : ConstraintSet.t) : LevelSet.t
+  := LevelSet.union (levels_of_cs cs1) (levels_of_cs cs2).
+Lemma levels_of_cs2_spec cs1 cs2 (lvls := levels_of_cs2 cs1 cs2)
+  : uGraph.global_uctx_invariants (lvls, cs1)
+    /\ uGraph.global_uctx_invariants (lvls, cs2).
+Proof.
+  split; apply global_uctx_invariants_union_or; constructor; apply levels_of_cs_spec.
+Qed.
+
+Definition levels_of_cscs (cs : ContextSet.t) (cstr : ConstraintSet.t) : LevelSet.t
+  := LevelSet.union (ContextSet.levels cs) (levels_of_cs2 cstr (ContextSet.constraints cs)).
+Lemma levels_of_cscs_spec cs cstr (lvls := levels_of_cscs cs cstr)
+  : uGraph.global_uctx_invariants (lvls, ContextSet.constraints cs)
+    /\ uGraph.global_uctx_invariants (lvls, cstr).
+Proof.
+  generalize (levels_of_cs2_spec cstr (ContextSet.constraints cs)).
+  split; apply global_uctx_invariants_union_or; constructor; apply levels_of_cs2_spec.
+Qed.
+
+Definition levels_of_algexpr (u : LevelAlgExpr.t) : VSet.t
+  := LevelExprSet.fold
+       (fun gc acc => match LevelExpr.get_noprop gc with
+                      | Some l => VSet.add l acc
+                      | None => acc
+                      end)
+       u
+       VSet.empty.
+Lemma levels_of_algexpr_spec u cstr (lvls := levels_of_algexpr u)
+  : gc_levels_declared (lvls, cstr) u.
+Proof.
+  subst lvls; cbv [levels_of_algexpr gc_levels_declared gc_expr_declared on_Some_or_None LevelExpr.get_noprop]; cbn [fst snd].
+  cbv [LevelExprSet.For_all]; cbn [fst snd].
+  repeat first [ apply conj
+               | progress intros
+               | progress destruct ?
+               | exact I
+               | progress rewrite <- ?LevelExprSet.elements_spec1, ?InA_In_eq in *
+               | rewrite LevelExprSetProp.fold_spec_right ].
+  all: lazymatch goal with
+       | [ H : List.In ?v ?ls |- VSet.In ?v' (List.fold_right ?f ?init (List.rev ?ls)) ]
+         => rewrite List.in_rev in H;
+            let ls' := fresh "ls" in
+            set (ls' := List.rev ls);
+            change (List.In v ls') in H;
+            change (VSet.In v' (List.fold_right f init ls'));
+            generalize init; induction ls'; cbn in *
+       end.
+  all: repeat first [ exfalso; assumption
+                    | progress destruct_head'_or
+                    | progress subst
+                    | progress intros
+                    | progress destruct ?
+                    | rewrite !VSetFact.add_iff
+                    | solve [ auto ] ].
+Qed.
+
+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'}.
+Proof.
+  pose proof (@uGraph.gc_leq0_levelalg_n_iff config.default_checker_flags (uGraph.Z_of_bool n) ϕ u u') as H.
+  pose proof (@uGraph.gc_consistent_iff config.default_checker_flags ϕ).
+  cbv [on_Some on_Some_or_None] in *.
+  destruct gc_of_constraints eqn:?.
+  all: try solve [ left; cbv [consistent] in *; hnf; intros; exfalso; intuition eauto ].
+  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)).
+  pose proof (fun x y => @gc_of_constraints_of_uctx config.default_checker_flags (x, y)) as H'.
+  pose proof (@is_consistent_spec config.default_checker_flags (levels_of_cs ϕ, ϕ)).
+  specialize_under_binders_by eapply gc_levels_declared_union_or.
+  specialize_under_binders_by eapply global_gc_uctx_invariants_union_or.
+  specialize_under_binders_by (constructor; eapply gc_of_uctx_invariants).
+  cbn [fst snd] in *.
+  specialize_under_binders_by eapply H'.
+  specialize_under_binders_by eassumption.
+  specialize_under_binders_by eapply levels_of_cs_spec.
+  specialize_under_binders_by reflexivity.
+  destruct is_consistent;
+    [ | left; now cbv [leq0_levelalg_n consistent] in *; intros; exfalso; intuition eauto ].
+  specialize_by intuition eauto.
+  let H := match goal with H : forall (b : bool), _ |- _ => H end in
+  specialize (H n u u').
+  specialize_under_binders_by (constructor; eapply gc_levels_declared_union_or; constructor; eapply levels_of_algexpr_spec).
+  match goal with H : is_true ?b <-> ?x, H' : ?y <-> ?x |- {?y} + {_} => destruct b eqn:?; [ left | right ] end.
+  all: intuition.
+Defined.
+
+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'}.
+Proof.
+  cbv [leq_levelalg_n]; destruct (@leq0_levelalg_n_dec n ϕ u u'); destruct ?; auto.
+Defined.
+
+Definition eq0_levelalg_dec ϕ u u' : {@eq0_levelalg ϕ u u'} + {~@eq0_levelalg ϕ u u'}.
+Proof.
+  pose proof (@eq0_leq0_levelalg ϕ u u') as H.
+  destruct (@leq0_levelalg_n_dec false ϕ u u'), (@leq0_levelalg_n_dec false ϕ u' u); constructor; destruct H; split_and; now auto.
+Defined.
+
+Definition eq_levelalg_dec {cf ϕ} u u' : {@eq_levelalg cf ϕ u u'} + {~@eq_levelalg cf ϕ u u'}.
+Proof.
+  cbv [eq_levelalg]; destruct ?; auto using eq0_levelalg_dec.
+Defined.
+
+Definition eq_universe__dec {CS eq_levelalg ϕ}
+           (eq_levelalg_dec : forall u u', {@eq_levelalg ϕ u u'} + {~@eq_levelalg ϕ u u'})
+           s s'
+  : {@eq_universe_ CS eq_levelalg ϕ s s'} + {~@eq_universe_ CS eq_levelalg ϕ s s'}.
+Proof.
+  cbv [eq_universe_]; repeat destruct ?; auto.
+Defined.
+
+Definition eq_universe_dec {cf ϕ} s s' : {@eq_universe cf ϕ s s'} + {~@eq_universe cf ϕ s s'} := eq_universe__dec eq_levelalg_dec _ _.
+
+Definition valid_constraints_dec cf ϕ cstrs : {@valid_constraints cf ϕ cstrs} + {~@valid_constraints cf ϕ cstrs}.
+Proof.
+  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.
+  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.
+  pose proof (levels_of_cs2_spec ϕ cstrs).
+  cbn [fst snd] in *.
+  destruct (consistent_dec ϕ); [ | now left; cbv [valid_constraints valid_constraints0 consistent not] in *; destruct ?; intros; eauto; exfalso; eauto ].
+  destruct_head'_and.
+  specialize_under_binders_by assumption.
+  cbv [uGraph.is_graph_of_uctx MCOption.on_Some] in *.
+  cbv [valid_constraints] in *; repeat destruct ?; auto.
+  { specialize_under_binders_by reflexivity.
+    destruct uGraph.check_constraints_gen; specialize_by reflexivity; auto. }
+  { rewrite uGraph.gc_consistent_iff in *.
+    cbv [uGraph.gc_of_uctx monad_utils.bind monad_utils.ret monad_utils.option_monad MCOption.on_Some] in *; cbn [fst snd] in *.
+    destruct ?.
+    all: try congruence.
+    all: exfalso; assumption. }
+Defined.
+
+Definition valid_constraints0_dec ϕ ctrs : {@valid_constraints0 ϕ ctrs} + {~@valid_constraints0 ϕ ctrs}
+  := @valid_constraints_dec config.default_checker_flags ϕ ctrs.
+
+Definition is_lSet_dec cf ϕ s : {@is_lSet cf ϕ s} + {~@is_lSet cf ϕ s}.
+Proof.
+  apply eq_universe_dec.
+Defined.
+
+Definition is_allowed_elimination_dec cf ϕ allowed u : {@is_allowed_elimination cf ϕ allowed u} + {~@is_allowed_elimination cf ϕ allowed u}.
+Proof.
+  cbv [is_allowed_elimination is_true]; destruct ?; auto;
+    try solve [ repeat decide equality ].
+  destruct (@is_lSet_dec cf ϕ u), is_propositional; intuition auto.
+Defined.
diff --git a/common/theories/uGraph.v b/common/theories/uGraph.v
index 18074b8ce..e22b5a4a2 100644
--- a/common/theories/uGraph.v
+++ b/common/theories/uGraph.v
@@ -1429,7 +1429,7 @@ Section CheckLeq.
       gc_expr_declared e' ->
       leqb_expr_n_gen leqb_level_n_gen lt e e' ->
       gc_leq0_levelalg_n lt uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
-  Proof.
+  Proof using Type.
     unfold leqb_expr_n.
     destruct e as [l k], e' as [l' k'];
     try (cbn in *; discriminate);
@@ -1449,7 +1449,7 @@ Section CheckLeq.
       (HHl' : gc_expr_declared e')
     : leqb_expr_n_gen leqb_level_n_gen ⎩ n ⎭ e e'
       <-> gc_leq0_levelalg_n ⎩ n ⎭ uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
-  Proof.
+  Proof using HC.
     split; [apply (leqb_expr_n_spec0_gen _ leqb_correct)|]; try assumption.
     destruct e as [l k] eqn:eqe, e' as [l' k'] eqn:eqe'; cbn; intro H;
       destruct HC as [v0 Hv0]; pose proof (H v0 Hv0) as H0; cbn in H0.
@@ -1471,7 +1471,7 @@ Section CheckLeq.
     n e1 u
     : gc_expr_declared e1 -> gc_levels_declared u -> leqb_expr_univ_n_gen leqb_level_n_gen n e1 u
       -> gc_leq0_levelalg_n n uctx.2 (LevelAlgExpr.make e1) u.
-  Proof.
+  Proof using Type.
     unfold leqb_expr_univ_n_gen; intros He1 Hu H.
     unfold_univ_rel0.
     rewrite val_fold_right.
@@ -1565,7 +1565,7 @@ Section CheckLeq.
       gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e) u ->
       exists (e' : LevelExpr.t), LevelExprSet.In e' u
             /\ gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
-  Proof.
+  Proof using HC HG Huctx.
     intros Hl Hu H.
     assert (HG1 : invariants G) by (rewrite HG; exact _).
     assert (HG2 : acyclic_no_loop G) by (rewrite HG; exact _).
@@ -1855,7 +1855,7 @@ Section CheckLeq.
       (Hu  : gc_levels_declared u)
     : leqb_expr_univ_n_gen leqb_level_n_gen ⎩ lt ⎭ e1 u
       <-> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e1) u.
-  Proof.
+  Proof using HC HG Huctx.
     split; [eapply leqb_expr_univ_n_spec0_gen; eauto|].
     unfold leqb_expr_univ_n_gen; intro HH.
     case_eq (LevelAlgExpr.exprs u). intros e u' ee.
@@ -1889,7 +1889,7 @@ Section CheckLeq.
     (Hu1  : gc_levels_declared u1)
     (Hu2  : gc_levels_declared u2)
 : leqb_levelalg_n_gen leqb_level_n_gen lt u1 u2 -> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 u1 u2.
-  Proof.
+  Proof using Type.
     unfold leqb_levelalg_n_gen. intros H.
     unfold_univ_rel0.
     unfold val, LevelAlgExpr.Evaluable.
@@ -1921,7 +1921,7 @@ Section CheckLeq.
         (Hu2  : gc_levels_declared l2)
     : leqb_levelalg_n_gen leqb_level_n_gen lt l1 l2
       <-> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 l1 l2.
-  Proof.
+  Proof using HC HG Huctx.
     split; [eapply leqb_levelalg_n_spec0_gen; eauto |].
     unfold leqb_levelalg_n_gen; intro HH.
     unfold LevelAlgExpr.exprs.
@@ -1949,7 +1949,7 @@ Section CheckLeq.
      (Hu1  : gc_levels_declared u1)
      (Hu2  : gc_levels_declared u2)
     : check_leqb_levelalg_gen leqb_level_n_gen u1 u2 <-> gc_leq_levelalg uctx.2 u1 u2.
-  Proof.
+  Proof using HC HG Huctx.
     unfold check_leqb_levelalg_gen,
           gc_leq_levelalg, gc_leq_levelalg_n,
           leqb_levelalg_n_gen, gc_leq0_levelalg_n.
@@ -1975,7 +1975,7 @@ Section CheckLeq.
       (Hu1  : gc_levels_declared l1)
       (Hu2  : gc_levels_declared l2)
     : check_eqb_levelalg_gen leqb_level_n_gen l1 l2 <-> gc_eq_levelalg uctx.2 l1 l2.
-  Proof.
+  Proof using HC HG Huctx.
     unfold check_eqb_levelalg_gen, gc_eq_levelalg.
     destruct check_univs; [|split; trivial].
     split; cbn.
@@ -2024,7 +2024,7 @@ Section CheckLeq.
     (Hu1 : gc_levels_declared' uctx.1 gc)
     : check_gc_constraint_gen leqb_level_n_gen gc
       -> if check_univs then forall v, gc_satisfies v uctx.2 -> gc_satisfies0 v gc else True.
-  Proof.
+  Proof using Huctx.
     unfold check_gc_constraint_gen.
     destruct check_univs; [cbn|trivial].
     destruct gc as [l z l'|k l|k n|l k|n k].
@@ -2056,7 +2056,7 @@ Section CheckLeq.
     ctrs (Hu1 : gcs_levels_declared uctx.1 ctrs)
     : check_gc_constraints_gen leqb_level_n_gen ctrs
       -> if check_univs then forall v, gc_satisfies v uctx.2 -> gc_satisfies v ctrs else True.
-  Proof.
+  Proof using Huctx.
     rewrite /gcs_levels_declared in Hu1. pose proof check_gc_constraint_spec_gen as XX.
     unfold check_gc_constraints_gen. destruct check_univs; [cbn|trivial].
     intros HH v Hv.
@@ -3252,3 +3252,56 @@ Proof.
   unfold is_consistent. by move=> /on_SomeP [? [-> <-]].
 Qed.
 
+From MetaCoq.Utils Require Import MCUtils.
+
+Lemma global_uctx_invariants_union_or lvls1 lvls2 cs
+  : global_uctx_invariants (lvls1, cs) \/ global_uctx_invariants (lvls2, cs)
+    -> global_uctx_invariants (LevelSet.union lvls1 lvls2, cs).
+Proof.
+  cbv [global_uctx_invariants uctx_invariants ConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
+  repeat first [ apply conj
+               | progress intros
+               | progress cbv beta iota in *
+               | progress destruct ?
+               | progress destruct_head'_and
+               | progress destruct_head'_or
+               | progress split_and
+               | rewrite !LevelSet.union_spec
+               | progress specialize_dep_under_binders_by eapply pair
+               | solve [ eauto ] ].
+Qed.
+
+Lemma global_gc_uctx_invariants_union_or lvls1 lvls2 cs
+  : global_gc_uctx_invariants (lvls1, cs) \/ global_gc_uctx_invariants (lvls2, cs)
+    -> global_gc_uctx_invariants (VSet.union lvls1 lvls2, cs).
+Proof.
+  cbv [global_gc_uctx_invariants uctx_invariants GoodConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
+  repeat first [ apply conj
+               | progress intros
+               | progress cbv beta iota in *
+               | progress subst
+               | progress destruct ?
+               | progress destruct_head'_and
+               | progress destruct_head'_or
+               | progress split_and
+               | rewrite !VSet.union_spec
+               | progress specialize_dep_under_binders_by eassumption
+               | solve [ eauto ] ].
+Qed.
+
+Lemma gc_levels_declared_union_or lvls1 lvls2 cstr u
+  : gc_levels_declared (lvls1, cstr) u \/ gc_levels_declared (lvls2, cstr) u
+    -> gc_levels_declared (VSet.union lvls1 lvls2, cstr) u.
+Proof.
+  cbv [gc_levels_declared LevelExprSet.For_all gc_expr_declared on_Some_or_None LevelExpr.get_noprop]; cbn [fst].
+  repeat first [ apply conj
+               | progress intros
+               | progress cbv beta iota in *
+               | progress destruct ?
+               | progress destruct_head'_and
+               | progress destruct_head'_or
+               | progress split_and
+               | rewrite !VSet.union_spec
+               | progress specialize_dep_under_binders_by eassumption
+               | solve [ eauto ] ].
+Qed.