Shared app_context, integrated Σ in ctx_inst

Author: yannl35133

common/theories/BasicAst.v

@@ -217,18 +217,13 @@ Record judgment_ {universe Term} := Judge {
   j_term : option Term;
   j_typ : Term;
   j_univ : option universe;
-  (* rel : option relevance; *)
+  (* j_rel : option relevance; *)
 }.
 Arguments judgment_ : clear implicits.
 Arguments Judge {universe Term} _ _ _.
-Notation Typ typ := (Judge None typ None).
-Notation TermTyp tm ty := (Judge (Some tm) ty None).
-Notation TermoptTyp tm typ := (Judge tm typ None).
-Notation TypUniv ty u := (Judge None ty (Some u)).
-Notation TermTypUniv tm ty u := (Judge (Some tm) ty (Some u)).
 
 Definition judgment_map {univ T A} (f: T -> A) (j : judgment_ univ T) :=
-  Judge (option_map f (j_term j)) (f (j_typ j)) (j_univ j) (* rel *).
+  Judge (option_map f (j_term j)) (f (j_typ j)) (j_univ j) (* (j_rel j) *).
 
 Section Contexts.
   Context {term : Type}.
@@ -244,8 +239,15 @@ End Contexts.
 
 Arguments context_decl : clear implicits.
 
-Definition judgment_of_decl {term universe} d : judgment_ term universe :=
-  TermoptTyp (decl_body d) (decl_type d).
+Notation Typ typ := (Judge None typ None).
+Notation TermTyp tm ty := (Judge (Some tm) ty None).
+Notation TermoptTyp tm typ := (Judge tm typ None).
+Notation TypUniv ty u := (Judge None ty (Some u)).
+Notation TermTypUniv tm ty u := (Judge (Some tm) ty (Some u)).
+
+Notation j_vass na ty := (Typ ty (* na.(binder_relevance) *)).
+Notation j_vdef na b ty := (TermTyp b ty (* na.(binder_relevance) *)).
+Notation j_decl d := (TermoptTyp (decl_body d) (decl_type d) (* (decl_name d).(binder_relevance) *)).
 
 
 Definition map_decl {term term'} (f : term -> term') (d : context_decl term) : context_decl term' :=
@@ -314,8 +316,46 @@ Definition snoc {A} (Γ : list A) (d : A) := d :: Γ.
 
 Notation " Γ ,, d " := (snoc Γ d) (at level 20, d at next level).
 
