Compare commits
No commits in common. "d48d9db1b74cbd044ac89d36ec29904c2d755fd0" and "ef3de3af3d68a1d768226f9ef0f9935fa560de6b" have entirely different histories.
d48d9db1b7
...
ef3de3af3d
2 changed files with 0 additions and 355 deletions
|
|
@ -657,18 +657,6 @@ Proof.
|
||||||
hauto lq:on use:Sub.bind_univ_noconf.
|
hauto lq:on use:Sub.bind_univ_noconf.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma T_AbsUniv_Imp' n Γ (a : PTm (S n)) i :
|
|
||||||
Γ ⊢ PAbs a ∈ PUniv i -> False.
|
|
||||||
Proof.
|
|
||||||
hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Abs_Inv.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma T_PairUniv_Imp' n Γ (a b : PTm n) i :
|
|
||||||
Γ ⊢ PPair a b ∈ PUniv i -> False.
|
|
||||||
Proof.
|
|
||||||
hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Pair_Inv.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma T_AbsBind_Imp n Γ a p A0 B0 (U : PTm n) :
|
Lemma T_AbsBind_Imp n Γ a p A0 B0 (U : PTm n) :
|
||||||
Γ ⊢ PAbs a ∈ U ->
|
Γ ⊢ PAbs a ∈ U ->
|
||||||
Γ ⊢ PBind p A0 B0 ∈ U ->
|
Γ ⊢ PBind p A0 B0 ∈ U ->
|
||||||
|
|
@ -946,7 +934,6 @@ Proof.
|
||||||
repeat split => //=; sfirstorder b:on use:ne_nf.
|
repeat split => //=; sfirstorder b:on use:ne_nf.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Lemma algo_metric_bind n k p0 (A0 : PTm n) B0 p1 A1 B1 :
|
Lemma algo_metric_bind n k p0 (A0 : PTm n) B0 p1 A1 B1 :
|
||||||
algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) ->
|
algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) ->
|
||||||
p0 = p1 /\ exists j, j < k /\ algo_metric j A0 A1 /\ algo_metric j B0 B1.
|
p0 = p1 /\ exists j, j < k /\ algo_metric j A0 A1 /\ algo_metric j B0 B1.
|
||||||
|
|
@ -972,16 +959,6 @@ Lemma T_Univ_Raise n Γ (a : PTm n) i j :
|
||||||
Γ ⊢ a ∈ PUniv j.
|
Γ ⊢ a ∈ PUniv j.
|
||||||
Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
|
Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
|
||||||
|
|
||||||
Lemma Bind_Univ_Inv n Γ p (A : PTm n) B i :
|
|
||||||
Γ ⊢ PBind p A B ∈ PUniv i ->
|
|
||||||
Γ ⊢ A ∈ PUniv i /\ funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i.
|
|
||||||
Proof.
|
|
||||||
move /Bind_Inv.
|
|
||||||
move => [i0][hA][hB]h.
|
|
||||||
move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]].
|
|
||||||
sfirstorder use:T_Univ_Raise.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma Abs_Pi_Inv n Γ (a : PTm (S n)) A B :
|
Lemma Abs_Pi_Inv n Γ (a : PTm (S n)) A B :
|
||||||
Γ ⊢ PAbs a ∈ PBind PPi A B ->
|
Γ ⊢ PAbs a ∈ PBind PPi A B ->
|
||||||
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B.
|
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B.
|
||||||
|
|
@ -1401,248 +1378,3 @@ with CoqLEq_R {n} : PTm n -> PTm n -> Prop :=
|
||||||
(* ----------------------- *)
|
(* ----------------------- *)
|
||||||
a ≪ b
|
a ≪ b
|
||||||
where "a ≪ b" := (CoqLEq_R a b) and "a ⋖ b" := (CoqLEq a b).
|
where "a ≪ b" := (CoqLEq_R a b) and "a ⋖ b" := (CoqLEq a b).
|
||||||
|
|
||||||
Scheme coqleq_ind := Induction for CoqLEq Sort Prop
|
|
||||||
with coqleq_r_ind := Induction for CoqLEq_R Sort Prop.
|
|
||||||
|
|
||||||
Combined Scheme coqleq_mutual from coqleq_ind, coqleq_r_ind.
|
|
||||||
|
|
||||||
Definition salgo_metric {n} k (a b : PTm n) :=
|
|
||||||
exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ ESub.R va vb /\ size_PTm va + size_PTm vb + i + j <= k.
|
|
||||||
|
|
||||||
Lemma salgo_metric_algo_metric n k (a b : PTm n) :
|
|
||||||
ishne a \/ ishne b ->
|
|
||||||
salgo_metric k a b ->
|
|
||||||
algo_metric k a b.
|
|
||||||
Proof.
|
|
||||||
move => h.
|
|
||||||
move => [i][j][va][vb][hva][hvb][nva][nvb][hS]sz.
|
|
||||||
rewrite/ESub.R in hS.
|
|
||||||
move : hS => [va'][vb'][h0][h1]h2.
|
|
||||||
suff : va' = vb' by sauto lq:on.
|
|
||||||
have {}hva : rtc RERed.R a va by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds.
|
|
||||||
have {}hvb : rtc RERed.R b vb by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds.
|
|
||||||
apply REReds.FromEReds in h0, h1.
|
|
||||||
have : ishne va' \/ ishne vb' by
|
|
||||||
hauto lq:on rew:off use:@relations.rtc_transitive, REReds.hne_preservation.
|
|
||||||
hauto lq:on use:Sub1.hne_refl.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma coqleq_sound_mutual : forall n,
|
|
||||||
(forall (a b : PTm n), a ⋖ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ) /\
|
|
||||||
(forall (a b : PTm n), a ≪ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ).
|
|
||||||
Proof.
|
|
||||||
apply coqleq_mutual.
|
|
||||||
- hauto lq:on use:wff_mutual ctrs:LEq.
|
|
||||||
- move => n A0 A1 B0 B1 hA ihA hB ihB Γ i.
|
|
||||||
move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1.
|
|
||||||
have hlA : Γ ⊢ A1 ≲ A0 by sfirstorder.
|
|
||||||
have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
|
|
||||||
apply Su_Transitive with (B := PBind PPi A1 B0).
|
|
||||||
by apply : Su_Pi; eauto using E_Refl, Su_Eq.
|
|
||||||
apply : Su_Pi; eauto using E_Refl, Su_Eq.
|
|
||||||
apply : ihB; eauto using ctx_eq_subst_one.
|
|
||||||
- move => n A0 A1 B0 B1 hA ihA hB ihB Γ i.
|
|
||||||
move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1.
|
|
||||||
have hlA : Γ ⊢ A0 ≲ A1 by sfirstorder.
|
|
||||||
have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
|
|
||||||
apply Su_Transitive with (B := PBind PSig A0 B1).
|
|
||||||
apply : Su_Sig; eauto using E_Refl, Su_Eq.
|
|
||||||
apply : ihB; by eauto using ctx_eq_subst_one.
|
|
||||||
apply : Su_Sig; eauto using E_Refl, Su_Eq.
|
|
||||||
- sauto lq:on use:coqeq_sound_mutual, Su_Eq.
|
|
||||||
- move => n a a' b b' ? ? ? ih Γ i ha hb.
|
|
||||||
have /Su_Eq ? : Γ ⊢ a ≡ a' ∈ PUniv i by sfirstorder use:HReds.ToEq.
|
|
||||||
have /E_Symmetric /Su_Eq ? : Γ ⊢ b ≡ b' ∈ PUniv i by sfirstorder use:HReds.ToEq.
|
|
||||||
suff : Γ ⊢ a' ≲ b' by eauto using Su_Transitive.
|
|
||||||
eauto using HReds.preservation.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma salgo_metric_case n k (a b : PTm n) :
|
|
||||||
salgo_metric k a b ->
|
|
||||||
(ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ salgo_metric k' a' b /\ k' < k.
|
|
||||||
Proof.
|
|
||||||
move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6.
|
|
||||||
case : a h0 => //=; try firstorder.
|
|
||||||
- inversion h0 as [|A B C D E F]; subst.
|
|
||||||
hauto qb:on use:ne_hne.
|
|
||||||
inversion E; subst => /=.
|
|
||||||
+ hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia.
|
|
||||||
+ hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
|
|
||||||
+ sfirstorder qb:on use:ne_hne.
|
|
||||||
- inversion h0 as [|A B C D E F]; subst.
|
|
||||||
hauto qb:on use:ne_hne.
|
|
||||||
inversion E; subst => /=.
|
|
||||||
+ hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
|
|
||||||
+ hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma CLE_HRedL n (a a' b : PTm n) :
|
|
||||||
HRed.R a a' ->
|
|
||||||
a' ≪ b ->
|
|
||||||
a ≪ b.
|
|
||||||
Proof.
|
|
||||||
hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma CLE_HRedR n (a a' b : PTm n) :
|
|
||||||
HRed.R a a' ->
|
|
||||||
b ≪ a' ->
|
|
||||||
b ≪ a.
|
|
||||||
Proof.
|
|
||||||
hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma algo_metric_caseR n k (a b : PTm n) :
|
|
||||||
salgo_metric k a b ->
|
|
||||||
(ishf b \/ ishne b) \/ exists k' b', HRed.R b b' /\ salgo_metric k' a b' /\ k' < k.
|
|
||||||
Proof.
|
|
||||||
move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6.
|
|
||||||
case : b h1 => //=; try by firstorder.
|
|
||||||
- inversion 1 as [|A B C D E F]; subst.
|
|
||||||
hauto qb:on use:ne_hne.
|
|
||||||
inversion E; subst => /=.
|
|
||||||
+ hauto q:on use:HRed.AppAbs unfold:salgo_metric solve+:lia.
|
|
||||||
+ hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:salgo_metric solve+:lia.
|
|
||||||
+ sfirstorder qb:on use:ne_hne.
|
|
||||||
- inversion 1 as [|A B C D E F]; subst.
|
|
||||||
hauto qb:on use:ne_hne.
|
|
||||||
inversion E; subst => /=.
|
|
||||||
+ hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
|
|
||||||
+ hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma salgo_metric_sub n k (a b : PTm n) :
|
|
||||||
salgo_metric k a b ->
|
|
||||||
Sub.R a b.
|
|
||||||
Proof.
|
|
||||||
rewrite /algo_metric.
|
|
||||||
move => [i][j][va][vb][h0][h1][h2][h3][[va' [vb' [hva [hvb hS]]]]]h5.
|
|
||||||
have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps.
|
|
||||||
have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps.
|
|
||||||
apply REReds.FromEReds in hva,hvb.
|
|
||||||
apply LoReds.ToRReds in h0,h1.
|
|
||||||
apply REReds.FromRReds in h0,h1.
|
|
||||||
rewrite /Sub.R. exists va', vb'. sfirstorder use:@relations.rtc_transitive.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma salgo_metric_pi n k (A0 : PTm n) B0 A1 B1 :
|
|
||||||
salgo_metric k (PBind PPi A0 B0) (PBind PPi A1 B1) ->
|
|
||||||
exists j, j < k /\ salgo_metric j A1 A0 /\ salgo_metric j B0 B1.
|
|
||||||
Proof.
|
|
||||||
move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
|
|
||||||
move : lored_nsteps_bind_inv h0 => /[apply].
|
|
||||||
move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
|
|
||||||
move : lored_nsteps_bind_inv h1 => /[apply].
|
|
||||||
move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
|
|
||||||
move /ESub.pi_inj : h4 => [? ?].
|
|
||||||
hauto qb:on solve+:lia.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma salgo_metric_sig n k (A0 : PTm n) B0 A1 B1 :
|
|
||||||
salgo_metric k (PBind PSig A0 B0) (PBind PSig A1 B1) ->
|
|
||||||
exists j, j < k /\ salgo_metric j A0 A1 /\ salgo_metric j B0 B1.
|
|
||||||
Proof.
|
|
||||||
move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
|
|
||||||
move : lored_nsteps_bind_inv h0 => /[apply].
|
|
||||||
move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
|
|
||||||
move : lored_nsteps_bind_inv h1 => /[apply].
|
|
||||||
move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
|
|
||||||
move /ESub.sig_inj : h4 => [? ?].
|
|
||||||
hauto qb:on solve+:lia.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma coqleq_complete' n k (a b : PTm n) :
|
|
||||||
salgo_metric k a b -> (forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b).
|
|
||||||
Proof.
|
|
||||||
move : k n a b.
|
|
||||||
elim /Wf_nat.lt_wf_ind.
|
|
||||||
move => n ih.
|
|
||||||
move => k a b /[dup] h /salgo_metric_case.
|
|
||||||
(* Cases where a and b can take steps *)
|
|
||||||
case; cycle 1.
|
|
||||||
move : k a b h.
|
|
||||||
qauto l:on use:HRed.preservation, CLE_HRedL, hred_hne.
|
|
||||||
case /algo_metric_caseR : (h); cycle 1.
|
|
||||||
qauto l:on use:HRed.preservation, CLE_HRedR, hred_hne.
|
|
||||||
(* Cases where neither a nor b can take steps *)
|
|
||||||
case => fb; case => fa.
|
|
||||||
- case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
|
|
||||||
+ case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
|
|
||||||
* move => p0 A0 B0 _ p1 A1 B1 _.
|
|
||||||
move => h.
|
|
||||||
have ? : p1 = p0 by
|
|
||||||
hauto lq:on rew:off use:salgo_metric_sub, Sub.bind_inj.
|
|
||||||
subst.
|
|
||||||
case : p0 h => //=.
|
|
||||||
** move /salgo_metric_pi.
|
|
||||||
move => [j [hj [hA hB]]] Γ i.
|
|
||||||
move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
|
|
||||||
have ihA : A0 ≪ A1 by hauto l:on.
|
|
||||||
econstructor; eauto using E_Refl; constructor=> //.
|
|
||||||
have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual.
|
|
||||||
suff : funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B1 ∈ PUniv i
|
|
||||||
by hauto l:on.
|
|
||||||
eauto using ctx_eq_subst_one.
|
|
||||||
** move /salgo_metric_sig.
|
|
||||||
move => [j [hj [hA hB]]] Γ i.
|
|
||||||
move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
|
|
||||||
have ihA : A1 ≪ A0 by hauto l:on.
|
|
||||||
econstructor; eauto using E_Refl; constructor=> //.
|
|
||||||
have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual.
|
|
||||||
suff : funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ∈ PUniv i
|
|
||||||
by hauto l:on.
|
|
||||||
eauto using ctx_eq_subst_one.
|
|
||||||
* hauto lq:on use:salgo_metric_sub, Sub.bind_univ_noconf.
|
|
||||||
+ case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
|
|
||||||
* hauto lq:on use:salgo_metric_sub, Sub.univ_bind_noconf.
|
|
||||||
* move => *. econstructor; eauto using rtc_refl.
|
|
||||||
hauto lq:on use:salgo_metric_sub, Sub.univ_inj, CLE_UnivCong.
|
|
||||||
(* Both cases are impossible *)
|
|
||||||
- have {}h : DJoin.R a b by
|
|
||||||
hauto lq:on use:salgo_metric_algo_metric, algo_metric_join.
|
|
||||||
case : b fb h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
|
|
||||||
+ hauto lq:on use:DJoin.hne_bind_noconf.
|
|
||||||
+ hauto lq:on use:DJoin.hne_univ_noconf.
|
|
||||||
- have {}h : DJoin.R b a by
|
|
||||||
hauto lq:on use:salgo_metric_algo_metric, algo_metric_join, DJoin.symmetric.
|
|
||||||
case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
|
|
||||||
+ hauto lq:on use:DJoin.hne_bind_noconf.
|
|
||||||
+ hauto lq:on use:DJoin.hne_univ_noconf.
|
|
||||||
- move => Γ i ha hb.
|
|
||||||
econstructor; eauto using rtc_refl.
|
|
||||||
apply CLE_NeuNeu. move {ih}.
|
|
||||||
have {}h : algo_metric n a b by
|
|
||||||
hauto lq:on use:salgo_metric_algo_metric.
|
|
||||||
eapply coqeq_complete'; eauto.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma coqleq_complete n Γ (a b : PTm n) :
|
|
||||||
Γ ⊢ a ≲ b -> a ≪ b.
|
|
||||||
Proof.
|
|
||||||
move => h.
|
|
||||||
suff : exists k, salgo_metric k a b by hauto lq:on use:coqleq_complete', regularity.
|
|
||||||
eapply fundamental_theorem in h.
|
|
||||||
move /logrel.SemLEq_SN_Sub : h.
|
|
||||||
move => h.
|
|
||||||
have : exists va vb : PTm n,
|
|
||||||
rtc LoRed.R a va /\
|
|
||||||
rtc LoRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb
|
|
||||||
by hauto l:on use:Sub.standardization_lo.
|
|
||||||
move => [va][vb][hva][hvb][nva][nvb]hj.
|
|
||||||
move /relations.rtc_nsteps : hva => [i hva].
|
|
||||||
move /relations.rtc_nsteps : hvb => [j hvb].
|
|
||||||
exists (i + j + size_PTm va + size_PTm vb).
|
|
||||||
hauto lq:on solve+:lia.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma coqleq_sound : forall n Γ (a b : PTm n) i j,
|
|
||||||
Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv j -> a ≪ b -> Γ ⊢ a ≲ b.
|
|
||||||
Proof.
|
|
||||||
move => n Γ a b i j.
|
|
||||||
have [*] : i <= i + j /\ j <= i + j by lia.
|
|
||||||
have : Γ ⊢ a ∈ PUniv (i + j) /\ Γ ⊢ b ∈ PUniv (i + j)
|
|
||||||
by sfirstorder use:T_Univ_Raise.
|
|
||||||
sfirstorder use:coqleq_sound_mutual.
|
|
||||||
Qed.
|
|
||||||
|
|
|
||||||
|
|
@ -2337,17 +2337,6 @@ Module DJoin.
|
||||||
case : c => //=.
|
case : c => //=.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma hne_bind_noconf n (a b : PTm n) :
|
|
||||||
R a b -> ishne a -> isbind b -> False.
|
|
||||||
Proof.
|
|
||||||
move => [c [h0 h1]] h2 h3.
|
|
||||||
have {h0 h1 h2 h3} : ishne c /\ isbind c by
|
|
||||||
hauto l:on use:REReds.hne_preservation,
|
|
||||||
REReds.bind_preservation.
|
|
||||||
move => [].
|
|
||||||
case : c => //=.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
|
Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
|
||||||
DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
|
DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
|
||||||
p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
|
p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
|
||||||
|
|
@ -2631,53 +2620,14 @@ Module Sub1.
|
||||||
R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
|
R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
|
||||||
Proof. move => h. move : m ρ. elim : n a b /h; hauto lq:on ctrs:R. Qed.
|
Proof. move => h. move : m ρ. elim : n a b /h; hauto lq:on ctrs:R. Qed.
|
||||||
|
|
||||||
Lemma hne_refl n (a b : PTm n) :
|
|
||||||
ishne a \/ ishne b -> R a b -> a = b.
|
|
||||||
Proof. hauto q:on inv:R. Qed.
|
|
||||||
|
|
||||||
End Sub1.
|
End Sub1.
|
||||||
|
|
||||||
Module ESub.
|
|
||||||
Definition R {n} (a b : PTm n) := exists c0 c1, rtc ERed.R a c0 /\ rtc ERed.R b c1 /\ Sub1.R c0 c1.
|
|
||||||
|
|
||||||
Lemma pi_inj n (A0 A1 : PTm n) B0 B1 :
|
|
||||||
R (PBind PPi A0 B0) (PBind PPi A1 B1) ->
|
|
||||||
R A1 A0 /\ R B0 B1.
|
|
||||||
Proof.
|
|
||||||
move => [u0 [u1 [h0 [h1 h2]]]].
|
|
||||||
move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst.
|
|
||||||
move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst.
|
|
||||||
sauto lq:on rew:off inv:Sub1.R.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma sig_inj n (A0 A1 : PTm n) B0 B1 :
|
|
||||||
R (PBind PSig A0 B0) (PBind PSig A1 B1) ->
|
|
||||||
R A0 A1 /\ R B0 B1.
|
|
||||||
Proof.
|
|
||||||
move => [u0 [u1 [h0 [h1 h2]]]].
|
|
||||||
move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst.
|
|
||||||
move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst.
|
|
||||||
sauto lq:on rew:off inv:Sub1.R.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
End ESub.
|
|
||||||
|
|
||||||
Module Sub.
|
Module Sub.
|
||||||
Definition R {n} (a b : PTm n) := exists c d, rtc RERed.R a c /\ rtc RERed.R b d /\ Sub1.R c d.
|
Definition R {n} (a b : PTm n) := exists c d, rtc RERed.R a c /\ rtc RERed.R b d /\ Sub1.R c d.
|
||||||
|
|
||||||
Lemma refl n (a : PTm n) : R a a.
|
Lemma refl n (a : PTm n) : R a a.
|
||||||
Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
|
Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
|
||||||
|
|
||||||
Lemma ToJoin n (a b : PTm n) :
|
|
||||||
ishne a \/ ishne b ->
|
|
||||||
R a b ->
|
|
||||||
DJoin.R a b.
|
|
||||||
Proof.
|
|
||||||
move => h [c][d][h0][h1]h2.
|
|
||||||
have : ishne c \/ ishne d by hauto q:on use:REReds.hne_preservation.
|
|
||||||
hauto lq:on rew:off use:Sub1.hne_refl.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c.
|
Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c.
|
||||||
Proof.
|
Proof.
|
||||||
rewrite /R.
|
rewrite /R.
|
||||||
|
|
@ -2829,41 +2779,4 @@ Module Sub.
|
||||||
move => [a0][b0][h0][h1]h2.
|
move => [a0][b0][h0][h1]h2.
|
||||||
hauto ctrs:rtc use:REReds.cong', Sub1.substing.
|
hauto ctrs:rtc use:REReds.cong', Sub1.substing.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma ToESub n (a b : PTm n) : nf a -> nf b -> R a b -> ESub.R a b.
|
|
||||||
Proof. hauto q:on use:REReds.ToEReds. Qed.
|
|
||||||
|
|
||||||
Lemma standardization n (a b : PTm n) :
|
|
||||||
SN a -> SN b -> R a b ->
|
|
||||||
exists va vb, rtc RRed.R a va /\ rtc RRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb.
|
|
||||||
Proof.
|
|
||||||
move => h0 h1 hS.
|
|
||||||
have : exists v, rtc RRed.R a v /\ nf v by sfirstorder use:LoReds.FromSN, LoReds.ToRReds.
|
|
||||||
move => [v [hv2 hv3]].
|
|
||||||
have : exists v, rtc RRed.R b v /\ nf v by sfirstorder use:LoReds.FromSN, LoReds.ToRReds.
|
|
||||||
move => [v' [hv2' hv3']].
|
|
||||||
move : (hv2) (hv2') => *.
|
|
||||||
apply DJoin.FromRReds in hv2, hv2'.
|
|
||||||
move/DJoin.symmetric in hv2'.
|
|
||||||
apply FromJoin in hv2, hv2'.
|
|
||||||
have hv : R v v' by eauto using transitive.
|
|
||||||
have {}hv : ESub.R v v' by hauto l:on use:ToESub.
|
|
||||||
hauto lq:on.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma standardization_lo n (a b : PTm n) :
|
|
||||||
SN a -> SN b -> R a b ->
|
|
||||||
exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb.
|
|
||||||
Proof.
|
|
||||||
move => /[dup] sna + /[dup] snb.
|
|
||||||
move : standardization; repeat move/[apply].
|
|
||||||
move => [va][vb][hva][hvb][nfva][nfvb]hj.
|
|
||||||
move /LoReds.FromSN : sna => [va' [hva' hva'0]].
|
|
||||||
move /LoReds.FromSN : snb => [vb' [hvb' hvb'0]].
|
|
||||||
exists va', vb'.
|
|
||||||
repeat split => //=.
|
|
||||||
have : va = va' /\ vb = vb' by sfirstorder use:red_uniquenf, LoReds.ToRReds.
|
|
||||||
case; congruence.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
End Sub.
|
End Sub.
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue