diff --git a/theories/algorithmic.v b/theories/algorithmic.v index 184872d..ab8fe97 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -5,6 +5,7 @@ Require Import ssreflect ssrbool. Require Import Psatz. From stdpp Require Import relations (rtc(..), nsteps(..)). Require Import Coq.Logic.FunctionalExtensionality. +Require Import Cdcl.Itauto. Module HRed. Lemma ToRRed (a b : PTm) : HRed.R a b -> RRed.R a b. @@ -97,7 +98,7 @@ Proof. - move => u v hC /andP [h0 h1] /synsub_to_usub ?. exfalso. suff : SNe (PApp u v) by hauto l:on use:Sub.bind_sne_noconf. - eapply ne_nf_embed => //=. sfirstorder b:on. + eapply ne_nf_embed => //=. itauto. - move => p0 p1 hC h ?. exfalso. have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity. hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv. @@ -198,7 +199,7 @@ Proof. - move => u v hC /andP [h0 h1] /synsub_to_usub ?. exfalso. suff : SNe (PApp u v) by hauto l:on use:Sub.sne_bind_noconf. - eapply ne_nf_embed => //=. sfirstorder b:on. + eapply ne_nf_embed => //=. itauto. - move => p0 p1 hC h ?. exfalso. have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity. hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv. @@ -251,6 +252,22 @@ Proof. apply : ctx_eq_subst_one; eauto. Qed. +Lemma T_Univ_Raise Γ (a : PTm) i j : + Γ ⊢ a ∈ PUniv i -> + i <= j -> + Γ ⊢ a ∈ PUniv j. +Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed. + +Lemma Bind_Univ_Inv Γ p (A : PTm) B i : + Γ ⊢ PBind p A B ∈ PUniv i -> + Γ ⊢ A ∈ PUniv i /\ (cons A Γ) ⊢ B ∈ PUniv i. +Proof. + move /Bind_Inv. + move => [i0][hA][hB]h. + move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]]. + sfirstorder use:T_Univ_Raise. +Qed. + Lemma Abs_Pi_Inv Γ (a : PTm) A B : Γ ⊢ PAbs a ∈ PBind PPi A B -> (cons A Γ) ⊢ a ∈ B. @@ -271,48 +288,6 @@ Proof. by asimpl; rewrite subst_scons_id. Qed. -Lemma T_Abs_Neu_Inv Γ (a u : PTm) U : - Γ ⊢ PAbs a ∈ U -> - Γ ⊢ u ∈ U -> - exists Δ V, Δ ⊢ a ∈ V /\ Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ V. -Proof. - move => /[dup] ha' + hu. - move /Abs_Inv => [A0][B0][ha]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. - exists Δ, B2. split => //. - by move /Abs_Pi_Inv in ha''. -Qed. - -Lemma T_Univ_Raise Γ (a : PTm) i j : - Γ ⊢ a ∈ PUniv i -> - i <= j -> - Γ ⊢ a ∈ PUniv j. -Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed. - -Lemma Bind_Univ_Inv Γ p (A : PTm) B i : - Γ ⊢ PBind p A B ∈ PUniv i -> - Γ ⊢ A ∈ PUniv i /\ (cons A Γ) ⊢ B ∈ PUniv i. -Proof. - move /Bind_Inv. - move => [i0][hA][hB]h. - move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]]. - sfirstorder use:T_Univ_Raise. -Qed. - Lemma Pair_Sig_Inv Γ (a b : PTm) A B : Γ ⊢ PPair a b ∈ PBind PSig A B -> Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B. @@ -447,18 +422,6 @@ Proof. hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R. Qed. -Lemma CE_HRedR (a b b' : PTm) : - HRed.R b b' -> - a ⇔ b' -> - a ⇔ b. -Proof. - hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R. -Qed. - -Lemma CE_Nf a b : - a ↔ b -> a ⇔ b. -Proof. hauto l:on ctrs:rtc. Qed. - Scheme coqeq_neu_ind := Induction for CoqEq_Neu Sort Prop with coqeq_ind := Induction for CoqEq Sort Prop @@ -710,12 +673,8 @@ Proof. hauto lq:on use:HReds.ToEq, E_Symmetric, E_Transitive. Qed. -Definition term_metric k (a b : PTm) := - exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k. - -Lemma term_metric_sym k (a b : PTm) : - term_metric k a b -> term_metric k b a. -Proof. hauto lq:on unfold:term_metric solve+:lia. Qed. +Definition algo_metric k (a b : PTm) := + exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ EJoin.R va vb /\ size_PTm va + size_PTm vb + i + j <= k. Lemma ne_hne (a : PTm) : ne a -> ishne a. Proof. elim : a => //=; sfirstorder b:on. Qed. @@ -739,56 +698,37 @@ Proof. - hauto lq:on use:ne_hne. Qed. -Lemma term_metric_case k (a b : PTm) : - term_metric k a b -> - (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ term_metric k' a' b /\ k' < k. +Lemma algo_metric_case k (a b : PTm) : + algo_metric k a b -> + (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ algo_metric k' a' b /\ k' < k. Proof. - move=>[i][j][va][vb][h0] [h1][h2][h3]h4. + move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6. case : a h0 => //=; try firstorder. - inversion h0 as [|A B C D E F]; subst. hauto qb:on use:ne_hne. inversion E; subst => /=. - + hauto lq:on use:HRed.AppAbs unfold:term_metric solve+:lia. - + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia. + + hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. + sfirstorder qb:on use:ne_hne. - inversion h0 as [|A B C D E F]; subst. hauto qb:on use:ne_hne. inversion E; subst => /=. - + hauto lq:on use:HRed.ProjPair unfold:term_metric solve+:lia. - + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia. + + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. - inversion h0 as [|A B C D E F]; subst. hauto qb:on use:ne_hne. inversion E; subst => /=. - + hauto lq:on use:HRed.IndZero unfold:term_metric solve+:lia. - + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia. + + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. + sfirstorder use:ne_hne. - + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. + sfirstorder use:ne_hne. + sfirstorder use:ne_hne. Qed. -Lemma A_Conf' a b : - ishf a \/ ishne a -> - ishf b \/ ishne b -> - tm_conf a b -> - algo_dom_r a b. -Proof. - move => ha hb. - move => ?. - apply A_NfNf. - apply A_Conf; sfirstorder use:hf_no_hred, hne_no_hred. -Qed. - -Lemma hne_nf_ne (a : PTm ) : - ishne a -> nf a -> ne a. -Proof. case : a => //=. Qed. - -Lemma lored_nsteps_renaming k (a b : PTm) (ξ : nat -> nat) : - nsteps LoRed.R k a b -> - nsteps LoRed.R k (ren_PTm ξ a) (ren_PTm ξ b). -Proof. - induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming. -Qed. +Lemma algo_metric_sym k (a b : PTm) : + algo_metric k a b -> algo_metric k b a. +Proof. hauto lq:on unfold:algo_metric solve+:lia. Qed. Lemma hred_hne (a b : PTm) : HRed.R a b -> @@ -946,18 +886,6 @@ Proof. hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Abs_Inv. Qed. -Lemma T_ZeroUniv_Imp' Γ i : - Γ ⊢ PZero ∈ PUniv i -> False. -Proof. - hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Zero_Inv. -Qed. - -Lemma T_SucUniv_Imp' Γ (a : PTm) i : - Γ ⊢ PSuc a ∈ PUniv i -> False. -Proof. - hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Suc_Inv. -Qed. - Lemma T_PairUniv_Imp' Γ (a b : PTm) i : Γ ⊢ PPair a b ∈ PUniv i -> False. Proof. @@ -1100,6 +1028,34 @@ Proof. exists (S i), a1. hauto lq:on ctrs:nsteps solve+:lia. Qed. +Lemma algo_metric_proj k p0 p1 (a0 a1 : PTm) : + algo_metric k (PProj p0 a0) (PProj p1 a1) -> + ishne a0 -> + ishne a1 -> + p0 = p1 /\ exists j, j < k /\ algo_metric j a0 a1. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 hne0 hne1. + move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply]. + move => [i0][a2][hi][?]ha02. subst. + move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply]. + move => [i1][a3][hj][?]ha13. subst. + simpl in *. + move /EJoin.hne_proj_inj : h4 => [h40 h41]. subst. + split => //. + exists (k - 1). split. simpl in *; lia. + rewrite/algo_metric. + do 4 eexists. repeat split; eauto. sfirstorder use:ne_nf. + sfirstorder use:ne_nf. + lia. +Qed. + + +Lemma hreds_nf_refl a b : + HRed.nf a -> + rtc HRed.R a b -> + a = b. +Proof. inversion 2; sfirstorder. Qed. + Lemma lored_nsteps_app_cong k (a0 a1 b : PTm) : nsteps LoRed.R k a0 a1 -> ishne a0 -> @@ -1147,542 +1103,656 @@ Lemma lored_nsteps_pair_inv k (a0 b0 C : PTm ) : exists i, (S j), a1, b1. sauto lq:on solve+:lia. Qed. -Lemma term_metric_abs : forall k a b, - term_metric k (PAbs a) (PAbs b) -> - exists k', k' < k /\ term_metric k' a b. -Proof. - move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h. - apply lored_nsteps_abs_inv in hva, hvb. - move : hva => [a'][hva]?. subst. - move : hvb => [b'][hvb]?. subst. - simpl in *. exists (k - 1). - hauto lq:on unfold:term_metric solve+:lia. +Lemma algo_metric_join k (a b : PTm ) : + algo_metric k a b -> + DJoin.R a b. + rewrite /algo_metric. + move => [i][j][va][vb][h0][h1][h2][h3][[v [h40 h41]]]h5. + have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps. + have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps. + apply REReds.FromEReds in h40,h41. + apply LoReds.ToRReds in h0,h1. + apply REReds.FromRReds in h0,h1. + rewrite /DJoin.R. exists v. sfirstorder use:@relations.rtc_transitive. Qed. -Lemma term_metric_pair : forall k a0 b0 a1 b1, - term_metric k (PPair a0 b0) (PPair a1 b1) -> - exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1. -Proof. - move => k a0 b0 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h. - apply lored_nsteps_pair_inv in hva, hvb. - decompose record hva => {hva}. - decompose record hvb => {hvb}. subst. +Lemma algo_metric_pair k (a0 b0 a1 b1 : PTm) : + SN (PPair a0 b0) -> + SN (PPair a1 b1) -> + algo_metric k (PPair a0 b0) (PPair a1 b1) -> + exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1. + move => sn0 sn1 /[dup] /algo_metric_join hj. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. + move : lored_nsteps_pair_inv h0;repeat move/[apply]. + move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. + move : lored_nsteps_pair_inv h1;repeat move/[apply]. + move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. simpl in *. exists (k - 1). - hauto lqb:on solve+:lia. + move /andP : h2 => [h20 h21]. + move /andP : h3 => [h30 h31]. + suff : EJoin.R a2 a3 /\ EJoin.R b2 b3 by hauto lq:on solve+:lia. + hauto l:on use:DJoin.ejoin_pair_inj. Qed. -Lemma term_metric_bind : forall k p0 a0 b0 p1 a1 b1, - term_metric k (PBind p0 a0 b0) (PBind p1 a1 b1) -> - exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1. +Lemma hne_nf_ne (a : PTm ) : + ishne a -> nf a -> ne a. +Proof. case : a => //=. Qed. + +Lemma lored_nsteps_renaming k (a b : PTm) (ξ : nat -> nat) : + nsteps LoRed.R k a b -> + nsteps LoRed.R k (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => k p0 a0 b0 p1 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h. - apply lored_nsteps_bind_inv in hva, hvb. - decompose record hva => {hva}. - decompose record hvb => {hvb}. subst. - simpl in *. exists (k - 1). - hauto lqb:on solve+:lia. + induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming. Qed. -Lemma term_metric_suc : forall k a b, - term_metric k (PSuc a) (PSuc b) -> - exists k', k' < k /\ term_metric k' a b. -Proof. - move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h. - apply lored_nsteps_suc_inv in hva, hvb. - move : hva => [a'][hva]?. subst. - move : hvb => [b'][hvb]?. subst. - simpl in *. exists (k - 1). - hauto lq:on unfold:term_metric solve+:lia. -Qed. - -Lemma term_metric_abs_neu k (a0 : PTm) u : - term_metric k (PAbs a0) u -> +Lemma algo_metric_neu_abs k (a0 : PTm) u : + algo_metric k u (PAbs a0) -> ishne u -> - exists j, j < k /\ term_metric j a0 (PApp (ren_PTm shift u) (VarPTm var_zero)). + exists j, j < k /\ algo_metric j (PApp (ren_PTm shift u) (VarPTm var_zero)) a0. Proof. - move => [i][j][va][vb][h0][h1][h2][h3]h4 neu. - have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps. - move /lored_nsteps_abs_inv : h0 => [a1][h01]?. subst. - exists (k - 1). - simpl in *. split. lia. - exists i,j,a1,(PApp (ren_PTm shift vb) (VarPTm var_zero)). - repeat split => //=. - apply lored_nsteps_app_cong. - by apply lored_nsteps_renaming. - by rewrite ishne_ren. - rewrite Bool.andb_true_r. - sfirstorder use:ne_nf_ren. - rewrite size_PTm_ren. lia. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 neu. + have neva : ne va by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps. + move /lored_nsteps_abs_inv : h1 => [a1][h01]?. subst. + exists (k - 1). simpl in *. split. lia. + have {}h0 : nsteps LoRed.R i (ren_PTm shift u) (ren_PTm shift va) + by eauto using lored_nsteps_renaming. + have {}h0 : nsteps LoRed.R i (PApp (ren_PTm shift u) (VarPTm var_zero)) (PApp (ren_PTm shift va) (VarPTm var_zero)). + apply lored_nsteps_app_cong => //=. + scongruence use:ishne_ren. + do 4 eexists. repeat split; eauto. + hauto b:on use:ne_nf_ren. + have h : EJoin.R (PAbs (PApp (ren_PTm shift va) (VarPTm var_zero))) (PAbs a1) by hauto q:on ctrs:rtc,ERed.R. + apply DJoin.ejoin_abs_inj; eauto. + hauto b:on drew:off use:ne_nf_ren. + simpl in *. rewrite size_PTm_ren. lia. Qed. -Lemma term_metric_pair_neu k (a0 b0 : PTm) u : - term_metric k (PPair a0 b0) u -> +Lemma algo_metric_neu_pair k (a0 b0 : PTm) u : + algo_metric k u (PPair a0 b0) -> ishne u -> - exists j, j < k /\ term_metric j (PProj PL u) a0 /\ term_metric j (PProj PR u) b0. + exists j, j < k /\ algo_metric j (PProj PL u) a0 /\ algo_metric j (PProj PR u) b0. Proof. - move => [i][j][va][vb][h0][h1][h2][h3]h4 neu. - have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps. - move /lored_nsteps_pair_inv : h0 => [i0][j0][a1][b1][?][?][?][?]?. subst. - exists (k-1). sauto qb:on use:lored_nsteps_proj_cong unfold:term_metric solve+:lia. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 neu. + move /lored_nsteps_pair_inv : h1. + move => [i0][j0][a1][b1][hi][hj][?][ha01]hb01. subst. + simpl in *. + have ? : ishne va by + hauto lq:on use:loreds_hne_preservation, @relations.rtc_nsteps. + have ? : ne va by sfirstorder use:hne_nf_ne. + exists (k - 1). split. lia. + move :lored_nsteps_proj_cong (neu) h0; repeat move/[apply]. + move => h. have hL := h PL. have {h} hR := h PR. + suff [? ?] : EJoin.R (PProj PL va) a1 /\ EJoin.R (PProj PR va) b1. + rewrite /algo_metric. + split; do 4 eexists; repeat split;eauto; sfirstorder b:on solve+:lia. + eapply DJoin.ejoin_pair_inj; hauto qb:on ctrs:rtc, ERed.R. Qed. -Lemma term_metric_app k (a0 b0 a1 b1 : PTm) : - term_metric k (PApp a0 b0) (PApp a1 b1) -> +Lemma algo_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 : + algo_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) -> ishne a0 -> ishne a1 -> - exists j, j < k /\ term_metric j a0 a1 /\ term_metric j b0 b1. + exists j, j < k /\ algo_metric j P0 P1 /\ algo_metric j a0 a1 /\ + algo_metric j b0 b1 /\ algo_metric j c0 c1. Proof. - move => [i][j][va][vb][h0][h1][h2][h3]h4. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 hne0 hne1. + move /lored_nsteps_ind_inv /(_ hne0) : h0. + move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst. + move /lored_nsteps_ind_inv /(_ hne1) : h1. + move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst. + move /EJoin.ind_inj : h4. + move => [?][?][?]?. + exists (k -1). simpl in *. + hauto lq:on rew:off use:ne_nf b:on solve+:lia. +Qed. + +Lemma algo_metric_app k (a0 b0 a1 b1 : PTm) : + algo_metric k (PApp a0 b0) (PApp a1 b1) -> + ishne a0 -> + ishne a1 -> + exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. move => hne0 hne1. move : lored_nsteps_app_inv h0 (hne0);repeat move/[apply]. move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. move : lored_nsteps_app_inv h1 (hne1);repeat move/[apply]. move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. - simpl in *. exists (k - 1). hauto lqb:on use:lored_nsteps_app_cong, ne_nf unfold:term_metric solve+:lia. + simpl in *. exists (k - 1). + move /andP : h2 => [h20 h21]. + move /andP : h3 => [h30 h31]. + move /EJoin.hne_app_inj : h4 => [h40 h41]. + split. lia. + split. + + rewrite /algo_metric. + exists i0,j0,a2,a3. + repeat split => //=. + sfirstorder b:on use:ne_nf. + sfirstorder b:on use:ne_nf. + lia. + + rewrite /algo_metric. + exists i1,j1,b2,b3. + repeat split => //=; sfirstorder b:on use:ne_nf. Qed. -Lemma term_metric_proj k p0 p1 (a0 a1 : PTm) : - term_metric k (PProj p0 a0) (PProj p1 a1) -> - ishne a0 -> - ishne a1 -> - exists j, j < k /\ term_metric j a0 a1. +Lemma algo_metric_suc k (a0 a1 : PTm) : + algo_metric k (PSuc a0) (PSuc a1) -> + exists j, j < k /\ algo_metric j a0 a1. Proof. - move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1. - move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply]. - move => [i0][a2][hi][?]ha02. subst. - move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply]. - move => [i1][a3][hj][?]ha13. subst. - exists (k- 1). hauto q:on use:ne_nf solve+:lia. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. + exists (k - 1). + move /lored_nsteps_suc_inv : h0. + move => [a0'][ha0]?. subst. + move /lored_nsteps_suc_inv : h1. + move => [b0'][hb0]?. subst. simpl in *. + split; first by lia. + rewrite /algo_metric. + hauto lq:on rew:off use:EJoin.suc_inj solve+:lia. Qed. -Lemma term_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 : - term_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) -> - ishne a0 -> - ishne a1 -> - exists j, j < k /\ term_metric j P0 P1 /\ term_metric j a0 a1 /\ - term_metric j b0 b1 /\ term_metric j c0 c1. +Lemma algo_metric_bind k p0 (A0 : PTm ) B0 p1 A1 B1 : + algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) -> + p0 = p1 /\ exists j, j < k /\ algo_metric j A0 A1 /\ algo_metric j B0 B1. Proof. - move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1. - move /lored_nsteps_ind_inv /(_ hne0) : h0. - move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst. - move /lored_nsteps_ind_inv /(_ hne1) : h1. - move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst. - exists (k -1). simpl in *. - hauto lq:on rew:off use:ne_nf b:on solve+:lia. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. + move : lored_nsteps_bind_inv h0 => /[apply]. + move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. + move : lored_nsteps_bind_inv h1 => /[apply]. + move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. + move /EJoin.bind_inj : h4 => [?][hEa]hEb. subst. + split => //. + exists (k - 1). split. simpl in *; lia. + simpl in *. + split. + - exists i0,j0,a2,a3. + repeat split => //=; sfirstorder b:on solve+:lia. + - exists i1,j1,b2,b3. sfirstorder b:on solve+:lia. Qed. -Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b. + +Lemma coqeq_complete' k (a b : PTm ) : + 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 => [:hneL]. + move : k a b. elim /Wf_nat.lt_wf_ind. - move => n ih a b h. - case /term_metric_case : (h); cycle 1. - move => [k'][a'][h0][h1]h2. - by apply : A_HRedL; eauto. - case /term_metric_sym /term_metric_case : (h); cycle 1. - move => [k'][b'][hb][/term_metric_sym h0]h1. - move => ha. have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred. - by apply : A_HRedR; eauto. - move => /[swap]. - case => hfa; case => hfb. - - move : hfa hfb h. - case : a; case : b => //=; eauto 5 using A_Conf' with adom. - + hauto lq:on use:term_metric_abs db:adom. - + hauto lq:on use:term_metric_pair db:adom. - + hauto lq:on use:term_metric_bind db:adom. - + hauto lq:on use:term_metric_suc db:adom. - - abstract : hneL n ih a b h hfa hfb. - case : a hfa h => //=. - + hauto lq:on use:term_metric_abs_neu db:adom. - + scrush use:term_metric_pair_neu db:adom. - + case : b hfb => //=; eauto 5 using A_Conf' with adom. - + case : b hfb => //=; eauto 5 using A_Conf' with adom. - + case : b hfb => //=; eauto 5 using A_Conf' with adom. - + case : b hfb => //=; eauto 5 using A_Conf' with adom. - + case : b hfb => //=; eauto 5 using A_Conf' with adom. - - hauto q:on use:algo_dom_sym, term_metric_sym. - - move {hneL}. - case : b hfa hfb h => //=; case a => //=; eauto 5 using A_Conf' with adom. - + move => a0 b0 a1 b1 nfa0 nfa1. - move /term_metric_app /(_ nfa0 nfa1) => [j][hj][ha]hb. - apply A_NfNf. - (* apply A_NfNf. apply A_NeuNeu. apply A_AppCong => //; eauto. *) - have nfa0' : HRed.nf a0 by sfirstorder use:hne_no_hred. - have nfb0' : HRed.nf a1 by sfirstorder use:hne_no_hred. - have ha0 : algo_dom a0 a1 by eauto using algo_dom_r_algo_dom. - constructor => //. eauto. - + move => p0 A0 p1 A1 neA0 neA1. - have {}nfa0 : HRed.nf A0 by sfirstorder use:hne_no_hred. - have {}nfb0 : HRed.nf A1 by sfirstorder use:hne_no_hred. - hauto lq:on use:term_metric_proj, algo_dom_r_algo_dom db:adom. - + move => P0 a0 b0 c0 P1 a1 b1 c1 nea0 nea1. - have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred. - have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred. - hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom. -Qed. + 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. -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. + 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 => //. -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. + 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. -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). - move => [:hConfNeuNf hhPairNeu hhAbsNeu]. - apply algo_dom_mutual. - - move => a b h ih hj. split => //. - move => Γ A. move : T_Abs_Inv; repeat move/[apply]. - move => [Δ][V][h0]h1. - have [? ?] : SN a /\ SN b by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - apply CE_Nf. constructor. apply : ih; eauto using DJoin.abs_inj. - - abstract : hhAbsNeu. - move => a u hu ha iha hj => //. - split => //= Γ A. - move => + h. have ? : SN u by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - move : T_Abs_Neu_Inv h; repeat move/[apply]. - move => [Δ][V][ha']hu'. - apply CE_Nf. constructor => //. apply : iha; eauto. - apply DJoin.abs_inj. - hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - apply : DJoin.transitive; eauto. - 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 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. - eapply algo_dom_sym in ha, hb. - eapply hhPairNeu => //=; eauto; hauto lq:on use:DJoin.symmetric, coqeq_symmetric_mutual. - - move {hhPairNeu hhAbsNeu}. hauto l:on. - - move {hhPairNeu hhAbsNeu}. - move => a0 a1 ha iha /DJoin.suc_inj hj. split => //. - 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 => {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}. - case : hb; case : ha. - + move {hConfNeuNf}. - move => h0 h1 h2 h3. split; last by sfirstorder use:hf_not_hne. - move : h0 h1 h2 h3. - case : b; case : a => //= *; try by (exfalso; eauto 2 using T_AbsPair_Imp, T_AbsUniv_Imp, T_AbsBind_Imp, T_AbsNat_Imp, T_AbsZero_Imp, T_AbsSuc_Imp, T_PairUniv_Imp, T_PairBind_Imp, T_PairNat_Imp, T_PairZero_Imp, T_PairSuc_Imp). - sfirstorder use:DJoin.bind_univ_noconf. - hauto q:on use:REReds.nat_inv, REReds.bind_inv. - hauto q:on use:REReds.zero_inv, REReds.bind_inv. - hauto q:on use:REReds.suc_inv, REReds.bind_inv. - hauto q:on use:REReds.bind_inv, REReds.univ_inv. - hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv. - hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv. - hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv. - hauto lq:on rew:off use:REReds.bind_inv, REReds.nat_inv. - hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv. - hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv. - hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv. - hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv. - hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv. - hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv. - hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv. - hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv. - hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv. - hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv. - hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv. - + abstract : hConfNeuNf a b. - move => h0 h1 h2 h3. split; last by sfirstorder use:hf_not_hne. - move : h0 h1 h2 h3. - case : b; case : a => //=; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv, REReds.bind_inv, REReds.nat_inv, REReds.univ_inv, REReds.zero_inv, REReds.suc_inv. - + rewrite tm_conf_sym. - move => h0 h1 h2 /DJoin.symmetric hb. - move : hConfNeuNf h0 h1 h2 hb; repeat move/[apply]. - qauto l:on use:coqeq_symmetric_mutual. - + move => neua neub hconf hj. - move {hConfNeuNf}. - exfalso. - move : neua neub hconf hj. - case : b; case : a => //=*; exfalso; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv. - - sfirstorder. - - move {hConfNeuNf hhPairNeu hhAbsNeu}. - move => a a' b hr ha iha hj Γ A wta wtb. - apply : CE_HRedL; eauto. - apply : iha; eauto; last by sfirstorder use:HRed.preservation. - apply : DJoin.transitive; eauto. - hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - apply DJoin.FromRRed1. by apply HRed.ToRRed. - - move {hConfNeuNf hhPairNeu hhAbsNeu}. - move => a b b' nfa hr h ih j Γ A wta wtb. - apply : CE_HRedR; eauto. - apply : ih; eauto; last by eauto using HRed.preservation. - apply : DJoin.transitive; eauto. - hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - apply DJoin.FromRRed0. by apply HRed.ToRRed. + 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 sn_term_metric (a b : PTm) : SN a -> SN b -> exists k, term_metric k a b. -Proof. - move /LoReds.FromSN => [va [ha0 ha1]]. - move /LoReds.FromSN => [vb [hb0 hb1]]. - eapply relations.rtc_nsteps in ha0. - eapply relations.rtc_nsteps in hb0. - hauto lq:on unfold:term_metric solve+:lia. -Qed. - -Lemma sn_algo_dom a b : SN a -> SN b -> algo_dom_r a b. -Proof. - move : sn_term_metric; repeat move/[apply]. - move => [k]+. - eauto using term_metric_algo_dom. -Qed. - Lemma coqeq_complete Γ (a b A : PTm) : Γ ⊢ a ≡ b ∈ A -> a ⇔ b. Proof. move => h. - have : algo_dom_r a b /\ DJoin.R a b by - hauto lq:on use:fundamental_theorem, logrel.SemEq_SemWt, logrel.SemWt_SN, sn_algo_dom. - hauto lq:on use:regularity, coqeq_complete'. + 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). Reserved Notation "a ⋖ b" (at level 70). Inductive CoqLEq : PTm -> PTm -> Prop := @@ -1724,6 +1794,27 @@ Scheme coqleq_ind := Induction for CoqLEq Sort Prop Combined Scheme coqleq_mutual from coqleq_ind, coqleq_r_ind. +Definition salgo_metric k (a b : PTm ) := + exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ ESub.R va vb /\ size_PTm va + size_PTm vb + i + j <= k. + +Lemma salgo_metric_algo_metric k (a b : PTm) : + ishne a \/ ishne b -> + salgo_metric k a b -> + algo_metric k a b. +Proof. + move => h. + move => [i][j][va][vb][hva][hvb][nva][nvb][hS]sz. + rewrite/ESub.R in hS. + move : hS => [va'][vb'][h0][h1]h2. + suff : va' = vb' by sauto lq:on. + have {}hva : rtc RERed.R a va by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds. + have {}hvb : rtc RERed.R b vb by hauto lq:on use:@relations.rtc_nsteps, REReds.FromRReds, LoReds.ToRReds. + apply REReds.FromEReds in h0, h1. + have : ishne va' \/ ishne vb' by + hauto lq:on rew:off use:@relations.rtc_transitive, REReds.hne_preservation. + hauto lq:on use:Sub1.hne_refl. +Qed. + Lemma coqleq_sound_mutual : (forall (a b : PTm), a ⋖ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ) /\ (forall (a b : PTm), a ≪ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ). @@ -1755,6 +1846,34 @@ Proof. eauto using HReds.preservation. Qed. +Lemma salgo_metric_case k (a b : PTm ) : + salgo_metric k a b -> + (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ salgo_metric k' a' b /\ k' < k. +Proof. + move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6. + case : a h0 => //=; try firstorder. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. + + sfirstorder qb:on use:ne_hne. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. + + sfirstorder use:ne_hne. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. + + sfirstorder use:ne_hne. + + sfirstorder use:ne_hne. +Qed. + Lemma CLE_HRedL (a a' b : PTm ) : HRed.R a a' -> a' ≪ b -> @@ -1771,116 +1890,191 @@ Proof. hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R. Qed. -Lemma subvar_inj (i j : nat) : - Sub.R (VarPTm i) (VarPTm j) -> i = j. + +Lemma algo_metric_caseR k (a b : PTm) : + salgo_metric k a b -> + (ishf b \/ ishne b) \/ exists k' b', HRed.R b b' /\ salgo_metric k' a b' /\ k' < k. Proof. - rewrite /Sub.R. - move => [c][d][h0][h1]h2. - apply REReds.var_inv in h0, h1. subst. - inversion h2; by subst. + move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6. + case : b h1 => //=; try by firstorder. + - inversion 1 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto q:on use:HRed.AppAbs unfold:salgo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:salgo_metric solve+:lia. + + sfirstorder qb:on use:ne_hne. + - inversion 1 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. + - inversion 1 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. + + sfirstorder use:ne_hne. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. + + sfirstorder use:ne_hne. + + sfirstorder use:ne_hne. Qed. -Lemma algo_dom_hf_hne (a b : PTm) : - algo_dom a b -> - (ishf a \/ ishne a) /\ (ishf b \/ ishne b). +Lemma salgo_metric_sub k (a b : PTm) : + salgo_metric k a b -> + Sub.R a b. Proof. - inversion 1;subst => //=; by sfirstorder b:on. + rewrite /algo_metric. + move => [i][j][va][vb][h0][h1][h2][h3][[va' [vb' [hva [hvb hS]]]]]h5. + have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps. + have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps. + apply REReds.FromEReds in hva,hvb. + apply LoReds.ToRReds in h0,h1. + apply REReds.FromRReds in h0,h1. + rewrite /Sub.R. exists va', vb'. sfirstorder use:@relations.rtc_transitive. Qed. -Lemma algo_dom_neu_neu_nonconf a b : - algo_dom a b -> - neuneu_nonconf a b -> - ishne a /\ ishne b. +Lemma salgo_metric_pi k (A0 : PTm) B0 A1 B1 : + salgo_metric k (PBind PPi A0 B0) (PBind PPi A1 B1) -> + exists j, j < k /\ salgo_metric j A1 A0 /\ salgo_metric j B0 B1. Proof. - move /algo_dom_hf_hne => h. - move => h1. - destruct a,b => //=; sfirstorder b:on. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. + move : lored_nsteps_bind_inv h0 => /[apply]. + move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. + move : lored_nsteps_bind_inv h1 => /[apply]. + move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. + move /ESub.pi_inj : h4 => [? ?]. + hauto qb:on solve+:lia. Qed. -Lemma coqleq_complete' : - (forall a b, salgo_dom a b -> Sub.R a b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ⋖ b) /\ - (forall a b, salgo_dom_r a b -> Sub.R a b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b). +Lemma salgo_metric_sig k (A0 : PTm) B0 A1 B1 : + salgo_metric k (PBind PSig A0 B0) (PBind PSig A1 B1) -> + exists j, j < k /\ salgo_metric j A0 A1 /\ salgo_metric j B0 B1. Proof. - apply salgo_dom_mutual. - - move => i j /Sub.univ_inj. - hauto lq:on ctrs:CoqLEq. - - move => A0 A1 B0 B1 hA ihA hB ihB /Sub.bind_inj. move => [_][hjA]hjB Γ i. - move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0]. - have {}ihA : A1 ≪ A0 by hauto l:on. - constructor => //. - have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual. - suff : (cons A1 Γ) ⊢ B0 ∈ PUniv i - by hauto l:on. - eauto using ctx_eq_subst_one. - - move => A0 A1 B0 B1 hA ihA hB ihB /Sub.bind_inj. move => [_][hjA]hjB Γ i. - move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0]. - have {}ihA : A0 ≪ A1 by hauto l:on. - constructor => //. - have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual. - suff : (cons A0 Γ) ⊢ B1 ∈ PUniv i - by hauto l:on. - eauto using ctx_eq_subst_one. - - sfirstorder. - - move => a b hconf hdom. - have [? ?] : ishne a /\ ishne b by sfirstorder use:algo_dom_neu_neu_nonconf. - move => h. apply Sub.ToJoin in h; last by tauto. - move => Γ i ha hb. - apply CLE_NeuNeu. hauto q:on use:coqeq_complete'. - - move => [:neunf] a b. - case => ha; case => hb. - move : ha hb. - + case : a => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp']. - * case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp']. - case => + + []//=. - hauto lq:on rew:off use:Sub.bind_inj. - hauto lq:on rew:off use:Sub.bind_inj. - hauto lq:on use:Sub.bind_univ_noconf. - hauto lq:on use:Sub.nat_bind_noconf. - * case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp']. - hauto lq:on use:Sub.univ_bind_noconf. - hauto lq:on use:Sub.nat_univ_noconf. - * case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp']. - hauto lq:on use:Sub.bind_nat_noconf. - hauto lq:on use:Sub.univ_nat_noconf. - + move => h0 h1. - apply Sub.ToJoin in h1; last by tauto. - move => Γ i wta wtb. exfalso. - abstract : neunf a b ha hb h0 h1 Γ i wta wtb. - case : a ha h0 h1 wta => //=; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'. - sfirstorder use: DJoin.hne_bind_noconf. - sfirstorder use: DJoin.hne_univ_noconf. - sfirstorder use:DJoin.hne_nat_noconf. - + move => h0 h1. apply Sub.ToJoin in h1; last by tauto. - hauto drew:off use:DJoin.symmetric, stm_conf_sym. - + move => h0 h1 Γ i wta wtb. - apply CLE_NeuNeu. - apply Sub.ToJoin in h1; last by tauto. - eapply coqeq_complete'; eauto. - apply algo_dom_r_algo_dom. - sfirstorder use:hne_no_hred. - sfirstorder use:hne_no_hred. - hauto lq:on use:sn_algo_dom, logrel.SemWt_SN, fundamental_theorem. - - hauto l:on. - - move => a a' b hr ha iha hj Γ A wta wtb. - apply : CLE_HRedL; eauto. - apply : iha; eauto; last by sfirstorder use:HRed.preservation. - apply : Sub.transitive; eauto. - hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - apply /Sub.FromJoin /DJoin.FromRRed1. by apply HRed.ToRRed. - - move => a b b' nfa hr h ih j Γ A wta wtb. - apply : CLE_HRedR; eauto. - apply : ih; eauto; last by eauto using HRed.preservation. - apply : Sub.transitive; eauto. - hauto lq:on use:fundamental_theorem, logrel.SemWt_SN. - apply /Sub.FromJoin /DJoin.FromRRed0. by apply HRed.ToRRed. + move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. + move : lored_nsteps_bind_inv h0 => /[apply]. + move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. + move : lored_nsteps_bind_inv h1 => /[apply]. + move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. + move /ESub.sig_inj : h4 => [? ?]. + hauto qb:on solve+:lia. Qed. + +Lemma coqleq_complete' k (a b : PTm ) : + salgo_metric k a b -> (forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b). +Proof. + move : k a b. + elim /Wf_nat.lt_wf_ind. + move => n ih. + move => a b /[dup] h /salgo_metric_case. + (* Cases where a and b can take steps *) + case; cycle 1. + move : a b h. + qauto l:on use:HRed.preservation, CLE_HRedL, hred_hne. + case /algo_metric_caseR : (h); cycle 1. + qauto l:on use:HRed.preservation, CLE_HRedR, hred_hne. + (* Cases where neither a nor b can take steps *) + case => fb; case => fa. + - case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + * move => p0 A0 B0 _ p1 A1 B1 _. + move => h. + have ? : p1 = p0 by + hauto lq:on rew:off use:salgo_metric_sub, Sub.bind_inj. + subst. + case : p0 h => //=. + ** move /salgo_metric_pi. + move => [j [hj [hA hB]]] Γ i. + move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0]. + have ihA : A0 ≪ A1 by hauto l:on. + econstructor; eauto using E_Refl; constructor=> //. + have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual. + suff : (cons A0 Γ) ⊢ B1 ∈ PUniv i + by hauto l:on. + eauto using ctx_eq_subst_one. + ** move /salgo_metric_sig. + move => [j [hj [hA hB]]] Γ i. + move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0]. + have ihA : A1 ≪ A0 by hauto l:on. + econstructor; eauto using E_Refl; constructor=> //. + have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual. + suff : (cons A1 Γ) ⊢ B0 ∈ PUniv i + by hauto l:on. + eauto using ctx_eq_subst_one. + * hauto lq:on use:salgo_metric_sub, Sub.bind_univ_noconf. + * hauto lq:on use:salgo_metric_sub, Sub.nat_bind_noconf. + * move => _ > _ /salgo_metric_sub. + hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv inv:Sub1.R. + * hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R. + + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + * hauto lq:on use:salgo_metric_sub, Sub.univ_bind_noconf. + * move => *. econstructor; eauto using rtc_refl. + hauto lq:on use:salgo_metric_sub, Sub.univ_inj, CLE_UnivCong. + * hauto lq:on rew:off use:REReds.univ_inv, REReds.nat_inv, salgo_metric_sub inv:Sub1.R. + * hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R. + * hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R. + (* Both cases are impossible *) + + case : b fb => //=. + * hauto lq:on use:T_AbsNat_Imp. + * hauto lq:on use:T_PairNat_Imp. + * hauto lq:on rew:off use:REReds.nat_inv, REReds.bind_inv, salgo_metric_sub inv:Sub1.R. + * hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R. + * hauto l:on. + * hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R. + * hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R. + + move => ? ? Γ i /Zero_Inv. + clear. + move /synsub_to_usub => [_ [_ ]]. + hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R. + + move => ? _ _ Γ i /Suc_Inv => [[_]]. + move /synsub_to_usub. + hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R. + - have {}h : DJoin.R a b by + hauto lq:on use:salgo_metric_algo_metric, algo_metric_join. + case : b fb h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + + hauto lq:on use:DJoin.hne_bind_noconf. + + hauto lq:on use:DJoin.hne_univ_noconf. + + hauto lq:on use:DJoin.hne_nat_noconf. + + move => _ _ Γ i _. + move /Zero_Inv. + hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R. + + move => p _ _ Γ i _ /Suc_Inv. + hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R. + - have {}h : DJoin.R b a by + hauto lq:on use:salgo_metric_algo_metric, algo_metric_join, DJoin.symmetric. + case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. + + hauto lq:on use:DJoin.hne_bind_noconf. + + hauto lq:on use:DJoin.hne_univ_noconf. + + hauto lq:on use:DJoin.hne_nat_noconf. + + move => _ _ Γ i. + move /Zero_Inv. + hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R. + + move => p _ _ Γ i /Suc_Inv. + hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R. + - move => Γ i ha hb. + econstructor; eauto using rtc_refl. + apply CLE_NeuNeu. move {ih}. + have {}h : algo_metric n a b by + hauto lq:on use:salgo_metric_algo_metric. + eapply coqeq_complete'; eauto. +Qed. + Lemma coqleq_complete Γ (a b : PTm) : Γ ⊢ a ≲ b -> a ≪ b. Proof. move => h. - have : salgo_dom_r a b /\ Sub.R a b by - hauto lq:on use:fundamental_theorem, logrel.SemLEq_SemWt, logrel.SemWt_SN, sn_algo_dom, algo_dom_salgo_dom. - hauto lq:on use:regularity, coqleq_complete'. + suff : exists k, salgo_metric k a b by hauto lq:on use:coqleq_complete', regularity. + eapply fundamental_theorem in h. + move /logrel.SemLEq_SN_Sub : h. + move => h. + have : exists va vb : PTm , + rtc LoRed.R a va /\ + rtc LoRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb + by hauto l:on use:Sub.standardization_lo. + move => [va][vb][hva][hvb][nva][nvb]hj. + move /relations.rtc_nsteps : hva => [i hva]. + move /relations.rtc_nsteps : hvb => [j hvb]. + exists (i + j + size_PTm va + size_PTm vb). + hauto lq:on solve+:lia. Qed. Lemma coqleq_sound : forall Γ (a b : PTm) i j, diff --git a/theories/common.v b/theories/common.v index 35267fc..3ea15d6 100644 --- a/theories/common.v +++ b/theories/common.v @@ -1,4 +1,4 @@ -Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect ssrbool. +Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect. From Equations Require Import Equations. Derive NoConfusion for nat PTag BTag PTm. Derive EqDec for BTag PTag PTm. @@ -6,7 +6,6 @@ From Ltac2 Require Ltac2. Import Ltac2.Notations. Import Ltac2.Control. From Hammer Require Import Tactics. -From stdpp Require Import relations (rtc(..)). Inductive lookup : nat -> list PTm -> PTm -> Prop := | here A Γ : lookup 0 (cons A Γ) (ren_PTm shift A) @@ -120,26 +119,6 @@ Definition isabs (a : PTm) := | _ => false end. -Definition tm_nonconf (a b : PTm) : bool := - match a, b with - | PAbs _, _ => (~~ ishf b) || isabs b - | _, PAbs _ => ~~ ishf a - | VarPTm _, VarPTm _ => true - | PPair _ _, _ => (~~ ishf b) || ispair b - | _, PPair _ _ => ~~ ishf a - | PZero, PZero => true - | PSuc _, PSuc _ => true - | PApp _ _, PApp _ _ => true - | PProj _ _, PProj _ _ => true - | PInd _ _ _ _, PInd _ _ _ _ => true - | PNat, PNat => true - | PUniv _, PUniv _ => true - | PBind _ _ _, PBind _ _ _ => true - | _,_=> false - end. - -Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b. - Definition ishf_ren (a : PTm) (ξ : nat -> nat) : ishf (ren_PTm ξ a) = ishf a. Proof. case : a => //=. Qed. @@ -196,406 +175,3 @@ Module HRed. Definition nf a := forall b, ~ R a b. End HRed. - -Inductive algo_dom : PTm -> PTm -> Prop := -| A_AbsAbs a b : - algo_dom_r a b -> - (* --------------------- *) - algo_dom (PAbs a) (PAbs b) - -| A_AbsNeu a u : - ishne u -> - algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) -> - (* --------------------- *) - algo_dom (PAbs a) u - -| A_NeuAbs a u : - ishne u -> - algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a -> - (* --------------------- *) - algo_dom u (PAbs a) - -| A_PairPair a0 a1 b0 b1 : - algo_dom_r a0 a1 -> - algo_dom_r b0 b1 -> - (* ---------------------------- *) - algo_dom (PPair a0 b0) (PPair a1 b1) - -| A_PairNeu a0 a1 u : - ishne u -> - algo_dom_r a0 (PProj PL u) -> - algo_dom_r a1 (PProj PR u) -> - (* ----------------------- *) - algo_dom (PPair a0 a1) u - -| A_NeuPair a0 a1 u : - ishne u -> - algo_dom_r (PProj PL u) a0 -> - algo_dom_r (PProj PR u) a1 -> - (* ----------------------- *) - algo_dom u (PPair a0 a1) - -| A_ZeroZero : - algo_dom PZero PZero - -| A_SucSuc a0 a1 : - algo_dom_r a0 a1 -> - algo_dom (PSuc a0) (PSuc a1) - -| A_UnivCong i j : - (* -------------------------- *) - algo_dom (PUniv i) (PUniv j) - -| A_BindCong p0 p1 A0 A1 B0 B1 : - algo_dom_r A0 A1 -> - algo_dom_r B0 B1 -> - (* ---------------------------- *) - algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1) - -| A_NatCong : - algo_dom PNat PNat - -| A_VarCong i j : - (* -------------------------- *) - algo_dom (VarPTm i) (VarPTm j) - -| A_AppCong u0 u1 a0 a1 : - ishne u0 -> - ishne u1 -> - algo_dom u0 u1 -> - algo_dom_r a0 a1 -> - (* ------------------------- *) - algo_dom (PApp u0 a0) (PApp u1 a1) - -| A_ProjCong p0 p1 u0 u1 : - ishne u0 -> - ishne u1 -> - algo_dom u0 u1 -> - (* --------------------- *) - algo_dom (PProj p0 u0) (PProj p1 u1) - -| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 : - ishne u0 -> - ishne u1 -> - algo_dom_r P0 P1 -> - algo_dom u0 u1 -> - algo_dom_r b0 b1 -> - algo_dom_r c0 c1 -> - algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) - -| A_Conf a b : - ishf a \/ ishne a -> - ishf b \/ ishne b -> - tm_conf a b -> - algo_dom a b - -with algo_dom_r : PTm -> PTm -> Prop := -| A_NfNf a b : - algo_dom a b -> - algo_dom_r a b - -| A_HRedL a a' b : - HRed.R a a' -> - algo_dom_r a' b -> - (* ----------------------- *) - algo_dom_r a b - -| A_HRedR a b b' : - HRed.nf a -> - HRed.R b b' -> - algo_dom_r a b' -> - (* ----------------------- *) - algo_dom_r a b. - -Scheme algo_ind := Induction for algo_dom Sort Prop - with algor_ind := Induction for algo_dom_r Sort Prop. - -Combined Scheme algo_dom_mutual from algo_ind, algor_ind. -#[export]Hint Constructors algo_dom algo_dom_r : adom. - -Definition stm_nonconf a b := - match a, b with - | PUniv _, PUniv _ => true - | PBind PPi _ _, PBind PPi _ _ => true - | PBind PSig _ _, PBind PSig _ _ => true - | PNat, PNat => true - | VarPTm _, VarPTm _ => true - | PApp _ _, PApp _ _ => true - | PProj _ _, PProj _ _ => true - | PInd _ _ _ _, PInd _ _ _ _ => true - | _, _ => false - end. - -Definition neuneu_nonconf a b := - match a, b with - | VarPTm _, VarPTm _ => true - | PApp _ _, PApp _ _ => true - | PProj _ _, PProj _ _ => true - | PInd _ _ _ _, PInd _ _ _ _ => true - | _, _ => false - end. - -Lemma stm_tm_nonconf a b : - stm_nonconf a b -> tm_nonconf a b. -Proof. apply /implyP. - destruct a ,b =>//=; hauto lq:on inv:PTag, BTag. -Qed. - -Definition stm_conf a b := ~~ stm_nonconf a b. - -Lemma tm_stm_conf a b : - tm_conf a b -> stm_conf a b. -Proof. - rewrite /tm_conf /stm_conf. - apply /contra /stm_tm_nonconf. -Qed. - -Inductive salgo_dom : PTm -> PTm -> Prop := -| S_UnivCong i j : - (* -------------------------- *) - salgo_dom (PUniv i) (PUniv j) - -| S_PiCong A0 A1 B0 B1 : - salgo_dom_r A1 A0 -> - salgo_dom_r B0 B1 -> - (* ---------------------------- *) - salgo_dom (PBind PPi A0 B0) (PBind PPi A1 B1) - -| S_SigCong A0 A1 B0 B1 : - salgo_dom_r A0 A1 -> - salgo_dom_r B0 B1 -> - (* ---------------------------- *) - salgo_dom (PBind PSig A0 B0) (PBind PSig A1 B1) - -| S_NatCong : - salgo_dom PNat PNat - -| S_NeuNeu a b : - neuneu_nonconf a b -> - algo_dom a b -> - salgo_dom a b - -| S_Conf a b : - ishf a \/ ishne a -> - ishf b \/ ishne b -> - stm_conf a b -> - salgo_dom a b - -with salgo_dom_r : PTm -> PTm -> Prop := -| S_NfNf a b : - salgo_dom a b -> - salgo_dom_r a b - -| S_HRedL a a' b : - HRed.R a a' -> - salgo_dom_r a' b -> - (* ----------------------- *) - salgo_dom_r a b - -| S_HRedR a b b' : - HRed.nf a -> - HRed.R b b' -> - salgo_dom_r a b' -> - (* ----------------------- *) - salgo_dom_r a b. - -#[export]Hint Constructors salgo_dom salgo_dom_r : sdom. -Scheme salgo_ind := Induction for salgo_dom Sort Prop - with salgor_ind := Induction for salgo_dom_r Sort Prop. - -Combined Scheme salgo_dom_mutual from salgo_ind, salgor_ind. - -Lemma hf_no_hred (a b : PTm) : - ishf a -> - HRed.R a b -> - False. -Proof. hauto l:on inv:HRed.R. Qed. - -Lemma hne_no_hred (a b : PTm) : - ishne a -> - HRed.R a b -> - False. -Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. - -Ltac2 destruct_salgo () := - lazy_match! goal with - | [_ : 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) - end. - -Ltac destruct_salgo := ltac2:(destruct_salgo ()). - -Lemma algo_dom_r_inv a b : - algo_dom_r a b -> exists a0 b0, algo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0. -Proof. - induction 1; hauto lq:on ctrs:rtc. -Qed. - -Lemma A_HRedsL a a' b : - rtc HRed.R a a' -> - algo_dom_r a' b -> - algo_dom_r a b. - induction 1; sfirstorder use:A_HRedL. -Qed. - -Lemma A_HRedsR a b b' : - HRed.nf a -> - rtc HRed.R b b' -> - algo_dom a b' -> - algo_dom_r a b. -Proof. induction 2; sauto. Qed. - -Lemma tm_conf_sym a b : tm_conf a b = tm_conf b a. -Proof. case : a; case : b => //=. Qed. - -Lemma algo_dom_no_hred (a b : PTm) : - algo_dom a b -> - HRed.nf a /\ HRed.nf b. -Proof. - induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf. -Qed. - - -Lemma A_HRedR' a b b' : - HRed.R b b' -> - algo_dom_r a b' -> - algo_dom_r a b. -Proof. - move => hb /algo_dom_r_inv. - move => [a0 [b0 [h0 [h1 h2]]]]. - have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc. - have ? : HRed.nf a0 by sfirstorder use:algo_dom_no_hred. - hauto lq:on use:A_HRedsL, A_HRedsR. -Qed. - -Lemma algo_dom_sym : - (forall a b (h : algo_dom a b), algo_dom b a) /\ - (forall a b (h : algo_dom_r a b), algo_dom_r b a). -Proof. - apply algo_dom_mutual; try qauto use:tm_conf_sym,A_HRedR' db:adom. -Qed. - -Lemma salgo_dom_r_inv a b : - salgo_dom_r a b -> exists a0 b0, salgo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0. -Proof. - induction 1; hauto lq:on ctrs:rtc. -Qed. - -Lemma S_HRedsL a a' b : - rtc HRed.R a a' -> - salgo_dom_r a' b -> - salgo_dom_r a b. - induction 1; sfirstorder use:S_HRedL. -Qed. - -Lemma S_HRedsR a b b' : - HRed.nf a -> - rtc HRed.R b b' -> - salgo_dom a b' -> - salgo_dom_r a b. -Proof. induction 2; sauto. Qed. - -Lemma stm_conf_sym a b : stm_conf a b = stm_conf b a. -Proof. case : a; case : b => //=; hauto lq:on inv:PTag, BTag. Qed. - -Lemma salgo_dom_no_hred (a b : PTm) : - salgo_dom a b -> - HRed.nf a /\ HRed.nf b. -Proof. - induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred, algo_dom_no_hred lq:on unfold:HRed.nf. -Qed. - -Lemma S_HRedR' a b b' : - HRed.R b b' -> - salgo_dom_r a b' -> - salgo_dom_r a b. -Proof. - move => hb /salgo_dom_r_inv. - move => [a0 [b0 [h0 [h1 h2]]]]. - have {h2} {}hb : rtc HRed.R b b0 by hauto lq:on ctrs:rtc. - have ? : HRed.nf a0 by sfirstorder use:salgo_dom_no_hred. - hauto lq:on use:S_HRedsL, S_HRedsR. -Qed. - -Ltac solve_conf := intros; split; - apply S_Conf; solve [destruct_salgo | sfirstorder ctrs:salgo_dom use:hne_no_hred, hf_no_hred]. - -Ltac solve_basic := hauto q:on ctrs:salgo_dom, salgo_dom_r, algo_dom use:algo_dom_sym. - -Lemma algo_dom_salgo_dom : - (forall a b, algo_dom a b -> salgo_dom a b /\ salgo_dom b a) /\ - (forall a b, algo_dom_r a b -> salgo_dom_r a b /\ salgo_dom_r b a). -Proof. - apply algo_dom_mutual => //=; try first [solve_conf | solve_basic]. - - case; case; hauto lq:on ctrs:salgo_dom use:algo_dom_sym inv:HRed.R unfold:HRed.nf. - - move => a b ha hb hc. split; - apply S_Conf; hauto l:on use:tm_conf_sym, tm_stm_conf. - - hauto lq:on ctrs:salgo_dom_r use:S_HRedR'. -Qed. - -Fixpoint hred (a : PTm) : option (PTm) := - match a with - | VarPTm i => None - | PAbs a => None - | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a) - | PApp a b => - match hred a with - | Some a => Some (PApp a b) - | None => None - end - | PPair a b => None - | PProj p (PPair a b) => if p is PL then Some a else Some b - | PProj p a => - match hred a with - | Some a => Some (PProj p a) - | None => None - end - | PUniv i => None - | PBind p A B => None - | PNat => None - | PZero => None - | PSuc a => None - | PInd P PZero b c => Some b - | PInd P (PSuc a) b c => - Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) - | PInd P a b c => - match hred a with - | Some a => Some (PInd P a b c) - | None => None - end - end. - -Lemma hred_complete (a b : PTm) : - HRed.R a b -> hred a = Some b. -Proof. - induction 1; hauto lq:on rew:off inv:HRed.R b:on. -Qed. - -Lemma hred_sound (a b : PTm): - hred a = Some b -> HRed.R a b. -Proof. - elim : a b; hauto q:on dep:on ctrs:HRed.R. -Qed. - -Lemma hred_deter (a b0 b1 : PTm) : - HRed.R a b0 -> HRed.R a b1 -> b0 = b1. -Proof. - move /hred_complete => + /hred_complete. congruence. -Qed. - -Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}. - destruct (hred a) eqn:eq. - right. exists p. by apply hred_sound in eq. - left. move => b /hred_complete. congruence. -Defined. - -Lemma hreds_nf_refl a b : - HRed.nf a -> - rtc HRed.R a b -> - a = b. -Proof. inversion 2; sfirstorder. Qed. - -Lemma algo_dom_r_algo_dom : forall a b, HRed.nf a -> HRed.nf b -> algo_dom_r a b -> algo_dom a b. -Proof. hauto l:on use:algo_dom_r_inv, hreds_nf_refl. Qed. diff --git a/theories/executable.v b/theories/executable.v index 558aa75..44557f9 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -11,6 +11,345 @@ Set Default Proof Mode "Classic". Require Import ssreflect ssrbool. From Hammer Require Import Tactics. +Definition tm_nonconf (a b : PTm) : bool := + match a, b with + | PAbs _, _ => (~~ ishf b) || isabs b + | _, PAbs _ => ~~ ishf a + | VarPTm _, VarPTm _ => true + | PPair _ _, _ => (~~ ishf b) || ispair b + | _, PPair _ _ => ~~ ishf a + | PZero, PZero => true + | PSuc _, PSuc _ => true + | PApp _ _, PApp _ _ => (~~ ishf a) && (~~ ishf b) + | PProj _ _, PProj _ _ => (~~ ishf a) && (~~ ishf b) + | PInd _ _ _ _, PInd _ _ _ _ => (~~ ishf a) && (~~ ishf b) + | PNat, PNat => true + | PUniv _, PUniv _ => true + | PBind _ _ _, PBind _ _ _ => true + | _,_=> false + end. + +Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b. + +Inductive eq_view : PTm -> PTm -> Type := +| V_AbsAbs a b : + eq_view (PAbs a) (PAbs b) +| V_AbsNeu a b : + ~~ ishf b -> + eq_view (PAbs a) b +| V_NeuAbs a b : + ~~ ishf a -> + eq_view a (PAbs b) +| V_VarVar i j : + eq_view (VarPTm i) (VarPTm j) +| V_PairPair a0 b0 a1 b1 : + eq_view (PPair a0 b0) (PPair a1 b1) +| V_PairNeu a0 b0 u : + ~~ ishf u -> + eq_view (PPair a0 b0) u +| V_NeuPair u a1 b1 : + ~~ ishf u -> + eq_view u (PPair a1 b1) +| V_ZeroZero : + eq_view PZero PZero +| V_SucSuc a b : + eq_view (PSuc a) (PSuc b) +| V_AppApp u0 b0 u1 b1 : + eq_view (PApp u0 b0) (PApp u1 b1) +| V_ProjProj p0 u0 p1 u1 : + eq_view (PProj p0 u0) (PProj p1 u1) +| V_IndInd P0 u0 b0 c0 P1 u1 b1 c1 : + eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) +| V_NatNat : + eq_view PNat PNat +| V_BindBind p0 A0 B0 p1 A1 B1 : + eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) +| V_UnivUniv i j : + eq_view (PUniv i) (PUniv j) +| V_Others a b : + tm_conf a b -> + eq_view a b. + +Equations tm_to_eq_view (a b : PTm) : eq_view a b := + tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b; + tm_to_eq_view (PAbs a) (PApp b0 b1) := V_AbsNeu a (PApp b0 b1) _; + tm_to_eq_view (PAbs a) (VarPTm i) := V_AbsNeu a (VarPTm i) _; + tm_to_eq_view (PAbs a) (PProj p b) := V_AbsNeu a (PProj p b) _; + tm_to_eq_view (PAbs a) (PInd P u b c) := V_AbsNeu a (PInd P u b c) _; + tm_to_eq_view (VarPTm i) (PAbs a) := V_NeuAbs (VarPTm i) a _; + tm_to_eq_view (PApp b0 b1) (PAbs b) := V_NeuAbs (PApp b0 b1) b _; + tm_to_eq_view (PProj p b) (PAbs a) := V_NeuAbs (PProj p b) a _; + tm_to_eq_view (PInd P u b c) (PAbs a) := V_NeuAbs (PInd P u b c) a _; + tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j; + tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1; + (* tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; *) + tm_to_eq_view (PPair a0 b0) (VarPTm i) := V_PairNeu a0 b0 (VarPTm i) _; + tm_to_eq_view (PPair a0 b0) (PApp c0 c1) := V_PairNeu a0 b0 (PApp c0 c1) _; + tm_to_eq_view (PPair a0 b0) (PProj p c) := V_PairNeu a0 b0 (PProj p c) _; + tm_to_eq_view (PPair a0 b0) (PInd P t0 t1 t2) := V_PairNeu a0 b0 (PInd P t0 t1 t2) _; + (* tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; *) + tm_to_eq_view (VarPTm i) (PPair a1 b1) := V_NeuPair (VarPTm i) a1 b1 _; + tm_to_eq_view (PApp t0 t1) (PPair a1 b1) := V_NeuPair (PApp t0 t1) a1 b1 _; + tm_to_eq_view (PProj t0 t1) (PPair a1 b1) := V_NeuPair (PProj t0 t1) a1 b1 _; + tm_to_eq_view (PInd t0 t1 t2 t3) (PPair a1 b1) := V_NeuPair (PInd t0 t1 t2 t3) a1 b1 _; + tm_to_eq_view PZero PZero := V_ZeroZero; + tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b; + tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1; + tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1; + tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1; + tm_to_eq_view PNat PNat := V_NatNat; + tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j; + tm_to_eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1; + tm_to_eq_view a b := V_Others a b _. + +Inductive algo_dom : PTm -> PTm -> Prop := +| A_AbsAbs a b : + algo_dom_r a b -> + (* --------------------- *) + algo_dom (PAbs a) (PAbs b) + +| A_AbsNeu a u : + ishne u -> + algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) -> + (* --------------------- *) + algo_dom (PAbs a) u + +| A_NeuAbs a u : + ishne u -> + algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a -> + (* --------------------- *) + algo_dom u (PAbs a) + +| A_PairPair a0 a1 b0 b1 : + algo_dom_r a0 a1 -> + algo_dom_r b0 b1 -> + (* ---------------------------- *) + algo_dom (PPair a0 b0) (PPair a1 b1) + +| A_PairNeu a0 a1 u : + ishne u -> + algo_dom_r a0 (PProj PL u) -> + algo_dom_r a1 (PProj PR u) -> + (* ----------------------- *) + algo_dom (PPair a0 a1) u + +| A_NeuPair a0 a1 u : + ishne u -> + algo_dom_r (PProj PL u) a0 -> + algo_dom_r (PProj PR u) a1 -> + (* ----------------------- *) + algo_dom u (PPair a0 a1) + +| A_ZeroZero : + algo_dom PZero PZero + +| A_SucSuc a0 a1 : + algo_dom_r a0 a1 -> + algo_dom (PSuc a0) (PSuc a1) + +| A_UnivCong i j : + (* -------------------------- *) + algo_dom (PUniv i) (PUniv j) + +| A_BindCong p0 p1 A0 A1 B0 B1 : + algo_dom_r A0 A1 -> + algo_dom_r B0 B1 -> + (* ---------------------------- *) + algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1) + +| A_NatCong : + algo_dom PNat PNat + +| A_VarCong i j : + (* -------------------------- *) + algo_dom (VarPTm i) (VarPTm j) + +| A_ProjCong p0 p1 u0 u1 : + ishne u0 -> + ishne u1 -> + algo_dom u0 u1 -> + (* --------------------- *) + algo_dom (PProj p0 u0) (PProj p1 u1) + +| A_AppCong u0 u1 a0 a1 : + ishne u0 -> + ishne u1 -> + algo_dom u0 u1 -> + algo_dom_r a0 a1 -> + (* ------------------------- *) + algo_dom (PApp u0 a0) (PApp u1 a1) + +| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 : + ishne u0 -> + ishne u1 -> + algo_dom_r P0 P1 -> + algo_dom u0 u1 -> + algo_dom_r b0 b1 -> + algo_dom_r c0 c1 -> + algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) + +| A_Conf a b : + HRed.nf a -> + HRed.nf b -> + tm_conf a b -> + algo_dom a b + +with algo_dom_r : PTm -> PTm -> Prop := +| A_NfNf a b : + algo_dom a b -> + algo_dom_r a b + +| A_HRedL a a' b : + HRed.R a a' -> + algo_dom_r a' b -> + (* ----------------------- *) + algo_dom_r a b + +| A_HRedR a b b' : + HRed.nf a -> + HRed.R b b' -> + algo_dom_r a b' -> + (* ----------------------- *) + algo_dom_r a b. + +Scheme algo_ind := Induction for algo_dom Sort Prop + with algor_ind := Induction for algo_dom_r Sort Prop. + +Combined Scheme algo_dom_mutual from algo_ind, algor_ind. + + +(* Inductive salgo_dom : PTm -> PTm -> Prop := *) +(* | S_UnivCong i j : *) +(* (* -------------------------- *) *) +(* salgo_dom (PUniv i) (PUniv j) *) + +(* | S_PiCong A0 A1 B0 B1 : *) +(* salgo_dom_r A1 A0 -> *) +(* salgo_dom_r B0 B1 -> *) +(* (* ---------------------------- *) *) +(* salgo_dom (PBind PPi A0 B0) (PBind PPi A1 B1) *) + +(* | S_SigCong A0 A1 B0 B1 : *) +(* salgo_dom_r A0 A1 -> *) +(* salgo_dom_r B0 B1 -> *) +(* (* ---------------------------- *) *) +(* salgo_dom (PBind PSig A0 B0) (PBind PSig A1 B1) *) + +(* | S_NatCong : *) +(* salgo_dom PNat PNat *) + +(* | S_NeuNeu a b : *) +(* ishne a -> *) +(* ishne b -> *) +(* algo_dom a b -> *) +(* (* ------------------- *) *) +(* salgo_dom *) + +(* | S_Conf a b : *) +(* HRed.nf a -> *) +(* HRed.nf b -> *) +(* tm_conf a b -> *) +(* salgo_dom a b *) + +(* with salgo_dom_r : PTm -> PTm -> Prop := *) +(* | S_NfNf a b : *) +(* salgo_dom a b -> *) +(* salgo_dom_r a b *) + +(* | S_HRedL a a' b : *) +(* HRed.R a a' -> *) +(* salgo_dom_r a' b -> *) +(* (* ----------------------- *) *) +(* salgo_dom_r a b *) + +(* | S_HRedR a b b' : *) +(* HRed.nf a -> *) +(* HRed.R b b' -> *) +(* salgo_dom_r a b' -> *) +(* (* ----------------------- *) *) +(* salgo_dom_r a b. *) + +(* Scheme salgo_ind := Induction for salgo_dom Sort Prop *) +(* with algor_ind := Induction for salgo_dom_r Sort Prop. *) + + +Lemma hf_no_hred (a b : PTm) : + ishf a -> + HRed.R a b -> + False. +Proof. hauto l:on inv:HRed.R. Qed. + +Lemma hne_no_hred (a b : PTm) : + ishne a -> + HRed.R a b -> + False. +Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. + +Lemma algo_dom_no_hred (a b : PTm) : + algo_dom a b -> + HRed.nf a /\ HRed.nf b. +Proof. + induction 1 =>//=; try hauto inv:HRed.R use:hne_no_hred, hf_no_hred lq:on unfold:HRed.nf. +Qed. + +Derive Signature for algo_dom algo_dom_r. + +Fixpoint hred (a : PTm) : option (PTm) := + match a with + | VarPTm i => None + | PAbs a => None + | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a) + | PApp a b => + match hred a with + | Some a => Some (PApp a b) + | None => None + end + | PPair a b => None + | PProj p (PPair a b) => if p is PL then Some a else Some b + | PProj p a => + match hred a with + | Some a => Some (PProj p a) + | None => None + end + | PUniv i => None + | PBind p A B => None + | PNat => None + | PZero => None + | PSuc a => None + | PInd P PZero b c => Some b + | PInd P (PSuc a) b c => + Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) + | PInd P a b c => + match hred a with + | Some a => Some (PInd P a b c) + | None => None + end + end. + +Lemma hred_complete (a b : PTm) : + HRed.R a b -> hred a = Some b. +Proof. + induction 1; hauto lq:on rew:off inv:HRed.R b:on. +Qed. + +Lemma hred_sound (a b : PTm): + hred a = Some b -> HRed.R a b. +Proof. + elim : a b; hauto q:on dep:on ctrs:HRed.R. +Qed. + +Lemma hred_deter (a b0 b1 : PTm) : + HRed.R a b0 -> HRed.R a b1 -> b0 = b1. +Proof. + move /hred_complete => + /hred_complete. congruence. +Qed. + +Definition fancy_hred (a : PTm) : HRed.nf a + {b | HRed.R a b}. + destruct (hred a) eqn:eq. + right. exists p. by apply hred_sound in eq. + left. move => b /hred_complete. congruence. +Defined. + Ltac2 destruct_algo () := lazy_match! goal with | [h : algo_dom ?a ?b |- _ ] => @@ -34,79 +373,70 @@ Ltac solve_check_equal := | _ => idtac end]. -Global Set Transparent Obligations. +#[derive(equations=no)]Equations check_equal (a b : PTm) (h : algo_dom a b) : + bool by struct h := + check_equal a b h with tm_to_eq_view a b := + check_equal _ _ h (V_VarVar i j) := nat_eqdec i j; + check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv); + check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); + check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); + check_equal _ _ h (V_PairPair a0 b0 a1 b1) := + check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal _ _ h (V_PairNeu a0 b0 u _) := + check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); + check_equal _ _ h (V_NeuPair u a1 b1 _) := + check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); + check_equal _ _ h V_NatNat := true; + check_equal _ _ h V_ZeroZero := true; + check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv); + check_equal _ _ h (V_ProjProj p0 a p1 b) := + PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); + check_equal _ _ h (V_AppApp a0 b0 a1 b1) := + check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) := + check_equal_r P0 P1 ltac:(check_equal_triv) && + check_equal u0 u1 ltac:(check_equal_triv) && + check_equal_r b0 b1 ltac:(check_equal_triv) && + check_equal_r c0 c1 ltac:(check_equal_triv); + check_equal _ _ h (V_UnivUniv i j) := nat_eqdec i j; + check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) := + BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); + check_equal _ _ _ _ := false -Local Obligation Tactic := try solve [check_equal_triv | sfirstorder]. - -Program Fixpoint check_equal (a b : PTm) (h : algo_dom a b) {struct h} : bool := - match a, b with - | VarPTm i, VarPTm j => nat_eqdec i j - | PAbs a, PAbs b => check_equal_r a b _ - | PAbs a, VarPTm _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _ - | PAbs a, PApp _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _ - | PAbs a, PInd _ _ _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _ - | PAbs a, PProj _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _ - | VarPTm _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _ - | PApp _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _ - | PProj _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _ - | PInd _ _ _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _ - | PPair a0 b0, PPair a1 b1 => - check_equal_r a0 a1 _ && check_equal_r b0 b1 _ - | PPair a0 b0, VarPTm _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _ - | PPair a0 b0, PProj _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _ - | PPair a0 b0, PApp _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _ - | PPair a0 b0, PInd _ _ _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _ - | VarPTm _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _ - | PApp _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _ - | PProj _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _ - | PInd _ _ _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _ - | PNat, PNat => true - | PZero, PZero => true - | PSuc a, PSuc b => check_equal_r a b _ - | PProj p0 a, PProj p1 b => PTag_eqdec p0 p1 && check_equal a b _ - | PApp a0 b0, PApp a1 b1 => check_equal a0 a1 _ && check_equal_r b0 b1 _ - | PInd P0 u0 b0 c0, PInd P1 u1 b1 c1 => - check_equal_r P0 P1 _ && check_equal u0 u1 _ && check_equal_r b0 b1 _ && check_equal_r c0 c1 _ - | PUniv i, PUniv j => nat_eqdec i j - | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_eqdec p0 p1 && check_equal_r A0 A1 _ && check_equal_r B0 B1 _ - | _, _ => false - end -with check_equal_r (a b : PTm) (h : algo_dom_r a b) {struct h} : bool := - match fancy_hred a with - | inr a' => check_equal_r (proj1_sig a') b _ - | inl ha' => match fancy_hred b with - | inr b' => check_equal_r a (proj1_sig b') _ - | inl hb' => check_equal a b _ - end - end. + (* check_equal a b h := false; *) + with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) : + bool by struct h0 := + check_equal_r a b h with (fancy_hred a) := + check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _; + check_equal_r a b h (inl h') with (fancy_hred b) := + | inr b' := check_equal_r a (proj1_sig b') _; + | inl h'' := check_equal a b _. Next Obligation. - simpl. intros. clear Heq_anonymous. destruct a' as [a' ha']. simpl. + intros. inversion h; subst => //=. - exfalso. sfirstorder use:algo_dom_no_hred. - assert (a' = a'0) by eauto using hred_deter. by subst. + exfalso. hauto l:on use:hred_complete unfold:HRed.nf. + exfalso. hauto l:on use:hred_complete unfold:HRed.nf. +Defined. + +Next Obligation. + intros. + destruct h. + exfalso. sfirstorder use: algo_dom_no_hred. exfalso. sfirstorder. + assert ( b' = b'0)by eauto using hred_deter. subst. + apply h. Defined. Next Obligation. - simpl. intros. clear Heq_anonymous Heq_anonymous0. - destruct b' as [b' hb']. simpl. - inversion h; subst. - - exfalso. - sfirstorder use:algo_dom_no_hred. - - exfalso. - sfirstorder. - - assert (b' = b'0) by eauto using hred_deter. by subst. + simpl. intros. + inversion h; subst =>//=. + exfalso. sfirstorder use:algo_dom_no_hred. + move {h}. + assert (a' = a'0) by eauto using hred_deter, hred_sound. by subst. + exfalso. sfirstorder use:hne_no_hred, hf_no_hred. Defined. -(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *) -Next Obligation. - move => /= a b hdom ha _ hb _. - inversion hdom; subst. - - assumption. - - exfalso; sfirstorder. - - exfalso; sfirstorder. -Defined. Lemma check_equal_abs_abs a b h : check_equal (PAbs a) (PAbs b) (A_AbsAbs a b h) = check_equal_r a b h. Proof. reflexivity. Qed. @@ -161,14 +491,14 @@ Proof. sfirstorder use:hred_complete, hred_sound. Qed. -Ltac simp_check_r := with_strategy opaque [check_equal] simpl in *. - Lemma check_equal_nfnf a b dom : check_equal_r a b (A_NfNf a b dom) = check_equal a b dom. Proof. have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:algo_dom_no_hred. have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none. - simp_check_r. + simpl. + rewrite /check_equal_r_functional. destruct (fancy_hred a). + simpl. destruct (fancy_hred b). reflexivity. exfalso. hauto l:on use:hred_complete. @@ -179,9 +509,11 @@ Lemma check_equal_hredl a b a' ha doma : check_equal_r a b (A_HRedL a a' b ha doma) = check_equal_r a' b doma. Proof. simpl. + rewrite /check_equal_r_functional. destruct (fancy_hred a). - hauto q:on unfold:HRed.nf. - destruct s as [x ?]. + rewrite /check_equal_r_functional. have ? : x = a' by eauto using hred_deter. subst. simpl. f_equal. @@ -192,7 +524,7 @@ Lemma check_equal_hredr a b b' hu r a0 : check_equal_r a b (A_HRedR a b b' hu r a0) = check_equal_r a b' a0. Proof. - simpl. + simpl. rewrite /check_equal_r_functional. destruct (fancy_hred a). - simpl. destruct (fancy_hred b) as [|[b'' hb']]. @@ -215,51 +547,31 @@ Proof. destruct a; destruct b => //=. Qed. #[export]Hint Rewrite check_equal_abs_abs check_equal_abs_neu check_equal_neu_abs check_equal_pair_pair check_equal_pair_neu check_equal_neu_pair check_equal_bind_bind check_equal_hredl check_equal_hredr check_equal_nfnf check_equal_conf : ce_prop. -Ltac2 destruct_salgo () := - lazy_match! goal with - | [h : salgo_dom ?a ?b |- _ ] => - if is_var a then destruct $a; ltac1:(done) else - (if is_var b then destruct $b; ltac1:(done) else ()) - end. +Obligation Tactic := try solve [check_equal_triv | sfirstorder]. -Ltac check_sub_triv := - intros;subst; - lazymatch goal with - (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *) - | [_ : salgo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo)) - | _ => idtac - end. - -Local Obligation Tactic := try solve [check_sub_triv | sfirstorder]. - -Program Fixpoint check_sub (a b : PTm) (h : salgo_dom a b) {struct h} := +Program Fixpoint check_sub (q : bool) (a b : PTm) (h : algo_dom a b) {struct h} := match a, b with | PBind PPi A0 B0, PBind PPi A1 B1 => - check_sub_r A1 A0 _ && check_sub_r B0 B1 _ + check_sub_r (negb q) A0 A1 _ && check_sub_r q B0 B1 _ | PBind PSig A0 B0, PBind PSig A1 B1 => - check_sub_r A0 A1 _ && check_sub_r B0 B1 _ + check_sub_r q A0 A1 _ && check_sub_r q B0 B1 _ | PUniv i, PUniv j => - PeanoNat.Nat.leb i j + if q then PeanoNat.Nat.leb i j else PeanoNat.Nat.leb j i | PNat, PNat => true - | PApp _ _ , PApp _ _ => check_equal a b _ - | VarPTm _, VarPTm _ => check_equal a b _ - | PInd _ _ _ _, PInd _ _ _ _ => check_equal a b _ - | PProj _ _, PProj _ _ => check_equal a b _ - | _, _ => false + | _ ,_ => ishne a && ishne b && check_equal a b h end -with check_sub_r (a b : PTm) (h : salgo_dom_r a b) {struct h} := +with check_sub_r (q : bool) (a b : PTm) (h : algo_dom_r a b) {struct h} := match fancy_hred a with - | inr a' => check_sub_r (proj1_sig a') b _ + | inr a' => check_sub_r q (proj1_sig a') b _ | inl ha' => match fancy_hred b with - | inr b' => check_sub_r a (proj1_sig b') _ - | inl hb' => check_sub a b _ + | inr b' => check_sub_r q a (proj1_sig b') _ + | inl hb' => check_sub q a b _ end end. - Next Obligation. simpl. intros. clear Heq_anonymous. destruct a' as [a' ha']. simpl. inversion h; subst => //=. - exfalso. sfirstorder use:salgo_dom_no_hred. + exfalso. sfirstorder use:algo_dom_no_hred. assert (a' = a'0) by eauto using hred_deter. by subst. exfalso. sfirstorder. Defined. @@ -269,7 +581,7 @@ Next Obligation. destruct b' as [b' hb']. simpl. inversion h; subst. - exfalso. - sfirstorder use:salgo_dom_no_hred. + sfirstorder use:algo_dom_no_hred. - exfalso. sfirstorder. - assert (b' = b'0) by eauto using hred_deter. by subst. @@ -277,30 +589,34 @@ Defined. (* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *) Next Obligation. - move => /= a b hdom ha _ hb _. + move => _ /= a b hdom ha _ hb _. inversion hdom; subst. - assumption. - exfalso; sfirstorder. - exfalso; sfirstorder. Defined. -Lemma check_sub_pi_pi A0 B0 A1 B1 h0 h1 : - check_sub (PBind PPi A0 B0) (PBind PPi A1 B1) (S_PiCong A0 A1 B0 B1 h0 h1) = - check_sub_r A1 A0 h0 && check_sub_r B0 B1 h1. +Lemma check_sub_pi_pi q A0 B0 A1 B1 h0 h1 : + check_sub q (PBind PPi A0 B0) (PBind PPi A1 B1) (A_BindCong PPi PPi A0 A1 B0 B1 h0 h1) = + check_sub_r (~~ q) A0 A1 h0 && check_sub_r q B0 B1 h1. Proof. reflexivity. Qed. -Lemma check_sub_sig_sig A0 B0 A1 B1 h0 h1 : - check_sub (PBind PSig A0 B0) (PBind PSig A1 B1) (S_SigCong A0 A1 B0 B1 h0 h1) = - check_sub_r A0 A1 h0 && check_sub_r B0 B1 h1. -Proof. reflexivity. Qed. +Lemma check_sub_sig_sig q A0 B0 A1 B1 h0 h1 : + check_sub q (PBind PSig A0 B0) (PBind PSig A1 B1) (A_BindCong PSig PSig A0 A1 B0 B1 h0 h1) = + check_sub_r q A0 A1 h0 && check_sub_r q B0 B1 h1. + reflexivity. Qed. Lemma check_sub_univ_univ i j : - check_sub (PUniv i) (PUniv j) (S_UnivCong i j) = PeanoNat.Nat.leb i j. + check_sub true (PUniv i) (PUniv j) (A_UnivCong i j) = PeanoNat.Nat.leb i j. Proof. reflexivity. Qed. -Lemma check_sub_nfnf a b dom : check_sub_r a b (S_NfNf a b dom) = check_sub a b dom. +Lemma check_sub_univ_univ' i j : + check_sub false (PUniv i) (PUniv j) (A_UnivCong i j) = PeanoNat.Nat.leb j i. + reflexivity. Qed. + +Lemma check_sub_nfnf q a b dom : check_sub_r q a b (A_NfNf a b dom) = check_sub q a b dom. Proof. - have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred. + have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:algo_dom_no_hred. have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none. simpl. destruct (fancy_hred b)=>//=. @@ -311,8 +627,8 @@ Proof. hauto l:on use:hred_complete. Qed. -Lemma check_sub_hredl a b a' ha doma : - check_sub_r a b (S_HRedL a a' b ha doma) = check_sub_r a' b doma. +Lemma check_sub_hredl q a b a' ha doma : + check_sub_r q a b (A_HRedL a a' b ha doma) = check_sub_r q a' b doma. Proof. simpl. destruct (fancy_hred a). @@ -324,9 +640,9 @@ Proof. apply PropExtensionality.proof_irrelevance. Qed. -Lemma check_sub_hredr a b b' hu r a0 : - check_sub_r a b (S_HRedR a b b' hu r a0) = - check_sub_r a b' a0. +Lemma check_sub_hredr q a b b' hu r a0 : + check_sub_r q a b (A_HRedR a b b' hu r a0) = + check_sub_r q a b' a0. Proof. simpl. destruct (fancy_hred a). @@ -341,10 +657,4 @@ Proof. sfirstorder use:hne_no_hred, hf_no_hred. Qed. -Lemma check_sub_neuneu a b i a0 : check_sub a b (S_NeuNeu a b i a0) = check_equal a b a0. -Proof. destruct a,b => //=. Qed. - -Lemma check_sub_conf a b n n0 i : check_sub a b (S_Conf a b n n0 i) = false. -Proof. destruct a,b=>//=; ecrush inv:BTag. Qed. - -#[export]Hint Rewrite check_sub_neuneu check_sub_conf check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop. +#[export]Hint Rewrite check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ' check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop. diff --git a/theories/executable_correct.v b/theories/executable_correct.v index 40debce..6ccee46 100644 --- a/theories/executable_correct.v +++ b/theories/executable_correct.v @@ -23,14 +23,6 @@ Proof. inversion 3; subst => //=. Qed. -Lemma coqeq_neuneu' u0 u1 : - neuneu_nonconf u0 u1 -> - u0 ↔ u1 -> - u0 ∼ u1. -Proof. - induction 2 => //=; destruct u => //=. -Qed. - Lemma check_equal_sound : (forall a b (h : algo_dom a b), check_equal a b h -> a ↔ b) /\ (forall a b (h : algo_dom_r a b), check_equal_r a b h -> a ⇔ b). @@ -71,15 +63,15 @@ Proof. - sfirstorder. - move => i j /sumboolP ?. subst. apply : CE_NeuNeu. apply CE_VarCong. - - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE. - rewrite check_equal_app_app in hE. - move /andP : hE => [h0 h1]. - sauto lq:on use:coqeq_neuneu. - move => p0 p1 u0 u1 neu0 neu1 h ih he. apply CE_NeuNeu. rewrite check_equal_proj_proj in he. move /andP : he => [/sumboolP ? h1]. subst. sauto lq:on use:coqeq_neuneu. + - move => u0 u1 a0 a1 hu0 hu1 hdom ih hdom' ih' hE. + rewrite check_equal_app_app in hE. + move /andP : hE => [h0 h1]. + sauto lq:on use:coqeq_neuneu. - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc. rewrite check_equal_ind_ind. move /andP => [/andP [/andP [h0 h1] h2 ] h3]. @@ -125,14 +117,14 @@ Proof. - simp check_equal. done. - move => i j. move => h. have {h} : ~ nat_eqdec i j by done. case : nat_eqdec => //=. ce_solv. - - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1. - rewrite check_equal_app_app. - move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu. - move => p0 p1 u0 u1 neu0 neu1 h ih. rewrite check_equal_proj_proj. move /negP /nandP. case. case : PTag_eqdec => //=. sauto lq:on. sauto lqb:on. + - move => u0 u1 a0 a1 hu0 hu1 h0 ih0 h1 ih1. + rewrite check_equal_app_app. + move /negP /nandP. sauto b:on inv:CoqEq, CoqEq_Neu. - move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc. rewrite check_equal_ind_ind. move => + h. @@ -180,31 +172,39 @@ Qed. Ltac simp_sub := with_strategy opaque [check_equal] simpl in *. +(* Reusing algo_dom results in an inefficient proof, but i'll brute force it so i can get the result more quickly *) Lemma check_sub_sound : - (forall a b (h : salgo_dom a b), check_sub a b h -> a ⋖ b) /\ - (forall a b (h : salgo_dom_r a b), check_sub_r a b h -> a ≪ b). + (forall a b (h : algo_dom a b), forall q, check_sub q a b h -> if q then a ⋖ b else b ⋖ a) /\ + (forall a b (h : algo_dom_r a b), forall q, check_sub_r q a b h -> if q then a ≪ b else b ≪ a). Proof. - apply salgo_dom_mutual; try done. + apply algo_dom_mutual; try done. + - move => a [] //=; hauto qb:on. + - move => a0 a1 []//=; hauto qb:on. - simpl. move => i j []; sauto lq:on use:Reflect.Nat_leb_le. - - move => A0 A1 B0 B1 s ihs s0 ihs0. - simp ce_prop. - hauto lqb:on ctrs:CoqLEq. - - move => A0 A1 B0 B1 s ihs s0 ihs0. - simp ce_prop. - hauto lqb:on ctrs:CoqLEq. - - qauto ctrs:CoqLEq. - - move => a b i a0. - simp ce_prop. - move => h. apply CLE_NeuNeu. - hauto lq:on use:check_equal_sound, coqeq_neuneu', coqeq_symmetric_mutual. - - move => a b n n0 i. - by simp ce_prop. - - move => a b h ih. simp ce_prop. hauto l:on. - - move => a a' b hr h ih. - simp ce_prop. - sauto lq:on rew:off. - - move => a b b' n r dom ihdom. + - move => p0 p1 A0 A1 B0 B1 a iha b ihb q. + case : p0; case : p1; try done; simp ce_prop. + sauto lqb:on. + sauto lqb:on. + - hauto l:on. + - move => i j q h. + have {}h : nat_eqdec i j by sfirstorder. + case : nat_eqdec h => //=; sauto lq:on. + - simp_sub. + sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound. + - simp_sub. + sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound. + - simp_sub. + sauto lqb:on use:coqeq_symmetric_mutual, coqeq_neuneu, check_equal_sound. + - move => a b n n0 i q h. + exfalso. + destruct a, b; try done; simp_sub; hauto lb:on use:check_equal_conf. + - move => a b doma ihdom q. + simp ce_prop. sauto lq:on. + - move => a a' b hr doma ihdom q. + simp ce_prop. move : ihdom => /[apply]. move {doma}. + sauto lq:on. + - move => a b b' n r dom ihdom q. simp ce_prop. move : ihdom => /[apply]. move {dom}. @@ -212,48 +212,91 @@ Proof. Qed. Lemma check_sub_complete : - (forall a b (h : salgo_dom a b), check_sub a b h = false -> ~ a ⋖ b) /\ - (forall a b (h : salgo_dom_r a b), check_sub_r a b h = false -> ~ a ≪ b). + (forall a b (h : algo_dom a b), forall q, check_sub q a b h = false -> if q then ~ a ⋖ b else ~ b ⋖ a) /\ + (forall a b (h : algo_dom_r a b), forall q, check_sub_r q a b h = false -> if q then ~ a ≪ b else ~ b ≪ a). Proof. - apply salgo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu]. - - move => i j /=. - move => + h. inversion h; subst => //=. - sfirstorder use:PeanoNat.Nat.leb_le. - hauto lq:on inv:CoqEq_Neu. - - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop. + apply algo_dom_mutual; try first [done | hauto depth:4 lq:on inv:CoqLEq, CoqEq_Neu]. + - move => i j q /=. + sauto lq:on rew:off use:PeanoNat.Nat.leb_le. + - move => p0 p1 A0 A1 B0 B1 a iha b ihb []. + + move => + h. inversion h; subst; simp ce_prop. + * move /nandP. + case. + by move => /negbTE {}/iha. + by move => /negbTE {}/ihb. + * move /nandP. + case. + by move => /negbTE {}/iha. + by move => /negbTE {}/ihb. + * inversion H. + + move => + h. inversion h; subst; simp ce_prop. + * move /nandP. + case. + by move => /negbTE {}/iha. + by move => /negbTE {}/ihb. + * move /nandP. + case. + by move => /negbTE {}/iha. + by move => /negbTE {}/ihb. + * inversion H. + - simp_sub. + sauto lq:on use:check_equal_complete. + - simp_sub. + move => p0 p1 u0 u1 i i0 a iha q. move /nandP. case. - move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu. - move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu. - - move => A0 A1 B0 B1 s ihs s' ihs'. simp ce_prop. + move /nandP. + case => //. + by move /negP. + by move /negP. + move /negP. + move => h. eapply check_equal_complete in h. + sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on. + - move => u0 u1 a0 a1 i i0 a hdom ihdom hdom' ihdom'. + simp_sub. move /nandP. case. - move => /negbTE {}/ihs. hauto q:on inv:CoqLEq, CoqEq_Neu. - move => /negbTE {}/ihs'. hauto q:on inv:CoqLEq, CoqEq_Neu. - - move => a b i hs. simp ce_prop. - move => + h. inversion h; subst => //=. - move => /negP h0. - eapply check_equal_complete in h0. - apply h0. by constructor. - - 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. - inversion h1; subst. - hauto l:on use:hreds_nf_refl. - - move => a a' b h dom. - simp ce_prop => /[apply]. - move => + h1. inversion h1; subst. - inversion H; subst. - + sfirstorder use:coqleq_no_hred unfold:HRed.nf. - + have ? : y = a' by eauto using hred_deter. subst. + move/nandP. + case. + by move/negP. + by move/negP. + move /negP. + move => h. eapply check_equal_complete in h. + sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on. + - move => P0 P1 u0 u1 b0 b1 c0 c1 i i0 dom ihdom dom' ihdom' dom'' ihdom'' dom''' ihdom''' q. + move /nandP. + case. + move /nandP. + case => //=. + by move/negP. + by move/negP. + move /negP => h. eapply check_equal_complete in h. + sauto use:coqeq_symmetric_mutual inv:CoqLEq lq:on. + - move => a b h ih q. simp ce_prop => {}/ih. + case : q => h0; + inversion 1; subst; hauto l:on use:algo_dom_no_hred, hreds_nf_refl. + - move => a a' b r dom ihdom q. + simp ce_prop => {}/ihdom. + case : q => h0. + inversion 1; subst. + inversion H0; subst. sfirstorder use:coqleq_no_hred. + have ? : a' = y by eauto using hred_deter. subst. + sauto lq:on. + inversion 1; subst. + inversion H1; subst. sfirstorder use:coqleq_no_hred. + have ? : a' = y by eauto using hred_deter. subst. + sauto lq:on. + - move => a b b' n r hr ih q. + simp ce_prop => {}/ih. + case : q. + + move => h. inversion 1; subst. + inversion H1; subst. + sfirstorder use:coqleq_no_hred. + have ? : b' = y by eauto using hred_deter. subst. + sauto lq:on. + + move => h. inversion 1; subst. + inversion H0; subst. + sfirstorder use:coqleq_no_hred. + have ? : b' = y by eauto using hred_deter. subst. sauto lq:on. - - move => a b b' u hr dom ihdom. - rewrite check_sub_hredr. - move => + h. inversion h; subst. - have {}u : HRed.nf a by sfirstorder use:hne_no_hred, hf_no_hred. - move => {}/ihdom. - inversion H0; subst. - + have ? : HRed.nf b'0 by hauto l:on use:coqleq_no_hred. - sfirstorder unfold:HRed.nf. - + sauto lq:on use:hred_deter. Qed. diff --git a/theories/fp_red.v b/theories/fp_red.v index 382f25b..9d8718b 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -10,7 +10,7 @@ From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn). From Hammer Require Import Tactics. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common. Require Import Btauto. - +Require Import Cdcl.Itauto. Ltac2 spec_refl () := List.iter @@ -2575,7 +2575,7 @@ Module LoReds. ~~ ishf a. Proof. move : hf_preservation. repeat move/[apply]. - case : a; case : b => //=; sfirstorder b:on. + case : a; case : b => //=; itauto. Qed. #[local]Ltac solve_s_rec := @@ -2633,7 +2633,7 @@ Module LoReds. rtc LoRed.R (PSuc a0) (PSuc a1). Proof. solve_s. Qed. - Local Ltac triv := simpl in *; sfirstorder b:on. + Local Ltac triv := simpl in *; itauto. Lemma FromSN_mutual : (forall (a : PTm) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\ @@ -3048,7 +3048,7 @@ Module DJoin. have {h0 h1 h2 h3} : isbind c /\ isuniv c by hauto l:on use:REReds.bind_preservation, REReds.univ_preservation. - case : c => //=; sfirstorder b:on. + case : c => //=; itauto. Qed. Lemma hne_univ_noconf (a b : PTm) : @@ -3078,7 +3078,7 @@ Module DJoin. Proof. move => [c [h0 h1]] h2 h3. have : ishne c /\ isnat c by sfirstorder use:REReds.hne_preservation, REReds.nat_preservation. - clear. case : c => //=; sfirstorder b:on. + clear. case : c => //=; itauto. Qed. Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 : @@ -3594,7 +3594,7 @@ Module Sub. hauto l:on use:REReds.bind_preservation, REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation. move : h2 h3. clear. - case : c => //=; sfirstorder b:on. + case : c => //=; itauto. Qed. Lemma univ_bind_noconf (a b : PTm) : @@ -3605,7 +3605,7 @@ Module Sub. hauto l:on use:REReds.bind_preservation, REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation. move : h2 h3. clear. - case : c => //=; sfirstorder b:on. + case : c => //=; itauto. Qed. Lemma bind_inj p0 p1 (A0 A1 : PTm) B0 B1 : diff --git a/theories/logrel.v b/theories/logrel.v index d4b4bd9..a479f81 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -6,7 +6,7 @@ Require Import ssreflect ssrbool. Require Import Logic.PropExtensionality (propositional_extensionality). From stdpp Require Import relations (rtc(..), rtc_subrel). Import Psatz. - +Require Import Cdcl.Itauto. Definition ProdSpace (PA : PTm -> Prop) (PF : PTm -> (PTm -> Prop) -> Prop) b : Prop := @@ -355,7 +355,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : SNe H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. + suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto. move : hA hAB. clear. hauto lq:on db:noconf. move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst. tauto. @@ -365,7 +365,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : SNe H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. + suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto. move : hAB hA h0. clear. hauto lq:on db:noconf. move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst. tauto. @@ -375,7 +375,7 @@ Proof. have {hU} {}h : Sub.R (PBind p A B) H by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have{h0} : isbind H. - suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. + suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto. have : isbind (PBind p A B) by scongruence. move : h. clear. hauto l:on db:noconf. case : H h1 h => //=. @@ -394,7 +394,7 @@ Proof. have {hU} {}h : Sub.R H (PBind p A B) by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have{h0} : isbind H. - suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by sfirstorder b:on. + suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto. have : isbind (PBind p A B) by scongruence. move : h. clear. move : (PBind p A B). hauto lq:on db:noconf. case : H h1 h => //=. @@ -413,7 +413,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R PNat H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : isnat H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on. + suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto. have : @isnat PNat by simpl. move : h0 hAB. clear. qauto l:on db:noconf. case : H h1 hAB h0 => //=. @@ -424,7 +424,7 @@ Proof. move => [H [/DJoin.FromRedSNs h [h1 h0]]]. have {h}{}hAB : Sub.R H PNat by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive. have {}h0 : isnat H. - suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by sfirstorder b:on. + suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto. have : @isnat PNat by simpl. move : h0 hAB. clear. qauto l:on db:noconf. case : H h1 hAB h0 => //=. @@ -1058,7 +1058,7 @@ Definition Γ_sub' Γ Δ := forall ρ, ρ_ok Δ ρ -> ρ_ok Γ ρ. Definition Γ_eq' Γ Δ := forall ρ, ρ_ok Δ ρ <-> ρ_ok Γ ρ. Lemma Γ_sub'_refl Γ : Γ_sub' Γ Γ. - rewrite /Γ_sub'. sfirstorder b:on. Qed. + rewrite /Γ_sub'. itauto. Qed. Lemma Γ_sub'_cons Γ Δ A B i j : Sub.R B A -> diff --git a/theories/termination.v b/theories/termination.v index c5bc37e..8afe24e 100644 --- a/theories/termination.v +++ b/theories/termination.v @@ -3,3 +3,280 @@ From Hammer Require Import Tactics. Require Import ssreflect ssrbool. From stdpp Require Import relations (nsteps (..), rtc(..)). Import Psatz. + +Lemma tm_conf_sym a b : tm_conf a b = tm_conf b a. +Proof. case : a; case : b => //=. Qed. + +#[export]Hint Constructors algo_dom algo_dom_r : adom. + +Lemma algo_dom_r_inv a b : + algo_dom_r a b -> exists a0 b0, algo_dom a0 b0 /\ rtc HRed.R a a0 /\ rtc HRed.R b b0. +Proof. + induction 1; hauto lq:on ctrs:rtc. +Qed. + +Lemma A_HRedsL a a' b : + rtc HRed.R a a' -> + algo_dom_r a' b -> + algo_dom_r a b. + induction 1; sfirstorder use:A_HRedL. +Qed. + +Lemma A_HRedsR a b b' : + HRed.nf a -> + rtc HRed.R b b' -> + algo_dom a b' -> + algo_dom_r a b. +Proof. induction 2; sauto. Qed. + +Lemma algo_dom_sym : + (forall a b (h : algo_dom a b), algo_dom b a) /\ + (forall a b (h : algo_dom_r a b), algo_dom_r b a). +Proof. + apply algo_dom_mutual; try qauto use:tm_conf_sym db:adom. + move => a a' b hr h ih. + move /algo_dom_r_inv : ih => [a0][b0][ih0][ih1]ih2. + have nfa0 : HRed.nf a0 by sfirstorder use:algo_dom_no_hred. + sauto use:A_HRedsL, A_HRedsR. +Qed. + +Definition term_metric k (a b : PTm) := + exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k. + +Lemma term_metric_sym k (a b : PTm) : + term_metric k a b -> term_metric k b a. +Proof. hauto lq:on unfold:term_metric solve+:lia. Qed. + +Lemma term_metric_case k (a b : PTm) : + term_metric k a b -> + (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ term_metric k' a' b /\ k' < k. +Proof. + move=>[i][j][va][vb][h0] [h1][h2][h3]h4. + case : a h0 => //=; try firstorder. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.AppAbs unfold:term_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia. + + sfirstorder qb:on use:ne_hne. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.ProjPair unfold:term_metric solve+:lia. + + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia. + - inversion h0 as [|A B C D E F]; subst. + hauto qb:on use:ne_hne. + inversion E; subst => /=. + + hauto lq:on use:HRed.IndZero unfold:term_metric solve+:lia. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia. + + sfirstorder use:ne_hne. + + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia. + + sfirstorder use:ne_hne. + + sfirstorder use:ne_hne. +Qed. + +Lemma A_Conf' a b : + ishf a \/ ishne a -> + ishf b \/ ishne b -> + tm_conf a b -> + algo_dom_r a b. +Proof. + move => ha hb. + have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred. + have {}hb : HRed.nf b by sfirstorder use:hf_no_hred, hne_no_hred. + move => ?. + apply A_NfNf. + by apply A_Conf. +Qed. + +Lemma term_metric_abs : forall k a b, + term_metric k (PAbs a) (PAbs b) -> + exists k', k' < k /\ term_metric k' a b. +Proof. + move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h. + apply lored_nsteps_abs_inv in hva, hvb. + move : hva => [a'][hva]?. subst. + move : hvb => [b'][hvb]?. subst. + simpl in *. exists (k - 1). + hauto lq:on unfold:term_metric solve+:lia. +Qed. + +Lemma term_metric_pair : forall k a0 b0 a1 b1, + term_metric k (PPair a0 b0) (PPair a1 b1) -> + exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1. +Proof. + move => k a0 b0 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h. + apply lored_nsteps_pair_inv in hva, hvb. + decompose record hva => {hva}. + decompose record hvb => {hvb}. subst. + simpl in *. exists (k - 1). + hauto lqb:on solve+:lia. +Qed. + +Lemma term_metric_bind : forall k p0 a0 b0 p1 a1 b1, + term_metric k (PBind p0 a0 b0) (PBind p1 a1 b1) -> + exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1. +Proof. + move => k p0 a0 b0 p1 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h. + apply lored_nsteps_bind_inv in hva, hvb. + decompose record hva => {hva}. + decompose record hvb => {hvb}. subst. + simpl in *. exists (k - 1). + hauto lqb:on solve+:lia. +Qed. + +Lemma term_metric_suc : forall k a b, + term_metric k (PSuc a) (PSuc b) -> + exists k', k' < k /\ term_metric k' a b. +Proof. + move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h. + apply lored_nsteps_suc_inv in hva, hvb. + move : hva => [a'][hva]?. subst. + move : hvb => [b'][hvb]?. subst. + simpl in *. exists (k - 1). + hauto lq:on unfold:term_metric solve+:lia. +Qed. + +Lemma term_metric_abs_neu k (a0 : PTm) u : + term_metric k (PAbs a0) u -> + ishne u -> + exists j, j < k /\ term_metric j a0 (PApp (ren_PTm shift u) (VarPTm var_zero)). +Proof. + move => [i][j][va][vb][h0][h1][h2][h3]h4 neu. + have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps. + move /lored_nsteps_abs_inv : h0 => [a1][h01]?. subst. + exists (k - 1). + simpl in *. split. lia. + exists i,j,a1,(PApp (ren_PTm shift vb) (VarPTm var_zero)). + repeat split => //=. + apply lored_nsteps_app_cong. + by apply lored_nsteps_renaming. + by rewrite ishne_ren. + rewrite Bool.andb_true_r. + sfirstorder use:ne_nf_ren. + rewrite size_PTm_ren. lia. +Qed. + +Lemma term_metric_pair_neu k (a0 b0 : PTm) u : + term_metric k (PPair a0 b0) u -> + ishne u -> + exists j, j < k /\ term_metric j (PProj PL u) a0 /\ term_metric j (PProj PR u) b0. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3]h4 neu. + have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps. + move /lored_nsteps_pair_inv : h0 => [i0][j0][a1][b1][?][?][?][?]?. subst. + exists (k-1). sauto qb:on use:lored_nsteps_proj_cong unfold:term_metric solve+:lia. +Qed. + +Lemma term_metric_app k (a0 b0 a1 b1 : PTm) : + term_metric k (PApp a0 b0) (PApp a1 b1) -> + ishne a0 -> + ishne a1 -> + exists j, j < k /\ term_metric j a0 a1 /\ term_metric j b0 b1. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3]h4. + move => hne0 hne1. + move : lored_nsteps_app_inv h0 (hne0);repeat move/[apply]. + move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. + move : lored_nsteps_app_inv h1 (hne1);repeat move/[apply]. + move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. + simpl in *. exists (k - 1). hauto lqb:on use:lored_nsteps_app_cong, ne_nf unfold:term_metric solve+:lia. +Qed. + +Lemma term_metric_proj k p0 p1 (a0 a1 : PTm) : + term_metric k (PProj p0 a0) (PProj p1 a1) -> + ishne a0 -> + ishne a1 -> + exists j, j < k /\ term_metric j a0 a1. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1. + move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply]. + move => [i0][a2][hi][?]ha02. subst. + move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply]. + move => [i1][a3][hj][?]ha13. subst. + exists (k- 1). hauto q:on use:ne_nf solve+:lia. +Qed. + +Lemma term_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 : + term_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) -> + ishne a0 -> + ishne a1 -> + exists j, j < k /\ term_metric j P0 P1 /\ term_metric j a0 a1 /\ + term_metric j b0 b1 /\ term_metric j c0 c1. +Proof. + move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1. + move /lored_nsteps_ind_inv /(_ hne0) : h0. + move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst. + move /lored_nsteps_ind_inv /(_ hne1) : h1. + move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst. + exists (k -1). simpl in *. + hauto lq:on rew:off use:ne_nf b:on solve+:lia. +Qed. + + +Lemma algo_dom_r_algo_dom : forall a b, HRed.nf a -> HRed.nf b -> algo_dom_r a b -> algo_dom a b. +Proof. hauto l:on use:algo_dom_r_inv, hreds_nf_refl. Qed. + +Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b. +Proof. + move => [:hneL]. + elim /Wf_nat.lt_wf_ind. + move => n ih a b h. + case /term_metric_case : (h); cycle 1. + move => [k'][a'][h0][h1]h2. + by apply : A_HRedL; eauto. + case /term_metric_sym /term_metric_case : (h); cycle 1. + move => [k'][b'][hb][/term_metric_sym h0]h1. + move => ha. have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred. + by apply : A_HRedR; eauto. + move => /[swap]. + case => hfa; case => hfb. + - move : hfa hfb h. + case : a; case : b => //=; eauto 5 using A_Conf' with adom. + + hauto lq:on use:term_metric_abs db:adom. + + hauto lq:on use:term_metric_pair db:adom. + + hauto lq:on use:term_metric_bind db:adom. + + hauto lq:on use:term_metric_suc db:adom. + - abstract : hneL n ih a b h hfa hfb. + case : a hfa h => //=. + + hauto lq:on use:term_metric_abs_neu db:adom. + + scrush use:term_metric_pair_neu db:adom. + + case : b hfb => //=; eauto 5 using A_Conf' with adom. + + case : b hfb => //=; eauto 5 using A_Conf' with adom. + + case : b hfb => //=; eauto 5 using A_Conf' with adom. + + case : b hfb => //=; eauto 5 using A_Conf' with adom. + + case : b hfb => //=; eauto 5 using A_Conf' with adom. + - hauto q:on use:algo_dom_sym, term_metric_sym. + - move {hneL}. + case : b hfa hfb h => //=; case a => //=; eauto 5 using A_Conf' with adom. + + move => a0 b0 a1 b1 nfa0 nfa1. + move /term_metric_app /(_ nfa0 nfa1) => [j][hj][ha]hb. + apply A_NfNf. apply A_AppCong => //; eauto. + have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred. + have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred. + eauto using algo_dom_r_algo_dom. + + move => p0 A0 p1 A1 neA0 neA1. + have {}nfa0 : HRed.nf A0 by sfirstorder use:hne_no_hred. + have {}nfb0 : HRed.nf A1 by sfirstorder use:hne_no_hred. + hauto lq:on use:term_metric_proj, algo_dom_r_algo_dom db:adom. + + move => P0 a0 b0 c0 P1 a1 b1 c1 nea0 nea1. + have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred. + have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred. + hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom. +Qed. + +Lemma sn_term_metric (a b : PTm) : SN a -> SN b -> exists k, term_metric k a b. +Proof. + move /LoReds.FromSN => [va [ha0 ha1]]. + move /LoReds.FromSN => [vb [hb0 hb1]]. + eapply relations.rtc_nsteps in ha0. + eapply relations.rtc_nsteps in hb0. + hauto lq:on unfold:term_metric solve+:lia. +Qed. + +Lemma sn_algo_dom a b : SN a -> SN b -> algo_dom_r a b. +Proof. + move : sn_term_metric; repeat move/[apply]. + move => [k]+. + eauto using term_metric_algo_dom. +Qed.