+Definition app_context {A} (Γ Γ': list A) := Γ' ++ Γ.
+
+Notation "Γ ,,, Γ'" := (app_context Γ Γ') (at level 25, Γ' at next level, left associativity).
+
+Lemma app_context_nil_l {T} Γ : [] ,,, Γ = Γ :> list T.
+Proof.
+  unfold app_context. rewrite app_nil_r. reflexivity.
+Qed.
+
+Lemma app_context_assoc {T} Γ Γ' Γ'' : Γ ,,, (Γ' ,,, Γ'') = Γ ,,, Γ' ,,, Γ'' :> list T.
+Proof. unfold app_context; now rewrite app_assoc. Qed.
+
+Lemma app_context_cons {T} Γ Γ' A : Γ ,,, (Γ' ,, A) = (Γ ,,, Γ') ,, A :> list T.
+Proof. exact (app_context_assoc _ _ [A]). Qed.
+
+Lemma app_context_push {T} Γ Δ Δ' d : (Γ ,,, Δ ,,, Δ') ,, d = (Γ ,,, Δ ,,, (Δ' ,, d)) :> list T.
+Proof using Type.
+  reflexivity.
+Qed.
+
+Lemma snoc_app_context {T Γ Δ d} : (Γ ,,, (d :: Δ)) =  (Γ ,,, Δ) ,,, [d] :> list T.
+Proof using Type.
+  reflexivity.
+Qed.
+
+Lemma app_context_length {T} (Γ Γ' : list T) : #|Γ ,,, Γ'| = #|Γ'| + #|Γ|.
+Proof. unfold app_context. now rewrite app_length. Qed.
+#[global] Hint Rewrite @app_context_length : len.
+
+Lemma nth_error_app_context_ge {T} v Γ Γ' :
+  #|Γ'| <= v -> nth_error (Γ ,,, Γ') v = nth_error Γ (v - #|Γ'|) :> option T.
+Proof. apply nth_error_app_ge. Qed.
+
+Lemma nth_error_app_context_lt {T} v Γ Γ' :
+  v < #|Γ'| -> nth_error (Γ ,,, Γ') v = nth_error Γ' v :> option T.
+Proof. apply nth_error_app_lt. Qed.
+
+
 Definition ondecl {A} (P : A -> Type) (d : context_decl A) :=
-  P d.(decl_type) × option_default P d.(decl_body) unit.
+  option_default P d.(decl_body) unit × P d.(decl_type).
 
 Notation onctx P := (All (ondecl P)).
 

common/theories/Environment.v

@@ -861,12 +861,6 @@ Module Environment (T : Term).
 
   Definition program : Type := global_env * term.
 
-  (* TODO MOVE AstUtils factorisation *)
-
-  Definition app_context (Γ Γ' : context) : context := Γ' ++ Γ.
-  Notation "Γ ,,, Γ'" :=
-    (app_context Γ Γ') (at level 25, Γ' at next level, left associativity).
-
   (** Make a lambda/let-in string of abstractions from a context [Γ], ending with term [t]. *)
 
   Definition mkLambda_or_LetIn d t :=
@@ -987,30 +981,6 @@ Module Environment (T : Term).
   Proof. unfold arities_context. now rewrite rev_map_length. Qed.
   #[global] Hint Rewrite arities_context_length : len.
 
-  Lemma app_context_nil_l Γ : [] ,,, Γ = Γ.
-  Proof.
-    unfold app_context. rewrite app_nil_r. reflexivity.
-  Qed.
-
-  Lemma app_context_assoc Γ Γ' Γ'' : Γ ,,, (Γ' ,,, Γ'') = Γ ,,, Γ' ,,, Γ''.
-  Proof. unfold app_context; now rewrite app_assoc. Qed.
-
-  Lemma app_context_cons Γ Γ' A : Γ ,,, (Γ' ,, A) = (Γ ,,, Γ') ,, A.
-  Proof. exact (app_context_assoc _ _ [A]). Qed.
-
-  Lemma app_context_length Γ Γ' : #|Γ ,,, Γ'| = #|Γ'| + #|Γ|.
-  Proof. unfold app_context. now rewrite app_length. Qed.
-  #[global] Hint Rewrite app_context_length : len.
-
-  Lemma nth_error_app_context_ge v Γ Γ' :
-    #|Γ'| <= v -> nth_error (Γ ,,, Γ') v = nth_error Γ (v - #|Γ'|).
-  Proof. apply nth_error_app_ge. Qed.
-
-  Lemma nth_error_app_context_lt v Γ Γ' :
-    v < #|Γ'| -> nth_error (Γ ,,, Γ') v = nth_error Γ' v.
-  Proof. apply nth_error_app_lt. Qed.
-
-
   Definition map_mutual_inductive_body f m :=
     match m with
     | Build_mutual_inductive_body finite ind_npars ind_pars ind_bodies ind_universes ind_variance =>

common/theories/EnvironmentTyping.v

@@ -319,7 +319,7 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E).
   (** Well-formedness of local environments embeds a sorting for each variable *)
 
   Definition on_local_decl (P : context -> judgment -> Type) Γ d :=
-    P Γ (TermoptTyp d.(decl_body) d.(decl_type)).
+    P Γ (j_decl d).
 
   Definition on_def_type (P : context -> judgment -> Type) Γ d :=
     P Γ (Typ d.(dtype)).
@@ -330,7 +330,10 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E).
   (* Various kinds of lifts *)
 
   Definition lift_wf_term wf_term (j : judgment) := option_default wf_term (j_term j) (unit : Type) × wf_term (j_typ j).
-  Notation lift_on_term on_term := (fun (Γ : context) => lift_wf_term (on_term Γ)).
+  Notation lift_wf_term1 wf_term := (fun (Γ : context) => lift_wf_term (wf_term Γ)).
+
+  Definition lift_wfb_term wfb_term (j : judgment) := option_default wfb_term (j_term j) true && wfb_term (j_typ j).
+  Notation lift_wfb_term1 wfb_term := (fun (Γ : context) => lift_wfb_term (wfb_term Γ)).
 
   Definition lift_sorting checking sorting : judgment -> Type :=
     fun j => option_default (fun tm => checking tm (j_typ j)) (j_term j) (unit : Type) ×
@@ -872,28 +875,28 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E).
   Defined.
 
   Section TypeCtxInst.
