Library MetaCoq.PCUIC.Syntax.PCUICRenameDef
(* Distributed under the terms of the MIT license. *)
From Coq Require Import Morphisms.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICInduction
PCUICLiftSubst PCUICUnivSubst PCUICOnFreeVars
PCUICSigmaCalculus PCUICTyping.
Require Import ssreflect ssrbool.
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.
Set Equations With UIP.
From Coq Require Import Morphisms.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICInduction
PCUICLiftSubst PCUICUnivSubst PCUICOnFreeVars
PCUICSigmaCalculus PCUICTyping.
Require Import ssreflect ssrbool.
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.
Set Equations With UIP.
Open Scope sigma_scope.
Set Keyed Unification.
Set Default Goal Selector "!".
Section Renaming.
Context `{cf : checker_flags}.
(* Notion of valid renaming without typing information. *)
We might want to relax this to allow "renamings" that change e.g.
the universes or names, but should generalize the renaming operation at
the same time Remark: renaming allows instantiating an assumption with a well-typed body
Definition urenaming (P : nat → bool) Γ Δ f :=
∀ i decl, P i →
nth_error Γ i = Some decl →
∑ decl', (nth_error Δ (f i) = Some decl') ×
(eq_binder_annot decl.(decl_name) decl'.(decl_name) ×
((rename (f ∘ rshiftk (S i)) decl.(decl_type) =
rename (rshiftk (S (f i))) decl'.(decl_type)) ×
on_Some_or_None (fun body ⇒ Some (rename (f ∘ rshiftk (S i)) body) =
option_map (rename (rshiftk (S (f i)))) decl'.(decl_body)) decl.(decl_body))).
(* Definition of a good renaming with respect to typing *)
Definition renaming P Σ Γ Δ f :=
wf_local Σ Δ × urenaming P Γ Δ f.
Definition renaming_closed Γ Δ f := urenaming (closedP #|Γ| xpredT) Γ Δ f.
End Renaming.