Prove some impossible cases

theories/algorithmic.v

@@ -831,6 +831,12 @@ Lemma algo_metric_join n k (a b : PTm n) :
   rewrite /DJoin.R. exists v. sfirstorder use:@relations.rtc_transitive.
 Qed.
 
+Lemma T_Univ_Raise n Γ (a : PTm n) i j :
+  Γ ⊢ a ∈ PUniv i ->
+  i <= j ->
+  Γ ⊢ a ∈ PUniv j.
+Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
+
 Lemma coqeq_complete n k (a b : PTm n) :
   algo_metric k a b ->
   (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\
@@ -909,22 +915,24 @@ Proof.
           by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
         have ? : Γ ⊢ PUniv i1 ≲ PUniv (max i0 i1)
           by hauto lq:on rew:off use:Su_Univ, wff_mutual solve+:lia.
-        have hA0' : Γ ⊢ A0 ∈ PUniv (max i0 i1) by eauto using T_Conv.
-        have hA1' : Γ ⊢ A1 ∈ PUniv (max i0 i1) by eauto using T_Conv.
+        have {}hA0 : Γ ⊢ A0 ∈ PUniv (max i0 i1) by eauto using T_Conv.
+        have {}hA1 : Γ ⊢ A1 ∈ PUniv (max i0 i1) by eauto using T_Conv.
+        have {}hB0 : funcomp (ren_PTm shift) (scons A0 Γ) ⊢
+                       B0 ∈ PUniv (max i0 i1)
+          by hauto lq:on use:T_Univ_Raise solve+:lia.
+        have {}hB1 : funcomp (ren_PTm shift) (scons A1 Γ) ⊢
+                       B1 ∈ PUniv (max i0 i1)
+          by hauto lq:on use:T_Univ_Raise solve+:lia.
+
         have ihA : A0 ⇔ A1 by hauto l:on.
         have hAE : Γ ⊢ A0 ≡ A1 ∈ PUniv (Nat.max i0 i1)
           by hauto l:on use:coqeq_sound_mutual.
         apply : CE_HRed; eauto using rtc_refl.
         constructor => //.
-        admit.
-        (* eapply ih; eauto. *)
-        (* move /Su_Eq in hAE. *)
-        (* apply : ctx_eq_subst_one; eauto. *)
 
-      (* Show that A0 and A1 are algorithmically equal *)
-      (* Use soundness to show that they are actually definitionally equal *)
-      (* Use that to show that B0 and B1 can be assigned the same type *)
-        (* admit. *)
+        eapply ih; eauto.
+        apply : ctx_eq_subst_one; eauto.
+        eauto using Su_Eq.
       * move => > /algo_metric_join.
         hauto lq:on use:DJoin.bind_univ_noconf.
     + case : b => //=.
@@ -943,9 +951,12 @@ Proof.
     (* NeuPair *)
     + admit.
     (* NeuBind: Impossible *)
-    + admit.
+    + move => b p p0 a /algo_metric_join h _ h0. exfalso.
+      move : h h0. clear.
+      move /Sub.FromJoin.
+      hauto l:on use:Sub.hne_bind_noconf.
     (* NeuUniv: Impossible *)
-    + admit.
+    + hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join.
   - move {ih}.
     move /algo_metric_sym in h.
     qauto l:on use:coqeq_symmetric_mutual.

theories/fp_red.v

@@ -1675,6 +1675,10 @@ Module RERed.
 End RERed.
 
 Module REReds.
+  Lemma hne_preservation n (a b : PTm n) :
+    rtc RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; eauto using RERed.hne_preservation, rtc_refl, rtc. Qed.
+
   Lemma sn_preservation n (a b : PTm n) :
     rtc RERed.R a b ->
     SN a ->
@@ -2284,6 +2288,17 @@ Module DJoin.
     case : c => //=; itauto.
   Qed.
 
+  Lemma hne_univ_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isuniv b -> False.
+  Proof.
+    move => [c [h0 h1]] h2 h3.
+    have {h0 h1 h2 h3} : ishne c /\ isuniv c by
+      hauto l:on use:REReds.hne_preservation,
+          REReds.univ_preservation.
+    move => [].
+    case : c => //=.
+  Qed.
+
   Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
     DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
     p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
@@ -2564,6 +2579,17 @@ Module Sub.
     qauto l:on inv:SNe.
   Qed.
 
+  Lemma hne_bind_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isbind b -> False.
+  Proof.
+    rewrite /R.
+    move => [c[d] [? []]] h0 h1 h2 h3.
+    have : ishne c by eauto using REReds.hne_preservation.
+    have : isbind d by eauto using REReds.bind_preservation.
+    move : h1. clear. inversion 1; subst => //=.
+    clear. case : d => //=.
+  Qed.
+
   Lemma bind_sne_noconf n (a b : PTm n) :
     R a b -> SNe b -> isbind a -> False.
   Proof.