Use hne and hf instead HRed.nf
This commit is contained in:
parent
30caf75002
commit
d1771adc48
4 changed files with 655 additions and 482 deletions
|
|
@ -1302,6 +1302,17 @@ Proof.
|
||||||
hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
|
hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Lemma ce_neu_neu_helper a b :
|
||||||
|
ishne a -> ishne b ->
|
||||||
|
(forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C).
|
||||||
|
Proof. sauto lq:on. Qed.
|
||||||
|
|
||||||
|
Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 :
|
||||||
|
ishne u0 -> ishne u1 ->
|
||||||
|
DJoin.R (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) ->
|
||||||
|
DJoin.R P0 P1 /\ DJoin.R u0 u1 /\ DJoin.R b0 b1 /\ DJoin.R c0 c1.
|
||||||
|
Proof. hauto q:on use:REReds.hne_ind_inv. Qed.
|
||||||
|
|
||||||
Lemma coqeq_complete' :
|
Lemma coqeq_complete' :
|
||||||
(forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)) /\
|
(forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)) /\
|
||||||
(forall a b, algo_dom_r a b -> DJoin.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b).
|
(forall a b, algo_dom_r a b -> DJoin.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b).
|
||||||
|
|
@ -1341,310 +1352,34 @@ Lemma coqeq_complete' :
|
||||||
move => Γ A /Suc_Inv ? /Suc_Inv ?. apply CE_Nf. hauto lq:on ctrs:CoqEq.
|
move => Γ A /Suc_Inv ? /Suc_Inv ?. apply CE_Nf. hauto lq:on ctrs:CoqEq.
|
||||||
- move => i j /DJoin.univ_inj ?. subst.
|
- move => i j /DJoin.univ_inj ?. subst.
|
||||||
split => //. hauto l:on.
|
split => //. hauto l:on.
|
||||||
- move => p0 p1 A0 A1 B0 B1.
|
- move => {hhPairNeu hhAbsNeu} p0 p1 A0 A1 B0 B1.
|
||||||
|
move => hA ihA hB ihB /DJoin.bind_inj. move => [?][hjA]hjB. subst.
|
||||||
|
split => // Γ A.
|
||||||
algo_metric k a b ->
|
move => hbd0 hbd1.
|
||||||
(forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\
|
have {hbd0} : exists i, Γ ⊢ PBind p1 A0 B0 ∈ PUniv i by move /Bind_Inv in hbd0; qauto use:T_Bind.
|
||||||
(forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C).
|
move => [i] => hbd0.
|
||||||
Proof.
|
have {hbd1} : exists i, Γ ⊢ PBind p1 A1 B1 ∈ PUniv i by move /Bind_Inv in hbd1; qauto use:T_Bind.
|
||||||
move : k a b.
|
move => [j] => hbd1.
|
||||||
elim /Wf_nat.lt_wf_ind.
|
have /Bind_Univ_Inv {hbd0} [? ?] : Γ ⊢ PBind p1 A0 B0 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
|
||||||
move => n ih.
|
have /Bind_Univ_Inv {hbd1} [? ?] : Γ ⊢ PBind p1 A1 B1 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
|
||||||
move => a b /[dup] h /algo_metric_case. move : a b h => [:hstepL].
|
move => [:eqa].
|
||||||
move => a b h.
|
apply CE_Nf. constructor; first by abstract : eqa; eauto.
|
||||||
(* Cases where a and b can take steps *)
|
eapply ihB; eauto. apply : ctx_eq_subst_one; eauto.
|
||||||
case; cycle 1.
|
apply : Su_Eq; eauto. sfirstorder use:coqeq_sound_mutual.
|
||||||
move : ih a b h.
|
- hauto l:on.
|
||||||
abstract : hstepL. qauto l:on use:HRed.preservation, CE_HRedL, hred_hne.
|
- move => {hhAbsNeu hhPairNeu} i j /DJoin.var_inj ?. subst. apply ce_neu_neu_helper => // Γ A B.
|
||||||
move /algo_metric_sym /algo_metric_case : (h).
|
move /Var_Inv => [h [A0 [h0 h1]]].
|
||||||
case; cycle 1.
|
move /Var_Inv => [h' [A1 [h0' h1']]].
|
||||||
move /algo_metric_sym : h.
|
split. by constructor.
|
||||||
move : hstepL ih => /[apply]/[apply].
|
suff : A0 = A1 by hauto lq:on db:wt.
|
||||||
repeat move /[apply].
|
eauto using lookup_deter.
|
||||||
move => hstepL.
|
- move => u0 u1 a0 a1 neu0 neu1 domu ihu doma iha. move /DJoin.hne_app_inj /(_ neu0 neu1) => [hju hja].
|
||||||
hauto lq:on use:coqeq_symmetric_mutual, algo_metric_sym.
|
apply ce_neu_neu_helper => //= Γ A B.
|
||||||
(* Cases where a and b can't take wh steps *)
|
move /App_Inv => [A0][B0][hb0][ha0]hS0.
|
||||||
move {hstepL}.
|
move /App_Inv => [A1][B1][hb1][ha1]hS1.
|
||||||
move : a b h. move => [:hnfneu].
|
move /(_ hju) : ihu.
|
||||||
move => a b h.
|
|
||||||
case => fb; case => fa.
|
|
||||||
- split; last by sfirstorder use:hf_not_hne.
|
|
||||||
move {hnfneu}.
|
|
||||||
case : a h fb fa => //=.
|
|
||||||
+ case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_AbsBind_Imp, T_AbsUniv_Imp, T_AbsZero_Imp, T_AbsSuc_Imp, T_AbsNat_Imp.
|
|
||||||
move => a0 a1 ha0 _ _ Γ A wt0 wt1.
|
|
||||||
move : T_Abs_Inv wt0 wt1; repeat move/[apply]. move => [Δ [V [wt1 wt0]]].
|
|
||||||
apply : CE_HRed; eauto using rtc_refl.
|
|
||||||
apply CE_AbsAbs.
|
|
||||||
suff [l [h0 h1]] : exists l, l < n /\ algo_metric l a1 a0 by eapply ih; eauto.
|
|
||||||
have ? : n > 0 by sauto solve+:lia.
|
|
||||||
exists (n - 1). split; first by lia.
|
|
||||||
move : (ha0). rewrite /algo_metric.
|
|
||||||
move => [i][j][va][vb][hr0][hr1][nfva][nfvb][[v [hr0' hr1']]] har.
|
|
||||||
apply lored_nsteps_abs_inv in hr0, hr1.
|
|
||||||
move : hr0 => [va' [hr00 hr01]].
|
|
||||||
move : hr1 => [vb' [hr10 hr11]]. move {ih}.
|
|
||||||
exists i,j,va',vb'. subst.
|
|
||||||
suff [v0 [hv00 hv01]] : exists v0, rtc ERed.R va' v0 /\ rtc ERed.R vb' v0.
|
|
||||||
repeat split =>//=. sfirstorder.
|
|
||||||
simpl in *; by lia.
|
|
||||||
move /algo_metric_join /DJoin.symmetric : ha0.
|
|
||||||
have : SN a0 /\ SN a1 by qauto l:on use:fundamental_theorem, logrel.SemWt_SN.
|
|
||||||
move => /[dup] [[ha00 ha10]] [].
|
|
||||||
move : DJoin.abs_inj; repeat move/[apply].
|
|
||||||
move : DJoin.standardization ha00 ha10; repeat move/[apply].
|
|
||||||
(* this is awful *)
|
|
||||||
move => [vb][va][h' [h'' [h''' [h'''' h'''''']]]].
|
|
||||||
have /LoReds.ToRReds {}hr00 : rtc LoRed.R a1 va'
|
|
||||||
by hauto lq:on use:@relations.rtc_nsteps.
|
|
||||||
have /LoReds.ToRReds {}hr10 : rtc LoRed.R a0 vb'
|
|
||||||
by hauto lq:on use:@relations.rtc_nsteps.
|
|
||||||
simpl in *.
|
|
||||||
have [*] : va' = va /\ vb' = vb by eauto using red_uniquenf. subst.
|
|
||||||
sfirstorder.
|
|
||||||
+ case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_PairBind_Imp, T_PairUniv_Imp, T_PairNat_Imp, T_PairSuc_Imp, T_PairZero_Imp.
|
|
||||||
move => a1 b1 a0 b0 h _ _ Γ A hu0 hu1.
|
|
||||||
have [sn0 sn1] : SN (PPair a0 b0) /\ SN (PPair a1 b1)
|
|
||||||
by qauto l:on use:fundamental_theorem, logrel.SemWt_SN.
|
|
||||||
apply : CE_HRed; eauto using rtc_refl.
|
|
||||||
move /Pair_Inv : hu0 => [A0][B0][ha0][hb0]hSu0.
|
|
||||||
move /Pair_Inv : hu1 => [A1][B1][ha1][hb1]hSu1.
|
|
||||||
move /Sub_Bind_InvR : (hSu0).
|
|
||||||
move => [i][A2][B2]hE.
|
|
||||||
have hSu12 : Γ ⊢ PBind PSig A1 B1 ≲ PBind PSig A2 B2
|
|
||||||
by eauto using Su_Transitive, Su_Eq.
|
|
||||||
have hSu02 : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2
|
|
||||||
by eauto using Su_Transitive, Su_Eq.
|
|
||||||
have hA02 : Γ ⊢ A0 ≲ A2 by eauto using Su_Sig_Proj1.
|
|
||||||
have hA12 : Γ ⊢ A1 ≲ A2 by eauto using Su_Sig_Proj1.
|
|
||||||
have ha0A2 : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
|
|
||||||
have ha1A2 : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
|
|
||||||
move /algo_metric_pair : h sn0 sn1; repeat move/[apply].
|
|
||||||
move => [j][hj][ih0 ih1].
|
|
||||||
have haE : a0 ⇔ a1 by hauto l:on.
|
|
||||||
apply CE_PairPair => //.
|
|
||||||
have {}haE : Γ ⊢ a0 ≡ a1 ∈ A2
|
|
||||||
by hauto l:on use:coqeq_sound_mutual.
|
|
||||||
have {}hb1 : Γ ⊢ b1 ∈ subst_PTm (scons a1 VarPTm) B2.
|
|
||||||
apply : T_Conv; eauto.
|
|
||||||
move /E_Refl in ha1. hauto l:on use:Su_Sig_Proj2.
|
|
||||||
eapply ih; cycle -1; eauto.
|
|
||||||
apply : T_Conv; eauto.
|
|
||||||
apply Su_Transitive with (B := subst_PTm (scons a0 VarPTm) B2).
|
|
||||||
move /E_Refl in ha0. hauto l:on use:Su_Sig_Proj2.
|
|
||||||
move : hE haE. clear.
|
|
||||||
move => h.
|
|
||||||
eapply regularity in h.
|
|
||||||
move : h => [_ [hB _]].
|
|
||||||
eauto using bind_inst.
|
|
||||||
+ case : b => //=.
|
|
||||||
* hauto lq:on use:T_AbsBind_Imp.
|
|
||||||
* hauto lq:on rew:off use:T_PairBind_Imp.
|
|
||||||
* move => p1 A1 B1 p0 A0 B0.
|
|
||||||
move /algo_metric_bind.
|
|
||||||
move => [?][j [ih0 [ih1 ih2]]]_ _. subst.
|
|
||||||
move => Γ A hU0 hU1.
|
|
||||||
move /Bind_Inv : hU0 => [i0 [hA0 [hB0 hS0]]].
|
|
||||||
move /Bind_Inv : hU1 => [i1 [hA1 [hB1 hS1]]].
|
|
||||||
have ? : Γ ⊢ PUniv i0 ≲ PUniv (max i0 i1)
|
|
||||||
by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
|
|
||||||
have ? : Γ ⊢ PUniv i1 ≲ PUniv (max i0 i1)
|
|
||||||
by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
|
|
||||||
have {}hA0 : Γ ⊢ A0 ∈ PUniv (max i0 i1) by eauto using T_Conv.
|
|
||||||
have {}hA1 : Γ ⊢ A1 ∈ PUniv (max i0 i1) by eauto using T_Conv.
|
|
||||||
have {}hB0 : (cons A0 Γ) ⊢ B0 ∈ PUniv (max i0 i1)
|
|
||||||
by hauto lq:on use:T_Univ_Raise solve+:lia.
|
|
||||||
have {}hB1 : (cons A1 Γ) ⊢ B1 ∈ PUniv (max i0 i1)
|
|
||||||
by hauto lq:on use:T_Univ_Raise solve+:lia.
|
|
||||||
|
|
||||||
have ihA : A0 ⇔ A1 by hauto l:on.
|
|
||||||
have hAE : Γ ⊢ A0 ≡ A1 ∈ PUniv (Nat.max i0 i1)
|
|
||||||
by hauto l:on use:coqeq_sound_mutual.
|
|
||||||
apply : CE_HRed; eauto using rtc_refl.
|
|
||||||
constructor => //.
|
|
||||||
|
|
||||||
eapply ih; eauto.
|
|
||||||
apply : ctx_eq_subst_one; eauto.
|
|
||||||
eauto using Su_Eq.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on use:DJoin.bind_univ_noconf.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on use:Sub.nat_bind_noconf, Sub.FromJoin.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
clear. hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv.
|
|
||||||
* move => > /algo_metric_join. clear.
|
|
||||||
hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv.
|
|
||||||
+ case : b => //=.
|
|
||||||
* hauto lq:on use:T_AbsUniv_Imp.
|
|
||||||
* hauto lq:on use:T_PairUniv_Imp.
|
|
||||||
* qauto l:on use:algo_metric_join, DJoin.bind_univ_noconf, DJoin.symmetric.
|
|
||||||
* move => i j /algo_metric_join /DJoin.univ_inj ? _ _ Γ A hi hj.
|
|
||||||
subst.
|
|
||||||
hauto l:on.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on use:Sub.nat_univ_noconf, Sub.FromJoin.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.suc_inv.
|
|
||||||
+ case : b => //=.
|
|
||||||
* qauto l:on use:T_AbsNat_Imp.
|
|
||||||
* qauto l:on use:T_PairNat_Imp.
|
|
||||||
* move => > /algo_metric_join /Sub.FromJoin. hauto l:on use:Sub.bind_nat_noconf.
|
|
||||||
* move => > /algo_metric_join /Sub.FromJoin. hauto lq:on use:Sub.univ_nat_noconf.
|
|
||||||
* hauto l:on.
|
|
||||||
* move /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv.
|
|
||||||
(* Zero *)
|
|
||||||
+ case : b => //=.
|
|
||||||
* hauto lq:on rew:off use:T_AbsZero_Imp.
|
|
||||||
* hauto lq: on use: T_PairZero_Imp.
|
|
||||||
* move =>> /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.zero_inv, REReds.bind_inv.
|
|
||||||
* move =>> /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv.
|
|
||||||
* move =>> /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv.
|
|
||||||
* hauto l:on.
|
|
||||||
* move =>> /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv.
|
|
||||||
(* Suc *)
|
|
||||||
+ case : b => //=.
|
|
||||||
* hauto lq:on rew:off use:T_AbsSuc_Imp.
|
|
||||||
* hauto lq:on use:T_PairSuc_Imp.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv.
|
|
||||||
* move => > /algo_metric_join.
|
|
||||||
hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv.
|
|
||||||
* move => a0 a1 h _ _.
|
|
||||||
move /algo_metric_suc : h => [j [h4 h5]].
|
|
||||||
move => Γ A /Suc_Inv [h0 h1] /Suc_Inv [h2 h3].
|
|
||||||
move : ih h4 h5;do!move/[apply].
|
|
||||||
move => [ih _].
|
|
||||||
move : ih h0 h2;do!move/[apply].
|
|
||||||
move => h. apply : CE_HRed; eauto using rtc_refl.
|
|
||||||
by constructor.
|
|
||||||
- move : a b h fb fa. abstract : hnfneu.
|
|
||||||
move => + b.
|
|
||||||
case : b => //=.
|
|
||||||
(* NeuAbs *)
|
|
||||||
+ move => a u halg _ nea. split => // Γ A hu /[dup] ha.
|
|
||||||
move /Abs_Inv => [A0][B0][_]hSu.
|
|
||||||
move /Sub_Bind_InvR : (hSu) => [i][A2][B2]hE.
|
|
||||||
have {}hu : Γ ⊢ u ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
|
|
||||||
have {}ha : Γ ⊢ PAbs a ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
|
|
||||||
have {}hE : Γ ⊢ PBind PPi A2 B2 ∈ PUniv i
|
|
||||||
by hauto l:on use:regularity.
|
|
||||||
have {i} [j {}hE] : exists j, Γ ⊢ A2 ∈ PUniv j
|
|
||||||
by qauto l:on use:Bind_Inv.
|
|
||||||
have hΓ : ⊢ cons A2 Γ by eauto using Wff_Cons'.
|
|
||||||
set Δ := cons _ _ in hΓ.
|
|
||||||
have {}hu : Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ B2.
|
|
||||||
apply : T_App'; cycle 1. apply : weakening_wt' => //=; eauto.
|
|
||||||
reflexivity.
|
|
||||||
rewrite -/ren_PTm.
|
|
||||||
apply T_Var; eauto using here.
|
|
||||||
rewrite -/ren_PTm. by asimpl; rewrite subst_scons_id.
|
|
||||||
move /Abs_Pi_Inv in ha.
|
|
||||||
move /algo_metric_neu_abs /(_ nea) : halg.
|
|
||||||
move => [j0][hj0]halg.
|
|
||||||
apply : CE_HRed; eauto using rtc_refl.
|
|
||||||
eapply CE_NeuAbs => //=.
|
|
||||||
eapply ih; eauto.
|
|
||||||
(* NeuPair *)
|
|
||||||
+ move => a0 b0 u halg _ neu.
|
|
||||||
split => // Γ A hu /[dup] wt.
|
|
||||||
move /Pair_Inv => [A0][B0][ha0][hb0]hU.
|
|
||||||
move /Sub_Bind_InvR : (hU) => [i][A2][B2]hE.
|
|
||||||
have {}wt : Γ ⊢ PPair a0 b0 ∈ PBind PSig A2 B2 by sauto lq:on.
|
|
||||||
have {}hu : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
|
|
||||||
move /Pair_Sig_Inv : wt => [{}ha0 {}hb0].
|
|
||||||
have /T_Proj1 huL := hu.
|
|
||||||
have /T_Proj2 {hu} huR := hu.
|
|
||||||
move /algo_metric_neu_pair /(_ neu) : halg => [j [hj [hL hR]]].
|
|
||||||
have heL : PProj PL u ⇔ a0 by hauto l:on.
|
|
||||||
eapply CE_HRed; eauto using rtc_refl.
|
|
||||||
apply CE_NeuPair; eauto.
|
|
||||||
eapply ih; eauto.
|
|
||||||
apply : T_Conv; eauto.
|
|
||||||
have {}hE : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i
|
|
||||||
by hauto l:on use:regularity.
|
|
||||||
have /E_Symmetric : Γ ⊢ PProj PL u ≡ a0 ∈ A2 by
|
|
||||||
hauto l:on use:coqeq_sound_mutual.
|
|
||||||
hauto l:on use:bind_inst.
|
|
||||||
(* NeuBind: Impossible *)
|
|
||||||
+ move => b p p0 a /algo_metric_join h _ h0. exfalso.
|
|
||||||
move : h h0. clear.
|
|
||||||
move /Sub.FromJoin.
|
|
||||||
hauto l:on use:Sub.hne_bind_noconf.
|
|
||||||
(* NeuUniv: Impossible *)
|
|
||||||
+ hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join.
|
|
||||||
+ hauto lq:on rew:off use:DJoin.hne_nat_noconf, algo_metric_join.
|
|
||||||
(* Zero *)
|
|
||||||
+ case => //=.
|
|
||||||
* move => i /algo_metric_join. clear.
|
|
||||||
hauto lq:on rew:off use:REReds.var_inv, REReds.zero_inv.
|
|
||||||
* move => >/algo_metric_join. clear.
|
|
||||||
hauto lq:on rew:off use:REReds.hne_app_inv, REReds.zero_inv.
|
|
||||||
* move => >/algo_metric_join. clear.
|
|
||||||
hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.zero_inv.
|
|
||||||
* move => >/algo_metric_join. clear.
|
|
||||||
move => h _ h2. exfalso.
|
|
||||||
hauto q:on use:REReds.hne_ind_inv, REReds.zero_inv.
|
|
||||||
(* Suc *)
|
|
||||||
+ move => a0.
|
|
||||||
case => //=; move => >/algo_metric_join; clear.
|
|
||||||
* hauto lq:on rew:off use:REReds.var_inv, REReds.suc_inv.
|
|
||||||
* hauto lq:on rew:off use:REReds.hne_app_inv, REReds.suc_inv.
|
|
||||||
* hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.suc_inv.
|
|
||||||
* hauto q:on use:REReds.hne_ind_inv, REReds.suc_inv.
|
|
||||||
- move {ih}.
|
|
||||||
move /algo_metric_sym in h.
|
|
||||||
qauto l:on use:coqeq_symmetric_mutual.
|
|
||||||
- move {hnfneu}.
|
|
||||||
(* Clear out some trivial cases *)
|
|
||||||
suff : (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ (exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)).
|
|
||||||
move => h0.
|
|
||||||
split. move => *. apply : CE_HRed; eauto using rtc_refl. apply CE_NeuNeu. by firstorder.
|
|
||||||
by firstorder.
|
|
||||||
|
|
||||||
case : a h fb fa => //=.
|
|
||||||
+ case : b => //=; move => > /algo_metric_join.
|
|
||||||
* move /DJoin.var_inj => i _ _. subst.
|
|
||||||
move => Γ A B /Var_Inv [? [B0 [h0 h1]]].
|
|
||||||
move /Var_Inv => [_ [C0 [h2 h3]]].
|
|
||||||
have ? : B0 = C0 by eauto using lookup_deter. subst.
|
|
||||||
sfirstorder use:T_Var.
|
|
||||||
* clear => ? ? _. exfalso.
|
|
||||||
hauto l:on use:REReds.var_inv, REReds.hne_app_inv.
|
|
||||||
* clear => ? ? _. exfalso.
|
|
||||||
hauto l:on use:REReds.var_inv, REReds.hne_proj_inv.
|
|
||||||
* clear => ? ? _. exfalso.
|
|
||||||
hauto q:on use:REReds.var_inv, REReds.hne_ind_inv.
|
|
||||||
+ case : b => //=;
|
|
||||||
lazymatch goal with
|
|
||||||
| [|- context[algo_metric _ (PApp _ _) (PApp _ _)]] => idtac
|
|
||||||
| _ => move => > /algo_metric_join
|
|
||||||
end.
|
|
||||||
* clear => *. exfalso.
|
|
||||||
hauto lq:on rew:off use:REReds.hne_app_inv, REReds.var_inv.
|
|
||||||
(* real case *)
|
|
||||||
* move => b1 a1 b0 a0 halg hne1 hne0 Γ A B wtA wtB.
|
|
||||||
move /App_Inv : wtA => [A0][B0][hb0][ha0]hS0.
|
|
||||||
move /App_Inv : wtB => [A1][B1][hb1][ha1]hS1.
|
|
||||||
move : algo_metric_app (hne0) (hne1) halg. repeat move/[apply].
|
|
||||||
move => [j [hj [hal0 hal1]]].
|
|
||||||
have /ih := hal0.
|
|
||||||
move /(_ hj).
|
|
||||||
move => [_ ihb].
|
move => [_ ihb].
|
||||||
move : ihb (hne0) (hne1) hb0 hb1. repeat move/[apply].
|
move : ihb (neu0) (neu1) hb0 hb1. repeat move/[apply].
|
||||||
move => [hb01][C][hT0][hT1][hT2]hT3.
|
move => [hb01][C][hT0][hT1][hT2]hT3.
|
||||||
move /Sub_Bind_InvL : (hT0).
|
move /Sub_Bind_InvL : (hT0).
|
||||||
move => [i][A2][B2]hE.
|
move => [i][A2][B2]hE.
|
||||||
|
|
@ -1656,11 +1391,11 @@ Proof.
|
||||||
have hSuA1 : Γ ⊢ A1 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
|
have hSuA1 : Γ ⊢ A1 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
|
||||||
have ha1' : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
|
have ha1' : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
|
||||||
have ha0' : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
|
have ha0' : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
|
||||||
move : ih (hj) hal1. repeat move/[apply].
|
move : iha hja. repeat move/[apply].
|
||||||
move => [ih _].
|
|
||||||
move : ih (ha0') (ha1'); repeat move/[apply].
|
|
||||||
move => iha.
|
move => iha.
|
||||||
split. qblast.
|
move : iha (ha0') (ha1'); repeat move/[apply].
|
||||||
|
move => iha.
|
||||||
|
split. sauto lq:on.
|
||||||
exists (subst_PTm (scons a0 VarPTm) B2).
|
exists (subst_PTm (scons a0 VarPTm) B2).
|
||||||
split.
|
split.
|
||||||
apply : Su_Transitive; eauto.
|
apply : Su_Transitive; eauto.
|
||||||
|
|
@ -1680,23 +1415,13 @@ Proof.
|
||||||
move /E_Symmetric in h01.
|
move /E_Symmetric in h01.
|
||||||
move /regularity_sub0 : hSu20 => [i0].
|
move /regularity_sub0 : hSu20 => [i0].
|
||||||
sfirstorder use:bind_inst.
|
sfirstorder use:bind_inst.
|
||||||
* clear => ? ? ?. exfalso.
|
- move => p0 p1 a0 a1 hne0 hne1 doma iha /DJoin.hne_proj_inj /(_ hne0 hne1) [? hja]. subst.
|
||||||
hauto q:on use:REReds.hne_app_inv, REReds.hne_proj_inv.
|
move : iha hja; repeat move/[apply].
|
||||||
* clear => ? ? ?. exfalso.
|
move => [_ iha]. apply ce_neu_neu_helper => // Γ A B.
|
||||||
hauto q:on use:REReds.hne_app_inv, REReds.hne_ind_inv.
|
move : iha (hne0) (hne1);repeat move/[apply].
|
||||||
+ case : b => //=.
|
move => ih.
|
||||||
* move => i p h /algo_metric_join. clear => ? _ ?. exfalso.
|
|
||||||
hauto l:on use:REReds.hne_proj_inv, REReds.var_inv.
|
|
||||||
* move => > /algo_metric_join. clear => ? ? ?. exfalso.
|
|
||||||
hauto l:on use:REReds.hne_proj_inv, REReds.hne_app_inv.
|
|
||||||
(* real case *)
|
|
||||||
* move => p1 a1 p0 a0 /algo_metric_proj ha hne1 hne0.
|
|
||||||
move : ha (hne0) (hne1); repeat move/[apply].
|
|
||||||
move => [? [j []]]. subst.
|
|
||||||
move : ih; repeat move/[apply].
|
|
||||||
move => [_ ih].
|
|
||||||
case : p1.
|
case : p1.
|
||||||
** move => Γ A B ha0 ha1.
|
** move => ha0 ha1.
|
||||||
move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0.
|
move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0.
|
||||||
move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1.
|
move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1.
|
||||||
move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
|
move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
|
||||||
|
|
@ -1712,7 +1437,7 @@ Proof.
|
||||||
hauto l:on use:Su_Sig_Proj1, Su_Transitive.
|
hauto l:on use:Su_Sig_Proj1, Su_Transitive.
|
||||||
apply T_Proj1 with (B := B2); eauto using T_Conv_E.
|
apply T_Proj1 with (B := B2); eauto using T_Conv_E.
|
||||||
apply T_Proj1 with (B := B2); eauto using T_Conv_E.
|
apply T_Proj1 with (B := B2); eauto using T_Conv_E.
|
||||||
** move => Γ A B ha0 ha1.
|
** move => ha0 ha1.
|
||||||
move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0.
|
move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0.
|
||||||
move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1.
|
move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1.
|
||||||
move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
|
move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
|
||||||
|
|
@ -1743,43 +1468,32 @@ Proof.
|
||||||
move /E_Symmetric in haE.
|
move /E_Symmetric in haE.
|
||||||
move /regularity_sub0 in hSu21.
|
move /regularity_sub0 in hSu21.
|
||||||
sfirstorder use:bind_inst.
|
sfirstorder use:bind_inst.
|
||||||
* move => > /algo_metric_join; clear => ? ? ?. exfalso.
|
- move {hhPairNeu hhAbsNeu}.
|
||||||
hauto q:on use:REReds.hne_proj_inv, REReds.hne_ind_inv.
|
move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc /hne_ind_inj.
|
||||||
(* ind ind case *)
|
move => /(_ neu0 neu1) [hjP][hju][hjb]hjc.
|
||||||
+ move => P a0 b0 c0.
|
apply ce_neu_neu_helper => // Γ A B.
|
||||||
case : b => //=;
|
move /Ind_Inv => [iP0][wtP0][wta0][wtb0][wtc0]hSu0.
|
||||||
lazymatch goal with
|
move /Ind_Inv => [iP1][wtP1][wta1][wtb1][wtc1]hSu1.
|
||||||
| [|- context[algo_metric _ (PInd _ _ _ _) (PInd _ _ _ _)]] => idtac
|
have {}iha : u0 ∼ u1 by qauto l:on.
|
||||||
| _ => move => > /algo_metric_join; clear => *; exfalso
|
|
||||||
end.
|
|
||||||
* hauto q:on use:REReds.hne_ind_inv, REReds.var_inv.
|
|
||||||
* hauto q:on use:REReds.hne_ind_inv, REReds.hne_app_inv.
|
|
||||||
* hauto q:on use:REReds.hne_ind_inv, REReds.hne_proj_inv.
|
|
||||||
* move => P1 a1 b1 c1 /[dup] halg /algo_metric_ind + h0 h1.
|
|
||||||
move /(_ h1 h0).
|
|
||||||
move => [j][hj][hP][ha][hb]hc Γ A B hL hR.
|
|
||||||
move /Ind_Inv : hL => [iP0][wtP0][wta0][wtb0][wtc0]hSu0.
|
|
||||||
move /Ind_Inv : hR => [iP1][wtP1][wta1][wtb1][wtc1]hSu1.
|
|
||||||
have {}iha : a0 ∼ a1 by qauto l:on.
|
|
||||||
have [] : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia.
|
have [] : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia.
|
||||||
move : T_Univ_Raise wtP0; do!move/[apply]. move => wtP0.
|
move : T_Univ_Raise wtP0; repeat move/[apply]. move => wtP0.
|
||||||
move : T_Univ_Raise wtP1; do!move/[apply]. move => wtP1.
|
move : T_Univ_Raise wtP1; repeat move/[apply]. move => wtP1.
|
||||||
have {}ihP : P ⇔ P1 by qauto l:on.
|
have {}ihP : P0 ⇔ P1 by qauto l:on.
|
||||||
set Δ := cons _ _ in wtP0, wtP1, wtc0, wtc1.
|
set Δ := cons _ _ in wtP0, wtP1, wtc0, wtc1.
|
||||||
have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
|
have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
|
||||||
have hPE : Δ ⊢ P ≡ P1 ∈ PUniv (max iP0 iP1)
|
have hPE : Δ ⊢ P0 ≡ P1 ∈ PUniv (max iP0 iP1)
|
||||||
by hauto l:on use:coqeq_sound_mutual.
|
by hauto l:on use:coqeq_sound_mutual.
|
||||||
have haE : Γ ⊢ a0 ≡ a1 ∈ PNat
|
have haE : Γ ⊢ u0 ≡ u1 ∈ PNat
|
||||||
by hauto l:on use:coqeq_sound_mutual.
|
by hauto l:on use:coqeq_sound_mutual.
|
||||||
have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual.
|
have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual.
|
||||||
have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) P ≡ subst_PTm (scons PZero VarPTm) P1 ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max iP0 iP1)).
|
have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) P0 ≡ subst_PTm (scons PZero VarPTm) P1 ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max iP0 iP1)).
|
||||||
eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero.
|
eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero.
|
||||||
have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P
|
have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P0
|
||||||
by eauto using T_Conv_E.
|
by eauto using T_Conv_E.
|
||||||
have {}ihb : b0 ⇔ b1 by hauto l:on.
|
have {}ihb : b0 ⇔ b1 by hauto l:on.
|
||||||
have hPSig : Γ ⊢ PBind PSig PNat P ≡ PBind PSig PNat P1 ∈ PUniv (Nat.max iP0 iP1) by eauto with wt.
|
have hPSig : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv (Nat.max iP0 iP1) by eauto with wt.
|
||||||
set T := ren_PTm shift _ in wtc0.
|
set T := ren_PTm shift _ in wtc0.
|
||||||
have : (cons P Δ) ⊢ c1 ∈ T.
|
have : (cons P0 Δ) ⊢ c1 ∈ T.
|
||||||
apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt.
|
apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt.
|
||||||
apply : Su_Eq; eauto.
|
apply : Su_Eq; eauto.
|
||||||
subst T. apply : weakening_su; eauto.
|
subst T. apply : weakening_su; eauto.
|
||||||
|
|
@ -1791,39 +1505,501 @@ Proof.
|
||||||
apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1.
|
apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1.
|
||||||
have {}ihc : c0 ⇔ c1 by qauto l:on.
|
have {}ihc : c0 ⇔ c1 by qauto l:on.
|
||||||
move => [:ih].
|
move => [:ih].
|
||||||
split. abstract : ih. move : h0 h1 ihP iha ihb ihc. clear. sauto lq:on.
|
split. abstract : ih. move : neu0 neu1 ihP iha ihb ihc. clear. sauto lq:on.
|
||||||
have hEInd : Γ ⊢ PInd P a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P by hfcrush use:coqeq_sound_mutual.
|
have hEInd : Γ ⊢ PInd P0 u0 b0 c0 ≡ PInd P1 u1 b1 c1 ∈ subst_PTm (scons u0 VarPTm) P0 by hfcrush use:coqeq_sound_mutual.
|
||||||
exists (subst_PTm (scons a0 VarPTm) P).
|
exists (subst_PTm (scons u0 VarPTm) P0).
|
||||||
repeat split => //=; eauto with wt.
|
repeat split => //=; eauto with wt.
|
||||||
apply : Su_Transitive.
|
apply : Su_Transitive.
|
||||||
apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt.
|
apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt.
|
||||||
apply : Su_Eq. apply E_Refl. by apply T_Nat'.
|
apply : Su_Eq. apply E_Refl. by apply T_Nat'.
|
||||||
apply : Su_Eq. apply hPE. by eauto.
|
apply : Su_Eq. apply hPE. by eauto.
|
||||||
move : hEInd. clear. hauto l:on use:regularity.
|
move : hEInd. clear. hauto l:on use:regularity.
|
||||||
Qed.
|
- move => a b ha hb.
|
||||||
|
move {hhPairNeu hhAbsNeu}.
|
||||||
|
Admitted.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
(* algo_metric k a b -> *)
|
||||||
|
(* (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ *)
|
||||||
|
(* (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C). *)
|
||||||
|
(* Proof. *)
|
||||||
|
(* move : k a b. *)
|
||||||
|
(* elim /Wf_nat.lt_wf_ind. *)
|
||||||
|
(* move => n ih. *)
|
||||||
|
(* move => a b /[dup] h /algo_metric_case. move : a b h => [:hstepL]. *)
|
||||||
|
(* move => a b h. *)
|
||||||
|
(* (* Cases where a and b can take steps *) *)
|
||||||
|
(* case; cycle 1. *)
|
||||||
|
(* move : ih a b h. *)
|
||||||
|
(* abstract : hstepL. qauto l:on use:HRed.preservation, CE_HRedL, hred_hne. *)
|
||||||
|
(* move /algo_metric_sym /algo_metric_case : (h). *)
|
||||||
|
(* case; cycle 1. *)
|
||||||
|
(* move /algo_metric_sym : h. *)
|
||||||
|
(* move : hstepL ih => /[apply]/[apply]. *)
|
||||||
|
(* repeat move /[apply]. *)
|
||||||
|
(* move => hstepL. *)
|
||||||
|
(* hauto lq:on use:coqeq_symmetric_mutual, algo_metric_sym. *)
|
||||||
|
(* (* Cases where a and b can't take wh steps *) *)
|
||||||
|
(* move {hstepL}. *)
|
||||||
|
(* move : a b h. move => [:hnfneu]. *)
|
||||||
|
(* move => a b h. *)
|
||||||
|
(* case => fb; case => fa. *)
|
||||||
|
(* - split; last by sfirstorder use:hf_not_hne. *)
|
||||||
|
(* move {hnfneu}. *)
|
||||||
|
(* case : a h fb fa => //=. *)
|
||||||
|
(* + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_AbsBind_Imp, T_AbsUniv_Imp, T_AbsZero_Imp, T_AbsSuc_Imp, T_AbsNat_Imp. *)
|
||||||
|
(* move => a0 a1 ha0 _ _ Γ A wt0 wt1. *)
|
||||||
|
(* move : T_Abs_Inv wt0 wt1; repeat move/[apply]. move => [Δ [V [wt1 wt0]]]. *)
|
||||||
|
(* apply : CE_HRed; eauto using rtc_refl. *)
|
||||||
|
(* apply CE_AbsAbs. *)
|
||||||
|
(* suff [l [h0 h1]] : exists l, l < n /\ algo_metric l a1 a0 by eapply ih; eauto. *)
|
||||||
|
(* have ? : n > 0 by sauto solve+:lia. *)
|
||||||
|
(* exists (n - 1). split; first by lia. *)
|
||||||
|
(* move : (ha0). rewrite /algo_metric. *)
|
||||||
|
(* move => [i][j][va][vb][hr0][hr1][nfva][nfvb][[v [hr0' hr1']]] har. *)
|
||||||
|
(* apply lored_nsteps_abs_inv in hr0, hr1. *)
|
||||||
|
(* move : hr0 => [va' [hr00 hr01]]. *)
|
||||||
|
(* move : hr1 => [vb' [hr10 hr11]]. move {ih}. *)
|
||||||
|
(* exists i,j,va',vb'. subst. *)
|
||||||
|
(* suff [v0 [hv00 hv01]] : exists v0, rtc ERed.R va' v0 /\ rtc ERed.R vb' v0. *)
|
||||||
|
(* repeat split =>//=. sfirstorder. *)
|
||||||
|
(* simpl in *; by lia. *)
|
||||||
|
(* move /algo_metric_join /DJoin.symmetric : ha0. *)
|
||||||
|
(* have : SN a0 /\ SN a1 by qauto l:on use:fundamental_theorem, logrel.SemWt_SN. *)
|
||||||
|
(* move => /[dup] [[ha00 ha10]] []. *)
|
||||||
|
(* move : DJoin.abs_inj; repeat move/[apply]. *)
|
||||||
|
(* move : DJoin.standardization ha00 ha10; repeat move/[apply]. *)
|
||||||
|
(* (* this is awful *) *)
|
||||||
|
(* move => [vb][va][h' [h'' [h''' [h'''' h'''''']]]]. *)
|
||||||
|
(* have /LoReds.ToRReds {}hr00 : rtc LoRed.R a1 va' *)
|
||||||
|
(* by hauto lq:on use:@relations.rtc_nsteps. *)
|
||||||
|
(* have /LoReds.ToRReds {}hr10 : rtc LoRed.R a0 vb' *)
|
||||||
|
(* by hauto lq:on use:@relations.rtc_nsteps. *)
|
||||||
|
(* simpl in *. *)
|
||||||
|
(* have [*] : va' = va /\ vb' = vb by eauto using red_uniquenf. subst. *)
|
||||||
|
(* sfirstorder. *)
|
||||||
|
(* + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_PairBind_Imp, T_PairUniv_Imp, T_PairNat_Imp, T_PairSuc_Imp, T_PairZero_Imp. *)
|
||||||
|
(* move => a1 b1 a0 b0 h _ _ Γ A hu0 hu1. *)
|
||||||
|
(* have [sn0 sn1] : SN (PPair a0 b0) /\ SN (PPair a1 b1) *)
|
||||||
|
(* by qauto l:on use:fundamental_theorem, logrel.SemWt_SN. *)
|
||||||
|
(* apply : CE_HRed; eauto using rtc_refl. *)
|
||||||
|
(* move /Pair_Inv : hu0 => [A0][B0][ha0][hb0]hSu0. *)
|
||||||
|
(* move /Pair_Inv : hu1 => [A1][B1][ha1][hb1]hSu1. *)
|
||||||
|
(* move /Sub_Bind_InvR : (hSu0). *)
|
||||||
|
(* move => [i][A2][B2]hE. *)
|
||||||
|
(* have hSu12 : Γ ⊢ PBind PSig A1 B1 ≲ PBind PSig A2 B2 *)
|
||||||
|
(* by eauto using Su_Transitive, Su_Eq. *)
|
||||||
|
(* have hSu02 : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2 *)
|
||||||
|
(* by eauto using Su_Transitive, Su_Eq. *)
|
||||||
|
(* have hA02 : Γ ⊢ A0 ≲ A2 by eauto using Su_Sig_Proj1. *)
|
||||||
|
(* have hA12 : Γ ⊢ A1 ≲ A2 by eauto using Su_Sig_Proj1. *)
|
||||||
|
(* have ha0A2 : Γ ⊢ a0 ∈ A2 by eauto using T_Conv. *)
|
||||||
|
(* have ha1A2 : Γ ⊢ a1 ∈ A2 by eauto using T_Conv. *)
|
||||||
|
(* move /algo_metric_pair : h sn0 sn1; repeat move/[apply]. *)
|
||||||
|
(* move => [j][hj][ih0 ih1]. *)
|
||||||
|
(* have haE : a0 ⇔ a1 by hauto l:on. *)
|
||||||
|
(* apply CE_PairPair => //. *)
|
||||||
|
(* have {}haE : Γ ⊢ a0 ≡ a1 ∈ A2 *)
|
||||||
|
(* by hauto l:on use:coqeq_sound_mutual. *)
|
||||||
|
(* have {}hb1 : Γ ⊢ b1 ∈ subst_PTm (scons a1 VarPTm) B2. *)
|
||||||
|
(* apply : T_Conv; eauto. *)
|
||||||
|
(* move /E_Refl in ha1. hauto l:on use:Su_Sig_Proj2. *)
|
||||||
|
(* eapply ih; cycle -1; eauto. *)
|
||||||
|
(* apply : T_Conv; eauto. *)
|
||||||
|
(* apply Su_Transitive with (B := subst_PTm (scons a0 VarPTm) B2). *)
|
||||||
|
(* move /E_Refl in ha0. hauto l:on use:Su_Sig_Proj2. *)
|
||||||
|
(* move : hE haE. clear. *)
|
||||||
|
(* move => h. *)
|
||||||
|
(* eapply regularity in h. *)
|
||||||
|
(* move : h => [_ [hB _]]. *)
|
||||||
|
(* eauto using bind_inst. *)
|
||||||
|
(* + case : b => //=. *)
|
||||||
|
(* * hauto lq:on use:T_AbsBind_Imp. *)
|
||||||
|
(* * hauto lq:on rew:off use:T_PairBind_Imp. *)
|
||||||
|
(* * move => p1 A1 B1 p0 A0 B0. *)
|
||||||
|
(* move /algo_metric_bind. *)
|
||||||
|
(* move => [?][j [ih0 [ih1 ih2]]]_ _. subst. *)
|
||||||
|
(* move => Γ A hU0 hU1. *)
|
||||||
|
(* move /Bind_Inv : hU0 => [i0 [hA0 [hB0 hS0]]]. *)
|
||||||
|
(* move /Bind_Inv : hU1 => [i1 [hA1 [hB1 hS1]]]. *)
|
||||||
|
(* have ? : Γ ⊢ PUniv i0 ≲ PUniv (max i0 i1) *)
|
||||||
|
(* by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia. *)
|
||||||
|
(* have ? : Γ ⊢ PUniv i1 ≲ PUniv (max i0 i1) *)
|
||||||
|
(* by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia. *)
|
||||||
|
(* have {}hA0 : Γ ⊢ A0 ∈ PUniv (max i0 i1) by eauto using T_Conv. *)
|
||||||
|
(* have {}hA1 : Γ ⊢ A1 ∈ PUniv (max i0 i1) by eauto using T_Conv. *)
|
||||||
|
(* have {}hB0 : (cons A0 Γ) ⊢ B0 ∈ PUniv (max i0 i1) *)
|
||||||
|
(* by hauto lq:on use:T_Univ_Raise solve+:lia. *)
|
||||||
|
(* have {}hB1 : (cons A1 Γ) ⊢ B1 ∈ PUniv (max i0 i1) *)
|
||||||
|
(* by hauto lq:on use:T_Univ_Raise solve+:lia. *)
|
||||||
|
|
||||||
|
(* have ihA : A0 ⇔ A1 by hauto l:on. *)
|
||||||
|
(* have hAE : Γ ⊢ A0 ≡ A1 ∈ PUniv (Nat.max i0 i1) *)
|
||||||
|
(* by hauto l:on use:coqeq_sound_mutual. *)
|
||||||
|
(* apply : CE_HRed; eauto using rtc_refl. *)
|
||||||
|
(* constructor => //. *)
|
||||||
|
|
||||||
|
(* eapply ih; eauto. *)
|
||||||
|
(* apply : ctx_eq_subst_one; eauto. *)
|
||||||
|
(* eauto using Su_Eq. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on use:DJoin.bind_univ_noconf. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on use:Sub.nat_bind_noconf, Sub.FromJoin. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* clear. hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv. *)
|
||||||
|
(* * move => > /algo_metric_join. clear. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv. *)
|
||||||
|
(* + case : b => //=. *)
|
||||||
|
(* * hauto lq:on use:T_AbsUniv_Imp. *)
|
||||||
|
(* * hauto lq:on use:T_PairUniv_Imp. *)
|
||||||
|
(* * qauto l:on use:algo_metric_join, DJoin.bind_univ_noconf, DJoin.symmetric. *)
|
||||||
|
(* * move => i j /algo_metric_join /DJoin.univ_inj ? _ _ Γ A hi hj. *)
|
||||||
|
(* subst. *)
|
||||||
|
(* hauto l:on. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on use:Sub.nat_univ_noconf, Sub.FromJoin. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.suc_inv. *)
|
||||||
|
(* + case : b => //=. *)
|
||||||
|
(* * qauto l:on use:T_AbsNat_Imp. *)
|
||||||
|
(* * qauto l:on use:T_PairNat_Imp. *)
|
||||||
|
(* * move => > /algo_metric_join /Sub.FromJoin. hauto l:on use:Sub.bind_nat_noconf. *)
|
||||||
|
(* * move => > /algo_metric_join /Sub.FromJoin. hauto lq:on use:Sub.univ_nat_noconf. *)
|
||||||
|
(* * hauto l:on. *)
|
||||||
|
(* * move /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv. *)
|
||||||
|
(* (* Zero *) *)
|
||||||
|
(* + case : b => //=. *)
|
||||||
|
(* * hauto lq:on rew:off use:T_AbsZero_Imp. *)
|
||||||
|
(* * hauto lq: on use: T_PairZero_Imp. *)
|
||||||
|
(* * move =>> /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.zero_inv, REReds.bind_inv. *)
|
||||||
|
(* * move =>> /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv. *)
|
||||||
|
(* * move =>> /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv. *)
|
||||||
|
(* * hauto l:on. *)
|
||||||
|
(* * move =>> /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv. *)
|
||||||
|
(* (* Suc *) *)
|
||||||
|
(* + case : b => //=. *)
|
||||||
|
(* * hauto lq:on rew:off use:T_AbsSuc_Imp. *)
|
||||||
|
(* * hauto lq:on use:T_PairSuc_Imp. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv. *)
|
||||||
|
(* * move => > /algo_metric_join. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv. *)
|
||||||
|
(* * move => a0 a1 h _ _. *)
|
||||||
|
(* move /algo_metric_suc : h => [j [h4 h5]]. *)
|
||||||
|
(* move => Γ A /Suc_Inv [h0 h1] /Suc_Inv [h2 h3]. *)
|
||||||
|
(* move : ih h4 h5;do!move/[apply]. *)
|
||||||
|
(* move => [ih _]. *)
|
||||||
|
(* move : ih h0 h2;do!move/[apply]. *)
|
||||||
|
(* move => h. apply : CE_HRed; eauto using rtc_refl. *)
|
||||||
|
(* by constructor. *)
|
||||||
|
(* - move : a b h fb fa. abstract : hnfneu. *)
|
||||||
|
(* move => + b. *)
|
||||||
|
(* case : b => //=. *)
|
||||||
|
(* (* NeuAbs *) *)
|
||||||
|
(* + move => a u halg _ nea. split => // Γ A hu /[dup] ha. *)
|
||||||
|
(* move /Abs_Inv => [A0][B0][_]hSu. *)
|
||||||
|
(* move /Sub_Bind_InvR : (hSu) => [i][A2][B2]hE. *)
|
||||||
|
(* have {}hu : Γ ⊢ u ∈ PBind PPi A2 B2 by eauto using T_Conv_E. *)
|
||||||
|
(* have {}ha : Γ ⊢ PAbs a ∈ PBind PPi A2 B2 by eauto using T_Conv_E. *)
|
||||||
|
(* have {}hE : Γ ⊢ PBind PPi A2 B2 ∈ PUniv i *)
|
||||||
|
(* by hauto l:on use:regularity. *)
|
||||||
|
(* have {i} [j {}hE] : exists j, Γ ⊢ A2 ∈ PUniv j *)
|
||||||
|
(* by qauto l:on use:Bind_Inv. *)
|
||||||
|
(* have hΓ : ⊢ cons A2 Γ by eauto using Wff_Cons'. *)
|
||||||
|
(* set Δ := cons _ _ in hΓ. *)
|
||||||
|
(* have {}hu : Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ B2. *)
|
||||||
|
(* apply : T_App'; cycle 1. apply : weakening_wt' => //=; eauto. *)
|
||||||
|
(* reflexivity. *)
|
||||||
|
(* rewrite -/ren_PTm. *)
|
||||||
|
(* apply T_Var; eauto using here. *)
|
||||||
|
(* rewrite -/ren_PTm. by asimpl; rewrite subst_scons_id. *)
|
||||||
|
(* move /Abs_Pi_Inv in ha. *)
|
||||||
|
(* move /algo_metric_neu_abs /(_ nea) : halg. *)
|
||||||
|
(* move => [j0][hj0]halg. *)
|
||||||
|
(* apply : CE_HRed; eauto using rtc_refl. *)
|
||||||
|
(* eapply CE_NeuAbs => //=. *)
|
||||||
|
(* eapply ih; eauto. *)
|
||||||
|
(* (* NeuPair *) *)
|
||||||
|
(* + move => a0 b0 u halg _ neu. *)
|
||||||
|
(* split => // Γ A hu /[dup] wt. *)
|
||||||
|
(* move /Pair_Inv => [A0][B0][ha0][hb0]hU. *)
|
||||||
|
(* move /Sub_Bind_InvR : (hU) => [i][A2][B2]hE. *)
|
||||||
|
(* have {}wt : Γ ⊢ PPair a0 b0 ∈ PBind PSig A2 B2 by sauto lq:on. *)
|
||||||
|
(* have {}hu : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E. *)
|
||||||
|
(* move /Pair_Sig_Inv : wt => [{}ha0 {}hb0]. *)
|
||||||
|
(* have /T_Proj1 huL := hu. *)
|
||||||
|
(* have /T_Proj2 {hu} huR := hu. *)
|
||||||
|
(* move /algo_metric_neu_pair /(_ neu) : halg => [j [hj [hL hR]]]. *)
|
||||||
|
(* have heL : PProj PL u ⇔ a0 by hauto l:on. *)
|
||||||
|
(* eapply CE_HRed; eauto using rtc_refl. *)
|
||||||
|
(* apply CE_NeuPair; eauto. *)
|
||||||
|
(* eapply ih; eauto. *)
|
||||||
|
(* apply : T_Conv; eauto. *)
|
||||||
|
(* have {}hE : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i *)
|
||||||
|
(* by hauto l:on use:regularity. *)
|
||||||
|
(* have /E_Symmetric : Γ ⊢ PProj PL u ≡ a0 ∈ A2 by *)
|
||||||
|
(* hauto l:on use:coqeq_sound_mutual. *)
|
||||||
|
(* hauto l:on use:bind_inst. *)
|
||||||
|
(* (* NeuBind: Impossible *) *)
|
||||||
|
(* + move => b p p0 a /algo_metric_join h _ h0. exfalso. *)
|
||||||
|
(* move : h h0. clear. *)
|
||||||
|
(* move /Sub.FromJoin. *)
|
||||||
|
(* hauto l:on use:Sub.hne_bind_noconf. *)
|
||||||
|
(* (* NeuUniv: Impossible *) *)
|
||||||
|
(* + hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join. *)
|
||||||
|
(* + hauto lq:on rew:off use:DJoin.hne_nat_noconf, algo_metric_join. *)
|
||||||
|
(* (* Zero *) *)
|
||||||
|
(* + case => //=. *)
|
||||||
|
(* * move => i /algo_metric_join. clear. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.var_inv, REReds.zero_inv. *)
|
||||||
|
(* * move => >/algo_metric_join. clear. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.hne_app_inv, REReds.zero_inv. *)
|
||||||
|
(* * move => >/algo_metric_join. clear. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.zero_inv. *)
|
||||||
|
(* * move => >/algo_metric_join. clear. *)
|
||||||
|
(* move => h _ h2. exfalso. *)
|
||||||
|
(* hauto q:on use:REReds.hne_ind_inv, REReds.zero_inv. *)
|
||||||
|
(* (* Suc *) *)
|
||||||
|
(* + move => a0. *)
|
||||||
|
(* case => //=; move => >/algo_metric_join; clear. *)
|
||||||
|
(* * hauto lq:on rew:off use:REReds.var_inv, REReds.suc_inv. *)
|
||||||
|
(* * hauto lq:on rew:off use:REReds.hne_app_inv, REReds.suc_inv. *)
|
||||||
|
(* * hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.suc_inv. *)
|
||||||
|
(* * hauto q:on use:REReds.hne_ind_inv, REReds.suc_inv. *)
|
||||||
|
(* - move {ih}. *)
|
||||||
|
(* move /algo_metric_sym in h. *)
|
||||||
|
(* qauto l:on use:coqeq_symmetric_mutual. *)
|
||||||
|
(* - move {hnfneu}. *)
|
||||||
|
(* (* Clear out some trivial cases *) *)
|
||||||
|
(* suff : (forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ (exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)). *)
|
||||||
|
(* move => h0. *)
|
||||||
|
(* split. move => *. apply : CE_HRed; eauto using rtc_refl. apply CE_NeuNeu. by firstorder. *)
|
||||||
|
(* by firstorder. *)
|
||||||
|
|
||||||
|
(* case : a h fb fa => //=. *)
|
||||||
|
(* + case : b => //=; move => > /algo_metric_join. *)
|
||||||
|
(* * move /DJoin.var_inj => i _ _. subst. *)
|
||||||
|
(* move => Γ A B /Var_Inv [? [B0 [h0 h1]]]. *)
|
||||||
|
(* move /Var_Inv => [_ [C0 [h2 h3]]]. *)
|
||||||
|
(* have ? : B0 = C0 by eauto using lookup_deter. subst. *)
|
||||||
|
(* sfirstorder use:T_Var. *)
|
||||||
|
(* * clear => ? ? _. exfalso. *)
|
||||||
|
(* hauto l:on use:REReds.var_inv, REReds.hne_app_inv. *)
|
||||||
|
(* * clear => ? ? _. exfalso. *)
|
||||||
|
(* hauto l:on use:REReds.var_inv, REReds.hne_proj_inv. *)
|
||||||
|
(* * clear => ? ? _. exfalso. *)
|
||||||
|
(* hauto q:on use:REReds.var_inv, REReds.hne_ind_inv. *)
|
||||||
|
(* + case : b => //=; *)
|
||||||
|
(* lazymatch goal with *)
|
||||||
|
(* | [|- context[algo_metric _ (PApp _ _) (PApp _ _)]] => idtac *)
|
||||||
|
(* | _ => move => > /algo_metric_join *)
|
||||||
|
(* end. *)
|
||||||
|
(* * clear => *. exfalso. *)
|
||||||
|
(* hauto lq:on rew:off use:REReds.hne_app_inv, REReds.var_inv. *)
|
||||||
|
(* (* real case *) *)
|
||||||
|
(* * move => b1 a1 b0 a0 halg hne1 hne0 Γ A B wtA wtB. *)
|
||||||
|
(* move /App_Inv : wtA => [A0][B0][hb0][ha0]hS0. *)
|
||||||
|
(* move /App_Inv : wtB => [A1][B1][hb1][ha1]hS1. *)
|
||||||
|
(* move : algo_metric_app (hne0) (hne1) halg. repeat move/[apply]. *)
|
||||||
|
(* move => [j [hj [hal0 hal1]]]. *)
|
||||||
|
(* have /ih := hal0. *)
|
||||||
|
(* move /(_ hj). *)
|
||||||
|
(* move => [_ ihb]. *)
|
||||||
|
(* move : ihb (hne0) (hne1) hb0 hb1. repeat move/[apply]. *)
|
||||||
|
(* move => [hb01][C][hT0][hT1][hT2]hT3. *)
|
||||||
|
(* move /Sub_Bind_InvL : (hT0). *)
|
||||||
|
(* move => [i][A2][B2]hE. *)
|
||||||
|
(* have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by *)
|
||||||
|
(* eauto using Su_Eq, Su_Transitive. *)
|
||||||
|
(* have hSu10 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A1 B1 by *)
|
||||||
|
(* eauto using Su_Eq, Su_Transitive. *)
|
||||||
|
(* have hSuA0 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Pi_Proj1. *)
|
||||||
|
(* have hSuA1 : Γ ⊢ A1 ≲ A2 by sfirstorder use:Su_Pi_Proj1. *)
|
||||||
|
(* have ha1' : Γ ⊢ a1 ∈ A2 by eauto using T_Conv. *)
|
||||||
|
(* have ha0' : Γ ⊢ a0 ∈ A2 by eauto using T_Conv. *)
|
||||||
|
(* move : ih (hj) hal1. repeat move/[apply]. *)
|
||||||
|
(* move => [ih _]. *)
|
||||||
|
(* move : ih (ha0') (ha1'); repeat move/[apply]. *)
|
||||||
|
(* move => iha. *)
|
||||||
|
(* split. qblast. *)
|
||||||
|
(* exists (subst_PTm (scons a0 VarPTm) B2). *)
|
||||||
|
(* split. *)
|
||||||
|
(* apply : Su_Transitive; eauto. *)
|
||||||
|
(* move /E_Refl in ha0. *)
|
||||||
|
(* hauto l:on use:Su_Pi_Proj2. *)
|
||||||
|
(* have h01 : Γ ⊢ a0 ≡ a1 ∈ A2 by sfirstorder use:coqeq_sound_mutual. *)
|
||||||
|
(* split. *)
|
||||||
|
(* apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2). *)
|
||||||
|
(* move /regularity_sub0 : hSu10 => [i0]. *)
|
||||||
|
(* hauto l:on use:bind_inst. *)
|
||||||
|
(* hauto lq:on rew:off use:Su_Pi_Proj2, Su_Transitive, E_Refl. *)
|
||||||
|
(* split. *)
|
||||||
|
(* by apply : T_App; eauto using T_Conv_E. *)
|
||||||
|
(* apply : T_Conv; eauto. *)
|
||||||
|
(* apply T_App with (A := A2) (B := B2); eauto. *)
|
||||||
|
(* apply : T_Conv_E; eauto. *)
|
||||||
|
(* move /E_Symmetric in h01. *)
|
||||||
|
(* move /regularity_sub0 : hSu20 => [i0]. *)
|
||||||
|
(* sfirstorder use:bind_inst. *)
|
||||||
|
(* * clear => ? ? ?. exfalso. *)
|
||||||
|
(* hauto q:on use:REReds.hne_app_inv, REReds.hne_proj_inv. *)
|
||||||
|
(* * clear => ? ? ?. exfalso. *)
|
||||||
|
(* hauto q:on use:REReds.hne_app_inv, REReds.hne_ind_inv. *)
|
||||||
|
(* + case : b => //=. *)
|
||||||
|
(* * move => i p h /algo_metric_join. clear => ? _ ?. exfalso. *)
|
||||||
|
(* hauto l:on use:REReds.hne_proj_inv, REReds.var_inv. *)
|
||||||
|
(* * move => > /algo_metric_join. clear => ? ? ?. exfalso. *)
|
||||||
|
(* hauto l:on use:REReds.hne_proj_inv, REReds.hne_app_inv. *)
|
||||||
|
(* (* real case *) *)
|
||||||
|
(* * move => p1 a1 p0 a0 /algo_metric_proj ha hne1 hne0. *)
|
||||||
|
(* move : ha (hne0) (hne1); repeat move/[apply]. *)
|
||||||
|
(* move => [? [j []]]. subst. *)
|
||||||
|
(* move : ih; repeat move/[apply]. *)
|
||||||
|
(* move => [_ ih]. *)
|
||||||
|
(* case : p1. *)
|
||||||
|
(* ** move => Γ A B ha0 ha1. *)
|
||||||
|
(* move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0. *)
|
||||||
|
(* move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1. *)
|
||||||
|
(* move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply]. *)
|
||||||
|
(* move => [ha [C [hS0 [hS1 [wta0 wta1]]]]]. *)
|
||||||
|
(* split. sauto lq:on. *)
|
||||||
|
(* move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2. *)
|
||||||
|
(* have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0 *)
|
||||||
|
(* by eauto using Su_Transitive, Su_Eq. *)
|
||||||
|
(* have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1 *)
|
||||||
|
(* by eauto using Su_Transitive, Su_Eq. *)
|
||||||
|
(* exists A2. split; eauto using Su_Sig_Proj1, Su_Transitive. *)
|
||||||
|
(* repeat split => //=. *)
|
||||||
|
(* hauto l:on use:Su_Sig_Proj1, Su_Transitive. *)
|
||||||
|
(* apply T_Proj1 with (B := B2); eauto using T_Conv_E. *)
|
||||||
|
(* apply T_Proj1 with (B := B2); eauto using T_Conv_E. *)
|
||||||
|
(* ** move => Γ A B ha0 ha1. *)
|
||||||
|
(* move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0. *)
|
||||||
|
(* move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1. *)
|
||||||
|
(* move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply]. *)
|
||||||
|
(* move => [ha [C [hS0 [hS1 [wta0 wta1]]]]]. *)
|
||||||
|
(* split. sauto lq:on. *)
|
||||||
|
(* move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2. *)
|
||||||
|
(* have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0 *)
|
||||||
|
(* by eauto using Su_Transitive, Su_Eq. *)
|
||||||
|
(* have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1 *)
|
||||||
|
(* by eauto using Su_Transitive, Su_Eq. *)
|
||||||
|
(* have hA20 : Γ ⊢ A2 ≲ A0 by eauto using Su_Sig_Proj1. *)
|
||||||
|
(* have hA21 : Γ ⊢ A2 ≲ A1 by eauto using Su_Sig_Proj1. *)
|
||||||
|
(* have {}wta0 : Γ ⊢ a0 ∈ PBind PSig A2 B2 by eauto using T_Conv_E. *)
|
||||||
|
(* have {}wta1 : Γ ⊢ a1 ∈ PBind PSig A2 B2 by eauto using T_Conv_E. *)
|
||||||
|
(* have haE : Γ ⊢ PProj PL a0 ≡ PProj PL a1 ∈ A2 *)
|
||||||
|
(* by sauto lq:on use:coqeq_sound_mutual. *)
|
||||||
|
(* exists (subst_PTm (scons (PProj PL a0) VarPTm) B2). *)
|
||||||
|
(* repeat split. *)
|
||||||
|
(* *** apply : Su_Transitive; eauto. *)
|
||||||
|
(* have : Γ ⊢ PProj PL a0 ≡ PProj PL a0 ∈ A2 *)
|
||||||
|
(* by qauto use:regularity, E_Refl. *)
|
||||||
|
(* sfirstorder use:Su_Sig_Proj2. *)
|
||||||
|
(* *** apply : Su_Transitive; eauto. *)
|
||||||
|
(* sfirstorder use:Su_Sig_Proj2. *)
|
||||||
|
(* *** eauto using T_Proj2. *)
|
||||||
|
(* *** apply : T_Conv. *)
|
||||||
|
(* apply : T_Proj2; eauto. *)
|
||||||
|
(* move /E_Symmetric in haE. *)
|
||||||
|
(* move /regularity_sub0 in hSu21. *)
|
||||||
|
(* sfirstorder use:bind_inst. *)
|
||||||
|
(* * move => > /algo_metric_join; clear => ? ? ?. exfalso. *)
|
||||||
|
(* hauto q:on use:REReds.hne_proj_inv, REReds.hne_ind_inv. *)
|
||||||
|
(* (* ind ind case *) *)
|
||||||
|
(* + move => P a0 b0 c0. *)
|
||||||
|
(* case : b => //=; *)
|
||||||
|
(* lazymatch goal with *)
|
||||||
|
(* | [|- context[algo_metric _ (PInd _ _ _ _) (PInd _ _ _ _)]] => idtac *)
|
||||||
|
(* | _ => move => > /algo_metric_join; clear => *; exfalso *)
|
||||||
|
(* end. *)
|
||||||
|
(* * hauto q:on use:REReds.hne_ind_inv, REReds.var_inv. *)
|
||||||
|
(* * hauto q:on use:REReds.hne_ind_inv, REReds.hne_app_inv. *)
|
||||||
|
(* * hauto q:on use:REReds.hne_ind_inv, REReds.hne_proj_inv. *)
|
||||||
|
(* * move => P1 a1 b1 c1 /[dup] halg /algo_metric_ind + h0 h1. *)
|
||||||
|
(* move /(_ h1 h0). *)
|
||||||
|
(* move => [j][hj][hP][ha][hb]hc Γ A B hL hR. *)
|
||||||
|
(* move /Ind_Inv : hL => [iP0][wtP0][wta0][wtb0][wtc0]hSu0. *)
|
||||||
|
(* move /Ind_Inv : hR => [iP1][wtP1][wta1][wtb1][wtc1]hSu1. *)
|
||||||
|
(* have {}iha : a0 ∼ a1 by qauto l:on. *)
|
||||||
|
(* have [] : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia. *)
|
||||||
|
(* move : T_Univ_Raise wtP0; do!move/[apply]. move => wtP0. *)
|
||||||
|
(* move : T_Univ_Raise wtP1; do!move/[apply]. move => wtP1. *)
|
||||||
|
(* have {}ihP : P ⇔ P1 by qauto l:on. *)
|
||||||
|
(* set Δ := cons _ _ in wtP0, wtP1, wtc0, wtc1. *)
|
||||||
|
(* have wfΔ :⊢ Δ by hauto l:on use:wff_mutual. *)
|
||||||
|
(* have hPE : Δ ⊢ P ≡ P1 ∈ PUniv (max iP0 iP1) *)
|
||||||
|
(* by hauto l:on use:coqeq_sound_mutual. *)
|
||||||
|
(* have haE : Γ ⊢ a0 ≡ a1 ∈ PNat *)
|
||||||
|
(* by hauto l:on use:coqeq_sound_mutual. *)
|
||||||
|
(* have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual. *)
|
||||||
|
(* have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) P ≡ subst_PTm (scons PZero VarPTm) P1 ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max iP0 iP1)). *)
|
||||||
|
(* eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero. *)
|
||||||
|
(* have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P *)
|
||||||
|
(* by eauto using T_Conv_E. *)
|
||||||
|
(* have {}ihb : b0 ⇔ b1 by hauto l:on. *)
|
||||||
|
(* have hPSig : Γ ⊢ PBind PSig PNat P ≡ PBind PSig PNat P1 ∈ PUniv (Nat.max iP0 iP1) by eauto with wt. *)
|
||||||
|
(* set T := ren_PTm shift _ in wtc0. *)
|
||||||
|
(* have : (cons P Δ) ⊢ c1 ∈ T. *)
|
||||||
|
(* apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt. *)
|
||||||
|
(* apply : Su_Eq; eauto. *)
|
||||||
|
(* subst T. apply : weakening_su; eauto. *)
|
||||||
|
(* eapply morphing. apply : Su_Eq. apply E_Symmetric. by eauto. *)
|
||||||
|
(* hauto l:on use:wff_mutual. *)
|
||||||
|
(* apply morphing_ext. set x := funcomp _ _. *)
|
||||||
|
(* have -> : x = funcomp (ren_PTm shift) VarPTm by asimpl. *)
|
||||||
|
(* apply : morphing_ren; eauto using renaming_shift. by apply morphing_id. *)
|
||||||
|
(* apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1. *)
|
||||||
|
(* have {}ihc : c0 ⇔ c1 by qauto l:on. *)
|
||||||
|
(* move => [:ih]. *)
|
||||||
|
(* split. abstract : ih. move : h0 h1 ihP iha ihb ihc. clear. sauto lq:on. *)
|
||||||
|
(* have hEInd : Γ ⊢ PInd P a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P by hfcrush use:coqeq_sound_mutual. *)
|
||||||
|
(* exists (subst_PTm (scons a0 VarPTm) P). *)
|
||||||
|
(* repeat split => //=; eauto with wt. *)
|
||||||
|
(* apply : Su_Transitive. *)
|
||||||
|
(* apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt. *)
|
||||||
|
(* apply : Su_Eq. apply E_Refl. by apply T_Nat'. *)
|
||||||
|
(* apply : Su_Eq. apply hPE. by eauto. *)
|
||||||
|
(* move : hEInd. clear. hauto l:on use:regularity. *)
|
||||||
|
(* Qed. *)
|
||||||
|
|
||||||
Lemma coqeq_sound : forall Γ (a b : PTm) A,
|
Lemma coqeq_sound : forall Γ (a b : PTm) A,
|
||||||
Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b -> Γ ⊢ a ≡ b ∈ A.
|
Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b -> Γ ⊢ a ≡ b ∈ A.
|
||||||
Proof. sfirstorder use:coqeq_sound_mutual. Qed.
|
Proof. sfirstorder use:coqeq_sound_mutual. Qed.
|
||||||
|
|
||||||
Lemma coqeq_complete Γ (a b A : PTm) :
|
(* Lemma coqeq_complete Γ (a b A : PTm) : *)
|
||||||
Γ ⊢ a ≡ b ∈ A -> a ⇔ b.
|
(* Γ ⊢ a ≡ b ∈ A -> a ⇔ b. *)
|
||||||
Proof.
|
(* Proof. *)
|
||||||
move => h.
|
(* move => h. *)
|
||||||
suff : exists k, algo_metric k a b by hauto lq:on use:coqeq_complete', regularity.
|
(* suff : exists k, algo_metric k a b by hauto lq:on use:coqeq_complete', regularity. *)
|
||||||
eapply fundamental_theorem in h.
|
(* eapply fundamental_theorem in h. *)
|
||||||
move /logrel.SemEq_SN_Join : h.
|
(* move /logrel.SemEq_SN_Join : h. *)
|
||||||
move => h.
|
(* move => h. *)
|
||||||
have : exists va vb : PTm,
|
(* have : exists va vb : PTm, *)
|
||||||
rtc LoRed.R a va /\
|
(* rtc LoRed.R a va /\ *)
|
||||||
rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb
|
(* rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb *)
|
||||||
by hauto l:on use:DJoin.standardization_lo.
|
(* by hauto l:on use:DJoin.standardization_lo. *)
|
||||||
move => [va][vb][hva][hvb][nva][nvb]hj.
|
(* move => [va][vb][hva][hvb][nva][nvb]hj. *)
|
||||||
move /relations.rtc_nsteps : hva => [i hva].
|
(* move /relations.rtc_nsteps : hva => [i hva]. *)
|
||||||
move /relations.rtc_nsteps : hvb => [j hvb].
|
(* move /relations.rtc_nsteps : hvb => [j hvb]. *)
|
||||||
exists (i + j + size_PTm va + size_PTm vb).
|
(* exists (i + j + size_PTm va + size_PTm vb). *)
|
||||||
hauto lq:on solve+:lia.
|
(* hauto lq:on solve+:lia. *)
|
||||||
Qed.
|
(* Qed. *)
|
||||||
|
|
||||||
|
|
||||||
Reserved Notation "a ≪ b" (at level 70).
|
Reserved Notation "a ≪ b" (at level 70).
|
||||||
|
|
|
||||||
|
|
@ -284,8 +284,8 @@ Inductive algo_dom : PTm -> PTm -> Prop :=
|
||||||
algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
|
algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
|
||||||
|
|
||||||
| A_Conf a b :
|
| A_Conf a b :
|
||||||
HRed.nf a ->
|
ishf a \/ ishne a ->
|
||||||
HRed.nf b ->
|
ishf b \/ ishne b ->
|
||||||
tm_conf a b ->
|
tm_conf a b ->
|
||||||
algo_dom a b
|
algo_dom a b
|
||||||
|
|
||||||
|
|
@ -376,8 +376,8 @@ Inductive salgo_dom : PTm -> PTm -> Prop :=
|
||||||
salgo_dom a b
|
salgo_dom a b
|
||||||
|
|
||||||
| S_Conf a b :
|
| S_Conf a b :
|
||||||
HRed.nf a ->
|
ishf a \/ ishne a ->
|
||||||
HRed.nf b ->
|
ishf b \/ ishne b ->
|
||||||
stm_conf a b ->
|
stm_conf a b ->
|
||||||
salgo_dom a b
|
salgo_dom a b
|
||||||
|
|
||||||
|
|
@ -417,7 +417,7 @@ Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
|
||||||
|
|
||||||
Ltac2 destruct_salgo () :=
|
Ltac2 destruct_salgo () :=
|
||||||
lazy_match! goal with
|
lazy_match! goal with
|
||||||
| [h : is_true (ishne ?a) |- is_true (stm_conf ?a _) ] =>
|
| [_ : is_true (ishne ?a) |- is_true (stm_conf ?a _) ] =>
|
||||||
if Constr.is_var a then destruct $a; ltac1:(done) else ()
|
if Constr.is_var a then destruct $a; ltac1:(done) else ()
|
||||||
| [|- is_true (stm_conf _ _)] =>
|
| [|- is_true (stm_conf _ _)] =>
|
||||||
unfold stm_conf; ltac1:(done)
|
unfold stm_conf; ltac1:(done)
|
||||||
|
|
|
||||||
|
|
@ -226,7 +226,7 @@ Ltac check_sub_triv :=
|
||||||
intros;subst;
|
intros;subst;
|
||||||
lazymatch goal with
|
lazymatch goal with
|
||||||
(* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
|
(* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
|
||||||
| [h : salgo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
|
| [_ : salgo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
|
||||||
| _ => idtac
|
| _ => idtac
|
||||||
end.
|
end.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -246,9 +246,6 @@ Proof.
|
||||||
move => /negP h0.
|
move => /negP h0.
|
||||||
eapply check_equal_complete in h0.
|
eapply check_equal_complete in h0.
|
||||||
apply h0. by constructor.
|
apply h0. by constructor.
|
||||||
- move => a b i0 i1 j. simp ce_prop.
|
|
||||||
move => _ h. inversion h; subst => //=.
|
|
||||||
hauto lq:on inv:CoqEq_Neu unfold:stm_conf.
|
|
||||||
- move => a b s ihs. simp ce_prop.
|
- move => a b s ihs. simp ce_prop.
|
||||||
move => h0 h1. apply ihs =>//.
|
move => h0 h1. apply ihs =>//.
|
||||||
have [? ?] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
|
have [? ?] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue