Library MetaCoq.PCUIC.utils.PCUICOnOne
(* Distributed under the terms of the MIT license. *)
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config.
From MetaCoq.PCUIC Require Import PCUICAst.
Require Import ssreflect.
Require Import Equations.Prop.DepElim.
From Equations.Type Require Import Relation Relation_Properties.
From Equations Require Import Equations.
Set Equations Transparent.
Set Default Goal Selector "!".
Notation rtrans_clos := clos_refl_trans_n1.
Lemma All2_many_OnOne2 :
∀ A (R : A → A → Type) l l',
All2 R l l' →
rtrans_clos (OnOne2 R) l l'.
Proof.
intros A R l l' h.
induction h.
- constructor.
- econstructor.
+ constructor. eassumption.
+ clear - IHh. rename IHh into h.
induction h.
× constructor.
× econstructor.
-- econstructor 2. eassumption.
-- assumption.
Qed.
Definition tDummy := tVar String.EmptyString.
Definition dummy_branch : branch term := mk_branch [] tDummy.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config.
From MetaCoq.PCUIC Require Import PCUICAst.
Require Import ssreflect.
Require Import Equations.Prop.DepElim.
From Equations.Type Require Import Relation Relation_Properties.
From Equations Require Import Equations.
Set Equations Transparent.
Set Default Goal Selector "!".
Notation rtrans_clos := clos_refl_trans_n1.
Lemma All2_many_OnOne2 :
∀ A (R : A → A → Type) l l',
All2 R l l' →
rtrans_clos (OnOne2 R) l l'.
Proof.
intros A R l l' h.
induction h.
- constructor.
- econstructor.
+ constructor. eassumption.
+ clear - IHh. rename IHh into h.
induction h.
× constructor.
× econstructor.
-- econstructor 2. eassumption.
-- assumption.
Qed.
Definition tDummy := tVar String.EmptyString.
Definition dummy_branch : branch term := mk_branch [] tDummy.
Reduction
One step strong beta-zeta-iota-fix-delta reduction
Arguments OnOne2 {A} P%type l l'.
Definition set_pcontext (p : predicate term) (pctx' : context) : predicate term :=
{| pparams := p.(pparams);
puinst := p.(puinst);
pcontext := pctx';
preturn := p.(preturn) |}.
Definition set_pcontext_two {p x} x' :
set_pcontext (set_pcontext p x') x = set_pcontext p x :=
eq_refl.
Definition set_preturn (p : predicate term) (pret' : term) : predicate term :=
{| pparams := p.(pparams);
puinst := p.(puinst);
pcontext := p.(pcontext);
preturn := pret' |}.
Definition set_preturn_two {p} pret pret' : set_preturn (set_preturn p pret') pret = set_preturn p pret :=
eq_refl.
Definition set_pparams (p : predicate term) (pars' : list term) : predicate term :=
{| pparams := pars';
puinst := p.(puinst);
pcontext := p.(pcontext);
preturn := p.(preturn) |}.
Definition set_pparams_two {p pars} pars' : set_pparams (set_pparams p pars') pars = set_pparams p pars :=
eq_refl.
Definition map_decl_na (f : aname → aname) (g : term → term) d :=
{| decl_name := f (decl_name d);
decl_body := option_map g (decl_body d);
decl_type := g (decl_type d) |}.
We do not allow alpha-conversion and P applies to only one of the
fields in the context declaration. Used to define one-step context reduction.
Definition on_one_decl (P : context → term → term → Type)
Γ (d : context_decl) (d' : context_decl) : Type :=
match d, d' with
| {| decl_name := na; decl_body := None; decl_type := ty |},
{| decl_name := na'; decl_body := None; decl_type := ty' |} ⇒
na = na' × P Γ ty ty'
| {| decl_name := na; decl_body := Some b; decl_type := ty |},
{| decl_name := na'; decl_body := Some b'; decl_type := ty' |} ⇒
na = na' ×
((P Γ ty ty' × b = b') +
(P Γ b b' × ty = ty'))
| _, _ ⇒ False
end.
Lemma on_one_decl_impl (P Q : context → term → term → Type) :
(∀ Γ, inclusion (P Γ) (Q Γ)) →
∀ Γ, inclusion (on_one_decl P Γ) (on_one_decl Q Γ).
Proof.
intros HP Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl; firstorder auto.
Qed.
Lemma on_one_decl_map_na (P : context → term → term → Type) f g :
∀ Γ,
inclusion (on_one_decl (fun Γ ⇒ on_Trel (P (map (map_decl_na f g) Γ)) g) Γ)
(on_Trel (on_one_decl P (map (map_decl_na f g) Γ)) (map_decl_na f g)).
Proof.
intros Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl in *; firstorder auto; subst; simpl;
auto.
Qed.
Lemma on_one_decl_map (P : context → term → term → Type) f :
∀ Γ,
inclusion (on_one_decl (fun Γ ⇒ on_Trel (P (map (map_decl f) Γ)) f) Γ)
(on_Trel (on_one_decl P (map (map_decl f) Γ)) (map_decl f)).
Proof.
intros Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl in *; firstorder auto; subst; simpl;
auto.
Qed.
Lemma on_one_decl_mapi_context (P : context → term → term → Type) f :
∀ Γ,
inclusion (on_one_decl (fun Γ ⇒ on_Trel (P (mapi_context f Γ)) (f #|Γ|)) Γ)
(on_Trel (on_one_decl P (mapi_context f Γ)) (map_decl (f #|Γ|))).
Proof.
intros Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl in *; firstorder auto; subst; simpl;
auto.
Qed.
Lemma on_one_decl_test_impl (P Q : context → term → term → Type) (p : term → bool) :
∀ Γ d d',
on_one_decl P Γ d d' →
test_decl p d →
(∀ x y, p x → P Γ x y → Q Γ x y) →
on_one_decl Q Γ d d'.
Proof.
intros Γ [na [b|] ty] [na' [b'|] ty'] ond []%andb_and; simpl; firstorder auto.
Qed.
Section OnOne_local_2.
Context (P : ∀ (Γ : context), context_decl → context_decl → Type).
Inductive OnOne2_local_env : context → context → Type :=
| onone2_localenv_cons_abs Γ na na' t t' :
P Γ (vass na t) (vass na' t') →
OnOne2_local_env (Γ ,, vass na t) (Γ ,, vass na' t')
| onone2_localenv_def Γ na na' b b' t t' :
P Γ (vdef na b t) (vdef na' b' t') →
OnOne2_local_env (Γ ,, vdef na b t) (Γ ,, vdef na' b' t')
| onone2_localenv_cons_tl Γ Γ' d :
OnOne2_local_env Γ Γ' →
OnOne2_local_env (Γ ,, d) (Γ' ,, d).
End OnOne_local_2.
#[global]
Instance OnOne2_local_env_length {P ctx ctx'} :
HasLen (OnOne2_local_env P ctx ctx') #|ctx| #|ctx'|.
Proof.
induction 1; simpl; lia.
Qed.
Lemma OnOne2_local_env_impl R S :
(∀ Δ, inclusion (R Δ) (S Δ)) →
inclusion (OnOne2_local_env R)
(OnOne2_local_env S).
Proof.
intros H x y H'.
induction H'; try solve [econstructor; firstorder].
Qed.
Lemma OnOne2_local_env_ondecl_impl P Q :
(∀ Γ, inclusion (P Γ) (Q Γ)) →
inclusion (OnOne2_local_env (on_one_decl P)) (OnOne2_local_env (on_one_decl P)).
Proof.
intros HP. now apply OnOne2_local_env_impl, on_one_decl_impl.
Qed.
Lemma OnOne2_local_env_map R Γ Δ (f : aname → aname) (g : term → term) :
OnOne2_local_env (fun Γ ⇒ on_Trel (R (map (map_decl_na f g) Γ)) (map_decl_na f g)) Γ Δ →
OnOne2_local_env R (map (map_decl_na f g) Γ) (map (map_decl_na f g) Δ).
Proof.
unfold on_Trel in *; induction 1; simpl; try solve [econstructor; intuition auto].
Qed.
Lemma OnOne2_local_env_map_context R Γ Δ (f : term → term) :
OnOne2_local_env (fun Γ ⇒ on_Trel (R (map (map_decl f) Γ)) (map_decl f)) Γ Δ →
OnOne2_local_env R (map_context f Γ) (map_context f Δ).
Proof.
unfold on_Trel in *; induction 1; simpl; try solve [econstructor; intuition auto].
Qed.
Lemma OnOne2_local_env_mapi_context R Γ Δ (f : nat → term → term) :
OnOne2_local_env (fun Γ ⇒ on_Trel (R (mapi_context f Γ)) (map_decl (f #|Γ|))) Γ Δ →
OnOne2_local_env R (mapi_context f Γ) (mapi_context f Δ).
Proof.
unfold on_Trel in *; induction 1; simpl; try solve [econstructor; intuition auto].
rewrite -(length_of X). now constructor.
Qed.
Lemma test_context_k_impl {p q : nat → term → bool} {k k'} {ctx} :
(∀ n t, p n t → q n t) →
k = k' →
test_context_k p k ctx → test_context_k q k' ctx.
Proof.
intros Hfg <-.
induction ctx as [|[na [b|] ty] ctx]; simpl; auto;
move/andb_and⇒ [testp testd]; rewrite (IHctx testp);
eapply test_decl_impl; tea; eauto.
Qed.
Lemma OnOne2_local_env_test_context_k {P ctx ctx'} {k} {p q : nat → term → bool} :
(∀ n t, q n t → p n t) →
OnOne2_local_env P ctx ctx' →
(∀ Γ d d',
P Γ d d' →
test_context_k q k Γ →
test_decl (q (#|Γ| + k)) d →
test_decl (p (#|Γ| + k)) d') →
test_context_k q k ctx →
test_context_k p k ctx'.
Proof.
intros hq onenv HPq.
induction onenv.
× move⇒ /= /andb_and [testq testd].
rewrite (test_context_k_impl _ _ testq) //.
simpl; eauto.
× move⇒ /= /andb_and [testq testd].
rewrite (test_context_k_impl _ _ testq) //.
simpl; eauto.
× move⇒ /= /andb_and [testq testd].
rewrite (IHonenv testq).
eapply test_decl_impl; tea.
intros x Hx. eapply hq.
now rewrite -(length_of onenv).
Qed.
Lemma on_one_decl_test_decl (P : context → term → term → Type) Γ
(p q : term → bool) d d' :
(∀ t, p t → q t) →
(∀ t t', P Γ t t' → p t → q t') →
on_one_decl P Γ d d' →
test_decl p d →
test_decl q d'.
Proof.
intros Hp.
unfold test_decl.
destruct d as [na [b|] ty], d' as [na' [b'|] ty']; simpl in × ⇒ //;
intuition auto; rtoProp;
subst; simpl; intuition eauto.
Qed.
Lemma OnOne2_local_env_impl_test {P Q ctx ctx'} {k} {p : nat → term → bool} :
OnOne2_local_env P ctx ctx' →
(∀ Γ d d',
P Γ d d' →
test_context_k p k Γ →
test_decl (p (#|Γ| + k)) d →
Q Γ d d') →
test_context_k p k ctx →
OnOne2_local_env Q ctx ctx'.
Proof.
intros onenv HPq.
induction onenv.
× move⇒ /= /andb_and [testq testd].
constructor; auto.
× move⇒ /= /andb_and [testq testd].
constructor; auto.
× move⇒ /= /andb_and [testq testd].
constructor; auto.
Qed.
Γ (d : context_decl) (d' : context_decl) : Type :=
match d, d' with
| {| decl_name := na; decl_body := None; decl_type := ty |},
{| decl_name := na'; decl_body := None; decl_type := ty' |} ⇒
na = na' × P Γ ty ty'
| {| decl_name := na; decl_body := Some b; decl_type := ty |},
{| decl_name := na'; decl_body := Some b'; decl_type := ty' |} ⇒
na = na' ×
((P Γ ty ty' × b = b') +
(P Γ b b' × ty = ty'))
| _, _ ⇒ False
end.
Lemma on_one_decl_impl (P Q : context → term → term → Type) :
(∀ Γ, inclusion (P Γ) (Q Γ)) →
∀ Γ, inclusion (on_one_decl P Γ) (on_one_decl Q Γ).
Proof.
intros HP Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl; firstorder auto.
Qed.
Lemma on_one_decl_map_na (P : context → term → term → Type) f g :
∀ Γ,
inclusion (on_one_decl (fun Γ ⇒ on_Trel (P (map (map_decl_na f g) Γ)) g) Γ)
(on_Trel (on_one_decl P (map (map_decl_na f g) Γ)) (map_decl_na f g)).
Proof.
intros Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl in *; firstorder auto; subst; simpl;
auto.
Qed.
Lemma on_one_decl_map (P : context → term → term → Type) f :
∀ Γ,
inclusion (on_one_decl (fun Γ ⇒ on_Trel (P (map (map_decl f) Γ)) f) Γ)
(on_Trel (on_one_decl P (map (map_decl f) Γ)) (map_decl f)).
Proof.
intros Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl in *; firstorder auto; subst; simpl;
auto.
Qed.
Lemma on_one_decl_mapi_context (P : context → term → term → Type) f :
∀ Γ,
inclusion (on_one_decl (fun Γ ⇒ on_Trel (P (mapi_context f Γ)) (f #|Γ|)) Γ)
(on_Trel (on_one_decl P (mapi_context f Γ)) (map_decl (f #|Γ|))).
Proof.
intros Γ x y.
destruct x as [na [b|] ty], y as [na' [b'|] ty']; simpl in *; firstorder auto; subst; simpl;
auto.
Qed.
Lemma on_one_decl_test_impl (P Q : context → term → term → Type) (p : term → bool) :
∀ Γ d d',
on_one_decl P Γ d d' →
test_decl p d →
(∀ x y, p x → P Γ x y → Q Γ x y) →
on_one_decl Q Γ d d'.
Proof.
intros Γ [na [b|] ty] [na' [b'|] ty'] ond []%andb_and; simpl; firstorder auto.
Qed.
Section OnOne_local_2.
Context (P : ∀ (Γ : context), context_decl → context_decl → Type).
Inductive OnOne2_local_env : context → context → Type :=
| onone2_localenv_cons_abs Γ na na' t t' :
P Γ (vass na t) (vass na' t') →
OnOne2_local_env (Γ ,, vass na t) (Γ ,, vass na' t')
| onone2_localenv_def Γ na na' b b' t t' :
P Γ (vdef na b t) (vdef na' b' t') →
OnOne2_local_env (Γ ,, vdef na b t) (Γ ,, vdef na' b' t')
| onone2_localenv_cons_tl Γ Γ' d :
OnOne2_local_env Γ Γ' →
OnOne2_local_env (Γ ,, d) (Γ' ,, d).
End OnOne_local_2.
#[global]
Instance OnOne2_local_env_length {P ctx ctx'} :
HasLen (OnOne2_local_env P ctx ctx') #|ctx| #|ctx'|.
Proof.
induction 1; simpl; lia.
Qed.
Lemma OnOne2_local_env_impl R S :
(∀ Δ, inclusion (R Δ) (S Δ)) →
inclusion (OnOne2_local_env R)
(OnOne2_local_env S).
Proof.
intros H x y H'.
induction H'; try solve [econstructor; firstorder].
Qed.
Lemma OnOne2_local_env_ondecl_impl P Q :
(∀ Γ, inclusion (P Γ) (Q Γ)) →
inclusion (OnOne2_local_env (on_one_decl P)) (OnOne2_local_env (on_one_decl P)).
Proof.
intros HP. now apply OnOne2_local_env_impl, on_one_decl_impl.
Qed.
Lemma OnOne2_local_env_map R Γ Δ (f : aname → aname) (g : term → term) :
OnOne2_local_env (fun Γ ⇒ on_Trel (R (map (map_decl_na f g) Γ)) (map_decl_na f g)) Γ Δ →
OnOne2_local_env R (map (map_decl_na f g) Γ) (map (map_decl_na f g) Δ).
Proof.
unfold on_Trel in *; induction 1; simpl; try solve [econstructor; intuition auto].
Qed.
Lemma OnOne2_local_env_map_context R Γ Δ (f : term → term) :
OnOne2_local_env (fun Γ ⇒ on_Trel (R (map (map_decl f) Γ)) (map_decl f)) Γ Δ →
OnOne2_local_env R (map_context f Γ) (map_context f Δ).
Proof.
unfold on_Trel in *; induction 1; simpl; try solve [econstructor; intuition auto].
Qed.
Lemma OnOne2_local_env_mapi_context R Γ Δ (f : nat → term → term) :
OnOne2_local_env (fun Γ ⇒ on_Trel (R (mapi_context f Γ)) (map_decl (f #|Γ|))) Γ Δ →
OnOne2_local_env R (mapi_context f Γ) (mapi_context f Δ).
Proof.
unfold on_Trel in *; induction 1; simpl; try solve [econstructor; intuition auto].
rewrite -(length_of X). now constructor.
Qed.
Lemma test_context_k_impl {p q : nat → term → bool} {k k'} {ctx} :
(∀ n t, p n t → q n t) →
k = k' →
test_context_k p k ctx → test_context_k q k' ctx.
Proof.
intros Hfg <-.
induction ctx as [|[na [b|] ty] ctx]; simpl; auto;
move/andb_and⇒ [testp testd]; rewrite (IHctx testp);
eapply test_decl_impl; tea; eauto.
Qed.
Lemma OnOne2_local_env_test_context_k {P ctx ctx'} {k} {p q : nat → term → bool} :
(∀ n t, q n t → p n t) →
OnOne2_local_env P ctx ctx' →
(∀ Γ d d',
P Γ d d' →
test_context_k q k Γ →
test_decl (q (#|Γ| + k)) d →
test_decl (p (#|Γ| + k)) d') →
test_context_k q k ctx →
test_context_k p k ctx'.
Proof.
intros hq onenv HPq.
induction onenv.
× move⇒ /= /andb_and [testq testd].
rewrite (test_context_k_impl _ _ testq) //.
simpl; eauto.
× move⇒ /= /andb_and [testq testd].
rewrite (test_context_k_impl _ _ testq) //.
simpl; eauto.
× move⇒ /= /andb_and [testq testd].
rewrite (IHonenv testq).
eapply test_decl_impl; tea.
intros x Hx. eapply hq.
now rewrite -(length_of onenv).
Qed.
Lemma on_one_decl_test_decl (P : context → term → term → Type) Γ
(p q : term → bool) d d' :
(∀ t, p t → q t) →
(∀ t t', P Γ t t' → p t → q t') →
on_one_decl P Γ d d' →
test_decl p d →
test_decl q d'.
Proof.
intros Hp.
unfold test_decl.
destruct d as [na [b|] ty], d' as [na' [b'|] ty']; simpl in × ⇒ //;
intuition auto; rtoProp;
subst; simpl; intuition eauto.
Qed.
Lemma OnOne2_local_env_impl_test {P Q ctx ctx'} {k} {p : nat → term → bool} :
OnOne2_local_env P ctx ctx' →
(∀ Γ d d',
P Γ d d' →
test_context_k p k Γ →
test_decl (p (#|Γ| + k)) d →
Q Γ d d') →
test_context_k p k ctx →
OnOne2_local_env Q ctx ctx'.
Proof.
intros onenv HPq.
induction onenv.
× move⇒ /= /andb_and [testq testd].
constructor; auto.
× move⇒ /= /andb_and [testq testd].
constructor; auto.
× move⇒ /= /andb_and [testq testd].
constructor; auto.
Qed.