-    Context (typing : forall (Σ : global_env_ext) (Γ : context), term -> term -> Type).
+    Context (typing : forall (Γ : context), term -> term -> Type).
 
     (* Γ |- s : Δ, where Δ is a telescope (reverse context) *)
-    Inductive ctx_inst Σ (Γ : context) : list term -> context -> Type :=
-    | ctx_inst_nil : ctx_inst Σ Γ [] []
+    Inductive ctx_inst (Γ : context) : list term -> context -> Type :=
+    | ctx_inst_nil : ctx_inst Γ [] []
     | ctx_inst_ass na t i inst Δ :
-        typing Σ Γ i t ->
-        ctx_inst Σ Γ inst (subst_telescope [i] 0 Δ) ->
-        ctx_inst Σ Γ (i :: inst) (vass na t :: Δ)
+        typing Γ i t ->
+        ctx_inst Γ inst (subst_telescope [i] 0 Δ) ->
+        ctx_inst Γ (i :: inst) (vass na t :: Δ)
     | ctx_inst_def na b t inst Δ :
-        ctx_inst Σ Γ inst (subst_telescope [b] 0 Δ) ->
-        ctx_inst Σ Γ inst (vdef na b t :: Δ).
+        ctx_inst Γ inst (subst_telescope [b] 0 Δ) ->
+        ctx_inst Γ inst (vdef na b t :: Δ).
     Derive Signature NoConfusion for ctx_inst.
   End TypeCtxInst.
 
-  Lemma ctx_inst_impl_gen Σ Γ inst Δ args P :
-    { P' & ctx_inst P' Σ Γ inst Δ } ->
+  Lemma ctx_inst_impl_gen Γ inst Δ args P :
+    { P' & ctx_inst P' Γ inst Δ } ->
     (forall t T,
-        All (fun P' => P' Σ Γ t T) args ->
-        P Σ Γ t T) ->
-    All (fun P' => ctx_inst P' Σ Γ inst Δ) args ->
-    ctx_inst P Σ Γ inst Δ.
+        All (fun P' => P' Γ t T) args ->
+        P Γ t T) ->
+    All (fun P' => ctx_inst P' Γ inst Δ) args ->
+    ctx_inst P Γ inst Δ.
   Proof.
     intros [? Hexists] HPQ H.
     induction Hexists; constructor; tea.
@@ -902,10 +905,10 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E).
     all: eapply All_impl; tea; cbn; intros *; inversion 1; subst; eauto.
   Qed.
 
