From 849d19708ee4d1e4eede8236123102e68a22db9c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 10 Mar 2025 14:30:36 -0400 Subject: [PATCH] Add new definition of algo_dom --- theories/algorithmic.v | 362 +++++++++++++++++++----------------- theories/common.v | 412 ++++++++++++++++++++++++++++++++++++++++- theories/executable.v | 212 --------------------- theories/termination.v | 261 -------------------------- 4 files changed, 599 insertions(+), 648 deletions(-) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index ab8fe97..dff32da 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -673,8 +673,12 @@ Proof. hauto lq:on use:HReds.ToEq, E_Symmetric, E_Transitive. 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. +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 ne_hne (a : PTm) : ne a -> ishne a. Proof. elim : a => //=; sfirstorder b:on. Qed. @@ -698,37 +702,58 @@ Proof. - hauto lq:on use:ne_hne. Qed. -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. +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][[v [h4 h5]]] h6. + 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:algo_metric solve+:lia. - + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. + + 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:algo_metric solve+:lia. - + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. + + 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:algo_metric solve+:lia. - + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. + + 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:algo_metric solve+:lia. + + 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 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 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 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 hred_hne (a b : PTm) : HRed.R a b -> @@ -1028,28 +1053,6 @@ 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 -> @@ -1103,174 +1106,185 @@ Lemma lored_nsteps_pair_inv k (a0 b0 C : PTm ) : exists i, (S j), a1, b1. sauto lq:on solve+:lia. Qed. -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 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. +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). - 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. + hauto lq:on unfold:term_metric solve+:lia. 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). +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. - induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming. + 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 algo_metric_neu_abs k (a0 : PTm) u : - algo_metric k u (PAbs a0) -> +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 /\ algo_metric j (PApp (ren_PTm shift u) (VarPTm var_zero)) a0. + 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]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. + 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 algo_metric_neu_pair k (a0 b0 : PTm) u : - algo_metric k u (PPair a0 b0) -> +Lemma term_metric_pair_neu k (a0 b0 : PTm) u : + term_metric k (PPair a0 b0) u -> ishne u -> - exists j, j < k /\ algo_metric j (PProj PL u) a0 /\ algo_metric j (PProj PR u) b0. + 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]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. + 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 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) -> +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 /\ algo_metric j P0 P1 /\ algo_metric j a0 a1 /\ - algo_metric j b0 b1 /\ algo_metric j c0 c1. + 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]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 => [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). - 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. + simpl in *. exists (k - 1). hauto lqb:on use:lored_nsteps_app_cong, ne_nf unfold:term_metric solve+:lia. Qed. -Lemma algo_metric_suc k (a0 a1 : PTm) : - algo_metric k (PSuc a0) (PSuc a1) -> - exists j, j < k /\ algo_metric j a0 a1. +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]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. + 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 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. +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]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. + 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 coqeq_complete' k (a b : PTm ) : + (forall a b, algo_dom a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) + 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). diff --git a/theories/common.v b/theories/common.v index 3ea15d6..c14bbb3 100644 --- a/theories/common.v +++ b/theories/common.v @@ -1,4 +1,4 @@ -Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect. +Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect ssrbool. From Equations Require Import Equations. Derive NoConfusion for nat PTag BTag PTm. Derive EqDec for BTag PTag PTm. @@ -6,6 +6,7 @@ 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) @@ -119,6 +120,28 @@ 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 _ _ => (~~ 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. + + + Definition ishf_ren (a : PTm) (ξ : nat -> nat) : ishf (ren_PTm ξ a) = ishf a. Proof. case : a => //=. Qed. @@ -175,3 +198,390 @@ 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_NeuNeu a b : + algo_dom_neu a b -> + algo_dom a b + +| A_Conf a b : + HRed.nf a -> + HRed.nf b -> + tm_conf a b -> + algo_dom a b + +with algo_dom_neu : PTm -> PTm -> Prop := +| A_VarCong i j : + (* -------------------------- *) + algo_dom_neu (VarPTm i) (VarPTm j) + +| A_AppCong u0 u1 a0 a1 : + ishne u0 -> + ishne u1 -> + algo_dom_neu u0 u1 -> + algo_dom_r a0 a1 -> + (* ------------------------- *) + algo_dom_neu (PApp u0 a0) (PApp u1 a1) + +| A_ProjCong p0 p1 u0 u1 : + ishne u0 -> + ishne u1 -> + algo_dom_neu u0 u1 -> + (* --------------------- *) + algo_dom_neu (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_neu u0 u1 -> + algo_dom_r b0 b1 -> + algo_dom_r c0 c1 -> + algo_dom_neu (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) + +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 algo_neu_ind := Induction for algo_dom_neu Sort Prop + with algor_ind := Induction for algo_dom_r Sort Prop. + +Combined Scheme algo_dom_mutual from algo_ind, algo_neu_ind, algor_ind. +#[export]Hint Constructors algo_dom algo_dom_neu 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 _ _ => (~~ ishf a) && (~~ ishf b) + | PProj _ _, PProj _ _ => (~~ ishf a) && (~~ ishf b) + | PInd _ _ _ _, PInd _ _ _ _ => (~~ ishf a) && (~~ ishf b) + | _, _ => 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 : + algo_dom_neu a b -> + salgo_dom a b + +| S_Conf a b : + HRed.nf a -> + HRed.nf 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. + +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 + | [h : 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_neu_hne (a b : PTm) : + algo_dom_neu a b -> + ishne a /\ ishne b. +Proof. inversion 1; subst => //=. 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 use:algo_dom_neu_hne 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, algo_dom_neu a b -> algo_dom_neu 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_neu_hne 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. + +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_neu a b -> True) /\ + (forall a b, algo_dom_r a b -> salgo_dom_r a b /\ salgo_dom_r b a). +Proof. + apply algo_dom_mutual => //=; + try hauto lq:on ctrs:salgo_dom, algo_dom_neu, salgo_dom_r use:S_Conf, hne_no_hred, algo_dom_sym, tm_stm_conf, S_HRedR' inv:HRed.R unfold:HRed.nf solve+:destruct_salgo. + - case;case; hauto lq:on ctrs:salgo_dom, algo_dom_neu, salgo_dom_r use:S_Conf, hne_no_hred, algo_dom_sym inv:HRed.R unfold:HRed.nf solve+:destruct_salgo. + - move => a b ha hb /[dup] /tm_stm_conf h. + rewrite tm_conf_sym => /tm_stm_conf h0. + hauto l:on use:S_Conf inv:HRed.R unfold:HRed.nf. +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. diff --git a/theories/executable.v b/theories/executable.v index 44557f9..fd03f2d 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -11,26 +11,6 @@ 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) @@ -102,121 +82,6 @@ Equations tm_to_eq_view (a b : PTm) : eq_view a b := 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 : *) @@ -273,83 +138,6 @@ Combined Scheme algo_dom_mutual from algo_ind, algor_ind. (* 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 |- _ ] => diff --git a/theories/termination.v b/theories/termination.v index 8afe24e..41400ef 100644 --- a/theories/termination.v +++ b/theories/termination.v @@ -4,267 +4,6 @@ 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]].