DCOIOmega.normalform
Require Import syntax par imports.
Module Type normalform_sig
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax).
(* Identifying neutral (ne) and normal (nf) terms *)
Fixpoint ne (a : tm) : bool :=
match a with
| var_tm _ => true
| tApp a ℓ0 b => ne a && nf b
| tAbs _ _ => false
| tPi _ A B => false
| tJ _ t p => nf t && ne p
| tUniv _ => false
(* | tZero => false *)
(* | tSuc _ => false *)
(* | tInd a b c => nf a && nf b && ne c *)
(* | tNat => false *)
| tEq _ _ _ => false
| tRefl => false
| tSig _ _ _ => false
| tPack _ _ _ => false
| tLet _ _ a b => ne a && nf b
| tVoid => false
| tAbsurd a => nf a
| tZero => false
| tNat => false
| tSuc _ => false
| tInd _ a b c => nf a && nf b && ne c
| tUnit => false
| tTT => false
| tSeq _ a b => ne a && nf b
end
with nf (a : tm) : bool :=
match a with
| var_tm _ => true
| tApp a ℓ0 b => ne a && nf b
| tAbs _ a => nf a
| tPi _ A B => nf A && nf B
| tJ _ t p => nf t && ne p
| tUniv _ => true
(* | tZero => true *)
(* | tSuc a => nf a *)
(* | tInd a b c => nf a && nf b && ne c *)
(* | tNat => true *)
| tEq _ a b => nf a && nf b
| tRefl => true
| tSig _ A B => nf A && nf B
| tPack _ a b => nf a && nf b
| tLet _ _ a b => ne a && nf b
| tVoid => true
| tAbsurd a => nf a
| tZero => true
| tNat => true
| tSuc a => nf a
| tInd _ a b c => nf a && nf b && ne c
| tUnit => true
| tTT => true
| tSeq _ a b => ne a && nf b
end.
(* Definition 5.1 (Weakly normalizing terms) *)
(* Terms that are weakly normalizing to a neutral or normal form. *)
Definition wn (a : tm) := exists b, a ⇒* b /\ nf b.
Definition wne (a : tm) := exists b, a ⇒* b /\ ne b.
Definition var_or_d a :=
match a with
| (tAbsurd tVoid) => true
| var_tm _ => true
| _ => false
end.
Definition ren_with_d (ξ : nat -> tm) :=
forall i, var_or_d (ξ i).
End normalform_sig.
Module normalform_fact
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax)
(Import normalform : normalform_sig lattice syntax par).
Module pf := par_facts lattice syntax par.
Import pf.
(* All neutral terms are normal forms *)
Lemma ne_nf (a : tm) : ne a -> nf a.
Proof. elim : a =>//; hauto q:on unfold:nf inv:Par. Qed.
(* Weakly neutral implies weakly normal *)
Lemma wne_wn a : wne a -> wn a.
Proof. sfirstorder use:ne_nf. Qed.
(* Normal implies weakly normal *)
Lemma nf_wn v : nf v -> wn v.
Proof. sfirstorder ctrs:rtc. Qed.
Function is_nat_val (a : tm) : bool :=
match a with
| tZero => true
| tSuc a => is_nat_val a
| _ => ne a
end.
(* natural number values are normal *)
Lemma nat_val_nf v : is_nat_val v -> nf v.
Proof. elim : v =>//=. Qed.
Lemma ne_nat_val v : ne v -> is_nat_val v.
Proof. elim : v =>//=. Qed.
(* Neutral and normal forms are stable under renaming *)
Lemma ne_nf_renaming (a : tm) :
forall (ξ : nat -> nat),
(ne a <-> ne (a⟨ξ⟩)) /\ (nf a <-> nf (a⟨ξ⟩)).
Proof.
elim : a; solve [auto; hauto b:on].
Qed.
(* Lemma 5.2 *)
Lemma nf_refl a b (h: a ⇒ b) : (nf a -> b = a) /\ (ne a -> b = a).
Proof.
elim : a b / h => // ; hauto b:on.
Qed.
Lemma nf_refl_star a b (h: a ⇒* b) : (nf a -> b = a) /\ (ne a -> b = a).
Proof.
induction h; hauto lq:on rew:off inv:tm ctrs:rtc use:nf_refl.
Qed.
(* Normal and neural forms are preserved by parallel reduction. *)
Lemma nf_ne_preservation a b (h : a ⇒ b) : (nf a ==> nf b) /\ (ne a ==> ne b).
Proof.
elim : a b / h => //; hauto lqb:on depth:2.
Qed.
Lemma nf_preservation : forall a b, (a ⇒ b) -> nf a -> nf b.
Proof. sfirstorder use:nf_ne_preservation b:on. Qed.
Lemma ne_preservation : forall a b, (a ⇒ b) -> ne a -> ne b.
Proof. sfirstorder use:nf_ne_preservation b:on. Qed.
Create HintDb nfne.
#[export]Hint Resolve ne_nat_val nf_wn nat_val_nf ne_nf wne_wn ne_preservation nf_preservation : nfne.
(* ------------------ antirenaming ------------------------- *)
Lemma ren_var_or_d ξ a : var_or_d a = var_or_d a⟨ξ⟩.
Proof. case : a; hauto q:on. Qed.
Lemma var_or_d_ne a : var_or_d a -> ne a && nf a.
Proof. case : a; try hauto lq:on. case => //=. Qed.
Lemma ren_with_d_ne ξ i : ren_with_d ξ -> ne (ξ i) && nf (ξ i).
Proof. sfirstorder use:var_or_d_ne unfold:ren_with_d. Qed.
Lemma ren_with_d_up_tm ξ (h : ren_with_d ξ) :
ren_with_d (up_tm_tm ξ).
Proof.
rewrite /ren_with_d in h *.
case => //= n.
asimpl.
move /(_ n) : h.
by rewrite -ren_var_or_d.
Qed.
Lemma ren_with_d_imp ξ i a :
ren_with_d ξ ->
ξ i = a ->
var_or_d a.
Proof. scongruence. Qed.
(* Lemma 5.13 (Antirenaming for normal and neutral forms) *)
Lemma ne_nf_renaming_with_d (a : tm) :
forall ξ, ren_with_d ξ ->
(ne a = ne (a[ξ])) /\ (nf a = nf (a[ξ])).
Proof.
elim : a; try solve [auto; hauto use:ren_with_d_ne, ren_with_d_up_tm b:on].
Qed.
(* Lemma 5.12 (Antirenaming for parallel reduction) *)
Local Lemma Par_antirenaming (a b0 : tm) ξ
(hξ : ren_with_d ξ)
(h : a[ξ] ⇒ b0) : exists b, (a ⇒ b) /\ b0 = b[ξ].
Proof.
move E : (a[ξ]) h hξ => a0 h.
move : a ξ E.
elim : a0 b0 / h.
- move => + []//. eauto with par.
- move => + []//=; eauto with par.
- move => ℓ0 A0 A1 B0 B1 h0 ih0 h1 ih1 [] // /=.
hauto q:on use:ren_with_d_imp.
qauto l:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ0 a0 a1 h ih [] //.
hauto q:on use:ren_with_d_imp.
move => ℓ1 a ξ [] ?.
qauto l:on ctrs:Par use:ren_with_d_up_tm.
- move => a0 a1 ℓ0 b0 b1 + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par.
- move => a a0 b0 b1 ℓ0 ha iha hb ihb []//.
hauto q:on use:ren_with_d_imp.
move => []//.
hauto q:on use:ren_with_d_imp.
move => ℓ1 t t0 t1 ξ [] *. subst.
specialize iha with (1 := eq_refl).
specialize ihb with (1 := eq_refl).
move : (iha ltac:(by auto using ren_with_d_up_tm)) => [a [? ?]]. subst.
move : (ihb ltac:(by auto)) => [b [? ?]]. subst.
exists (subst_tm (b..) a).
split; last by asimpl.
hauto lq:on ctrs:Par.
- hauto q:on ctrs:Par inv:tm.
- move => + + + + []//=.
hauto q:on ctrs:Par inv:Par use:ren_with_d_imp.
qauto l:on ctrs:Par.
- hauto q:on inv:tm ctrs:Par.
- move => > ++++ [] //.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par.
- move => ? t0 t1 h0 h1 []//.
hauto q:on use:ren_with_d_imp.
move => ? t []//.
hauto q:on use:ren_with_d_imp.
move => ξ [?]. subst.
hauto q:on ctrs:Par.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ0 ℓ1 ? ? ? a1 b1 c1 ha iha hb ihb hc ihc []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ2 ℓ3 []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ4 a0 b0 c0 ξ [*]. subst.
specialize iha with (1 := eq_refl).
specialize ihb with (1 := eq_refl).
specialize ihc with (1 := eq_refl).
move /(_ ltac:(auto)) : iha => [a2 [iha ?]].
move /(_ ltac:(auto)) : ihb => [b2 [ihb ?]].
move /(_ ltac:(auto using ren_with_d_up_tm)) : ihc => [c2 [ihc ?]]. subst.
exists (c2[b2 .: a2 ..]).
split; [by auto with par | by asimpl].
- move => []//=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => a b ? iha []//=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc []//=.
hauto q:on use:ren_with_d_imp.
hauto lq:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ a0 a1 b ha iha []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ0 a2 b2 c2 ξ [? ? ?] h hξ. subst.
case : c2 h=>//=.
hauto q:on use:ren_with_d_imp.
qauto l:on ctrs:Par.
- move => ℓ a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ0 a2 b2 c2 ξ [? ? ?] h hξ. subst.
case : c2 h=>//=.
hauto q:on use:ren_with_d_imp.
move => t [?]. subst.
specialize ihc with (1 := eq_refl).
specialize ihb with (1 := eq_refl).
specialize iha with (1 := eq_refl).
have : ren_with_d (up_tm_tm (up_tm_tm ξ)) by auto using ren_with_d_up_tm.
move /ihb => {}ihb.
move /iha : (hξ) => {}iha.
move /ihc : (hξ) => {}ihc.
move : iha ihb ihc. clear.
move => [t'][h0]?.
move => [b2'][h1]?.
move => [t0'][h2]?. subst.
eexists.
split. apply P_IndSuc; eauto.
by asimpl.
- case=>//=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- case => //=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ a0 a1 b0 b1 ha iha hb ihb []//=.
hauto q:on use:ren_with_d_imp.
hauto lq:on ctrs:Par.
- move => ℓ b0 b1 hb ihb []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ0 [] //=.
move => n t ξ [*]. subst.
hauto q:on use:ren_with_d_imp.
hauto lq:on ctrs:Par.
- hauto q:on inv:tm.
Qed.
Local Lemma Pars_antirenaming (a b0 : tm) ξ
(hξ : ren_with_d ξ)
(h : (a[ξ] ⇒* b0)) : exists b, b0 = b[ξ] /\ (a ⇒* b).
Proof.
move E : (a[ξ]) h => a0 h.
move : a E.
elim : a0 b0 / h.
- hauto lq:on ctrs:rtc.
- move => a b c h0 h ih a0 ?. subst.
move /Par_antirenaming : h0.
hauto lq:on ctrs:rtc, eq.
Qed.
(* Lemma 5.14 (Antirenaming for weak normalization) *)
Lemma wn_antirenaming a (ξ : nat -> tm) (hξ : ren_with_d ξ) : wn (a[ξ]) -> wn a.
Proof.
rewrite /wn.
move => [v [rv nfv]].
move: Pars_antirenaming (hξ) (rv); repeat move/[apply]. move => [b [hb ?]]. subst.
hauto q:on use:ne_nf_renaming_with_d.
Qed.
(* ------------------------------------------------------ *)
(* We can construct proofs that terms are weakly neutral
and weakly normal compositionally. *)
Lemma wne_absurd a :
wn a -> wne (tAbsurd a).
Proof.
move => [a0 [? ?]].
exists (tAbsurd a0).
sfirstorder use:S_Absurd.
Qed.
Lemma wne_j ℓp (t p : tm) :
wn t -> wne p -> wne (tJ ℓp t p).
Proof.
move => [t0 [? ?]] [p0 [? ?]].
exists (tJ ℓp t0 p0).
hauto lq:on b:on use:S_J.
Qed.
Lemma wne_ind ℓ (a b c : tm) :
wn a -> wn b -> wne c -> wne (tInd ℓ a b c).
Proof.
move => [a0 [? ?]] [b0 [? ?]] [c0 [? ?]].
exists (tInd ℓ a0 b0 c0).
qauto l:on use:S_Ind b:on.
Qed.
Lemma wne_app ℓ0 (a b : tm) :
wne a -> wn b -> wne (tApp a ℓ0 b).
Proof.
move => [a0 [? ?]] [b0 [? ?]].
exists (tApp a0 ℓ0 b0).
hauto b:on use:S_AppLR.
Qed.
Lemma wne_seq ℓ0 (a b : tm) :
wne a -> wn b -> wne (tSeq ℓ0 a b).
Proof.
move => [a0 [? ?]] [b0 [? ?]].
exists (tSeq ℓ0 a0 b0).
hauto b:on use:S_Seq.
Qed.
Lemma wne_let ℓ0 ℓ1 (a b : tm) :
wne a -> wn b -> wne (tLet ℓ0 ℓ1 a b).
Proof.
move => [a0 [? ?]] [b0 [? ?]].
exists (tLet ℓ0 ℓ1 a0 b0).
hauto b:on use:S_Let.
Qed.
Lemma wn_abs ℓ0 (a : tm) (h : wn a) : wn (tAbs ℓ0 a).
Proof.
move : h => [v [? ?]].
exists (tAbs ℓ0 v).
eauto using S_Abs.
Qed.
Lemma wn_pi ℓ0 A B : wn A -> wn B -> wn (tPi ℓ0 A B).
Proof.
move => [A0 [? ?]] [B0 [? ?]].
exists (tPi ℓ0 A0 B0).
hauto lqb:on use:S_Pi.
Qed.
Lemma wn_sig ℓ0 A B : wn A -> wn B -> wn (tSig ℓ0 A B).
Proof.
move => [A0 [? ?]] [B0 [? ?]].
exists (tSig ℓ0 A0 B0).
hauto lqb:on use:S_Sig.
Qed.
Lemma wn_pack ℓ0 A B : wn A -> wn B -> wn (tPack ℓ0 A B).
Proof.
move => [A0 [? ?]] [B0 [? ?]].
exists (tPack ℓ0 A0 B0).
hauto lqb:on use:S_Pack.
Qed.
Lemma wn_eq ℓ0 a b : wn a -> wn b -> wn (tEq ℓ0 a b).
Proof.
rewrite /wn.
move => [va [? ?]] [vb [? ?]].
exists (tEq ℓ0 va vb).
split.
- by apply S_Eq.
- hauto lqb:on.
Qed.
(* --------------------------------------------------------------- *)
(* This lemma is is like an
inversion principle for terms with normal forms. If a term applied to a
variable is normal, then the term itself is normal. *)
Lemma ext_wn ℓ0 (a : tm) :
wn (tApp a ℓ0 (tAbsurd tVoid)) ->
wn a.
Proof.
set tD := tAbsurd tVoid.
move E : (tApp a ℓ0 tD) => a0 [v [hr hv]].
move : a E.
move : hv.
elim : a0 v / hr.
- hauto inv:tm ctrs:rtc b:on db: nfne.
- move => a0 a1 a2 hr0 hr1 ih hnfa2.
move /(_ hnfa2) in ih.
move => a.
case : a0 hr0=>// => b0 ℓ b1.
elim /Par_inv=>//.
+ hauto q:on inv:Par ctrs:rtc b:on.
+ move => ? a0 a3 b2 b3 ℓ1 ? ? [? ? ?] ? [? ? ?]. subst.
have ? : b3 = tD by hauto lq:on inv:Par. subst.
suff : wn (tAbs ℓ a3) by hauto lq:on ctrs:Par, rtc unfold:wn.
have : wn (subst_tm (tD ..) a3) by sfirstorder.
move /wn_antirenaming => h.
apply : wn_abs.
apply h.
case => //=.
Qed.
Lemma confluent_nf a b v (h : a ⇒* b) (h0 : a ⇒* v) (h1 : nf v) :
b ⇒* v.
Proof.
have : exists v' , b ⇒* v' /\ v ⇒* v' by sfirstorder use:Pars_confluent unfold:confluent.
hauto l:on use:nf_refl_star.
Qed.
End normalform_fact.
Module Type normalform_sig
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax).
(* Identifying neutral (ne) and normal (nf) terms *)
Fixpoint ne (a : tm) : bool :=
match a with
| var_tm _ => true
| tApp a ℓ0 b => ne a && nf b
| tAbs _ _ => false
| tPi _ A B => false
| tJ _ t p => nf t && ne p
| tUniv _ => false
(* | tZero => false *)
(* | tSuc _ => false *)
(* | tInd a b c => nf a && nf b && ne c *)
(* | tNat => false *)
| tEq _ _ _ => false
| tRefl => false
| tSig _ _ _ => false
| tPack _ _ _ => false
| tLet _ _ a b => ne a && nf b
| tVoid => false
| tAbsurd a => nf a
| tZero => false
| tNat => false
| tSuc _ => false
| tInd _ a b c => nf a && nf b && ne c
| tUnit => false
| tTT => false
| tSeq _ a b => ne a && nf b
end
with nf (a : tm) : bool :=
match a with
| var_tm _ => true
| tApp a ℓ0 b => ne a && nf b
| tAbs _ a => nf a
| tPi _ A B => nf A && nf B
| tJ _ t p => nf t && ne p
| tUniv _ => true
(* | tZero => true *)
(* | tSuc a => nf a *)
(* | tInd a b c => nf a && nf b && ne c *)
(* | tNat => true *)
| tEq _ a b => nf a && nf b
| tRefl => true
| tSig _ A B => nf A && nf B
| tPack _ a b => nf a && nf b
| tLet _ _ a b => ne a && nf b
| tVoid => true
| tAbsurd a => nf a
| tZero => true
| tNat => true
| tSuc a => nf a
| tInd _ a b c => nf a && nf b && ne c
| tUnit => true
| tTT => true
| tSeq _ a b => ne a && nf b
end.
(* Definition 5.1 (Weakly normalizing terms) *)
(* Terms that are weakly normalizing to a neutral or normal form. *)
Definition wn (a : tm) := exists b, a ⇒* b /\ nf b.
Definition wne (a : tm) := exists b, a ⇒* b /\ ne b.
Definition var_or_d a :=
match a with
| (tAbsurd tVoid) => true
| var_tm _ => true
| _ => false
end.
Definition ren_with_d (ξ : nat -> tm) :=
forall i, var_or_d (ξ i).
End normalform_sig.
Module normalform_fact
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax)
(Import normalform : normalform_sig lattice syntax par).
Module pf := par_facts lattice syntax par.
Import pf.
(* All neutral terms are normal forms *)
Lemma ne_nf (a : tm) : ne a -> nf a.
Proof. elim : a =>//; hauto q:on unfold:nf inv:Par. Qed.
(* Weakly neutral implies weakly normal *)
Lemma wne_wn a : wne a -> wn a.
Proof. sfirstorder use:ne_nf. Qed.
(* Normal implies weakly normal *)
Lemma nf_wn v : nf v -> wn v.
Proof. sfirstorder ctrs:rtc. Qed.
Function is_nat_val (a : tm) : bool :=
match a with
| tZero => true
| tSuc a => is_nat_val a
| _ => ne a
end.
(* natural number values are normal *)
Lemma nat_val_nf v : is_nat_val v -> nf v.
Proof. elim : v =>//=. Qed.
Lemma ne_nat_val v : ne v -> is_nat_val v.
Proof. elim : v =>//=. Qed.
(* Neutral and normal forms are stable under renaming *)
Lemma ne_nf_renaming (a : tm) :
forall (ξ : nat -> nat),
(ne a <-> ne (a⟨ξ⟩)) /\ (nf a <-> nf (a⟨ξ⟩)).
Proof.
elim : a; solve [auto; hauto b:on].
Qed.
(* Lemma 5.2 *)
Lemma nf_refl a b (h: a ⇒ b) : (nf a -> b = a) /\ (ne a -> b = a).
Proof.
elim : a b / h => // ; hauto b:on.
Qed.
Lemma nf_refl_star a b (h: a ⇒* b) : (nf a -> b = a) /\ (ne a -> b = a).
Proof.
induction h; hauto lq:on rew:off inv:tm ctrs:rtc use:nf_refl.
Qed.
(* Normal and neural forms are preserved by parallel reduction. *)
Lemma nf_ne_preservation a b (h : a ⇒ b) : (nf a ==> nf b) /\ (ne a ==> ne b).
Proof.
elim : a b / h => //; hauto lqb:on depth:2.
Qed.
Lemma nf_preservation : forall a b, (a ⇒ b) -> nf a -> nf b.
Proof. sfirstorder use:nf_ne_preservation b:on. Qed.
Lemma ne_preservation : forall a b, (a ⇒ b) -> ne a -> ne b.
Proof. sfirstorder use:nf_ne_preservation b:on. Qed.
Create HintDb nfne.
#[export]Hint Resolve ne_nat_val nf_wn nat_val_nf ne_nf wne_wn ne_preservation nf_preservation : nfne.
(* ------------------ antirenaming ------------------------- *)
Lemma ren_var_or_d ξ a : var_or_d a = var_or_d a⟨ξ⟩.
Proof. case : a; hauto q:on. Qed.
Lemma var_or_d_ne a : var_or_d a -> ne a && nf a.
Proof. case : a; try hauto lq:on. case => //=. Qed.
Lemma ren_with_d_ne ξ i : ren_with_d ξ -> ne (ξ i) && nf (ξ i).
Proof. sfirstorder use:var_or_d_ne unfold:ren_with_d. Qed.
Lemma ren_with_d_up_tm ξ (h : ren_with_d ξ) :
ren_with_d (up_tm_tm ξ).
Proof.
rewrite /ren_with_d in h *.
case => //= n.
asimpl.
move /(_ n) : h.
by rewrite -ren_var_or_d.
Qed.
Lemma ren_with_d_imp ξ i a :
ren_with_d ξ ->
ξ i = a ->
var_or_d a.
Proof. scongruence. Qed.
(* Lemma 5.13 (Antirenaming for normal and neutral forms) *)
Lemma ne_nf_renaming_with_d (a : tm) :
forall ξ, ren_with_d ξ ->
(ne a = ne (a[ξ])) /\ (nf a = nf (a[ξ])).
Proof.
elim : a; try solve [auto; hauto use:ren_with_d_ne, ren_with_d_up_tm b:on].
Qed.
(* Lemma 5.12 (Antirenaming for parallel reduction) *)
Local Lemma Par_antirenaming (a b0 : tm) ξ
(hξ : ren_with_d ξ)
(h : a[ξ] ⇒ b0) : exists b, (a ⇒ b) /\ b0 = b[ξ].
Proof.
move E : (a[ξ]) h hξ => a0 h.
move : a ξ E.
elim : a0 b0 / h.
- move => + []//. eauto with par.
- move => + []//=; eauto with par.
- move => ℓ0 A0 A1 B0 B1 h0 ih0 h1 ih1 [] // /=.
hauto q:on use:ren_with_d_imp.
qauto l:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ0 a0 a1 h ih [] //.
hauto q:on use:ren_with_d_imp.
move => ℓ1 a ξ [] ?.
qauto l:on ctrs:Par use:ren_with_d_up_tm.
- move => a0 a1 ℓ0 b0 b1 + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par.
- move => a a0 b0 b1 ℓ0 ha iha hb ihb []//.
hauto q:on use:ren_with_d_imp.
move => []//.
hauto q:on use:ren_with_d_imp.
move => ℓ1 t t0 t1 ξ [] *. subst.
specialize iha with (1 := eq_refl).
specialize ihb with (1 := eq_refl).
move : (iha ltac:(by auto using ren_with_d_up_tm)) => [a [? ?]]. subst.
move : (ihb ltac:(by auto)) => [b [? ?]]. subst.
exists (subst_tm (b..) a).
split; last by asimpl.
hauto lq:on ctrs:Par.
- hauto q:on ctrs:Par inv:tm.
- move => + + + + []//=.
hauto q:on ctrs:Par inv:Par use:ren_with_d_imp.
qauto l:on ctrs:Par.
- hauto q:on inv:tm ctrs:Par.
- move => > ++++ [] //.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par.
- move => ? t0 t1 h0 h1 []//.
hauto q:on use:ren_with_d_imp.
move => ? t []//.
hauto q:on use:ren_with_d_imp.
move => ξ [?]. subst.
hauto q:on ctrs:Par.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => > + + + + []//.
hauto q:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ0 ℓ1 ? ? ? a1 b1 c1 ha iha hb ihb hc ihc []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ2 ℓ3 []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ4 a0 b0 c0 ξ [*]. subst.
specialize iha with (1 := eq_refl).
specialize ihb with (1 := eq_refl).
specialize ihc with (1 := eq_refl).
move /(_ ltac:(auto)) : iha => [a2 [iha ?]].
move /(_ ltac:(auto)) : ihb => [b2 [ihb ?]].
move /(_ ltac:(auto using ren_with_d_up_tm)) : ihc => [c2 [ihc ?]]. subst.
exists (c2[b2 .: a2 ..]).
split; [by auto with par | by asimpl].
- move => []//=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => a b ? iha []//=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc []//=.
hauto q:on use:ren_with_d_imp.
hauto lq:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ a0 a1 b ha iha []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ0 a2 b2 c2 ξ [? ? ?] h hξ. subst.
case : c2 h=>//=.
hauto q:on use:ren_with_d_imp.
qauto l:on ctrs:Par.
- move => ℓ a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ0 a2 b2 c2 ξ [? ? ?] h hξ. subst.
case : c2 h=>//=.
hauto q:on use:ren_with_d_imp.
move => t [?]. subst.
specialize ihc with (1 := eq_refl).
specialize ihb with (1 := eq_refl).
specialize iha with (1 := eq_refl).
have : ren_with_d (up_tm_tm (up_tm_tm ξ)) by auto using ren_with_d_up_tm.
move /ihb => {}ihb.
move /iha : (hξ) => {}iha.
move /ihc : (hξ) => {}ihc.
move : iha ihb ihc. clear.
move => [t'][h0]?.
move => [b2'][h1]?.
move => [t0'][h2]?. subst.
eexists.
split. apply P_IndSuc; eauto.
by asimpl.
- case=>//=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- case => //=.
hauto l:on use:ren_with_d_imp.
hauto q:on ctrs:Par use:ren_with_d_up_tm.
- move => ℓ a0 a1 b0 b1 ha iha hb ihb []//=.
hauto q:on use:ren_with_d_imp.
hauto lq:on ctrs:Par.
- move => ℓ b0 b1 hb ihb []//=.
hauto q:on use:ren_with_d_imp.
move => ℓ0 [] //=.
move => n t ξ [*]. subst.
hauto q:on use:ren_with_d_imp.
hauto lq:on ctrs:Par.
- hauto q:on inv:tm.
Qed.
Local Lemma Pars_antirenaming (a b0 : tm) ξ
(hξ : ren_with_d ξ)
(h : (a[ξ] ⇒* b0)) : exists b, b0 = b[ξ] /\ (a ⇒* b).
Proof.
move E : (a[ξ]) h => a0 h.
move : a E.
elim : a0 b0 / h.
- hauto lq:on ctrs:rtc.
- move => a b c h0 h ih a0 ?. subst.
move /Par_antirenaming : h0.
hauto lq:on ctrs:rtc, eq.
Qed.
(* Lemma 5.14 (Antirenaming for weak normalization) *)
Lemma wn_antirenaming a (ξ : nat -> tm) (hξ : ren_with_d ξ) : wn (a[ξ]) -> wn a.
Proof.
rewrite /wn.
move => [v [rv nfv]].
move: Pars_antirenaming (hξ) (rv); repeat move/[apply]. move => [b [hb ?]]. subst.
hauto q:on use:ne_nf_renaming_with_d.
Qed.
(* ------------------------------------------------------ *)
(* We can construct proofs that terms are weakly neutral
and weakly normal compositionally. *)
Lemma wne_absurd a :
wn a -> wne (tAbsurd a).
Proof.
move => [a0 [? ?]].
exists (tAbsurd a0).
sfirstorder use:S_Absurd.
Qed.
Lemma wne_j ℓp (t p : tm) :
wn t -> wne p -> wne (tJ ℓp t p).
Proof.
move => [t0 [? ?]] [p0 [? ?]].
exists (tJ ℓp t0 p0).
hauto lq:on b:on use:S_J.
Qed.
Lemma wne_ind ℓ (a b c : tm) :
wn a -> wn b -> wne c -> wne (tInd ℓ a b c).
Proof.
move => [a0 [? ?]] [b0 [? ?]] [c0 [? ?]].
exists (tInd ℓ a0 b0 c0).
qauto l:on use:S_Ind b:on.
Qed.
Lemma wne_app ℓ0 (a b : tm) :
wne a -> wn b -> wne (tApp a ℓ0 b).
Proof.
move => [a0 [? ?]] [b0 [? ?]].
exists (tApp a0 ℓ0 b0).
hauto b:on use:S_AppLR.
Qed.
Lemma wne_seq ℓ0 (a b : tm) :
wne a -> wn b -> wne (tSeq ℓ0 a b).
Proof.
move => [a0 [? ?]] [b0 [? ?]].
exists (tSeq ℓ0 a0 b0).
hauto b:on use:S_Seq.
Qed.
Lemma wne_let ℓ0 ℓ1 (a b : tm) :
wne a -> wn b -> wne (tLet ℓ0 ℓ1 a b).
Proof.
move => [a0 [? ?]] [b0 [? ?]].
exists (tLet ℓ0 ℓ1 a0 b0).
hauto b:on use:S_Let.
Qed.
Lemma wn_abs ℓ0 (a : tm) (h : wn a) : wn (tAbs ℓ0 a).
Proof.
move : h => [v [? ?]].
exists (tAbs ℓ0 v).
eauto using S_Abs.
Qed.
Lemma wn_pi ℓ0 A B : wn A -> wn B -> wn (tPi ℓ0 A B).
Proof.
move => [A0 [? ?]] [B0 [? ?]].
exists (tPi ℓ0 A0 B0).
hauto lqb:on use:S_Pi.
Qed.
Lemma wn_sig ℓ0 A B : wn A -> wn B -> wn (tSig ℓ0 A B).
Proof.
move => [A0 [? ?]] [B0 [? ?]].
exists (tSig ℓ0 A0 B0).
hauto lqb:on use:S_Sig.
Qed.
Lemma wn_pack ℓ0 A B : wn A -> wn B -> wn (tPack ℓ0 A B).
Proof.
move => [A0 [? ?]] [B0 [? ?]].
exists (tPack ℓ0 A0 B0).
hauto lqb:on use:S_Pack.
Qed.
Lemma wn_eq ℓ0 a b : wn a -> wn b -> wn (tEq ℓ0 a b).
Proof.
rewrite /wn.
move => [va [? ?]] [vb [? ?]].
exists (tEq ℓ0 va vb).
split.
- by apply S_Eq.
- hauto lqb:on.
Qed.
(* --------------------------------------------------------------- *)
(* This lemma is is like an
inversion principle for terms with normal forms. If a term applied to a
variable is normal, then the term itself is normal. *)
Lemma ext_wn ℓ0 (a : tm) :
wn (tApp a ℓ0 (tAbsurd tVoid)) ->
wn a.
Proof.
set tD := tAbsurd tVoid.
move E : (tApp a ℓ0 tD) => a0 [v [hr hv]].
move : a E.
move : hv.
elim : a0 v / hr.
- hauto inv:tm ctrs:rtc b:on db: nfne.
- move => a0 a1 a2 hr0 hr1 ih hnfa2.
move /(_ hnfa2) in ih.
move => a.
case : a0 hr0=>// => b0 ℓ b1.
elim /Par_inv=>//.
+ hauto q:on inv:Par ctrs:rtc b:on.
+ move => ? a0 a3 b2 b3 ℓ1 ? ? [? ? ?] ? [? ? ?]. subst.
have ? : b3 = tD by hauto lq:on inv:Par. subst.
suff : wn (tAbs ℓ a3) by hauto lq:on ctrs:Par, rtc unfold:wn.
have : wn (subst_tm (tD ..) a3) by sfirstorder.
move /wn_antirenaming => h.
apply : wn_abs.
apply h.
case => //=.
Qed.
Lemma confluent_nf a b v (h : a ⇒* b) (h0 : a ⇒* v) (h1 : nf v) :
b ⇒* v.
Proof.
have : exists v' , b ⇒* v' /\ v ⇒* v' by sfirstorder use:Pars_confluent unfold:confluent.
hauto l:on use:nf_refl_star.
Qed.
End normalform_fact.