Add boolean versions of the varieties of extends

common/_CoqProject.in

@@ -11,5 +11,6 @@ theories/MonadBasicAst.v
 theories/Environment.v
 theories/Reflect.v
 theories/EnvironmentTyping.v
+theories/EnvironmentReflect.v
 theories/EnvMap.v
 theories/Transform.v

common/theories/Environment.v

@@ -2,7 +2,7 @@
 From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes.
-From Equations.Prop Require Import Classes.
+From Equations.Prop Require Import Classes EqDecInstances.
 
 Module Type Term.
 
@@ -28,8 +28,13 @@ End Term.
 
 Module Type TermDecide (Import T : Term).
   #[export] Declare Instance term_eq_dec : EqDec term.
+  #[export] Hint Extern 0 (ReflectEq term) => exact (@EqDec_ReflectEq term term_eq_dec) : typeclass_instances.
 End TermDecide.
 
+Module TermDecideReflectInstances (Import T : Term) (Import TDec : TermDecide T).
+  #[export] Hint Extern 0 (ReflectEq term) => exact (@EqDec_ReflectEq term term_eq_dec) : typeclass_instances.
+End TermDecideReflectInstances.
+
 Module Retroknowledge.
 
   Record t := mk_retroknowledge {
@@ -44,6 +49,20 @@ Module Retroknowledge.
     option_extends x.(retro_float64) y.(retro_float64).
   Existing Class extends.
 
+  Definition extendsb (x y : t) :=
+    option_extendsb x.(retro_int63) y.(retro_int63) &&
+    option_extendsb x.(retro_float64) y.(retro_float64).
+
+  Lemma extendsT x y : reflect (extends x y) (extendsb x y).
+  Proof.
+    rewrite /extends/extendsb; do 2 case: option_extendsT; cbn; constructor; intuition.
+  Qed.
+
+  Lemma extends_spec x y : extendsb x y <-> extends x y.
+  Proof.
+    rewrite /extends/extendsb -!option_extends_spec /is_true !Bool.andb_true_iff //=.
+  Qed.
+
   #[global] Instance extends_refl x : extends x x.
   Proof.
     split; apply option_extends_refl.
@@ -54,7 +73,15 @@ Module Retroknowledge.
     intros x y z [] []; split; cbn; now etransitivity; tea.
   Qed.
 
+  #[export,program] Instance reflect_t : ReflectEq t := {
+      eqb x y := (x.(retro_int63) == y.(retro_int63)) &&
+                   (x.(retro_float64) == y.(retro_float64))
+    }.
+  Next Obligation.
+    do 2 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence.
+  Qed.
 End Retroknowledge.
+Export (hints) Retroknowledge.
 
 Module Environment (T : Term).
 
@@ -983,8 +1010,25 @@ Module Type EnvironmentDecide (T : Term) (Import E : EnvironmentSig T).
   #[export] Declare Instance mutual_inductive_body_eq_dec : EqDec mutual_inductive_body.
   #[export] Declare Instance constant_body_eq_dec : EqDec constant_body.
   #[export] Declare Instance global_decl_eq_dec : EqDec global_decl.
+  #[export] Hint Extern 0 (ReflectEq context) => exact (@EqDec_ReflectEq context context_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq constructor_body) => exact (@EqDec_ReflectEq constructor_body constructor_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq projection_body) => exact (@EqDec_ReflectEq projection_body projection_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq one_inductive_body) => exact (@EqDec_ReflectEq one_inductive_body one_inductive_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq mutual_inductive_body) => exact (@EqDec_ReflectEq mutual_inductive_body mutual_inductive_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq constant_body) => exact (@EqDec_ReflectEq constant_body constant_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq global_decl) => exact (@EqDec_ReflectEq global_decl global_decl_eq_dec) : typeclass_instances.
 End EnvironmentDecide.
 
