Library MetaCoq.Checker.uGraph
Definition on_Some {A} (P : A → Prop) : option A → Prop :=
fun x ⇒ match x with
| Some x ⇒ P x
| None ⇒ False
end.
Definition on_Some_or_None {A} (P : A → Prop) : option A → Prop :=
fun x ⇒ match x with
| Some x ⇒ P x
| None ⇒ True
end.
Lemma InA_In_eq {A} x (l : list A) : InA eq x l ↔ In x l.
Module ConstraintSetFact := WFactsOn UnivConstraintDec ConstraintSet.
Module ConstraintSetProp := WPropertiesOn UnivConstraintDec ConstraintSet.
Inductive variable_level := mLevel (_ : string) | mVar (_ : nat).
Inductive good_constraint :=
| gc_le : variable_level → variable_level → good_constraint
| gc_lt : variable_level → variable_level → good_constraint
| gc_lt_set : nat → good_constraint
| gc_eq_set : nat → good_constraint.
Module GoodConstraintDec.
Definition t : Set := good_constraint.
Definition eq : t → t → Prop := eq.
Definition eq_equiv : RelationClasses.Equivalence eq := _.
Definition variable_level_dec : ∀ x y : variable_level, {x = y} + {x ≠ y}.
Defined.
Definition eq_dec : ∀ x y : t, {eq x y} + {¬ eq x y}.
Defined.
End GoodConstraintDec.
Module GoodConstraintSet := MSets.MSetWeakList.Make GoodConstraintDec.
Module GoodConstraintSetFact := WFactsOn GoodConstraintDec GoodConstraintSet.
Module GoodConstraintSetProp := WPropertiesOn GoodConstraintDec GoodConstraintSet.
Definition GoodConstraintSet_pair x y
:= GoodConstraintSet.add y (GoodConstraintSet.singleton x).
Lemma GoodConstraintSet_pair_In x y z
: GoodConstraintSet.In x (GoodConstraintSet_pair y z)
→ x = y ∨ x = z.
Definition gc_val0 (v : valuation) (l : variable_level) : nat :=
match l with
| mLevel s ⇒ Pos.to_nat (v.(valuation_mono) s)
| mVar x ⇒ v.(valuation_poly) x
end.
Definition gc_satisfies0 v (gc : good_constraint) : bool :=
match gc with
| gc_le l l' ⇒ gc_val0 v l <=? gc_val0 v l'
| gc_lt l l' ⇒ gc_val0 v l <? gc_val0 v l'
| gc_lt_set l ⇒ 0 <? v.(valuation_poly) l
| gc_eq_set l ⇒ 0 =? v.(valuation_poly) l
end.
Definition gc_satisfies v : GoodConstraintSet.t → bool :=
GoodConstraintSet.for_all (gc_satisfies0 v).
Definition gc_consistent ctrs : Prop := ∃ v, gc_satisfies v ctrs.
Lemma gc_satisfies_pair v gc1 gc2 :
(gc_satisfies0 v gc1 ∧ gc_satisfies0 v gc2) ↔
gc_satisfies v (GoodConstraintSet_pair gc1 gc2).
Definition gc_of_constraint `{checker_flags} (uc : univ_constraint) : option GoodConstraintSet.t
:= let empty := Some GoodConstraintSet.empty in
let singleton := fun x ⇒ Some (GoodConstraintSet.singleton x) in
let pair := fun x y ⇒ Some (GoodConstraintSet_pair x y) in
match uc with
| (Level.lProp, Le, Level.lProp) ⇒ empty
| (Level.lProp, Le, _) ⇒ if prop_sub_type then empty else None
| (Level.lProp, Eq, Level.lProp) ⇒ empty
| (Level.lProp, Eq, _) ⇒ None
| (Level.lProp, Lt, Level.lProp) ⇒ None
| (Level.lProp, Lt, _) ⇒ if prop_sub_type then empty else None
| (Level.lSet, Le, Level.lProp) ⇒ None
| (Level.lSet, Le, _) ⇒ empty
| (Level.lSet, Eq, Level.lProp) ⇒ None
| (Level.lSet, Eq, Level.lSet) ⇒ empty
| (Level.lSet, Eq, Level.Level _) ⇒ None
| (Level.lSet, Eq, Level.Var n) ⇒ singleton (gc_eq_set n)
| (Level.lSet, Lt, Level.lProp) ⇒ None
| (Level.lSet, Lt, Level.lSet) ⇒ None
| (Level.lSet, Lt, Level.Level _) ⇒ empty
| (Level.lSet, Lt, Level.Var n) ⇒ singleton (gc_lt_set n)
| (Level.Level _, Le, Level.lProp) ⇒ None
| (Level.Level _, Le, Level.lSet) ⇒ None
| (Level.Level l, Le, Level.Level l')
⇒ singleton (gc_le (mLevel l) (mLevel l'))
| (Level.Level l, Le, Level.Var n) ⇒ singleton (gc_le (mLevel l) (mVar n))
| (Level.Level _, Eq, Level.lProp) ⇒ None
| (Level.Level _, Eq, Level.lSet) ⇒ None
| (Level.Level l, Eq, Level.Level l')
⇒ pair (gc_le (mLevel l) (mLevel l')) (gc_le (mLevel l') (mLevel l))
| (Level.Level l, Eq, Level.Var n)
⇒ pair (gc_le (mLevel l) (mVar n)) (gc_le (mVar n) (mLevel l))
| (Level.Level _, Lt, Level.lProp) ⇒ None
| (Level.Level _, Lt, Level.lSet) ⇒ None
| (Level.Level l, Lt, Level.Level l')
⇒ singleton (gc_lt (mLevel l) (mLevel l'))
| (Level.Level l, Lt, Level.Var n) ⇒ singleton (gc_lt (mLevel l) (mVar n))
| (Level.Var _, Le, Level.lProp) ⇒ None
| (Level.Var n, Le, Level.lSet) ⇒ singleton (gc_eq_set n)
| (Level.Var n, Le, Level.Level l) ⇒ singleton (gc_le (mVar n) (mLevel l))
| (Level.Var n, Le, Level.Var n') ⇒ singleton (gc_le (mVar n) (mVar n'))
| (Level.Var _, Eq, Level.lProp) ⇒ None
| (Level.Var n, Eq, Level.lSet) ⇒ singleton (gc_eq_set n)
| (Level.Var n, Eq, Level.Level l)
⇒ pair (gc_le (mVar n) (mLevel l)) (gc_le (mLevel l) (mVar n))
| (Level.Var n, Eq, Level.Var n')
⇒ pair (gc_le (mVar n) (mVar n')) (gc_le (mVar n') (mVar n))
| (Level.Var _, Lt, Level.lProp) ⇒ None
| (Level.Var _, Lt, Level.lSet) ⇒ None
| (Level.Var n, Lt, Level.Level l) ⇒ singleton (gc_lt (mVar n) (mLevel l))
| (Level.Var n, Lt, Level.Var n') ⇒ singleton (gc_lt (mVar n) (mVar n'))
end.
Section GC.
Context `{cf : checker_flags}.
Lemma gc_of_constraint_spec v uc :
satisfies0 v uc ↔ on_Some (gc_satisfies v) (gc_of_constraint uc).
Definition add_gc_of_constraint uc (S : option GoodConstraintSet.t)
:= S1 <- S ;;
S2 <- gc_of_constraint uc ;;
ret (GoodConstraintSet.union S1 S2).
Definition gc_of_constraints (ctrs : constraints) : option GoodConstraintSet.t
:= ConstraintSet.fold add_gc_of_constraint
ctrs (Some GoodConstraintSet.empty).
Lemma gc_of_constraints_spec v ctrs :
satisfies v ctrs ↔ on_Some (gc_satisfies v) (gc_of_constraints ctrs).
Lemma gc_consistent_iff ctrs :
consistent ctrs ↔ on_Some gc_consistent (gc_of_constraints ctrs).
Definition gc_leq_universe_n n ctrs u u'
:= ∀ v, gc_satisfies v ctrs → (Z.of_nat n + val v u ≤ val v u')%Z.
Definition gc_eq_universe0 φ u u' :=
∀ v, gc_satisfies v φ → val v u = val v u'.
Definition gc_leq_universe φ u u'
:= if check_univs then gc_leq_universe_n 0 φ u u' else True.
Definition gc_eq_universe φ u u'
:= if check_univs then gc_eq_universe0 φ u u' else True.
Lemma gc_leq_universe_n_iff n ctrs u u' :
leq_universe_n n ctrs u u'
↔ on_Some_or_None (fun ctrs ⇒ gc_leq_universe_n n ctrs u u')
(gc_of_constraints ctrs).
Lemma gc_eq_universe0_iff ctrs u u' :
eq_universe0 ctrs u u'
↔ on_Some_or_None (fun ctrs ⇒ gc_eq_universe0 ctrs u u')
(gc_of_constraints ctrs).
Lemma gc_leq_universe_iff ctrs u u' :
leq_universe ctrs u u'
↔ on_Some_or_None (fun ctrs ⇒ gc_leq_universe ctrs u u')
(gc_of_constraints ctrs).
Lemma gc_eq_universe_iff ctrs u u' :
eq_universe ctrs u u'
↔ on_Some_or_None (fun ctrs ⇒ gc_eq_universe ctrs u u')
(gc_of_constraints ctrs).
End GC.
Inductive no_prop_level := lSet | vtn (l : variable_level).
Coercion vtn : variable_level >-> no_prop_level.
Module VariableLevel.
Definition t := variable_level.
Definition lt : t → t → Prop :=
fun x y ⇒ match x, y with
| mLevel _, mVar _ ⇒ True
| mLevel s, mLevel s' ⇒ string_lt s s'
| mVar n, mVar n' ⇒ n < n'
| mVar _, mLevel _ ⇒ False
end.
Definition lt_strorder : StrictOrder lt.
Qed.
Definition lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) lt.
Qed.
Definition compare : t → t → comparison :=
fun x y ⇒ match x, y with
| mLevel _, mVar _ ⇒ Datatypes.Lt
| mLevel s, mLevel s' ⇒ string_compare s s'
| mVar n, mVar n' ⇒ Nat.compare n n'
| mVar _, mLevel _ ⇒ Datatypes.Gt
end.
Definition compare_spec :
∀ x y : t, CompareSpec (x = y) (lt x y) (lt y x) (compare x y).
Qed.
Definition eq_dec : ∀ x y : t, {x = y} + {x ≠ y}.
Defined.
End VariableLevel.
Module NoPropLevel.
Definition t : Set := no_prop_level.
Definition eq : t → t → Prop := eq.
Definition eq_equiv : RelationClasses.Equivalence eq := _.
Definition lt : t → t → Prop :=
fun x y ⇒ match x, y with
| lSet, lSet ⇒ False
| lSet, vtn _ ⇒ True
| vtn v, vtn v' ⇒ VariableLevel.lt v v'
| vtn _, lSet ⇒ False
end.
Definition lt_strorder : StrictOrder lt.
Qed.
Definition lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) lt.
Qed.
Definition compare : t → t → comparison :=
fun x y ⇒ match x, y with
| lSet, lSet ⇒ Datatypes.Eq
| lSet, vtn _ ⇒ Datatypes.Lt
| vtn v, vtn v' ⇒ VariableLevel.compare v v'
| vtn _, lSet ⇒ Datatypes.Gt
end.
Definition compare_spec :
∀ x y : t, CompareSpec (x = y) (lt x y) (lt y x) (compare x y).
Qed.
Definition eq_dec : ∀ x y : t, {x = y} + {x ≠ y}.
Defined.
End NoPropLevel.
Module Import wGraph := wGraph.WeightedGraph NoPropLevel.
Definition universes_graph := wGraph.t.
Definition init_graph : universes_graph
:= (VSet.singleton lSet, EdgeSet.empty, lSet).
Lemma init_graph_invariants : invariants init_graph.
Definition no_prop_of_level l :=
match l with
| Level.lProp ⇒ None
| Level.lSet ⇒ Some lSet
| Level.Level s ⇒ Some (vtn (mLevel s))
| Level.Var n ⇒ Some (vtn (mVar n))
end.
Definition no_prop_levels (X : LevelSet.t) : VSet.t
:= LevelSet.fold (fun l X ⇒ match no_prop_of_level l with
| Some l ⇒ VSet.add l X
| None ⇒ X
end)
X VSet.empty.
Definition declared := LevelSet.In.
Definition uctx_invariants (uctx : ContextSet.t)
:= ConstraintSet.For_all (fun '(l, _, l') ⇒ declared l uctx.1 ∧ declared l' uctx.1)
uctx.2.
Definition global_uctx_invariants (uctx : ContextSet.t)
:= LevelSet.In Level.lSet uctx.1 ∧ uctx_invariants uctx.
Definition global_gc_uctx_invariants (uctx : VSet.t × GoodConstraintSet.t)
:= VSet.In lSet uctx.1 ∧ GoodConstraintSet.For_all (fun gc ⇒ match gc with
| gc_le l l'
| gc_lt l l' ⇒ VSet.In l uctx.1 ∧ VSet.In l' uctx.1
| gc_lt_set n
| gc_eq_set n ⇒ VSet.In (mVar n) uctx.1
end) uctx.2.
Definition gc_of_uctx `{checker_flags} (uctx : ContextSet.t)
: option (VSet.t × GoodConstraintSet.t)
:= ctrs <- gc_of_constraints uctx.2 ;;
ret (no_prop_levels uctx.1, ctrs).
Definition level_of_variable l :=
match l with
| mLevel s ⇒ Level.Level s
| mVar n ⇒ Level.Var n
end.
Definition level_of_no_prop l :=
match l with
| lSet ⇒ Level.lSet
| vtn l ⇒ level_of_variable l
end.
Coercion level_of_no_prop : no_prop_level >-> Level.t.
Lemma no_prop_of_level_no_prop l
: no_prop_of_level (level_of_no_prop l) = Some l.
Lemma no_prop_levels_no_prop_level (l : no_prop_level) levels
: declared l levels → VSet.In l (no_prop_levels levels).
Lemma gc_of_constraint_iff `{cf:checker_flags} ctrs0 ctrs gc
(HH : gc_of_constraints ctrs0 = Some ctrs)
: GoodConstraintSet.In gc ctrs
↔ ConstraintSet.Exists
(fun e ⇒ on_Some (GoodConstraintSet.In gc) (gc_of_constraint e)) ctrs0.
Lemma gc_of_uctx_invariants `{cf:checker_flags} uctx uctx'
(H : gc_of_uctx uctx = Some uctx')
: global_uctx_invariants uctx → global_gc_uctx_invariants uctx'.
Definition edge_of_level (l : variable_level) : EdgeSet.elt :=
match l with
| mLevel l ⇒ (lSet, 1, vtn (mLevel l))
| mVar n ⇒ (lSet, 0, vtn (mVar n))
end.
Definition EdgeSet_pair x y
:= EdgeSet.add y (EdgeSet.singleton x).
Definition EdgeSet_triple x y z
:= EdgeSet.add z (EdgeSet_pair x y).
Definition edge_of_constraint (gc : good_constraint) : EdgeSet.elt :=
match gc with
| gc_le l l' ⇒ (vtn l, 0, vtn l')
| gc_lt l l' ⇒ (vtn l, 1, vtn l')
| gc_lt_set n ⇒ (lSet, 1, vtn (mVar n))
| gc_eq_set n ⇒ (vtn (mVar n), 0, lSet)
end.
Definition vtn_inj x y : vtn x = vtn y → x = y.
Definition vtn_lSet x : vtn x ≠ lSet.
Lemma source_edge_of_level g : (edge_of_level g)..s = lSet.
Lemma target_edge_of_level g : (edge_of_level g)..t = g.
Definition make_graph (uctx : VSet.t × GoodConstraintSet.t) : wGraph.t :=
let init_edges := VSet.fold (fun l E ⇒ match l with
| vtn l ⇒ EdgeSet.add (edge_of_level l) E
| lSet ⇒ E end) uctx.1 EdgeSet.empty in
let edges := GoodConstraintSet.fold
(fun ctr ⇒ EdgeSet.add (edge_of_constraint ctr)) uctx.2 init_edges in
(uctx.1, edges, lSet).
Lemma make_graph_E uctx e
: EdgeSet.In e (wGraph.E (make_graph uctx))
↔ (∃ l, VSet.In (vtn l) uctx.1 ∧ e = edge_of_level l)
∨ (GoodConstraintSet.Exists (fun gc ⇒ e = edge_of_constraint gc) uctx.2).
Lemma make_graph_invariants uctx (Hi : global_gc_uctx_invariants uctx)
: invariants (make_graph uctx).
Definition labelling_of_valuation (v : valuation) : labelling
:= fun x ⇒ match x with
| lSet ⇒ 0
| vtn (mLevel l) ⇒ Pos.to_nat (v.(valuation_mono) l)
| vtn (mVar n) ⇒ v.(valuation_poly) n
end.
Definition valuation_of_labelling (l : labelling) : valuation
:= {| valuation_mono := fun s ⇒ Pos.of_nat (l (vtn (mLevel s)));
valuation_poly := fun n ⇒ l (vtn (mVar n)) |}.
Section MakeGraph.
Context uctx (Huctx : global_gc_uctx_invariants uctx).
Let ctrs := uctx.2.
Let G : universes_graph := make_graph uctx.
Lemma valuation_labelling_eq l (Hl : correct_labelling G l)
: ∀ x, VSet.In x uctx.1
→ labelling_of_valuation (valuation_of_labelling l) x = l x.
Lemma make_graph_spec v :
gc_satisfies v ctrs ↔ correct_labelling G (labelling_of_valuation v).
Corollary make_graph_spec' l :
correct_labelling G l → gc_satisfies (valuation_of_labelling l) ctrs.
Corollary make_graph_spec2 :
gc_consistent ctrs ↔ ∃ l, correct_labelling G l.
Corollary consistent_no_loop : gc_consistent ctrs → acyclic_no_loop G.
End MakeGraph.
Definition is_consistent `{checker_flags} uctx :=
match gc_of_uctx uctx with
| Some uctx ⇒ is_acyclic (make_graph uctx)
| None ⇒ false
end.
Lemma is_consistent_spec `{checker_flags} uctx (Huctx : global_uctx_invariants uctx)
: is_consistent uctx ↔ consistent uctx.2.
Section CheckLeq.
Context {cf:checker_flags}.
Context (G : universes_graph)
uctx (Huctx: global_gc_uctx_invariants uctx) (HC : gc_consistent uctx.2)
(HG : G = make_graph uctx).
Lemma val_level_of_variable_level v (l : variable_level)
: val0 v l = Z.of_nat (gc_val0 v l).
Lemma labelling_of_valuation_val0 v (l : no_prop_level)
: Z.of_nat (labelling_of_valuation v l) = val0 v l.
Lemma leq_universe_vertices0 n (l l' : no_prop_level)
: leq_vertices G n l l'
→ gc_leq_universe_n n uctx.2 (Universe.make l) (Universe.make l').
Lemma leq_universe_vertices1 n l l'
(Hl : VSet.In l (wGraph.V G)) (Hl' : VSet.In l' (wGraph.V G))
: gc_leq_universe_n n uctx.2 (Universe.make l) (Universe.make l')
→ leq_vertices G n l l'.
Lemma leq_universe_vertices n (l l' : no_prop_level)
(Hl : VSet.In l (wGraph.V G)) (Hl' : VSet.In l' (wGraph.V G))
: gc_leq_universe_n n uctx.2 (Universe.make l) (Universe.make l')
↔ leq_vertices G n l l'.
Definition leqb_no_prop_n n (l l' : no_prop_level)
:= leqb_vertices G n l l'.
Lemma leqb_no_prop_n_spec0 n l l'
: leqb_no_prop_n n l l'
→ gc_leq_universe_n n uctx.2 (Universe.make l) (Universe.make l').
Lemma leqb_no_prop_n_spec n l l'
(Hl : VSet.In l uctx.1) (Hl' : VSet.In l' uctx.1)
: leqb_no_prop_n n l l'
↔ gc_leq_universe_n n uctx.2 (Universe.make l) (Universe.make l').
Definition leqb_level_n n l l' :=
match no_prop_of_level l, no_prop_of_level l' with
| None, None ⇒ n =? 0
| None, Some l' ⇒ match n with
| O ⇒ true
| S n ⇒ leqb_no_prop_n n lSet l'
end
| Some l, None ⇒ false
| Some l, Some l' ⇒ leqb_no_prop_n n l l'
end.
Lemma no_prop_of_level_inv {l l0}
: no_prop_of_level l = Some l0 → level_of_no_prop l0 = l.
Definition gc_level_declared l
:= on_Some_or_None (fun l ⇒ VSet.In l uctx.1) (no_prop_of_level l).
Lemma leqb_level_n_spec0 n l l'
: leqb_level_n n l l'
→ gc_leq_universe_n n uctx.2 (Universe.make l) (Universe.make l').
Lemma leqb_level_n_spec n l l'
(HHl : gc_level_declared l)
(HHl' : gc_level_declared l')
: leqb_level_n n l l'
↔ gc_leq_universe_n n uctx.2 (Universe.make l) (Universe.make l').
Definition leqb_level l l' := negb check_univs || leqb_level_n 0 l l'.
Definition eqb_level l l' := leqb_level l l' && leqb_level l' l.
Definition eqb_univ_instance (u1 u2 : universe_instance)
:= forallb2 eqb_level u1 u2.
Definition leqb_expr_n n (e1 e2 : Universe.Expr.t) :=
match e1.2 && negb (Level.is_prop e1.1), e2.2 && negb (Level.is_prop e2.1) with
| false, false
| true, true ⇒ leqb_level_n n e1.1 e2.1
| true, false ⇒ leqb_level_n (S n) e1.1 e2.1
| false, true ⇒ leqb_level_n (Peano.pred n) e1.1 e2.1
end.
Lemma no_prop_of_level_not_is_prop {l l0}
: no_prop_of_level l = Some l0 → Level.is_prop l = false.
Lemma no_prop_of_level_is_prop {l}
: no_prop_of_level l = None → Level.is_prop l = true.
Conjecture constraint_strengthening : ∀ l l',
(∀ v, gc_satisfies v uctx.2 → (val0 v l ≤ val0 v l' + 1)%Z) →
∀ v, gc_satisfies v uctx.2 → (val0 v l ≤ val0 v l')%Z.
Lemma leqb_expr_n_spec0 n e e'
: leqb_expr_n n e e'
→ gc_leq_universe_n n uctx.2 (Universe.make' e) (Universe.make' e').
Lemma leqb_expr_n_spec n e e'
(HHl : gc_level_declared e.1)
(HHl' : gc_level_declared e'.1)
: leqb_expr_n n e e'
↔ gc_leq_universe_n n uctx.2 (Universe.make' e) (Universe.make' e').
Fixpoint leqb_univ_expr_n n (u : universe) (e2 : Universe.Expr.t) :=
match u with
| NEL.sing e1 ⇒ leqb_expr_n n e1 e2
| NEL.cons e1 u ⇒ leqb_expr_n n e1 e2 && leqb_univ_expr_n n u e2
end.
Definition gc_levels_declared (u : universe)
:= List.Forall (fun e ⇒ gc_level_declared e.1) (NEL.to_list u).
Lemma leqb_univ_expr_n_spec0 n u e2
: leqb_univ_expr_n n u e2
→ gc_leq_universe_n n uctx.2 u (Universe.make' e2).
Lemma leqb_univ_expr_n_spec n u e2
(Hu : gc_levels_declared u)
(He2 : gc_level_declared e2.1)
: leqb_univ_expr_n n u e2
↔ gc_leq_universe_n n uctx.2 u (Universe.make' e2).
Definition leqb_univ_expr u e2 :=
negb check_univs || leqb_univ_expr_n 0 u e2.
Fixpoint try_leqb_universe_n n (u1 u2 : universe) :=
match u2 with
| NEL.sing e ⇒ leqb_univ_expr_n n u1 e
| NEL.cons e u2 ⇒ leqb_univ_expr_n n u1 e || try_leqb_universe_n n u1 u2
end.
Lemma try_leqb_universe_n_spec n u1 u2
: try_leqb_universe_n n u1 u2 → gc_leq_universe_n n uctx.2 u1 u2.
Definition try_leqb_universe (u1 u2 : universe) :=
negb check_univs || try_leqb_universe_n 0 u1 u2.
Definition try_eqb_universe (u1 u2 : universe) :=
negb check_univs || (try_leqb_universe_n 0 u1 u2 && try_leqb_universe_n 0 u2 u1).
Definition check_gc_constraint (gc : good_constraint) :=
negb check_univs || match gc with
| gc_le l l' ⇒ leqb_no_prop_n 0 l l'
| gc_lt l l' ⇒ leqb_no_prop_n 1 l l'
| gc_lt_set n ⇒ leqb_no_prop_n 1 lSet (mVar n)
| gc_eq_set n ⇒ leqb_no_prop_n 0 (mVar n) lSet
end.
Definition check_gc_constraints
:= GoodConstraintSet.for_all check_gc_constraint.
Definition check_constraints ctrs :=
match gc_of_constraints ctrs with
| Some ctrs ⇒ check_gc_constraints ctrs
| None ⇒ false
end.
Lemma toto l : level_of_no_prop (vtn l) = level_of_variable l.
Lemma check_gc_constraint_spec gc
: check_gc_constraint gc
→ if check_univs then ∀ v, gc_satisfies v uctx.2 → gc_satisfies0 v gc else True.
Lemma check_gc_constraints_spec ctrs
: check_gc_constraints ctrs
→ if check_univs then ∀ v, gc_satisfies v uctx.2 → gc_satisfies v ctrs else True.
End CheckLeq.
Section CheckLeq2.
Context {cf:checker_flags}.
Definition is_graph_of_uctx G uctx
:= on_Some (fun uctx ⇒ make_graph uctx = G) (gc_of_uctx uctx).
Context (G : universes_graph)
uctx (Huctx: global_uctx_invariants uctx) (HC : consistent uctx.2)
(HG : is_graph_of_uctx G uctx).
Let uctx' : VSet.t × GoodConstraintSet.t.
Defined.
Let Huctx': global_gc_uctx_invariants uctx'.
Qed.
Let HC' : gc_consistent uctx'.2.
Qed.
Let HG' : G = make_graph uctx'.
Qed.
Definition level_declared l := LevelSet.In l uctx.1.
Definition levels_declared (u : universe)
:= List.Forall (fun e ⇒ level_declared e.1) (NEL.to_list u).
Lemma level_gc_declared_declared l
: level_declared l → gc_level_declared uctx' l.
Lemma levels_gc_declared_declared u
: levels_declared u → gc_levels_declared uctx' u.
Lemma leqb_univ_expr_n_spec' n u e2
(Hu : levels_declared u)
(He2 : level_declared e2.1)
: leqb_univ_expr_n G n u e2
↔ leq_universe_n n uctx.2 u (Universe.make' e2).
Lemma try_leqb_universe_spec u1 u2
: try_leqb_universe G u1 u2 → leq_universe uctx.2 u1 u2.
Lemma eq_leq_universe φ u u' :
eq_universe0 φ u u' ↔ leq_universe0 φ u u' ∧ leq_universe0 φ u' u.
Lemma try_eqb_universe_spec u1 u2
: try_eqb_universe G u1 u2 → eq_universe uctx.2 u1 u2.
Lemma check_constraints_spec ctrs
: check_constraints G ctrs → valid_constraints uctx.2 ctrs.
End CheckLeq2.