diff --git a/theories/algorithmic.v b/theories/algorithmic.v
index ace67ac..eb93263 100644
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
@@ -1302,6 +1302,17 @@ Proof.
hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
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' :
(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).
@@ -1341,489 +1352,654 @@ Lemma coqeq_complete' :
move => Γ A /Suc_Inv ? /Suc_Inv ?. apply CE_Nf. hauto lq:on ctrs:CoqEq.
- move => i j /DJoin.univ_inj ?. subst.
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.
+ move => hbd0 hbd1.
+ have {hbd0} : exists i, Γ ⊢ PBind p1 A0 B0 ∈ PUniv i by move /Bind_Inv in hbd0; qauto use:T_Bind.
+ move => [i] => hbd0.
+ have {hbd1} : exists i, Γ ⊢ PBind p1 A1 B1 ∈ PUniv i by move /Bind_Inv in hbd1; qauto use:T_Bind.
+ move => [j] => hbd1.
+ have /Bind_Univ_Inv {hbd0} [? ?] : Γ ⊢ PBind p1 A0 B0 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
+ have /Bind_Univ_Inv {hbd1} [? ?] : Γ ⊢ PBind p1 A1 B1 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
+ move => [:eqa].
+ apply CE_Nf. constructor; first by abstract : eqa; eauto.
+ eapply ihB; eauto. apply : ctx_eq_subst_one; eauto.
+ apply : Su_Eq; eauto. sfirstorder use:coqeq_sound_mutual.
+ - hauto l:on.
+ - move => {hhAbsNeu hhPairNeu} i j /DJoin.var_inj ?. subst. apply ce_neu_neu_helper => // Γ A B.
+ move /Var_Inv => [h [A0 [h0 h1]]].
+ move /Var_Inv => [h' [A1 [h0' h1']]].
+ split. by constructor.
+ suff : A0 = A1 by hauto lq:on db:wt.
+ eauto using lookup_deter.
+ - move => u0 u1 a0 a1 neu0 neu1 domu ihu doma iha. move /DJoin.hne_app_inj /(_ neu0 neu1) => [hju hja].
+ apply ce_neu_neu_helper => //= Γ A B.
+ move /App_Inv => [A0][B0][hb0][ha0]hS0.
+ move /App_Inv => [A1][B1][hb1][ha1]hS1.
+ move /(_ hju) : ihu.
+ move => [_ ihb].
+ move : ihb (neu0) (neu1) 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 : iha hja. repeat move/[apply].
+ move => iha.
+ move : iha (ha0') (ha1'); repeat move/[apply].
+ move => iha.
+ split. sauto lq:on.
+ 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.
+ - move => p0 p1 a0 a1 hne0 hne1 doma iha /DJoin.hne_proj_inj /(_ hne0 hne1) [? hja]. subst.
+ move : iha hja; repeat move/[apply].
+ move => [_ iha]. apply ce_neu_neu_helper => // Γ A B.
+ move : iha (hne0) (hne1);repeat move/[apply].
+ move => ih.
+ case : p1.
+ ** move => 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 => 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 {hhPairNeu hhAbsNeu}.
+ move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc /hne_ind_inj.
+ move => /(_ neu0 neu1) [hjP][hju][hjb]hjc.
+ apply ce_neu_neu_helper => // Γ A B.
+ move /Ind_Inv => [iP0][wtP0][wta0][wtb0][wtc0]hSu0.
+ move /Ind_Inv => [iP1][wtP1][wta1][wtb1][wtc1]hSu1.
+ have {}iha : u0 ∼ u1 by qauto l:on.
+ have [] : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia.
+ move : T_Univ_Raise wtP0; repeat move/[apply]. move => wtP0.
+ move : T_Univ_Raise wtP1; repeat move/[apply]. move => wtP1.
+ have {}ihP : P0 ⇔ P1 by qauto l:on.
+ set Δ := cons _ _ in wtP0, wtP1, wtc0, wtc1.
+ have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
+ have hPE : Δ ⊢ P0 ≡ P1 ∈ PUniv (max iP0 iP1)
+ by hauto l:on use:coqeq_sound_mutual.
+ have haE : Γ ⊢ u0 ≡ u1 ∈ 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) 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.
+ have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P0
+ by eauto using T_Conv_E.
+ have {}ihb : b0 ⇔ b1 by hauto l:on.
+ 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.
+ have : (cons P0 Δ) ⊢ 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 : neu0 neu1 ihP iha ihb ihc. clear. sauto lq:on.
+ 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 u0 VarPTm) P0).
+ 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.
+ - 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 => //.
+(* 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. *)
- 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.
+(* 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 => //. *)
- 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.
+(* 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,
Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b -> Γ ⊢ a ≡ b ∈ A.
Proof. sfirstorder use:coqeq_sound_mutual. Qed.
-Lemma coqeq_complete Γ (a b A : PTm) :
- Γ ⊢ a ≡ b ∈ A -> a ⇔ b.
-Proof.
- move => h.
- suff : exists k, algo_metric k a b by hauto lq:on use:coqeq_complete', regularity.
- eapply fundamental_theorem in h.
- move /logrel.SemEq_SN_Join : h.
- move => h.
- have : exists va vb : PTm,
- rtc LoRed.R a va /\
- rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb
- by hauto l:on use:DJoin.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 coqeq_complete Γ (a b A : PTm) : *)
+(* Γ ⊢ a ≡ b ∈ A -> a ⇔ b. *)
+(* Proof. *)
+(* move => h. *)
+(* suff : exists k, algo_metric k a b by hauto lq:on use:coqeq_complete', regularity. *)
+(* eapply fundamental_theorem in h. *)
+(* move /logrel.SemEq_SN_Join : h. *)
+(* move => h. *)
+(* have : exists va vb : PTm, *)
+(* rtc LoRed.R a va /\ *)
+(* rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb *)
+(* by hauto l:on use:DJoin.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. *)
Reserved Notation "a ≪ b" (at level 70).
diff --git a/theories/common.v b/theories/common.v
index 18f4dfb..39713ba 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -284,8 +284,8 @@ Inductive algo_dom : PTm -> PTm -> Prop :=
algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
| A_Conf a b :
- HRed.nf a ->
- HRed.nf b ->
+ ishf a \/ ishne a ->
+ ishf b \/ ishne b ->
tm_conf a b ->
algo_dom a b
@@ -376,8 +376,8 @@ Inductive salgo_dom : PTm -> PTm -> Prop :=
salgo_dom a b
| S_Conf a b :
- HRed.nf a ->
- HRed.nf b ->
+ ishf a \/ ishne a ->
+ ishf b \/ ishne b ->
stm_conf a b ->
salgo_dom a b
@@ -417,7 +417,7 @@ Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
Ltac2 destruct_salgo () :=
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 ()
| [|- is_true (stm_conf _ _)] =>
unfold stm_conf; ltac1:(done)
diff --git a/theories/executable.v b/theories/executable.v
index 238fe45..e62e3c3 100644
--- a/theories/executable.v
+++ b/theories/executable.v
@@ -226,7 +226,7 @@ Ltac check_sub_triv :=
intros;subst;
lazymatch goal with
(* | [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
end.
diff --git a/theories/executable_correct.v b/theories/executable_correct.v
index d51af9d..4b76638 100644
--- a/theories/executable_correct.v
+++ b/theories/executable_correct.v
@@ -246,9 +246,6 @@ Proof.
move => /negP h0.
eapply check_equal_complete in h0.
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 => h0 h1. apply ihs =>//.
have [? ?] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.