-  Lemma ctx_inst_impl P Q Σ Σ' Γ inst Δ :
-    ctx_inst P Σ Γ inst Δ ->
-    (forall t T, P Σ Γ t T -> Q Σ' Γ t T) ->
-    ctx_inst Q Σ' Γ inst Δ.
+  Lemma ctx_inst_impl P Q Γ inst Δ :
+    ctx_inst P Γ inst Δ ->
+    (forall t T, P Γ t T -> Q Γ t T) ->
+    ctx_inst Q Γ inst Δ.
   Proof.
     intros H HPQ. induction H; econstructor; auto.
   Qed.
@@ -1369,7 +1372,7 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT
         sorts_local_ctx Σ (arities_context mdecl.(ind_bodies) ,,, mdecl.(ind_params))
                       cdecl.(cstr_args) cunivs;
       on_cindices :
-        ctx_inst (fun Σ Γ t T => P Σ Γ (TermTyp t T)) Σ (arities_context mdecl.(ind_bodies) ,,, mdecl.(ind_params) ,,, cdecl.(cstr_args))
+        ctx_inst (fun Γ t T => P Σ Γ (TermTyp t T)) (arities_context mdecl.(ind_bodies) ,,, mdecl.(ind_params) ,,, cdecl.(cstr_args))
                       cdecl.(cstr_indices)
                       (List.rev (lift_context #|cdecl.(cstr_args)| 0 ind_indices));
 
@@ -1806,7 +1809,7 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT
       { eapply All_map, All_impl; tea; intros *; destr_prod; destruct 1; cbn; tea. } }
     { eapply ctx_inst_impl_gen; tea.
       { eexists; tea. }
-      { intros; eapply H1, All_eta3; cbn. apply All_map_inv with (P:=fun P => P _ _ t T1) (f:=fun P Σ Γ t T => snd P Σ Γ (TermTyp t T)); tea. }
+      { intros; eapply H1, All_eta3; cbn. apply All_map_inv with (P:=fun P => P _ t T1) (f:=fun P Γ t T => snd P Σ Γ (TermTyp t T)); tea. }
       { eapply All_map, All_impl; tea; intros *; destr_prod; destruct 1; cbn; tea. } }
     { move => ? H'.
       match goal with H : _ |- _ => specialize (H _ H'); revert H end => H''.

erasure/theories/ESubstitution.v

@@ -180,7 +180,7 @@ Lemma erases_weakening' (Σ : global_env_ext) (Γ Γ' Γ'' : context) (t T : ter
     Σ ;;; Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ' |- (lift #|Γ''| #|Γ'| t) ⇝ℇ (ELiftSubst.lift #|Γ''| #|Γ'| t').
 Proof.
   intros HΣ HΓ'' * H He.
-  generalize_eqs H. intros eqw. rewrite <- eqw in *.
+  remember (Γ ,,, Γ') as Γ0 eqn:eqw.
   revert Γ Γ' Γ'' HΓ'' eqw t' He.
   revert Σ HΣ Γ0 t T H .
   apply (typing_ind_env (fun Σ Γ0 t T =>  forall Γ Γ' Γ'',
@@ -393,7 +393,7 @@ Lemma erases_subst (Σ : global_env_ext) Γ Γ' Δ t s t' s' T :
   Σ ;;; (Γ ,,, subst_context s 0 Δ) |- (subst s #|Δ| t) ⇝ℇ ELiftSubst.subst s' #|Δ| t'.
 Proof.
   intros HΣ HΔ Hs Ht He.
-  generalize_eqs Ht. intros eqw.
+  remember (Γ ,,, Γ' ,,, Δ) as Γ0 eqn:eqw in Ht.
   revert Γ Γ' Δ t' s Hs HΔ He eqw.
   revert Σ HΣ Γ0 t T Ht.
   eapply (typing_ind_env (fun Σ Γ0 t T =>

pcuic/theories/Bidirectional/BDFromPCUIC.v

@@ -24,20 +24,20 @@ Proof.
   lia.
 Qed.
 
-Lemma ctx_inst_length {ty Σ Γ args Δ} :
-PCUICTyping.ctx_inst ty Σ Γ args Δ ->
-#|args| = context_assumptions Δ.
+Lemma ctx_inst_length {ty Γ args Δ} :
+  PCUICTyping.ctx_inst ty Γ args Δ ->
+  #|args| = context_assumptions Δ.
 Proof.
-induction 1; simpl; auto.
-rewrite /subst_telescope in IHX.
-rewrite context_assumptions_mapi in IHX. congruence.
-rewrite context_assumptions_mapi in IHX. congruence.
+  induction 1; simpl; auto.
+  rewrite /subst_telescope in IHX.
+  rewrite context_assumptions_mapi in IHX. congruence.
+  rewrite context_assumptions_mapi in IHX. congruence.
 Qed.
 
 
-Lemma ctx_inst_app_impl {P Q Σ Γ} {Δ : context} {Δ' args} (c : PCUICTyping.ctx_inst P Σ Γ args (Δ ++ Δ')) :
-  (forall Γ' t T, P Σ Γ' t T -> Q Σ Γ' t T) ->
-  PCUICTyping.ctx_inst Q Σ Γ (firstn (context_assumptions Δ) args) Δ.
+Lemma ctx_inst_app_impl {P Q Γ} {Δ : context} {Δ' args} (c : PCUICTyping.ctx_inst P Γ args (Δ ++ Δ')) :
+  (forall t T, P Γ t T -> Q Γ t T) ->
+  PCUICTyping.ctx_inst Q Γ (firstn (context_assumptions Δ) args) Δ.
 Proof.
   revert args Δ' c.
   induction Δ using ctx_length_ind; intros.
@@ -238,7 +238,7 @@ Proof.
       * rewrite subst_instance_app_ctx rev_app_distr in Hinst.
         replace (pparams p) with (firstn (context_assumptions (List.rev (subst_instance (puinst p)(ind_params mdecl)))) (pparams p ++ indices)).
         eapply ctx_inst_app_impl ; tea.
-        1: intros ??? [] ; by apply conv_check.
+        1: intros ?? [] ; by apply conv_check.
         rewrite context_assumptions_rev context_assumptions_subst_instance.
         erewrite PCUICGlobalMaps.onNpars.
         2: eapply on_declared_minductive ; eauto.
@@ -472,8 +472,8 @@ Proof.
 Qed.
 
 Theorem ctx_inst_typing_bd `{checker_flags} (Σ : global_env_ext) Γ l Δ (wfΣ : wf Σ) :
-  PCUICTyping.ctx_inst typing Σ Γ l Δ ->
-  PCUICTyping.ctx_inst checking Σ Γ l Δ.
+  PCUICTyping.ctx_inst (typing Σ) Γ l Δ ->
+  PCUICTyping.ctx_inst (checking Σ) Γ l Δ.
 Proof.
   intros inl.
   induction inl.

pcuic/theories/Bidirectional/BDStrengthening.v

@@ -591,8 +591,8 @@ Lemma rename_telescope P f Γ Δ tel tys:
   on_ctx_free_vars P Γ ->
   forallb (on_free_vars P) tys ->
   on_free_vars_ctx P (List.rev tel) ->
-  PCUICTyping.ctx_inst (fun _ => Pcheck) Σ Γ tys tel ->
-  PCUICTyping.ctx_inst checking Σ Δ (map (rename f) tys) (rename_telescope f tel).
+  PCUICTyping.ctx_inst Pcheck Γ tys tel ->
+  PCUICTyping.ctx_inst (checking Σ) Δ (map (rename f) tys) (rename_telescope f tel).
 Proof using Type.
   intros ur hΓ htys htel ins.
   induction ins in Δ, ur, hΓ, htys, htel |- *.

pcuic/theories/Bidirectional/BDToPCUIC.v

@@ -153,7 +153,7 @@ Section BDToPCUICTyping.
   Qed.
 
   Lemma ctx_inst_impl Γ (wfΓ : wf_local Σ Γ) (Δ : context) (wfΔ : wf_local_rel Σ Γ (List.rev Δ)) :
-    forall args, PCUICTyping.ctx_inst (fun _ => Pcheck) Σ Γ args Δ -> ctx_inst Σ Γ args Δ.
+    forall args, PCUICTyping.ctx_inst Pcheck Γ args Δ -> ctx_inst Σ Γ args Δ.
   Proof using wfΣ.
     revert wfΔ.
     induction Δ using ctx_length_ind.
@@ -479,8 +479,8 @@ Qed.
 
 Theorem ctx_inst_bd_typing `{checker_flags} (Σ : global_env_ext) Γ l Δ (wfΣ : wf Σ) :
   wf_local Σ (Γ,,,Δ) ->
-  PCUICTyping.ctx_inst checking Σ Γ l (List.rev Δ) ->
-  PCUICTyping.ctx_inst typing Σ Γ l (List.rev Δ).
+  PCUICTyping.ctx_inst (checking Σ) Γ l (List.rev Δ) ->
+  PCUICTyping.ctx_inst (typing Σ) Γ l (List.rev Δ).
 Proof.
   intros wfΓ inl.
   rewrite -(List.rev_involutive Δ) in wfΓ.

pcuic/theories/Bidirectional/BDTyping.v

@@ -83,7 +83,7 @@ Inductive infering `{checker_flags} (Σ : global_env_ext) (Γ : context) : term
   consistent_instance_ext Σ (ind_universes mdecl) (puinst p) ->
   wf_local_bd_rel Σ Γ predctx ->
   is_allowed_elimination Σ (ind_kelim idecl) ps ->
-  ctx_inst checking Σ Γ (pparams p)
+  ctx_inst (checking Σ) Γ (pparams p)
       (List.rev mdecl.(ind_params)@[p.(puinst)]) ->
   isCoFinite mdecl.(ind_finite) = false ->
   R_global_instance Σ (eq_universe Σ) (leq_universe Σ)
@@ -401,9 +401,9 @@ Section BidirectionalInduction.
       wf_local_bd_rel Σ Γ predctx ->
       PΓ_rel Γ predctx ->
       is_allowed_elimination Σ (ind_kelim idecl) ps ->
-      ctx_inst checking Σ Γ (pparams p)
+      ctx_inst (checking Σ) Γ (pparams p)
           (List.rev mdecl.(ind_params)@[p.(puinst)]) ->
-      ctx_inst (fun _ => Pcheck) Σ Γ p.(pparams)
+      ctx_inst Pcheck Γ p.(pparams)
           (List.rev (subst_instance p.(puinst) mdecl.(ind_params))) ->
       isCoFinite mdecl.(ind_finite) = false ->
       R_global_instance Σ (eq_universe Σ) (leq_universe Σ)