yiyunliu/pair-eta
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Make the internal language even smaller

Browse source
This commit is contained in:
Yiyun Liu 2025-04-03 21:18:17 -04:00
parent f402f4e528
commit 3b8fe388dc
4 changed files with 133 additions and 504 deletions
Download patch file Download diff file Expand all files Collapse all files

400
theories/fp_red.v
View file

@ -66,11 +66,7 @@ Module Par.
R a0 a1 ->
R (PProj p a0) (PProj p a1)
| ConstCong k :
R (PConst k) (PConst k)
| Univ i :
R (PUniv i) (PUniv i)
| Bot :
R PBot PBot.
R (PConst k) (PConst k).
Lemma refl (a : PTm) : R a a.
elim : a; hauto ctrs:R.
@ -130,8 +126,6 @@ Module Par.
- qauto l:on ctrs:R.
- qauto l:on ctrs:R.
- hauto l:on inv:option ctrs:R use:renaming.
- qauto l:on ctrs:R.
- qauto l:on ctrs:R.
Qed.
Lemma substing (a b : PTm) (ρ : nat -> PTm) :
@ -204,8 +198,6 @@ Module Par.
eexists. split. by apply ProjCong; eauto.
done.
- hauto q:on inv:PTm ctrs:R.
- hauto q:on inv:PTm ctrs:R.
- hauto q:on inv:PTm ctrs:R.
Qed.
End Par.
@ -267,14 +259,6 @@ Module Pars.
End Pars.
Definition var_or_const (a : PTm) :=
match a with
| VarPTm _ => true
| PBot => true
| _ => false
end.
(***************** Beta rules only ***********************)
Module RPar.
Inductive R : PTm -> PTm -> Prop :=
@ -314,11 +298,7 @@ Module RPar.
R a0 a1 ->
R (PProj p a0) (PProj p a1)
| ConstCong k :
R (PConst k) (PConst k)
| Univ i :
R (PUniv i) (PUniv i)
| Bot :
R PBot PBot.
R (PConst k) (PConst k).
Derive Dependent Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
@ -384,8 +364,6 @@ Module RPar.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R use:morphing_up.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R.
Qed.
Lemma substing (a b : PTm) (ρ : nat -> PTm) :
@ -404,120 +382,56 @@ Module RPar.
- simpl. apply Var.
Qed.
Lemma var_or_const_imp (a b : PTm) :
var_or_const a ->
a = b -> ~~ var_or_const b -> False.
Proof.
hauto lq:on inv:PTm.
Qed.
Lemma var_or_const_up (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
(forall i, var_or_const (up_PTm_PTm ρ i)).
Proof.
move => h /= [|i].
- sfirstorder.
- asimpl.
move /(_ i) in h.
rewrite /funcomp.
move : (ρ i) h.
case => //=.
Qed.
Ltac2 rec solve_anti_ren () :=
let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
intro $x;
lazy_match! Constr.type (Control.hyp x) with
| nat -> nat => (ltac1:(case;hauto q:on depth:2 ctrs:R))
| nat -> PTm => (ltac1:(case;hauto q:on depth:2 ctrs:R))
| _ => solve_anti_ren ()
end.
Local Ltac antiimp := qauto l:on use:var_or_const_imp.
Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b.
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
R (ren_PTm ρ a) b -> exists b0, R a b0 /\ ren_PTm ρ b0 = b.
Proof.
move E : (subst_PTm ρ a) => u hρ h.
move : ρ hρ a E. elim : u b/h.
- move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move E : (ren_PTm ρ a) => u h.
move : ρ a E. elim : u b/h; try solve_anti_ren.
- move => a0 a1 b0 b1 ha iha hb ihb ρ []//=.
move => c c0 [+ ?]. subst.
case : c => //=; first by antiimp.
case : c => //=.
move => c [?]. subst.
spec_refl.
have /var_or_const_up hρ' := hρ.
move : iha hρ' => /[apply] iha.
move : ihb hρ => /[apply] ihb.
spec_refl.
move : iha => [c1][ih0]?. subst.
move : ihb => [c2][ih1]?. subst.
eexists. split.
apply AppAbs; eauto.
by asimpl.
- move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ρ hρ.
move => []//=;
first by antiimp.
move => []//=; first by antiimp.
move => t t0 t1 [*]. subst.
have {}/iha := hρ => iha.
have {}/ihb := hρ => ihb.
have {}/ihc := hρ => ihc.
- move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ρ.
move => []//=.
move => []//=.
move => p p0 p1 [*]. subst.
spec_refl.
move : iha => [? [*]].
move : ihb => [? [*]].
move : ihc => [? [*]].
move : ihc => [? [*]]. subst.
eexists. split.
apply AppPair; hauto. subst.
apply AppPair; hauto.
by asimpl.
- move => p a0 a1 ha iha ρ hρ []//=;
first by antiimp.
move => p0 []//= t [*]; first by antiimp. subst.
have /var_or_const_up {}/iha := hρ => iha.
- move => p a0 a1 ha iha ρ []//=.
move => p0 []//= t [*]. subst.
spec_refl. move : iha => [b0 [? ?]]. subst.
eexists. split. apply ProjAbs; eauto. by asimpl.
- move => p a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move => p0 []//=; first by antiimp. move => t t0[*].
- move => p a0 a1 b0 b1 ha iha hb ihb ρ []//=.
move => p0 []//=. move => t t0[*].
subst.
have {}/iha := (hρ) => iha.
have {}/ihb := (hρ) => ihb.
spec_refl.
move : iha => [b0 [? ?]].
move : ihb => [c0 [? ?]]. subst.
eexists. split. by eauto using ProjPair.
hauto q:on.
- move => i ρ hρ []//=.
hauto l:on.
- move => a0 a1 ha iha ρ hρ []//=; first by antiimp.
move => t [*]. subst.
have /var_or_const_up {}/iha := hρ => iha.
spec_refl.
move :iha => [b0 [? ?]]. subst.
eexists. split. by apply AbsCong; eauto.
by asimpl.
- move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move => t t0 [*]. subst.
have {}/iha := (hρ) => iha.
have {}/ihb := (hρ) => ihb.
spec_refl.
move : iha => [b0 [? ?]]. subst.
move : ihb => [c0 [? ?]]. subst.
eexists. split. by apply AppCong; eauto.
done.
- move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move => t t0[*]. subst.
have {}/iha := (hρ) => iha.
have {}/ihb := (hρ) => ihb.
spec_refl.
move : iha => [b0 [? ?]]. subst.
move : ihb => [c0 [? ?]]. subst.
eexists. split. by apply PairCong; eauto.
by asimpl.
- move => p a0 a1 ha iha ρ hρ []//=;
first by antiimp.
move => p0 t [*]. subst.
have {}/iha := (hρ) => iha.
spec_refl.
move : iha => [b0 [? ?]]. subst.
eexists. split. apply ProjCong; eauto. reflexivity.
- hauto q:on ctrs:R inv:PTm.
- hauto q:on ctrs:R inv:PTm.
- hauto q:on ctrs:R inv:PTm.
Qed.
End RPar.
@ -552,11 +466,7 @@ Module RPar'.
R a0 a1 ->
R (PProj p a0) (PProj p a1)
| ConstCong k :
R (PConst k) (PConst k)
| UnivCong i :
R (PUniv i) (PUniv i)
| BotCong :
R PBot PBot.
R (PConst k) (PConst k).
Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
@ -620,8 +530,6 @@ Module RPar'.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R.
- hauto l:on ctrs:R use:morphing_up.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R.
Qed.
Lemma substing (a b : PTm) (ρ : nat -> PTm) :
@ -638,100 +546,39 @@ Module RPar'.
hauto l:on ctrs:R inv:nat.
Qed.
Lemma var_or_const_imp (a b : PTm) :
var_or_const a ->
a = b -> ~~ var_or_const b -> False.
Proof.
hauto lq:on inv:PTm.
Qed.
Ltac2 rec solve_anti_ren () :=
let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
intro $x;
lazy_match! Constr.type (Control.hyp x) with
| nat -> nat => (ltac1:(case;hauto q:on depth:2 ctrs:R))
| nat -> PTm => (ltac1:(case;hauto q:on depth:2 ctrs:R))
| _ => solve_anti_ren ()
end.
Lemma var_or_const_up (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
(forall i, var_or_const (up_PTm_PTm ρ i)).
Proof.
move => h /= [|i].
- sfirstorder.
- asimpl.
move /(_ i) in h.
rewrite /funcomp.
move : (ρ i) h.
case => //=.
Qed.
Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
Local Ltac antiimp := qauto l:on use:var_or_const_imp.
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b.
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
R (ren_PTm ρ a) b -> exists b0, R a b0 /\ ren_PTm ρ b0 = b.
Proof.
move E : (subst_PTm ρ a) => u hρ h.
move : ρ hρ a E. elim : u b/h.
- move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move => c c0 [+ ?]. subst.
case : c => //=; first by antiimp.
move => c [?]. subst.
spec_refl.
have /var_or_const_up hρ' := hρ.
move : iha hρ' => /[apply] iha.
move : ihb hρ => /[apply] ihb.
move E : (ren_PTm ρ a) => u h.
move : ρ a E. elim : u b/h; try solve_anti_ren.
- move => a0 a1 b0 b1 ha iha hb ihb ρ []//=.
move => []//=.
move => p p0 [*]. subst.
spec_refl.
move : iha => [c1][ih0]?. subst.
move : ihb => [c2][ih1]?. subst.
eexists. split.
apply AppAbs; eauto.
by asimpl.
- move => p a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move => p0 []//=; first by antiimp. move => t t0[*].
- move => p a0 a1 b0 b1 ha iha hb ihb ρ []//=.
move => p0 []//=. move => t t0[*].
subst.
have {}/iha := (hρ) => iha.
have {}/ihb := (hρ) => ihb.
spec_refl.
move : iha => [b0 [? ?]].
move : ihb => [c0 [? ?]]. subst.
eexists. split. by eauto using ProjPair.
hauto q:on.
- move => i ρ hρ []//=.
hauto l:on.
- move => a0 a1 ha iha ρ hρ []//=; first by antiimp.
move => t [*]. subst.
have /var_or_const_up {}/iha := hρ => iha.
spec_refl.
move :iha => [b0 [? ?]]. subst.
eexists. split. by apply AbsCong; eauto.
by asimpl.
- move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move => t t0 [*]. subst.
have {}/iha := (hρ) => iha.
have {}/ihb := (hρ) => ihb.
spec_refl.
move : iha => [b0 [? ?]]. subst.
move : ihb => [c0 [? ?]]. subst.
eexists. split. by apply AppCong; eauto.
done.
- move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
first by antiimp.
move => t t0[*]. subst.
have {}/iha := (hρ) => iha.
have {}/ihb := (hρ) => ihb.
spec_refl.
move : iha => [b0 [? ?]]. subst.
move : ihb => [c0 [? ?]]. subst.
eexists. split. by apply PairCong; eauto.
by asimpl.
- move => p a0 a1 ha iha ρ hρ []//=;
first by antiimp.
move => p0 t [*]. subst.
have {}/iha := (hρ) => iha.
spec_refl.
move : iha => [b0 [? ?]]. subst.
eexists. split. apply ProjCong; eauto. reflexivity.
- hauto q:on ctrs:R inv:PTm.
- move => i ρ hρ []//=; first by antiimp.
hauto l:on.
- hauto q:on inv:PTm ctrs:R.
Qed.
End RPar'.
@ -852,11 +699,7 @@ Module EPar.
R a0 a1 ->
R (PProj p a0) (PProj p a1)
| ConstCong k :
R (PConst k) (PConst k)
| UnivCong i :
R (PUniv i) (PUniv i)
| BotCong :
R PBot PBot.
R (PConst k) (PConst k).
Lemma refl (a : PTm) : EPar.R a a.
Proof.
@ -899,8 +742,6 @@ Module EPar.
- hauto q:on ctrs:R.
- hauto q:on ctrs:R.
- hauto l:on ctrs:R use:renaming inv:nat.
- hauto lq:on ctrs:R.
- hauto lq:on ctrs:R.
Qed.
Lemma substing a0 a1 (b0 b1 : PTm) :
@ -1022,17 +863,15 @@ Module RPars.
rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
Proof. hauto lq:on use:morphing inv:nat. Qed.
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
rtc RPar.R (subst_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_PTm ρ b0 = b.
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
rtc RPar.R (ren_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ ren_PTm ρ b0 = b.
Proof.
move E :(subst_PTm ρ a) => u hρ h.
move E :(ren_PTm ρ a) => u h.
move : a E.
elim : u b /h.
- sfirstorder.
- move => a b c h0 h1 ih1 a0 ?. subst.
move /RPar.antirenaming : h0.
move /(_ hρ).
move => [b0 [h2 ?]]. subst.
hauto lq:on rew:off ctrs:rtc.
Qed.
@ -1103,17 +942,15 @@ Module RPars'.
rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
Proof. hauto lq:on use:morphing inv:nat. Qed.
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
rtc RPar'.R (subst_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_PTm ρ b0 = b.
Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
rtc RPar'.R (ren_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ ren_PTm ρ b0 = b.
Proof.
move E :(subst_PTm ρ a) => u hρ h.
move E :(ren_PTm ρ a) => u h.
move : a E.
elim : u b /h.
- sfirstorder.
- move => a b c h0 h1 ih1 a0 ?. subst.
move /RPar'.antirenaming : h0.
move /(_ hρ).
move => [b0 [h2 ?]]. subst.
hauto lq:on rew:off ctrs:rtc.
Qed.
@ -1300,8 +1137,6 @@ Proof.
hauto lq:on use:RPars.ProjCong, relations.rtc_transitive.
+ hauto lq:on ctrs:EPar.R use:RPars.ProjCong.
- hauto l:on ctrs:EPar.R inv:RPar.R.
- hauto l:on ctrs:EPar.R inv:RPar.R.
- hauto l:on ctrs:EPar.R inv:RPar.R.
Qed.
Lemma commutativity1 (a b0 b1 : PTm) :
@ -1400,34 +1235,6 @@ Lemma Const_EPar' k (u : PTm) :
- hauto l:on ctrs:OExp.R.
Qed.
Lemma Bot_EPar' (u : PTm) :
EPar.R (PBot) u ->
rtc OExp.R (PBot) u.
move E : (PBot) => t h.
move : E. elim : t u /h => //=.
- move => a0 a1 h ih ?. subst.
specialize ih with (1 := eq_refl).
hauto lq:on ctrs:OExp.R use:rtc_r.
- move => a0 a1 h ih ?. subst.
specialize ih with (1 := eq_refl).
hauto lq:on ctrs:OExp.R use:rtc_r.
- hauto l:on ctrs:OExp.R.
Qed.
Lemma Univ_EPar' i (u : PTm) :
EPar.R (PUniv i) u ->
rtc OExp.R (PUniv i) u.
move E : (PUniv i) => t h.
move : E. elim : t u /h => //=.
- move => a0 a1 h ih ?. subst.
specialize ih with (1 := eq_refl).
hauto lq:on ctrs:OExp.R use:rtc_r.
- move => a0 a1 h ih ?. subst.
specialize ih with (1 := eq_refl).
hauto lq:on ctrs:OExp.R use:rtc_r.
- hauto l:on ctrs:OExp.R.
Qed.
Lemma EPar_diamond (c a1 b1 : PTm) :
EPar.R c a1 ->
EPar.R c b1 ->
@ -1469,8 +1276,6 @@ Proof.
move => [d1 h1].
exists d1. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
- qauto use:Const_EPar', EPar.refl.
- qauto use:Univ_EPar', EPar.refl.
- qauto use:Bot_EPar', EPar.refl.
Qed.
Function tstar (a : PTm) :=
@ -1486,8 +1291,6 @@ Function tstar (a : PTm) :=
| PProj p (PAbs a) => (PAbs (PProj p (tstar a)))
| PProj p a => PProj p (tstar a)
| PConst k => PConst k
| PUniv i => PUniv i
| PBot => PBot
end.
Lemma RPar_triangle (a : PTm) : forall b, RPar.R a b -> RPar.R b (tstar a).
@ -1504,8 +1307,6 @@ Proof.
- hauto lq:on inv:RPar.R ctrs:RPar.R.
- hauto lq:on inv:RPar.R ctrs:RPar.R.
- hauto lq:on inv:RPar.R ctrs:RPar.R.
- hauto lq:on inv:RPar.R ctrs:RPar.R.
- hauto lq:on inv:RPar.R ctrs:RPar.R.
Qed.
Function tstar' (a : PTm) :=
@ -1518,8 +1319,6 @@ Function tstar' (a : PTm) :=
| PProj p (PPair a b) => if p is PL then (tstar' a) else (tstar' b)
| PProj p a => PProj p (tstar' a)
| PConst k => PConst k
| PUniv i => PUniv i
| PBot => PBot
end.
Lemma RPar'_triangle (a : PTm) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
@ -1534,8 +1333,6 @@ Proof.
- hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
Qed.
Lemma RPar_diamond (c a1 b1 : PTm) :
@ -1583,11 +1380,7 @@ Inductive prov : PTm -> PTm -> Prop :=
| P_Const k :
prov (PConst k) (PConst k)
| P_Var i :
prov (VarPTm i) (VarPTm i)
| P_Univ i :
prov (PUniv i) (PUniv i)
| P_Bot :
prov PBot PBot.
prov (VarPTm i) (VarPTm i).
Lemma ERed_EPar (a b : PTm) : ERed.R a b -> EPar.R a b.
Proof.
@ -1605,8 +1398,6 @@ Proof.
- eauto using EReds.PairCong.
- eauto using EReds.ProjCong.
- auto using rtc_refl.
- auto using rtc_refl.
- auto using rtc_refl.
Qed.
Lemma EPar_Par (a b : PTm) : EPar.R a b -> Par.R a b.
@ -1658,8 +1449,6 @@ Proof.
+ hauto lq:on ctrs:prov.
- hauto lq:on ctrs:prov inv:RPar.R.
- hauto l:on ctrs:RPar.R inv:RPar.R.
- hauto l:on ctrs:RPar.R inv:RPar.R.
- hauto l:on ctrs:RPar.R inv:RPar.R.
Qed.
@ -1668,7 +1457,7 @@ Proof.
split.
move => h. constructor. move => b. asimpl. by constructor.
inversion 1; subst.
specialize H2 with (b := PBot).
specialize H2 with (b := (VarPTm var_zero)).
move : H2. asimpl. inversion 1; subst. done.
Qed.
@ -1703,8 +1492,6 @@ Proof.
- hauto lq:on inv:ERed.R, prov ctrs:prov.
- hauto lq:on inv:ERed.R, prov ctrs:prov.
- hauto lq:on inv:ERed.R, prov ctrs:prov.
- hauto lq:on inv:ERed.R, prov ctrs:prov.
- hauto lq:on inv:ERed.R, prov ctrs:prov.
Qed.
Lemma prov_ereds (u : PTm) a b : prov u a -> rtc ERed.R a b -> prov u b.
@ -1714,14 +1501,12 @@ Qed.
Fixpoint extract (a : PTm) : PTm :=
match a with
| PAbs a => subst_PTm (scons PBot VarPTm) (extract a)
| PAbs a => subst_PTm (scons (PConst 0) VarPTm) (extract a)
| PApp a b => extract a
| PPair a b => extract a
| PProj p a => extract a
| PConst k => PConst k
| VarPTm i => VarPTm i
| PUniv i => PUniv i
| PBot => PBot
end.
Lemma ren_extract (a : PTm) (ξ : nat -> nat) :
@ -1736,8 +1521,6 @@ Proof.
- hauto q:on.
- hauto q:on.
- hauto q:on.
- sfirstorder.
- sfirstorder.
Qed.
Lemma ren_morphing (a : PTm) (ρ : nat -> PTm) :
@ -1756,17 +1539,15 @@ Proof.
Qed.
Lemma ren_subst_bot (a : PTm) :
extract (subst_PTm (scons PBot VarPTm) a) = subst_PTm (scons PBot VarPTm) (extract a).
extract (subst_PTm (scons (PConst 0) VarPTm) a) = subst_PTm (scons (PConst 0) VarPTm) (extract a).
Proof.
apply ren_morphing. destruct i => //=.
Qed.
Definition prov_extract_spec u (a : PTm) :=
match u with
| PUniv i => extract a = PUniv i
| VarPTm i => extract a = VarPTm i
| (PConst i) => extract a = (PConst i)
| PBot => extract a = PBot
| _ => True
end.
@ -1778,23 +1559,16 @@ Proof.
- move => h a ha ih.
case : h ha ih => //=.
+ move => i ha ih.
move /(_ PBot) in ih.
move /(_ (PConst 0)) in ih.
rewrite -ih.
by rewrite ren_subst_bot.
+ move => p _ /(_ PBot).
by rewrite ren_subst_bot.
+ move => i h /(_ PBot).
by rewrite ren_subst_bot => ->.
+ move /(_ PBot).
move => h /(_ PBot).
+ move => p _ /(_ (PConst 0)).
by rewrite ren_subst_bot.
- hauto lq:on.
- hauto lq:on.
- hauto lq:on.
- case => //=.
- sfirstorder.
- sfirstorder.
- sfirstorder.
Qed.
Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b :=
@ -1970,8 +1744,6 @@ Proof.
- sfirstorder use:ERPars.PairCong.
- sfirstorder use:ERPars.ProjCong.
- sfirstorder.
- sfirstorder.
- sfirstorder.
Qed.
Lemma Pars_ERPar (a b : PTm) : rtc Par.R a b -> rtc ERPar.R a b.
@ -2139,15 +1911,6 @@ Proof.
hauto lq:on use:rtc_union.
Qed.
Lemma pars_univ_inv i (c : PTm) :
rtc Par.R (PUniv i) c ->
extract c = PUniv i.
Proof.
have : prov (PUniv i) (PUniv i : PTm) by sfirstorder.
move : prov_pars. repeat move/[apply].
apply prov_extract.
Qed.
Lemma pars_const_inv i (c : PTm) :
rtc Par.R (PConst i) c ->
extract c = PConst i.
@ -2166,14 +1929,6 @@ Proof.
apply prov_extract.
Qed.
Lemma pars_univ_inj i j (C : PTm) :
rtc Par.R (PUniv i) C ->
rtc Par.R (PUniv j) C ->
i = j.
Proof.
sauto l:on use:pars_univ_inv.
Qed.
Lemma pars_const_inj i j (C : PTm) :
rtc Par.R (PConst i) C ->
rtc Par.R (PConst j) C ->
@ -2202,12 +1957,6 @@ Proof. sfirstorder unfold:join. Qed.
Lemma join_refl (a : PTm) : join a a.
Proof. hauto lq:on ctrs:rtc unfold:join. Qed.
Lemma join_univ_inj i j :
join (PUniv i : PTm) (PUniv j) -> i = j.
Proof.
sfirstorder use:pars_univ_inj.
Qed.
Lemma join_const_inj i j :
join (PConst i : PTm) (PConst j) -> i = j.
Proof.
@ -2224,22 +1973,18 @@ Fixpoint ne (a : PTm) :=
| VarPTm i => true
| PApp a b => ne a && nf b
| PAbs a => false
| PUniv _ => false
| PProj _ a => ne a
| PPair _ _ => false
| PConst _ => false
| PBot => true
end
with nf (a : PTm) :=
match a with
| VarPTm i => true
| PApp a b => ne a && nf b
| PAbs a => nf a
| PUniv _ => true
| PProj _ a => ne a
| PPair a b => nf a && nf b
| PConst _ => true
| PBot => true
end.
Lemma ne_nf a : ne a -> nf a.
@ -2297,31 +2042,30 @@ Qed.
Create HintDb nfne.
#[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne.
Lemma ne_nf_antiren (a : PTm) (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
(ne (subst_PTm ρ a) -> ne a) /\ (nf (subst_PTm ρ a) -> nf a).
Lemma ne_nf_antiren (a : PTm) (ρ : nat -> nat) :
(ne (ren_PTm ρ a) -> ne a) /\ (nf (ren_PTm ρ a) -> nf a).
Proof.
move : ρ. elim : a => //;
hauto b:on drew:off use:RPar.var_or_const_up.
hauto b:on drew:off .
Qed.
Lemma wn_antirenaming a (ρ : nat -> PTm) :
(forall i, var_or_const (ρ i)) ->
wn (subst_PTm ρ a) -> wn a.
Lemma wn_antirenaming a (ρ : nat -> nat) :
wn (ren_PTm ρ a) -> wn a.
Proof.
rewrite /wn => hρ.
rewrite /wn.
move => [v [rv nfv]].
move /RPars'.antirenaming : rv.
move /(_ hρ) => [b [hb ?]]. subst.
move => [b [hb ?]]. subst.
exists b. split => //=.
move : nfv.
by eapply ne_nf_antiren.
Qed.
Lemma ext_wn (a : PTm) :
wn (PApp a PBot) ->
wn (PApp a (VarPTm var_zero)) ->
wn a.
Proof.
set PBot := VarPTm var_zero.
move E : (PApp a (PBot)) => a0 [v [hr hv]].
move : a E.
move : hv.
@ -2335,10 +2079,12 @@ Proof.
+ move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst.
have ? : b3 = (PBot) by hauto lq:on inv:RPar'.R. subst.
suff : wn (PAbs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn.
have : wn (subst_PTm (scons (PBot) VarPTm) a3) by sfirstorder.
have : wn (subst_PTm (scons (VarPTm var_zero) VarPTm) a3) by sfirstorder.
asimpl.
move => h. apply wn_abs.
move : h. apply wn_antirenaming.
hauto lq:on rew:off inv:nat.
move : h.
have -> : subst_PTm (scons (VarPTm var_zero) VarPTm) a3 = ren_PTm (scons var_zero id) a3 by substify; asimpl.
apply wn_antirenaming.
+ hauto q:on inv:RPar'.R ctrs:rtc b:on.
Qed.