From 96b31397265910c301fe6fd10adeb6578be2ee3e Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 6 Mar 2025 15:39:27 -0500 Subject: [PATCH 1/4] Prove termination --- theories/algorithmic.v | 6 + theories/executable.v | 5 + theories/executable_correct.v | 13 -- theories/termination.v | 258 +++++++++++++++++++++++++++++++++- 4 files changed, 266 insertions(+), 16 deletions(-) diff --git a/theories/algorithmic.v b/theories/algorithmic.v index 8a9146a..ab8fe97 100644 --- a/theories/algorithmic.v +++ b/theories/algorithmic.v @@ -1050,6 +1050,12 @@ Proof. 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 -> diff --git a/theories/executable.v b/theories/executable.v index 0586a41..156e691 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -486,3 +486,8 @@ Lemma check_equal_conf a b nfa nfb nfab : 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. + +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. diff --git a/theories/executable_correct.v b/theories/executable_correct.v index 0720d03..fdfee5a 100644 --- a/theories/executable_correct.v +++ b/theories/executable_correct.v @@ -4,12 +4,6 @@ Require Import ssreflect ssrbool. From stdpp Require Import relations (rtc(..)). From Hammer Require Import Tactics. -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. - - Lemma coqeqr_no_hred a b : a ∼ b -> HRed.nf a /\ HRed.nf b. Proof. induction 1; sauto lq:on unfold:HRed.nf. Qed. @@ -18,7 +12,6 @@ Proof. induction 1; qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred unfold:HRed.nf. Qed. - Lemma coqeq_neuneu u0 u1 : ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1. Proof. @@ -88,12 +81,6 @@ Proof. sauto lq:on rew:off. Qed. -Lemma hreds_nf_refl a b : - HRed.nf a -> - rtc HRed.R a b -> - a = b. -Proof. inversion 2; sfirstorder. Qed. - Ltac ce_solv := move => *; simp ce_prop in *; hauto qb:on rew:off inv:CoqEq, CoqEq_Neu. Lemma check_equal_complete : diff --git a/theories/termination.v b/theories/termination.v index 61f1e1d..53474b6 100644 --- a/theories/termination.v +++ b/theories/termination.v @@ -1,14 +1,266 @@ Require Import common Autosubst2.core Autosubst2.unscoped Autosubst2.syntax algorithmic fp_red executable. From Hammer Require Import Tactics. Require Import ssreflect ssrbool. -From stdpp Require Import relations (nsteps (..)). +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. + move : hva => [?][?][?][?][?][?][?][?]?. + move : 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. + move : hva => [?][?][?][?][?][?][?][?]?. + move : 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 : (fancy_hred a); cycle 1. - move => [a' ha']. apply : A_HRedL; eauto. + 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. From 6f154cc9c61961a896a260b2dede10b44bf7890b Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 6 Mar 2025 16:20:32 -0500 Subject: [PATCH 2/4] Add stub for check_sub --- theories/executable.v | 22 ++++++++++++++++++---- theories/termination.v | 16 ++++++++++++++++ 2 files changed, 34 insertions(+), 4 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 156e691..a6fa438 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -212,6 +212,11 @@ with algo_dom_r : PTm -> PTm -> Prop := (* ----------------------- *) 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. + Lemma hf_no_hred (a b : PTm) : ishf a -> HRed.R a b -> @@ -351,7 +356,6 @@ Ltac solve_check_equal := | inr b' := check_equal_r a (proj1_sig b') _; | inl h'' := check_equal a b _. - Next Obligation. intros. inversion h; subst => //=. @@ -487,7 +491,17 @@ 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. -Scheme algo_ind := Induction for algo_dom Sort Prop - with algor_ind := Induction for algo_dom_r Sort Prop. +Obligation Tactic := solve [check_equal_triv | sfirstorder]. -Combined Scheme algo_dom_mutual from algo_ind, algor_ind. +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 (negb q) A0 A1 _ && check_sub_r q B0 B1 _ + | PBind PSig A0 B0, PBind PSig A1 B1 => + check_sub_r q A0 A1 _ && check_sub_r q B0 B1 _ + | PUniv i, PUniv j => + if q then PeanoNat.Nat.leb i j else PeanoNat.Nat.leb j i + | PNat, PNat => true + | _ ,_ => ishne a && ishne b && check_equal a b h + end +with check_sub_r (q : bool) (a b : PTm) (h : algo_dom_r a b) {struct h} := false. diff --git a/theories/termination.v b/theories/termination.v index 53474b6..0f8314d 100644 --- a/theories/termination.v +++ b/theories/termination.v @@ -264,3 +264,19 @@ Proof. 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. From fe52d78ec5b96c6a5db5919b120c35db3091c9db Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 6 Mar 2025 19:20:54 -0500 Subject: [PATCH 3/4] Start the soundness proof for check_sub --- theories/executable.v | 101 +++++++++++++++++++++++++++++++++- theories/executable_correct.v | 23 ++++++++ 2 files changed, 122 insertions(+), 2 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index a6fa438..4ca9c5b 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -491,7 +491,7 @@ 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. -Obligation Tactic := solve [check_equal_triv | sfirstorder]. +Obligation Tactic := try solve [check_equal_triv | sfirstorder]. Program Fixpoint check_sub (q : bool) (a b : PTm) (h : algo_dom a b) {struct h} := match a, b with @@ -504,4 +504,101 @@ Program Fixpoint check_sub (q : bool) (a b : PTm) (h : algo_dom a b) {struct h} | PNat, PNat => true | _ ,_ => ishne a && ishne b && check_equal a b h end -with check_sub_r (q : bool) (a b : PTm) (h : algo_dom_r a b) {struct h} := false. +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 q (proj1_sig a') b _ + | inl ha' => match fancy_hred b with + | 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:algo_dom_no_hred. + assert (a' = a'0) by eauto using hred_deter. by subst. + exfalso. sfirstorder. +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. +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_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 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 true (PUniv i) (PUniv j) (A_UnivCong i j) = PeanoNat.Nat.leb i j. +Proof. reflexivity. Qed. + +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: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)=>//=. + destruct (fancy_hred a) =>//=. + destruct s as [a' ha']. simpl. + hauto l:on use:hred_complete. + destruct s as [b' hb']. simpl. + hauto l:on use:hred_complete. +Qed. + +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). + - hauto q:on unfold:HRed.nf. + - destruct s as [x ?]. + have ? : x = a' by eauto using hred_deter. subst. + simpl. + f_equal. + apply PropExtensionality.proof_irrelevance. +Qed. + +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). + - simpl. + destruct (fancy_hred b) as [|[b'' hb']]. + + hauto lq:on unfold:HRed.nf. + + simpl. + have ? : (b'' = b') by eauto using hred_deter. subst. + f_equal. + apply PropExtensionality.proof_irrelevance. + - exfalso. + sfirstorder use:hne_no_hred, hf_no_hred. +Qed. + +#[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 fdfee5a..3cc6233 100644 --- a/theories/executable_correct.v +++ b/theories/executable_correct.v @@ -164,3 +164,26 @@ Proof. sfirstorder unfold:HRed.nf. + sauto lq:on use:hred_deter. Qed. + +Ltac simp_sub := with_strategy opaque [check_equal] simpl. + +Lemma check_sub_sound : + (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 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. + - admit. + - 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. + move => p0 p1 u0 u1 i i0 dom ihdom q. + move /andP => [/andP [h00 h01] h1]. + best use:check_sub_ + +best b:on use:check_equal_sound. From 437c97455e7d55255349d02b26071e831b1c2be3 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 6 Mar 2025 20:42:08 -0500 Subject: [PATCH 4/4] Finish the soundness and completeness proof of the subtyping algorithm --- theories/executable.v | 56 +++++++++++++++ theories/executable_correct.v | 125 ++++++++++++++++++++++++++++++++-- theories/termination.v | 8 +-- 3 files changed, 179 insertions(+), 10 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 4ca9c5b..44557f9 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -217,6 +217,62 @@ Scheme algo_ind := Induction for algo_dom 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 -> diff --git a/theories/executable_correct.v b/theories/executable_correct.v index 3cc6233..6ccee46 100644 --- a/theories/executable_correct.v +++ b/theories/executable_correct.v @@ -12,6 +12,11 @@ Proof. induction 1; qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred unfold:HRed.nf. Qed. +Lemma coqleq_no_hred a b : a ⋖ b -> HRed.nf a /\ HRed.nf b. +Proof. + induction 1; qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred, coqeqr_no_hred unfold:HRed.nf. +Qed. + Lemma coqeq_neuneu u0 u1 : ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1. Proof. @@ -165,8 +170,9 @@ Proof. + sauto lq:on use:hred_deter. Qed. -Ltac simp_sub := with_strategy opaque [check_equal] simpl. +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 : 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). @@ -176,14 +182,121 @@ Proof. - move => a0 a1 []//=; hauto qb:on. - simpl. move => i j []; sauto lq:on use:Reflect.Nat_leb_le. - - admit. + - 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. - move => p0 p1 u0 u1 i i0 dom ihdom q. - move /andP => [/andP [h00 h01] h1]. - best use:check_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}. + sauto lq:on rew:off. +Qed. -best b:on use:check_equal_sound. +Lemma check_sub_complete : + (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 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 /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/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. +Qed. diff --git a/theories/termination.v b/theories/termination.v index 0f8314d..8afe24e 100644 --- a/theories/termination.v +++ b/theories/termination.v @@ -107,8 +107,8 @@ Lemma term_metric_pair : forall k a0 b0 a1 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. - move : hva => [?][?][?][?][?][?][?][?]?. - move : hvb => [?][?][?][?][?][?][?][?]?. subst. + decompose record hva => {hva}. + decompose record hvb => {hvb}. subst. simpl in *. exists (k - 1). hauto lqb:on solve+:lia. Qed. @@ -119,8 +119,8 @@ Lemma term_metric_bind : forall k p0 a0 b0 p1 a1 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. - move : hva => [?][?][?][?][?][?][?][?]?. - move : hvb => [?][?][?][?][?][?][?][?]?. subst. + decompose record hva => {hva}. + decompose record hvb => {hvb}. subst. simpl in *. exists (k - 1). hauto lqb:on solve+:lia. Qed.