Add stub for the new coqleq_complete'

theories/algorithmic.v

@@ -1647,26 +1647,31 @@ 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.
-  suff : exists k, algo_metric k a b by hauto lq:on use:coqeq_complete', regularity.
+  have : algo_dom_r a b /\ DJoin.R a b by
-  eapply fundamental_theorem in h.
+    hauto lq:on use:fundamental_theorem, logrel.SemEq_SemWt, logrel.SemWt_SN, sn_algo_dom.
-  move /logrel.SemEq_SN_Join : h.
+  hauto lq:on use:regularity, coqeq_complete'.
-  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 :=
@@ -1708,269 +1713,176 @@ 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 ) := *)
+Lemma coqleq_sound_mutual :
-(*   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. *)
+    (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 ).
+Proof.
+  apply coqleq_mutual.
+  - hauto lq:on use:wff_mutual ctrs:LEq.
+  - move => A0 A1 B0 B1 hA ihA hB ihB Γ i.
+    move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1.
+    have hlA  : Γ ⊢ A1 ≲ A0 by sfirstorder.
+    have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
+    apply Su_Transitive with (B := PBind PPi A1 B0).
+    by apply : Su_Pi; eauto using E_Refl, Su_Eq.
+    apply : Su_Pi; eauto using E_Refl, Su_Eq.
+    apply : ihB; eauto using ctx_eq_subst_one.
+  - move => A0 A1 B0 B1 hA ihA hB ihB Γ i.
+    move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1.
+    have hlA  : Γ ⊢ A0 ≲ A1 by sfirstorder.
+    have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
+    apply Su_Transitive with (B := PBind PSig A0 B1).
+    apply : Su_Sig; eauto using E_Refl, Su_Eq.
+    apply : ihB; by eauto using ctx_eq_subst_one.
+    apply : Su_Sig; eauto using E_Refl, Su_Eq.
+  - sauto lq:on use:coqeq_sound_mutual, Su_Eq.
+  - sauto lq:on use:coqeq_sound_mutual, Su_Eq.
+  - move => a a' b b' ? ? ? ih Γ i ha hb.
+    have /Su_Eq ? : Γ ⊢ a ≡ a' ∈ PUniv i by sfirstorder use:HReds.ToEq.
+    have /E_Symmetric /Su_Eq ? : Γ ⊢ b ≡ b' ∈ PUniv i by sfirstorder use:HReds.ToEq.
+    suff : Γ ⊢ a' ≲ b' by eauto using Su_Transitive.
+    eauto using HReds.preservation.
+Qed.
 
