add nbe for types

theories/Algorithmic/Subtyping/Definitions.v

@@ -28,10 +28,9 @@ where "⊢anf M ⊆ N" := (alg_subtyping_nf M N) (in custom judg) : type_scope.
 
 
 Inductive alg_subtyping : ctx -> typ -> typ -> Prop :=
-| alg_subtyp_run :
-  forall Γ M N i j A B,
-    nbe Γ M {{{ Type@i }}} A ->
-    nbe Γ N {{{ Type@j }}} B ->
+| alg_subtyp_run : forall Γ M N A B,
+    nbe_ty Γ M A ->
+    nbe_ty Γ N B ->
     {{ ⊢anf A ⊆ B }} ->
     {{ Γ ⊢a M ⊆ N }}
 where "Γ ⊢a M ⊆ N" := (alg_subtyping Γ M N) (in custom judg) : type_scope.

theories/Algorithmic/Subtyping/Lemmas.v

@@ -87,7 +87,7 @@ Proof.
     assert {{ Γ ⊢ Type@j : Type@(S j) }} by mauto.
     on_all_hyp: fun H => apply soundness in H.
     destruct_all.
-    econstructor; try eassumption.
+    econstructor; mauto 2.
     progressive_inversion.
     mauto.
   - assert {{ Γ ⊢ Π A B : Type@i }} as HΠ1 by mauto.
@@ -100,7 +100,7 @@ Proof.
     apply soundness in HΠ1.
     apply soundness in HΠ2.
     destruct_all.
-    econstructor; try eassumption.
+    econstructor; mauto 2.
     progressive_inversion.
     simpl in *.
     functional_initial_env_rewrite_clear.
@@ -118,6 +118,7 @@ Proof.
   intros. destruct H.
   on_all_hyp: fun H => apply soundness in H.
   destruct_all.
+  on_all_hyp: fun H => apply nbe_type_to_nbe_ty in H.
   functional_nbe_rewrite_clear.
   gen_presups.
   eapply alg_subtyping_nf_sound in H3; try eassumption.

theories/Core/Semantic/NbE.v

@@ -114,12 +114,49 @@ Qed.
 #[export]
 Hint Resolve functional_nbe_of_typ : mcltt.
 
+
+Inductive nbe_ty : ctx -> typ -> nf -> Prop :=
+| nbe_ty_run :
+  `( initial_env Γ p ->
+     {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ Rtyp m in (length Γ) ↘ W }} ->
+     nbe_ty Γ M W ).
+
+#[export]
+Hint Constructors nbe_ty : mcltt.
+
+Lemma functional_nbe_ty : forall Γ M w w',
+    nbe_ty Γ M w ->
+    nbe_ty Γ M w' ->
+    w = w'.
+Proof.
+  intros.
+  inversion_clear H; inversion_clear H0;
+    functional_initial_env_rewrite_clear;
+  functional_eval_rewrite_clear;
+  functional_read_rewrite_clear;
+  reflexivity.
+Qed.
+
+Lemma nbe_type_to_nbe_ty : forall Γ M i w,
+    nbe Γ M {{{ Type@i }}} w ->
+    nbe_ty Γ M w.
+Proof.
+  intros. progressive_inversion.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve functional_nbe_ty nbe_type_to_nbe_ty : mcltt.
+
 Ltac functional_nbe_rewrite_clear1 :=
   let tactic_error o1 o2 := fail 3 "functional_nbe equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : nbe ?G ?M ?A ?W, H2 : nbe ?G ?M ?A ?W' |- _ =>
       clean replace W' with W by first [solve [mauto 2] | tactic_error W' W]; clear H2
   | H1 : nbe ?G ?A {{{ Type@?i }}} ?W, H2 : nbe ?G ?A {{{ Type@?j }}} ?W' |- _ =>
       clean replace W' with W by first [solve [mauto 2] | tactic_error W' W]
+  | H1 : nbe_ty ?G ?M ?W, H2 : nbe_ty ?G ?M ?W' |- _ =>
+      clean replace W' with W by first [solve [mauto 2] | tactic_error W' W]; clear H2
   end.
 Ltac functional_nbe_rewrite_clear := repeat functional_nbe_rewrite_clear1.