+Module EnvironmentDecideReflectInstances (T : Term) (Import E : EnvironmentSig T) (Import EDec : EnvironmentDecide T E).
+  #[export] Hint Extern 0 (ReflectEq context) => exact (@EqDec_ReflectEq context context_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq constructor_body) => exact (@EqDec_ReflectEq constructor_body constructor_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq projection_body) => exact (@EqDec_ReflectEq projection_body projection_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq one_inductive_body) => exact (@EqDec_ReflectEq one_inductive_body one_inductive_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq mutual_inductive_body) => exact (@EqDec_ReflectEq mutual_inductive_body mutual_inductive_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq constant_body) => exact (@EqDec_ReflectEq constant_body constant_body_eq_dec) : typeclass_instances.
+  #[export] Hint Extern 0 (ReflectEq global_decl) => exact (@EqDec_ReflectEq global_decl global_decl_eq_dec) : typeclass_instances.
+End EnvironmentDecideReflectInstances.
+
 Module Type TermUtils (T: Term) (E: EnvironmentSig T).
   Import T E.
 

common/theories/EnvironmentReflect.v

@@ -0,0 +1,119 @@
+(* Distributed under the terms of the MIT license. *)
+From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Common Require Import BasicAst Primitive Universes Environment Reflect.
+From Equations.Prop Require Import Classes EqDecInstances.
+
+Module EnvironmentReflect (T : Term) (Import E : EnvironmentSig T) (Import TDec : TermDecide T) (Import EDec : EnvironmentDecide T E).
+
+  Local Notation extendsb_decls_part Σ Σ'
+    := (forallb (fun d => let c := d.1 in skipn (#|lookup_envs Σ' c| - #|lookup_envs Σ c|) (lookup_envs Σ' c) == lookup_envs Σ c) (declarations Σ)) (only parsing).
+  Local Notation strictly_extendsb_decls_part Σ Σ'
+    := (skipn (#|Σ'.(declarations)| - #|Σ.(declarations)|) Σ'.(declarations) == Σ.(declarations)) (only parsing).
+
+  Lemma extends_decls_partT (Σ Σ' : global_env)
+    : reflectT (forall c, ∑ decls, lookup_envs Σ' c = decls ++ lookup_envs Σ c) (extendsb_decls_part Σ Σ').
+  Proof.
+    case: (@forallbP _ _ _ _ (fun _ => eqb_specT _ _)) => H; constructor.
+    all: setoid_rewrite Forall_forall in H.
+    { move => c.
+      specialize (fun d => H (c, d)).
+      cbn [fst] in *.
+      specialize (fun pf : { d : _ | In (c, d) _ } => H (proj1_sig pf) (proj2_sig pf)).
+      destruct (lookup_envs Σ c) eqn:H'.
+      { eexists; rewrite app_nil_r; reflexivity. }
+      rewrite <- H; clear H.
+      { eexists; symmetry; apply firstn_skipn. }
+      unfold lookup_envs in *.
+      move: H'; elim: (declarations Σ); cbn [lookup_globals] => //= ??.
+      case: eqb_specT => ?; subst.
+      all: move => H H'; try destruct (H H'); rdest; eauto. }
+    { intro H'; apply H; clear H; intros [c ?]; specialize (H' c).
+      destruct H' as [decls H'].
+      cbn [fst].
+      rewrite H' app_length Nat.add_sub skipn_all_app //. }
+  Qed.
+
+  Lemma strictly_extends_decls_partT (Σ Σ' : global_env)
+    : reflectT (∑ Σ'', declarations Σ' = Σ'' ++ declarations Σ) (strictly_extendsb_decls_part Σ Σ').
+  Proof.
+    case: eqb_specT => H; constructor.
+    { rewrite -H.
+      eexists; symmetry; apply firstn_skipn. }
+    { move => [Σ'' H'].
+      move: H. rewrite H' app_length Nat.add_sub skipn_all_app //. }
+  Qed.
+
+  Definition extendsb (Σ Σ' : global_env) : bool
+    := Σ.(universes) ⊂?_cs Σ'.(universes)
+       && extendsb_decls_part Σ Σ'
+       && Retroknowledge.extendsb Σ.(retroknowledge) Σ'.(retroknowledge).
+
+  Definition extends_declsb (Σ Σ' : global_env) : bool
+    := (Σ.(universes) == Σ'.(universes))
+       && extendsb_decls_part Σ Σ'
+       && (Σ.(retroknowledge) == Σ'.(retroknowledge)).
+
+  Definition extends_strictly_on_declsb (Σ Σ' : global_env) : bool
+    := (Σ.(universes) ⊂?_cs Σ'.(universes))
+       && strictly_extendsb_decls_part Σ Σ'
+       && Retroknowledge.extendsb Σ.(retroknowledge) Σ'.(retroknowledge).
+
+  Definition strictly_extends_declsb (Σ Σ' : global_env) : bool
+    := (Σ.(universes) == Σ'.(universes))
+       && strictly_extendsb_decls_part Σ Σ'
+       && (Σ.(retroknowledge) == Σ'.(retroknowledge)).
+
+  Lemma extendsT Σ Σ' : reflectT (extends Σ Σ') (extendsb Σ Σ').
+  Proof.
+    rewrite /extends/extendsb.
+    case: extends_decls_partT; case: Retroknowledge.extendsT; case: ContextSet.subsetP; cbn;
+      constructor; intuition.
+  Qed.
+
+  Lemma extends_declsT Σ Σ' : reflectT (extends_decls Σ Σ') (extends_declsb Σ Σ').
+  Proof.
+    rewrite /extends_decls/extends_declsb.
+    case: extends_decls_partT; case: eqb_specT; case: eqb_specT; cbn;
+      constructor; intuition.
+  Qed.
+
+  Lemma extends_strictly_on_declsT Σ Σ' : reflectT (extends_strictly_on_decls Σ Σ') (extends_strictly_on_declsb Σ Σ').
+  Proof.
+    rewrite /extends_strictly_on_decls/extends_strictly_on_declsb.
+    case: strictly_extends_decls_partT; case: Retroknowledge.extendsT; case: ContextSet.subsetP; cbn;
+      constructor; intuition.
+  Qed.
+
+  Lemma strictly_extends_declsT Σ Σ' : reflectT (strictly_extends_decls Σ Σ') (strictly_extends_declsb Σ Σ').
+  Proof.
+    rewrite /strictly_extends_decls/strictly_extends_declsb.
+    case: strictly_extends_decls_partT; case: eqb_specT; case: eqb_specT; cbn;
+      constructor; intuition.
+  Qed.
+
+  Lemma extends_spec Σ Σ' : extendsb Σ Σ' <~> extends Σ Σ'.
+  Proof.
+    case: extendsT; split; intuition congruence.
+  Qed.
+
+  Lemma extends_decls_spec Σ Σ' : extends_declsb Σ Σ' <~> extends_decls Σ Σ'.
+  Proof.
+    case: extends_declsT; split; intuition congruence.
+  Qed.
+
+  Lemma extends_strictly_on_decls_spec Σ Σ' : extends_strictly_on_declsb Σ Σ' <~> extends_strictly_on_decls Σ Σ'.
+  Proof.
+    case: extends_strictly_on_declsT; split; intuition congruence.
+  Qed.
+
+  Lemma strictly_extends_decls_spec Σ Σ' : strictly_extends_declsb Σ Σ' <~> strictly_extends_decls Σ Σ'.
+  Proof.
+    case: strictly_extends_declsT; split; intuition congruence.
+  Qed.
+
+End EnvironmentReflect.
+
+Module Type EnvironmentReflectSig (T : Term) (E : EnvironmentSig T) (TDec : TermDecide T) (EDec : EnvironmentDecide T E).
+  Include EnvironmentReflect T E TDec EDec.
+End EnvironmentReflectSig.

common/theories/Universes.v

@@ -172,6 +172,8 @@ Module LS := LevelSet.
 Ltac lsets := LevelSetDecide.fsetdec.
 Notation "(=_lset)" := LevelSet.Equal (at level 0).
 Infix "=_lset" := LevelSet.Equal (at level 30).
+Notation "(==_lset)" := LevelSet.equal (at level 0).
+Infix "==_lset" := LevelSet.equal (at level 30).
 
 Section LevelSetMoreFacts.
 
@@ -1496,6 +1498,8 @@ Ltac csets := ConstraintSetDecide.fsetdec.
 
 Notation "(=_cset)" := ConstraintSet.Equal (at level 0).
 Infix "=_cset" := ConstraintSet.Equal (at level 30).
+Notation "(==_cset)" := ConstraintSet.equal (at level 0).
+Infix "==_cset" := ConstraintSet.equal (at level 30).
 
 Definition declared_cstr_levels levels (cstr : UnivConstraint.t) :=
   let '(l1,_,l2) := cstr in
@@ -1600,21 +1604,28 @@ Module ContextSet.
   Definition is_empty (uctx : t)
     := LevelSet.is_empty (fst uctx) && ConstraintSet.is_empty (snd uctx).
 
-  Definition equal (x y : t) : Prop :=
+  Definition Equal (x y : t) : Prop :=
     x.1 =_lset y.1 /\ x.2 =_cset y.2.
 
-  Definition subset (x y : t) : Prop :=
+  Definition equal (x y : t) : bool :=
+    x.1 ==_lset y.1 && x.2 ==_cset y.2.
+
+  Definition Subset (x y : t) : Prop :=
     LevelSet.Subset (levels x) (levels y) /\
     ConstraintSet.Subset (constraints x) (constraints y).
 
+  Definition subset (x y : t) : bool :=
+    LevelSet.subset (levels x) (levels y) &&
+    ConstraintSet.subset (constraints x) (constraints y).
+
   Definition inter (x y : t) : t :=
     (LevelSet.inter (levels x) (levels y),
       ConstraintSet.inter (constraints x) (constraints y)).
 
   Definition inter_spec (x y : t) :
-    subset (inter x y) x /\
-      subset (inter x y) y /\
-      forall z, subset z x -> subset z y -> subset z (inter x y).
+    Subset (inter x y) x /\
+      Subset (inter x y) y /\
+      forall z, Subset z x -> Subset z y -> Subset z (inter x y).
   Proof.
     split; last split.
     1,2: split=> ?; [move=> /LevelSet.inter_spec [//]|move=> /ConstraintSet.inter_spec [//]].
@@ -1626,21 +1637,45 @@ Module ContextSet.
     (LevelSet.union (levels x) (levels y), ConstraintSet.union (constraints x) (constraints y)).
 
   Definition union_spec (x y : t) :
-    subset x (union x y) /\
-      subset y (union x y) /\
-      forall z, subset x z -> subset y z -> subset (union x y) z.
+    Subset x (union x y) /\
+      Subset y (union x y) /\
+      forall z, Subset x z -> Subset y z -> Subset (union x y) z.
   Proof.
     split; last split.
     1,2: split=> ??; [apply/LevelSet.union_spec|apply/ConstraintSet.union_spec ]; by constructor.
     move=> ? [??] [??]; split=> ?;
     [move=>/LevelSet.union_spec|move=>/ConstraintSet.union_spec]=>-[]; auto.
   Qed.
+
+  Lemma equal_spec s s' : equal s s' <-> Equal s s'.
+  Proof.
+    rewrite /equal/Equal/is_true Bool.andb_true_iff LevelSet.equal_spec ConstraintSet.equal_spec.
+    reflexivity.
+  Qed.
+
+  Lemma subset_spec s s' : subset s s' <-> Subset s s'.
+  Proof.
+    rewrite /subset/Subset/is_true Bool.andb_true_iff LevelSet.subset_spec ConstraintSet.subset_spec.
+    reflexivity.
+  Qed.
+
+  Lemma subsetP s s' : reflect (Subset s s') (subset s s').
+  Proof.
+    generalize (subset_spec s s').
+    destruct subset; case; constructor; intuition.
+  Qed.
 End ContextSet.
 
-Notation "(=_cs)" := ContextSet.equal (at level 0).
-Notation "(⊂_cs)" := ContextSet.subset (at level 0).
-Infix "=_cs" := ContextSet.equal (at level 30).
-Infix "⊂_cs" := ContextSet.subset (at level 30).
+Export (hints) ContextSet.
+
+Notation "(=_cs)" := ContextSet.Equal (at level 0).
+Notation "(⊂_cs)" := ContextSet.Subset (at level 0).
+Infix "=_cs" := ContextSet.Equal (at level 30).
+Infix "⊂_cs" := ContextSet.Subset (at level 30).
+Notation "(==_cs)" := ContextSet.equal (at level 0).
+Notation "(⊂?_cs)" := ContextSet.subset (at level 0).
+Infix "==_cs" := ContextSet.equal (at level 30).
+Infix "⊂?_cs" := ContextSet.subset (at level 30).
 
 Lemma incl_cs_refl cs : cs ⊂_cs cs.
 Proof.

pcuic/theories/Syntax/PCUICReflect.v

@@ -4,6 +4,7 @@ From Equations Require Import Equations.
 
 From MetaCoq.PCUIC Require Import PCUICAst PCUICInduction.
 From MetaCoq.Utils Require Import utils.
+From MetaCoq.Common Require Import EnvironmentReflect.
 From MetaCoq.Common Require Export Reflect.
 
 Open Scope pcuic.
@@ -375,6 +376,7 @@ Qed.
 
 Module PCUICTermDecide <: TermDecide PCUICTerm.
   #[export] Instance term_eq_dec : EqDec term := _.
+  Include TermDecideReflectInstances PCUICTerm.
 End PCUICTermDecide.
 
 Module PCUICEnvironmentDecide <: EnvironmentDecide PCUICTerm PCUICEnvironment.
@@ -385,4 +387,7 @@ Module PCUICEnvironmentDecide <: EnvironmentDecide PCUICTerm PCUICEnvironment.
   #[export] Instance mutual_inductive_body_eq_dec : EqDec mutual_inductive_body := _.
   #[export] Instance constant_body_eq_dec : EqDec constant_body := _.
   #[export] Instance global_decl_eq_dec : EqDec global_decl := _.
+  Include EnvironmentDecideReflectInstances PCUICTerm PCUICEnvironment.
 End PCUICEnvironmentDecide.
+
+Module PCUICEnvironmentReflect := EnvironmentReflect PCUICTerm PCUICEnvironment PCUICTermDecide PCUICEnvironmentDecide.

quotation/theories/ToPCUIC/Common/Universes.v

@@ -63,8 +63,8 @@ Export (hints) QuoteUniverses1.
   UContext.t
   AUContext.t
   ContextSet.t
-  ContextSet.equal
-  ContextSet.subset
+  ContextSet.Equal
+  ContextSet.Subset
   : quotation.
 
 #[export] Typeclasses Transparent

quotation/theories/ToTemplate/Common/Universes.v

@@ -63,8 +63,8 @@ Export (hints) QuoteUniverses1.
   UContext.t
   AUContext.t
   ContextSet.t
-  ContextSet.equal
-  ContextSet.subset
+  ContextSet.Equal
+  ContextSet.Subset
   : quotation.
 
 #[export] Typeclasses Transparent

template-coq/theories/ReflectAst.v

@@ -2,7 +2,7 @@
 (* For primitive integers and floats  *)
 From Coq Require Numbers.Cyclic.Int63.Uint63 Floats.PrimFloat Floats.FloatAxioms.
 From MetaCoq.Utils Require Import utils.
-From MetaCoq.Common Require Import BasicAst Reflect Environment.
+From MetaCoq.Common Require Import BasicAst Reflect Environment EnvironmentReflect.
 From MetaCoq.Template Require Import AstUtils Ast Induction.
 Require Import ssreflect.
 From Equations Require Import Equations.
@@ -248,6 +248,7 @@ Defined.
 
 Module TemplateTermDecide <: TermDecide TemplateTerm.
   #[export] Instance term_eq_dec : EqDec term := _.
+  Include TermDecideReflectInstances TemplateTerm.
 End TemplateTermDecide.
 
 Module EnvDecide <: EnvironmentDecide TemplateTerm Env.
@@ -258,4 +259,7 @@ Module EnvDecide <: EnvironmentDecide TemplateTerm Env.
   #[export] Instance mutual_inductive_body_eq_dec : EqDec mutual_inductive_body := _.
   #[export] Instance constant_body_eq_dec : EqDec constant_body := _.
   #[export] Instance global_decl_eq_dec : EqDec global_decl := _.
+  Include EnvironmentDecideReflectInstances TemplateTerm Env.
 End EnvDecide.
+
+Module EnvReflect := EnvironmentReflect TemplateTerm Env TemplateTermDecide EnvDecide.