-(* Lemma salgo_metric_algo_metric k (a b : PTm) : *)
+Lemma CLE_HRedL (a a' b : PTm )  :
-(*   ishne a \/ ishne b -> *)
+  HRed.R a a' ->
-(*   salgo_metric k a b -> *)
+  a' ≪ b ->
-(*   algo_metric k a b. *)
+  a ≪ b.
-(* Proof. *)
+Proof.
-(*   move => h. *)
+  hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
-(*   move => [i][j][va][vb][hva][hvb][nva][nvb][hS]sz. *)
+Qed.
-(*   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 : *)
+Lemma CLE_HRedR (a a' b : PTm)  :
-(*     (forall (a b : PTm), a ⋖ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ) /\ *)
+  HRed.R a a' ->
-(*     (forall (a b : PTm), a ≪ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ). *)
+  b ≪ a' ->
-(* Proof. *)
+  b ≪ a.
-(*   apply coqleq_mutual. *)
+Proof.
-(*   - hauto lq:on use:wff_mutual ctrs:LEq. *)
+  hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
-(*   - move => A0 A1 B0 B1 hA ihA hB ihB Γ i. *)
+Qed.
-(*     move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1. *)
-(*     have hlA  : Γ ⊢ A1 ≲ A0 by sfirstorder. *)
-(*     have hΓ : ⊢ Γ by sfirstorder use:wff_mutual. *)
-(*     apply Su_Transitive with (B := PBind PPi A1 B0). *)
-(*     by apply : Su_Pi; eauto using E_Refl, Su_Eq. *)
-(*     apply : Su_Pi; eauto using E_Refl, Su_Eq. *)
-(*     apply : ihB; eauto using ctx_eq_subst_one. *)
-(*   - move => A0 A1 B0 B1 hA ihA hB ihB Γ i. *)
-(*     move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1. *)
-(*     have hlA  : Γ ⊢ A0 ≲ A1 by sfirstorder. *)
-(*     have hΓ : ⊢ Γ by sfirstorder use:wff_mutual. *)
-(*     apply Su_Transitive with (B := PBind PSig A0 B1). *)
-(*     apply : Su_Sig; eauto using E_Refl, Su_Eq. *)
-(*     apply : ihB; by eauto using ctx_eq_subst_one. *)
-(*     apply : Su_Sig; eauto using E_Refl, Su_Eq. *)
-(*   - sauto lq:on use:coqeq_sound_mutual, Su_Eq. *)
-(*   - sauto lq:on use:coqeq_sound_mutual, Su_Eq. *)
-(*   - move => a a' b b' ? ? ? ih Γ i ha hb. *)
-(*     have /Su_Eq ? : Γ ⊢ a ≡ a' ∈ PUniv i by sfirstorder use:HReds.ToEq. *)
-(*     have /E_Symmetric /Su_Eq ? : Γ ⊢ b ≡ b' ∈ PUniv i by sfirstorder use:HReds.ToEq. *)
-(*     suff : Γ ⊢ a' ≲ b' by eauto using Su_Transitive. *)
-(*     eauto using HReds.preservation. *)
-(* Qed. *)
 
-(* Lemma salgo_metric_case k (a b : PTm ) : *)
+Lemma coqleq_complete' :
-(*   salgo_metric k a b -> *)
+  (forall a b, salgo_dom a b -> Sub.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⋖ b) /\
-(*   (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ salgo_metric k' a' b /\ k' < k. *)
+  (forall a b, salgo_dom_r a b -> Sub.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ≪ b).
-(* Proof. *)
+Proof.
-(*   move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6. *)
+  apply salgo_dom_mutual.
-(*   case : a h0 => //=; try firstorder. *)
+  - move => i j /Sub.univ_inj.
-(*   - inversion h0 as [|A B C D E F]; subst. *)
+    hauto lq:on ctrs:CoqLEq.
-(*     hauto qb:on use:ne_hne. *)
+  - admit.
-(*     inversion E; subst => /=. *)
+  - admit.
-(*     + hauto lq:on use:HRed.AppAbs unfold:algo_metric solve+:lia. *)
+  - sfirstorder.
-(*     + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. *)
+  - admit.
-(*     + sfirstorder qb:on use:ne_hne. *)
+  - admit.
-(*   - inversion h0 as [|A B C D E F]; subst. *)
+  - hauto l:on.
-(*     hauto qb:on use:ne_hne. *)
+  - move => a a' b hr ha iha hj Γ A wta wtb.
-(*     inversion E; subst => /=. *)
+    apply : CLE_HRedL; eauto.
-(*     + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia. *)
+    apply : iha; eauto; last by sfirstorder use:HRed.preservation.
-(*     + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. *)
+    apply : Sub.transitive; eauto.
-(*   - inversion h0 as [|A B C D E F]; subst. *)
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
-(*     hauto qb:on use:ne_hne. *)
+    apply /Sub.FromJoin /DJoin.FromRRed1. by apply HRed.ToRRed.
-(*     inversion E; subst => /=. *)
+  - move => a b b' nfa hr h ih j Γ A wta wtb.
-(*     + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia. *)
+    apply : CLE_HRedR; eauto.
-(*     + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. *)
+    apply : ih; eauto; last by eauto using HRed.preservation.
-(*     + sfirstorder use:ne_hne. *)
+    apply : Sub.transitive; eauto.
-(*     + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. *)
+    hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
-(*     + sfirstorder use:ne_hne. *)
+    apply /Sub.FromJoin /DJoin.FromRRed0. by apply HRed.ToRRed.
-(*     + sfirstorder use:ne_hne. *)
+Admitted.
-(* Qed. *)
-
-(* Lemma CLE_HRedL (a a' b : PTm )  : *)
-(*   HRed.R a a' -> *)
-(*   a' ≪ b -> *)
-(*   a ≪ b. *)
-(* Proof. *)
-(*   hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R. *)
-(* Qed. *)
-
-(* Lemma CLE_HRedR (a a' b : PTm)  : *)
-(*   HRed.R a a' -> *)
-(*   b ≪ a' -> *)
-(*   b ≪ a. *)
-(* Proof. *)
-(*   hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R. *)
-(* Qed. *)
 
 
-(* Lemma algo_metric_caseR k (a b : PTm) : *)
+  move : k a b.
-(*   salgo_metric k a b -> *)
+  elim /Wf_nat.lt_wf_ind.
-(*   (ishf b \/ ishne b) \/ exists k' b', HRed.R b b' /\ salgo_metric k' a b' /\ k' < k. *)
+  move => n ih.
-(* Proof. *)
+  move => a b /[dup] h /salgo_metric_case.
-(*   move=>[i][j][va][vb][h0] [h1][h2][h3][[v [h4 h5]]] h6. *)
+  (* Cases where a and b can take steps *)
-(*   case : b h1 => //=; try by firstorder. *)
+  case; cycle 1.
-(*   - inversion 1 as [|A B C D E F]; subst. *)
+  move : a b h.
-(*     hauto qb:on use:ne_hne. *)
+  qauto l:on use:HRed.preservation, CLE_HRedL, hred_hne.
-(*     inversion E; subst => /=. *)
+  case /algo_metric_caseR : (h); cycle 1.
-(*     + hauto q:on use:HRed.AppAbs unfold:salgo_metric solve+:lia. *)
+  qauto l:on use:HRed.preservation, CLE_HRedR, hred_hne.
-(*     + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:salgo_metric solve+:lia. *)
+  (* Cases where neither a nor b can take steps *)
-(*     + sfirstorder qb:on use:ne_hne. *)
+  case => fb; case => fa.
-(*   - inversion 1 as [|A B C D E F]; subst. *)
+  - case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-(*     hauto qb:on use:ne_hne. *)
+    + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-(*     inversion E; subst => /=. *)
+      * move => p0 A0 B0 _ p1 A1 B1 _.
-(*     + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia. *)
+        move => h.
-(*     + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia. *)
+        have ? : p1 = p0 by
-(*   - inversion 1 as [|A B C D E F]; subst. *)
+          hauto lq:on rew:off use:salgo_metric_sub, Sub.bind_inj.
-(*     hauto qb:on use:ne_hne. *)
+        subst.
-(*     inversion E; subst => /=. *)
+        case : p0 h => //=.
-(*     + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia. *)
+        ** move /salgo_metric_pi.
-(*     + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. *)
+           move => [j [hj [hA hB]]] Γ i.
-(*     + sfirstorder use:ne_hne. *)
+           move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
-(*     + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia. *)
+           have ihA : A0 ≪ A1 by hauto l:on.
-(*     + sfirstorder use:ne_hne. *)
+           econstructor; eauto using E_Refl; constructor=> //.
-(*     + sfirstorder use:ne_hne. *)
+           have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual.
-(* Qed. *)
+           suff : (cons A0 Γ) ⊢ B1 ∈ PUniv i
-
+             by hauto l:on.
-(* Lemma salgo_metric_sub k (a b : PTm) : *)
+           eauto using ctx_eq_subst_one.
-(*   salgo_metric k a b -> *)
+        ** move /salgo_metric_sig.
-(*   Sub.R a b. *)
+           move => [j [hj [hA hB]]] Γ i.
-(* Proof. *)
+           move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
-(*   rewrite /algo_metric. *)
+           have ihA : A1 ≪ A0 by hauto l:on.
-(*   move => [i][j][va][vb][h0][h1][h2][h3][[va' [vb' [hva [hvb hS]]]]]h5. *)
+           econstructor; eauto using E_Refl; constructor=> //.
-(*   have {}h0 : rtc LoRed.R a va by hauto lq:on use:@relations.rtc_nsteps. *)
+           have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual.
-(*   have {}h1 : rtc LoRed.R b vb by hauto lq:on use:@relations.rtc_nsteps. *)
+           suff : (cons A1 Γ) ⊢ B0 ∈ PUniv i
-(*   apply REReds.FromEReds in hva,hvb. *)
+             by hauto l:on.
-(*   apply LoReds.ToRReds in h0,h1. *)
+           eauto using ctx_eq_subst_one.
-(*   apply REReds.FromRReds in h0,h1. *)
+      * hauto lq:on use:salgo_metric_sub, Sub.bind_univ_noconf.
-(*   rewrite /Sub.R. exists va', vb'. sfirstorder use:@relations.rtc_transitive. *)
+      * hauto lq:on use:salgo_metric_sub, Sub.nat_bind_noconf.
-(* Qed. *)
+      * move => _ > _ /salgo_metric_sub.
-
+        hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv inv:Sub1.R.
-(* Lemma salgo_metric_pi k (A0 : PTm) B0 A1 B1  : *)
+      * hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R.
-(*   salgo_metric k (PBind PPi A0 B0) (PBind PPi A1 B1) -> *)
+    + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-(*   exists j, j < k /\ salgo_metric j A1 A0 /\ salgo_metric j B0 B1. *)
+      * hauto lq:on use:salgo_metric_sub, Sub.univ_bind_noconf.
-(* Proof. *)
+      * move => *. econstructor; eauto using rtc_refl.
-(*   move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. *)
+        hauto lq:on use:salgo_metric_sub, Sub.univ_inj, CLE_UnivCong.
-(*   move : lored_nsteps_bind_inv h0 => /[apply]. *)
+      * hauto lq:on rew:off use:REReds.univ_inv, REReds.nat_inv, salgo_metric_sub inv:Sub1.R.
-(*   move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. *)
+      * hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R.
-(*   move : lored_nsteps_bind_inv h1 => /[apply]. *)
+      * hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R.
-(*   move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. *)
+  (* Both cases are impossible *)
-(*   move /ESub.pi_inj : h4 => [? ?]. *)
+    + case : b fb => //=.
-(*   hauto qb:on solve+:lia. *)
+      * hauto lq:on use:T_AbsNat_Imp.
-(* Qed. *)
+      * 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.
-(* Lemma salgo_metric_sig k (A0 : PTm) B0 A1 B1  : *)
+      * hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R.
-(*   salgo_metric k (PBind PSig A0 B0) (PBind PSig A1 B1) -> *)
+      * hauto l:on.
-(*   exists j, j < k /\ salgo_metric j A0 A1 /\ salgo_metric j B0 B1. *)
+      * hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R.
-(* Proof. *)
+      * hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R.
-(*   move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. *)
+    + move => ? ? Γ i /Zero_Inv.
-(*   move : lored_nsteps_bind_inv h0 => /[apply]. *)
+      clear.
-(*   move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst. *)
+      move /synsub_to_usub => [_ [_ ]].
-(*   move : lored_nsteps_bind_inv h1 => /[apply]. *)
+      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R.
-(*   move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst. *)
+    + move => ? _ _ Γ i /Suc_Inv => [[_]].
-(*   move /ESub.sig_inj : h4 => [? ?]. *)
+      move /synsub_to_usub.
-(*   hauto qb:on solve+:lia. *)
+      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R.
-(* Qed. *)
+  - have {}h : DJoin.R a b by
-
+       hauto lq:on use:salgo_metric_algo_metric, algo_metric_join.
-(* Lemma coqleq_complete' k (a b : PTm ) : *)
+    case : b fb h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-(*   salgo_metric k a b -> (forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b). *)
+    + hauto lq:on use:DJoin.hne_bind_noconf.
-(* Proof. *)
+    + hauto lq:on use:DJoin.hne_univ_noconf.
-(*   move : k a b. *)
+    + hauto lq:on use:DJoin.hne_nat_noconf.
-(*   elim /Wf_nat.lt_wf_ind. *)
+    + move => _ _ Γ i _.
-(*   move => n ih. *)
+      move /Zero_Inv.
-(*   move => a b /[dup] h /salgo_metric_case. *)
+      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-(*   (* Cases where a and b can take steps *) *)
+    + move => p _ _ Γ i _ /Suc_Inv.
-(*   case; cycle 1. *)
+      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-(*   move : a b h. *)
+  - have {}h : DJoin.R b a by
-(*   qauto l:on use:HRed.preservation, CLE_HRedL, hred_hne. *)
+      hauto lq:on use:salgo_metric_algo_metric, algo_metric_join, DJoin.symmetric.
-(*   case /algo_metric_caseR : (h); cycle 1. *)
+    case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
-(*   qauto l:on use:HRed.preservation, CLE_HRedR, hred_hne. *)
+    + hauto lq:on use:DJoin.hne_bind_noconf.
-(*   (* Cases where neither a nor b can take steps *) *)
+    + hauto lq:on use:DJoin.hne_univ_noconf.
-(*   case => fb; case => fa. *)
+    + hauto lq:on use:DJoin.hne_nat_noconf.
-(*   - case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. *)
+    + move => _ _ Γ i.
-(*     + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'. *)
+      move /Zero_Inv.
-(*       * move => p0 A0 B0 _ p1 A1 B1 _. *)
+      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-(*         move => h. *)
+    + move => p _ _ Γ i /Suc_Inv.
-(*         have ? : p1 = p0 by *)
+      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
-(*           hauto lq:on rew:off use:salgo_metric_sub, Sub.bind_inj. *)
+  - move => Γ i ha hb.
-(*         subst. *)
+    econstructor; eauto using rtc_refl.
-(*         case : p0 h => //=. *)
+    apply CLE_NeuNeu. move {ih}.
-(*         ** move /salgo_metric_pi. *)
+    have {}h : algo_metric n a b by
-(*            move => [j [hj [hA hB]]] Γ i. *)
+      hauto lq:on use:salgo_metric_algo_metric.
-(*            move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0]. *)
+    eapply coqeq_complete'; eauto.
-(*            have ihA : A0 ≪ A1 by hauto l:on. *)
+Qed.
-(*            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. *)

theories/common.v

@@ -403,6 +403,8 @@ with salgo_dom_r : PTm -> PTm -> Prop :=
 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 ->

theories/executable.v

@@ -341,4 +341,10 @@ Proof.
     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_pi_pi check_sub_sig_sig : ce_prop.
+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.

theories/executable_correct.v

@@ -180,17 +180,6 @@ Qed.
 
 Ltac simp_sub := with_strategy opaque [check_equal] simpl in *.
 
-Combined Scheme salgo_dom_mutual from salgo_ind, salgor_ind.
-
-(* 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_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.
-
-Hint Rewrite check_sub_neuneu check_sub_conf : ce_prop.
-
 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).

theories/termination.v

@@ -3,19 +3,3 @@ From Hammer Require Import Tactics.
 Require Import ssreflect ssrbool.
 From stdpp Require Import relations (nsteps (..), rtc(..)).
 Import Psatz.
-
-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.