Add constants to the reduction semantics
This commit is contained in:
parent
0f1e85c853
commit
f3718707f2
3 changed files with 74 additions and 130 deletions
|
|
@ -69,9 +69,8 @@ Module Par.
|
|||
R A0 A1 ->
|
||||
R B0 B1 ->
|
||||
R (TBind p A0 B0) (TBind p A1 B1)
|
||||
(* Bot is useful for making the prov function computable *)
|
||||
| BotCong :
|
||||
R Bot Bot
|
||||
| ConstCong k :
|
||||
R (Const k) (Const k)
|
||||
| UnivCong i :
|
||||
R (Univ i) (Univ i).
|
||||
|
||||
|
|
@ -212,7 +211,7 @@ Module Par.
|
|||
move : ihB => [c0 [? ?]]. subst.
|
||||
eexists. split. by apply BindCong; eauto.
|
||||
by asimpl.
|
||||
- move => n n0 ξ []//=. hauto l:on.
|
||||
- move => n k m ξ []//=. hauto l:on.
|
||||
- move => n i n0 ξ []//=. hauto l:on.
|
||||
Qed.
|
||||
|
||||
|
|
@ -275,10 +274,10 @@ Module Pars.
|
|||
|
||||
End Pars.
|
||||
|
||||
Definition var_or_bot {n} (a : Tm n) :=
|
||||
Definition var_or_const {n} (a : Tm n) :=
|
||||
match a with
|
||||
| VarTm _ => true
|
||||
| Bot => true
|
||||
| Const _ => true
|
||||
| _ => false
|
||||
end.
|
||||
|
||||
|
|
@ -324,8 +323,8 @@ Module RPar.
|
|||
R A0 A1 ->
|
||||
R B0 B1 ->
|
||||
R (TBind p A0 B0) (TBind p A1 B1)
|
||||
| BotCong :
|
||||
R Bot Bot
|
||||
| ConstCong k :
|
||||
R (Const k) (Const k)
|
||||
| UnivCong i :
|
||||
R (Univ i) (Univ i).
|
||||
|
||||
|
|
@ -571,8 +570,8 @@ Module RPar'.
|
|||
R A0 A1 ->
|
||||
R B0 B1 ->
|
||||
R (TBind p A0 B0) (TBind p A1 B1)
|
||||
| BotCong :
|
||||
R Bot Bot
|
||||
| ConstCong k :
|
||||
R (Const k) (Const k)
|
||||
| UnivCong i :
|
||||
R (Univ i) (Univ i).
|
||||
|
||||
|
|
@ -656,16 +655,16 @@ Module RPar'.
|
|||
qauto l:on ctrs:R inv:option.
|
||||
Qed.
|
||||
|
||||
Lemma var_or_bot_imp {n} (a b : Tm n) :
|
||||
var_or_bot a ->
|
||||
a = b -> ~~ var_or_bot b -> False.
|
||||
Lemma var_or_const_imp {n} (a b : Tm n) :
|
||||
var_or_const a ->
|
||||
a = b -> ~~ var_or_const b -> False.
|
||||
Proof.
|
||||
hauto lq:on inv:Tm.
|
||||
Qed.
|
||||
|
||||
Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
|
||||
(forall i, var_or_bot (ρ i)) ->
|
||||
(forall i, var_or_bot (up_Tm_Tm ρ i)).
|
||||
Lemma var_or_const_up n m (ρ : fin n -> Tm m) :
|
||||
(forall i, var_or_const (ρ i)) ->
|
||||
(forall i, var_or_const (up_Tm_Tm ρ i)).
|
||||
Proof.
|
||||
move => h /= [i|].
|
||||
- asimpl.
|
||||
|
|
@ -676,10 +675,10 @@ Module RPar'.
|
|||
- sfirstorder.
|
||||
Qed.
|
||||
|
||||
Local Ltac antiimp := qauto l:on use:var_or_bot_imp.
|
||||
Local Ltac antiimp := qauto l:on use:var_or_const_imp.
|
||||
|
||||
Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
|
||||
(forall i, var_or_bot (ρ i)) ->
|
||||
(forall i, var_or_const (ρ i)) ->
|
||||
R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
|
||||
Proof.
|
||||
move E : (subst_Tm ρ a) => u hρ h.
|
||||
|
|
@ -690,7 +689,7 @@ Module RPar'.
|
|||
case : c => //=; first by antiimp.
|
||||
move => c [?]. subst.
|
||||
spec_refl.
|
||||
have /var_or_bot_up hρ' := hρ.
|
||||
have /var_or_const_up hρ' := hρ.
|
||||
move : iha hρ' => /[apply] iha.
|
||||
move : ihb hρ => /[apply] ihb.
|
||||
spec_refl.
|
||||
|
|
@ -714,7 +713,7 @@ Module RPar'.
|
|||
hauto l:on.
|
||||
- move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
|
||||
move => t [*]. subst.
|
||||
have /var_or_bot_up {}/iha := hρ => iha.
|
||||
have /var_or_const_up {}/iha := hρ => iha.
|
||||
spec_refl.
|
||||
move :iha => [b0 [? ?]]. subst.
|
||||
eexists. split. by apply AbsCong; eauto.
|
||||
|
|
@ -750,7 +749,7 @@ Module RPar'.
|
|||
first by antiimp.
|
||||
move => ? t t0 [*]. subst.
|
||||
have {}/iha := (hρ) => iha.
|
||||
have /var_or_bot_up {}/ihB := (hρ) => ihB.
|
||||
have /var_or_const_up {}/ihB := (hρ) => ihB.
|
||||
spec_refl.
|
||||
move : iha => [b0 [? ?]].
|
||||
move : ihB => [c0 [? ?]]. subst.
|
||||
|
|
@ -894,8 +893,8 @@ Module EPar.
|
|||
R A0 A1 ->
|
||||
R B0 B1 ->
|
||||
R (TBind p A0 B0) (TBind p A1 B1)
|
||||
| BotCong :
|
||||
R Bot Bot
|
||||
| ConstCong k :
|
||||
R (Const k) (Const k)
|
||||
| UnivCong i :
|
||||
R (Univ i) (Univ i).
|
||||
|
||||
|
|
@ -1070,7 +1069,7 @@ Module RPars.
|
|||
Proof. hauto lq:on use:morphing inv:option. Qed.
|
||||
|
||||
Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
|
||||
(forall i, var_or_bot (ρ i)) ->
|
||||
(forall i, var_or_const (ρ i)) ->
|
||||
rtc RPar.R (subst_Tm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_Tm ρ b0 = b.
|
||||
Proof.
|
||||
move E :(subst_Tm ρ a) => u hρ h.
|
||||
|
|
@ -1157,7 +1156,7 @@ Module RPars'.
|
|||
Proof. hauto lq:on use:morphing inv:option. Qed.
|
||||
|
||||
Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
|
||||
(forall i, var_or_bot (ρ i)) ->
|
||||
(forall i, var_or_const (ρ i)) ->
|
||||
rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b.
|
||||
Proof.
|
||||
move E :(subst_Tm ρ a) => u hρ h.
|
||||
|
|
@ -1444,15 +1443,15 @@ Proof.
|
|||
- hauto l:on ctrs:OExp.R.
|
||||
Qed.
|
||||
|
||||
Lemma Bot_EPar' n (u : Tm n) :
|
||||
EPar.R Bot u ->
|
||||
rtc OExp.R Bot u.
|
||||
move E : Bot => t h.
|
||||
move : E. elim : n t u /h => //=.
|
||||
- move => n a0 a1 h ih ?. subst.
|
||||
Lemma Const_EPar' n k (u : Tm n) :
|
||||
EPar.R (Const k) u ->
|
||||
rtc OExp.R (Const k) u.
|
||||
move E : (Const k) => t h.
|
||||
move : k E. elim : n t u /h => //=.
|
||||
- move => n a0 a1 h ih k ?. subst.
|
||||
specialize ih with (1 := eq_refl).
|
||||
hauto lq:on ctrs:OExp.R use:rtc_r.
|
||||
- move => n a0 a1 h ih ?. subst.
|
||||
- move => n a0 a1 h ih k ?. subst.
|
||||
specialize ih with (1 := eq_refl).
|
||||
hauto lq:on ctrs:OExp.R use:rtc_r.
|
||||
- hauto l:on ctrs:OExp.R.
|
||||
|
|
@ -1519,7 +1518,7 @@ Proof.
|
|||
move : OExp.commutativity0 h2; repeat move/[apply].
|
||||
move => [d h].
|
||||
exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
|
||||
- qauto use:Bot_EPar', EPar.refl.
|
||||
- qauto use:Const_EPar', EPar.refl.
|
||||
- qauto use:Univ_EPar', EPar.refl.
|
||||
Qed.
|
||||
|
||||
|
|
@ -1536,7 +1535,7 @@ Function tstar {n} (a : Tm n) :=
|
|||
| Proj p (Abs a) => (Abs (Proj p (tstar a)))
|
||||
| Proj p a => Proj p (tstar a)
|
||||
| TBind p a b => TBind p (tstar a) (tstar b)
|
||||
| Bot => Bot
|
||||
| Const k => Const k
|
||||
| Univ i => Univ i
|
||||
end.
|
||||
|
||||
|
|
@ -1568,7 +1567,7 @@ Function tstar' {n} (a : Tm n) :=
|
|||
| Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b)
|
||||
| Proj p a => Proj p (tstar' a)
|
||||
| TBind p a b => TBind p (tstar' a) (tstar' b)
|
||||
| Bot => Bot
|
||||
| Const k => Const k
|
||||
| Univ i => Univ i
|
||||
end.
|
||||
|
||||
|
|
@ -1616,63 +1615,6 @@ Proof.
|
|||
sfirstorder use:relations.diamond_confluent, EPar_diamond.
|
||||
Qed.
|
||||
|
||||
Fixpoint depth_tm {n} (a : Tm n) :=
|
||||
match a with
|
||||
| VarTm _ => 1
|
||||
| TBind _ A B => 1 + max (depth_tm A) (depth_tm B)
|
||||
| Abs a => 1 + depth_tm a
|
||||
| App a b => 1 + max (depth_tm a) (depth_tm b)
|
||||
| Proj p a => 1 + depth_tm a
|
||||
| Pair a b => 1 + max (depth_tm a) (depth_tm b)
|
||||
| Bot => 1
|
||||
| Univ i => 1
|
||||
end.
|
||||
|
||||
Lemma depth_ren n m (ξ: fin n -> fin m) a :
|
||||
depth_tm a = depth_tm (ren_Tm ξ a).
|
||||
Proof.
|
||||
move : m ξ. elim : n / a; scongruence.
|
||||
Qed.
|
||||
|
||||
Lemma depth_subst n m (ρ : fin n -> Tm m) a :
|
||||
(forall i, depth_tm (ρ i) = 1) ->
|
||||
depth_tm a = depth_tm (subst_Tm ρ a).
|
||||
Proof.
|
||||
move : m ρ. elim : n / a.
|
||||
- sfirstorder.
|
||||
- move => n a iha m ρ hρ.
|
||||
simpl.
|
||||
f_equal. apply iha.
|
||||
destruct i as [i|].
|
||||
+ simpl.
|
||||
by rewrite -depth_ren.
|
||||
+ by simpl.
|
||||
- hauto lq:on rew:off.
|
||||
- hauto lq:on rew:off.
|
||||
- hauto lq:on rew:off.
|
||||
- move => n p a iha b ihb m ρ hρ.
|
||||
simpl. f_equal.
|
||||
f_equal.
|
||||
by apply iha.
|
||||
apply ihb.
|
||||
destruct i as [i|].
|
||||
+ simpl.
|
||||
by rewrite -depth_ren.
|
||||
+ by simpl.
|
||||
- sfirstorder.
|
||||
- sfirstorder.
|
||||
Qed.
|
||||
|
||||
Lemma depth_subst_bool n (a : Tm (S n)) :
|
||||
depth_tm a = depth_tm (subst_Tm (scons Bot VarTm) a).
|
||||
Proof.
|
||||
apply depth_subst.
|
||||
destruct i as [i|] => //=.
|
||||
Qed.
|
||||
|
||||
Local Ltac prov_tac := sfirstorder use:depth_ren.
|
||||
Local Ltac extract_tac := rewrite -?depth_subst_bool;hauto use:depth_subst_bool.
|
||||
|
||||
Definition prov_bind {n} p0 A0 B0 (a : Tm n) :=
|
||||
match a with
|
||||
| TBind p A B => p = p0 /\ rtc Par.R A A0 /\ rtc Par.R B B0
|
||||
|
|
@ -1704,8 +1646,8 @@ Inductive prov {n} : Tm n -> Tm n -> Prop :=
|
|||
| P_Proj h p a :
|
||||
prov h a ->
|
||||
prov h (Proj p a)
|
||||
| P_Bot :
|
||||
prov Bot Bot
|
||||
| P_Const k :
|
||||
prov (Const k) (Const k)
|
||||
| P_Var i :
|
||||
prov (VarTm i) (VarTm i)
|
||||
| P_Univ i :
|
||||
|
|
@ -1789,7 +1731,7 @@ Proof.
|
|||
split.
|
||||
move => h. constructor. move => b. asimpl. by constructor.
|
||||
inversion 1; subst.
|
||||
specialize H2 with (b := Bot).
|
||||
specialize H2 with (b := Const TPi).
|
||||
move : H2. asimpl. inversion 1; subst. done.
|
||||
Qed.
|
||||
|
||||
|
|
@ -1845,11 +1787,11 @@ Qed.
|
|||
Fixpoint extract {n} (a : Tm n) : Tm n :=
|
||||
match a with
|
||||
| TBind p A B => TBind p A B
|
||||
| Abs a => subst_Tm (scons Bot VarTm) (extract a)
|
||||
| Abs a => subst_Tm (scons (Const TPi) VarTm) (extract a)
|
||||
| App a b => extract a
|
||||
| Pair a b => extract a
|
||||
| Proj p a => extract a
|
||||
| Bot => Bot
|
||||
| Const k => Const k
|
||||
| VarTm i => VarTm i
|
||||
| Univ i => Univ i
|
||||
end.
|
||||
|
|
@ -1886,7 +1828,7 @@ Proof.
|
|||
Qed.
|
||||
|
||||
Lemma ren_subst_bot n (a : Tm (S n)) :
|
||||
extract (subst_Tm (scons Bot VarTm) a) = subst_Tm (scons Bot VarTm) (extract a).
|
||||
extract (subst_Tm (scons (Const TPi) VarTm) a) = subst_Tm (scons (Const TPi) VarTm) (extract a).
|
||||
Proof.
|
||||
apply ren_morphing. destruct i as [i|] => //=.
|
||||
Qed.
|
||||
|
|
@ -1896,7 +1838,7 @@ Definition prov_extract_spec {n} u (a : Tm n) :=
|
|||
| TBind p A B => exists A0 B0, extract a = TBind p A0 B0 /\ rtc Par.R A A0 /\ rtc Par.R B B0
|
||||
| Univ i => extract a = Univ i
|
||||
| VarTm i => extract a = VarTm i
|
||||
| Bot => extract a = Bot
|
||||
| (Const TPi) => extract a = (Const TPi)
|
||||
| _ => True
|
||||
end.
|
||||
|
||||
|
|
@ -1909,22 +1851,22 @@ Proof.
|
|||
- move => h a ha ih.
|
||||
case : h ha ih => //=.
|
||||
+ move => i ha ih.
|
||||
move /(_ Bot) in ih.
|
||||
move /(_ (Const TPi)) in ih.
|
||||
rewrite -ih.
|
||||
by rewrite ren_subst_bot.
|
||||
+ move => p A B h ih.
|
||||
move /(_ Bot) : ih => [A0][B0][h0][h1]h2.
|
||||
move /(_ (Const TPi)) : ih => [A0][B0][h0][h1]h2.
|
||||
rewrite ren_subst_bot in h0.
|
||||
rewrite h0.
|
||||
eauto.
|
||||
+ move => _ /(_ Bot).
|
||||
+ move => p _ /(_ (Const TPi)).
|
||||
by rewrite ren_subst_bot.
|
||||
+ move => i h /(_ Bot).
|
||||
+ move => i h /(_ (Const TPi)).
|
||||
by rewrite ren_subst_bot => ->.
|
||||
- hauto lq:on.
|
||||
- hauto lq:on.
|
||||
- hauto lq:on.
|
||||
- sfirstorder.
|
||||
- case => //=.
|
||||
- sfirstorder.
|
||||
- sfirstorder.
|
||||
Qed.
|
||||
|
|
@ -2400,23 +2342,24 @@ Fixpoint ne {n} (a : Tm n) :=
|
|||
match a with
|
||||
| VarTm i => true
|
||||
| TBind _ A B => false
|
||||
| Bot => true
|
||||
| App a b => ne a && nf b
|
||||
| Abs a => false
|
||||
| Univ _ => false
|
||||
| Proj _ a => ne a
|
||||
| Pair _ _ => false
|
||||
| Const _ => false
|
||||
end
|
||||
with nf {n} (a : Tm n) :=
|
||||
match a with
|
||||
| VarTm i => true
|
||||
| TBind _ A B => nf A && nf B
|
||||
| Bot => true
|
||||
| (Const TPi) => true
|
||||
| App a b => ne a && nf b
|
||||
| Abs a => nf a
|
||||
| Univ _ => true
|
||||
| Proj _ a => ne a
|
||||
| Pair a b => nf a && nf b
|
||||
| Const _ => true
|
||||
end.
|
||||
|
||||
Lemma ne_nf n a : @ne n a -> nf a.
|
||||
|
|
@ -2482,15 +2425,15 @@ Create HintDb nfne.
|
|||
#[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne.
|
||||
|
||||
Lemma ne_nf_antiren n m (a : Tm n) (ρ : fin n -> Tm m) :
|
||||
(forall i, var_or_bot (ρ i)) ->
|
||||
(forall i, var_or_const (ρ i)) ->
|
||||
(ne (subst_Tm ρ a) -> ne a) /\ (nf (subst_Tm ρ a) -> nf a).
|
||||
Proof.
|
||||
move : m ρ. elim : n / a => //;
|
||||
hauto b:on drew:off use:RPar.var_or_bot_up.
|
||||
hauto b:on drew:off use:RPar.var_or_const_up.
|
||||
Qed.
|
||||
|
||||
Lemma wn_antirenaming n m a (ρ : fin n -> Tm m) :
|
||||
(forall i, var_or_bot (ρ i)) ->
|
||||
(forall i, var_or_const (ρ i)) ->
|
||||
wn (subst_Tm ρ a) -> wn a.
|
||||
Proof.
|
||||
rewrite /wn => hρ.
|
||||
|
|
@ -2503,10 +2446,10 @@ Proof.
|
|||
Qed.
|
||||
|
||||
Lemma ext_wn n (a : Tm n) :
|
||||
wn (App a Bot) ->
|
||||
wn (App a (Const TPi)) ->
|
||||
wn a.
|
||||
Proof.
|
||||
move E : (App a Bot) => a0 [v [hr hv]].
|
||||
move E : (App a (Const TPi)) => a0 [v [hr hv]].
|
||||
move : a E.
|
||||
move : hv.
|
||||
elim : a0 v / hr.
|
||||
|
|
@ -2517,9 +2460,9 @@ Proof.
|
|||
case : a0 hr0=>// => b0 b1.
|
||||
elim /RPar'.inv=>// _.
|
||||
+ move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst.
|
||||
have ? : b3 = Bot by hauto lq:on inv:RPar'.R. subst.
|
||||
have ? : b3 = (Const TPi) by hauto lq:on inv:RPar'.R. subst.
|
||||
suff : wn (Abs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn.
|
||||
have : wn (subst_Tm (scons Bot VarTm) a3) by sfirstorder.
|
||||
have : wn (subst_Tm (scons (Const TPi) VarTm) a3) by sfirstorder.
|
||||
move => h. apply wn_abs.
|
||||
move : h. apply wn_antirenaming.
|
||||
hauto lq:on rew:off inv:option.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue