diff --git a/theories/algorithmic.v b/theories/algorithmic.v index c8a4799..a870f9f 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -1345,10 +1345,74 @@ Lemma coqeq_complete' : apply DJoin.symmetric. apply DJoin.FromEJoin. eexists. split. apply relations.rtc_once. apply ERed.AppEta. apply rtc_refl. - hauto q:on use:coqeq_symmetric_mutual, DJoin.symmetric, algo_dom_sym. - - move {hhAbsNeu hhPairNeu}. - admit. - - move {hhAbsNeu}. abstract : hhPairNeu. - admit. + - move {hhAbsNeu hhPairNeu hConfNeuNf}. + move => a0 a1 b0 b1 doma iha domb ihb /DJoin.pair_inj hj. + split => //. + move => Γ A wt0 wt1. + have [] : SN (PPair a0 b0) /\ SN (PPair a1 b1) by hauto lq:on use:logrel.SemWt_SN, fundamental_theorem. + move : hj; repeat move/[apply]. + move => [hja hjb]. + move /Pair_Inv : wt0 => [A0][B0][ha0][hb0]hSu0. + move /Pair_Inv : wt1 => [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 : iha (ha0A2) (ha1A2) hja; repeat move/[apply]. + move => h. + apply CE_Nf. + 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 ihb; 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. + - abstract : hhPairNeu. move {hConfNeuNf}. + move => a0 b0 u neu doma iha domb ihb hj. + split => // Γ A /[dup] wt /Pair_Inv + [A0][B0][ha0][hb0]hU. + move => wtu. + 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. + have heL : a0 ⇔ PProj PL u . apply : iha; eauto. + apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto. + apply : N_Exp; eauto. apply N_ProjPairL. + hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. + hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. + apply DJoin.FromRRed1. apply RRed.ProjPair. + eapply CE_HRed; eauto using rtc_refl. + apply CE_PairNeu; eauto. + eapply ihb; eauto. + apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto. + apply : N_Exp; eauto. apply N_ProjPairR. + hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. + hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. + apply DJoin.FromRRed1. apply RRed.ProjPair. + apply : T_Conv; eauto. + have {}hE : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i + by hauto l:on use:regularity. + have /E_Symmetric : Γ ⊢ a0 ≡ PProj PL u ∈ A2 by + hauto l:on use:coqeq_sound_mutual. + hauto l:on use:bind_inst. - move {hhAbsNeu}. move => a0 a1 u hu ha iha hb ihb /DJoin.symmetric hj. split => // *. eapply coqeq_symmetric_mutual. @@ -1577,490 +1641,30 @@ Lemma coqeq_complete' : apply : DJoin.transitive; eauto. hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. apply DJoin.FromRRed0. by apply HRed.ToRRed. -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. *) +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).