Update type checker to use Coq 8.20 feature

theories/Extraction/PseudoMonadic.v

@@ -1,8 +1,25 @@
 From Coq Require Extraction.
+From Coq Require Import RelationClasses.
 
-(* We cannot use class based generalization for
-   the following definitions as Coq does not support
-   polymorphism across [Prop] and [Set] *)
+Polymorphic Class Pure@{s0 s1 s2|u0 u1 u2|} (P: Type@{s0|u0} -> Type@{s1|u1} -> Type@{s2|u2}) :=
+  pure : forall {A : Type@{s0|u0}} {B : Type@{s1|u1}}, A -> P A B.
+
+Instance sumbool_Pure : Pure sumbool :=
+  { pure _ _ a := left a }.
+
+Instance sumor_Pure : Pure sumor :=
+  { pure _ _ a := inleft a }.
+
+(* We can even merge the following two classes, but then
+   instance search cannot easily find the right instance.
+ *)
+Polymorphic Class FailablePseudoMonad@{s0 s1 s2 s3 s4 s5|u0 u1 u2 u3 u4 u5|}
+  (P: Type@{s0|u0} -> Type@{s1|u1} -> Type@{s2|u2})
+  (R: Type@{s3|u3} -> Type@{s4|u4} -> Type@{s5|u5}) :=
+  pmbind : forall {A : Type@{s0|u0}} {B : Type@{s1|u1}}, P A B -> forall {C : Type@{s3|u3}} {D : Type@{s4|u4}}, (B -> D) -> (A -> R C D) -> R C D.
+(* "pm" stands for PseudoMonadic *)
+Notation "'let*pm' a ':=' ab 'while' fail 'in' next" := (pmbind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+Extraction Inline pmbind.
 
 Definition sumbool_failable_bind {A B} (ab : {A} + {B}) {C D : Prop} (fail : B -> D) (next : A -> {C} + {D}) :=
   match ab with
@@ -12,8 +29,8 @@ Definition sumbool_failable_bind {A B} (ab : {A} + {B}) {C D : Prop} (fail : B -
 Transparent sumbool_failable_bind.
 Arguments sumbool_failable_bind /.
 
-Notation "'let*b' a ':=' ab 'while' fail 'in' next" := (sumbool_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
-Notation "'pureb' a" := (left a) (at level 0, only parsing).
+Instance sumbool_FailablePseudoMonad : FailablePseudoMonad sumbool sumbool :=
+  { pmbind _ _ ab _ _ fail next := sumbool_failable_bind ab fail next }.
 
 Definition sumor_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> C + {D}) :=
   match ab with
@@ -23,18 +40,8 @@ Definition sumor_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail : B ->
 Transparent sumor_failable_bind.
 Arguments sumor_failable_bind /.
 
-Notation "'let*o' a ':=' ab 'while' fail 'in' next" := (sumor_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
-Notation "'pureo' a" := (inleft a) (at level 0, only parsing).
-
-Definition sumbool_sumor_failable_bind {A B} (ab : {A} + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> C + {D}) :=
-  match ab with
-  | left a => next a
-  | right b => inright (fail b)
-  end.
-Transparent sumbool_sumor_failable_bind.
-Arguments sumbool_sumor_failable_bind /.
-
-Notation "'let*b->o' a ':=' ab 'while' fail 'in' next" := (sumbool_sumor_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+Instance sumor_FailablePseudoMonad : FailablePseudoMonad sumor sumor :=
+  { pmbind _ _ ab _ _ fail next := sumor_failable_bind ab fail next }.
 
 Definition sumor_sumbool_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> {C} + {D}) :=
   match ab with
@@ -44,6 +51,18 @@ Definition sumor_sumbool_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail
 Transparent sumor_sumbool_failable_bind.
 Arguments sumor_sumbool_failable_bind /.
 
-Notation "'let*o->b' a ':=' ab 'while' fail 'in' next" := (sumor_sumbool_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+Instance sumor_sumbool_FailablePseudoMonad : FailablePseudoMonad sumor sumbool :=
+  { pmbind _ _ ab _ _ fail next := sumor_sumbool_failable_bind ab fail next }.
+
+Definition sumbool_sumor_failable_bind {A B} (ab : {A} + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> C + {D}) :=
+  match ab with
+  | left a => next a
+  | right b => inright (fail b)
+  end.
+Transparent sumbool_sumor_failable_bind.
+Arguments sumbool_sumor_failable_bind /.
+
+Instance sumbool_sumor_FailablePseudoMonad : FailablePseudoMonad sumbool sumor :=
+  { pmbind _ _ ab _ _ fail next := sumbool_sumor_failable_bind ab fail next }.
 
 Extraction Inline sumbool_failable_bind sumor_failable_bind sumbool_sumor_failable_bind sumor_sumbool_failable_bind.

theories/Extraction/Subtyping.v

@@ -24,12 +24,12 @@ Ltac subtyping_tac :=
 #[tactic="subtyping_tac"]
 Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆ B }} } :=
 | n{{{ Type@i }}}, n{{{ Type@j }}} =>
-    let*b _ := Compare_dec.le_lt_dec i j while _ in
-    pureb _
+    let*pm _ := Compare_dec.le_lt_dec i j while _ in
+    pure _
 | n{{{ Π A B }}}, n{{{ Π A' B' }}} =>
-    let*b _ := nf_eq_dec A A' while _ in
-    let*b _ := subtyping_nf_impl B B' while _ in
-    pureb _
+    let*pm _ := nf_eq_dec A A' while _ in
+    let*pm _ := subtyping_nf_impl B B' while _ in
+    pure _
 (* Pseudo-monadic syntax for the next catch-all branch
    generates some unsolved obligations *)
 | A, B with nf_eq_dec A B => {
@@ -77,8 +77,8 @@ Equations subtyping_impl G A B (H : subtyping_order G A B) :
 | G, A, B, H =>
     let (a, Ha) := nbe_ty_impl G A _ in
     let (b, Hb) := nbe_ty_impl G B _ in
-    let*b _ := subtyping_nf_impl a b while _ in
-    pureb _.
+    let*pm _ := subtyping_nf_impl a b while _ in
+    pure _.
 Next Obligation.
   progressive_inversion.
   functional_nbe_rewrite_clear.

theories/Extraction/TypeCheck.v

@@ -33,26 +33,26 @@ Section lookup.
     repeat impl_obl_tac1;
     intuition (mauto 4).
 
-  #[tactic="impl_obl_tac"]
+  #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
   Equations lookup G (HG : {{ ⊢ G }}) x : { A | {{ #x : A ∈ G }} } + { forall A, ~ {{ #x : A ∈ G }} } :=
   | {{{ G, A }}}, HG, x with x => {
-    | 0 => pureo (exist _ {{{ A[Wk] }}} _)
+    | 0 => pure (exist _ {{{ A[Wk] }}} _)
     | S x' =>
-        let*o (exist _ B _) := lookup G _ x' while _ in
-        pureo (exist _ {{{ B[Wk] }}} _)
+        let*pm (exist _ B _) := lookup G _ x' while _ in
+        pure (exist _ {{{ B[Wk] }}} _)
     }
   | {{{ ⋅ }}}, HG, x => inright _.
 End lookup.
 
 Section type_check.
   Equations get_level_of_type_nf (A : nf) : { i | A = n{{{ Type@i }}} } + { forall i, A <> n{{{ Type@i }}} } :=
-  | n{{{ Type@i }}} => pureo (exist _ i _)
+  | n{{{ Type@i }}} => pure (exist _ i _)
   | _               => inright _
   .
 
   (* Don't forget to use 9th bit of [Extraction Flag] (for example, [Set Extraction Flag 1007.]) *)
   Equations get_subterms_of_type_pi (A : nf) : { B & { C | A = n{{{ Π B C }}} } } + { forall B C, A <> n{{{ Π B C }}} } :=
-  | n{{{ Π B C }}} => pureo (existT _ B (exist _ C _))
+  | n{{{ Π B C }}} => pure (existT _ B (exist _ C _))
   | _              => inright _
   .
 
@@ -125,87 +125,87 @@ Section type_check.
   #[local]
   Ltac impl_obl_tac :=
     clear_defs;
-    repeat impl_obl_tac_helper;
+    try match goal with
+      | H: type_check_order _ |- _ => progressive_invert H
+      end;
+    repeat match goal with
+      | H: type_infer_order _ |- _ => progressive_invert H
+      end;
     destruct_conjs;
     match goal with
     | |- {{ ⊢ ~_ }} => gen_presups; mautosolve 4
     | H: {{ ~?G ⊢ ~?A : Type@?i }} |- {{ ~?G ⊢ ~?A : Type@(Nat.max ?i ?j) }} => apply lift_exp_max_left; mautosolve 4
     | H: {{ ~?G ⊢ ~?A : Type@?j }} |- {{ ~?G ⊢ ~?A : Type@(Nat.max ?i ?j) }} => apply lift_exp_max_right; mautosolve 4
     | |- {{ ~_ ⊢ ~_ : ~_ }} => gen_presups; mautosolve 4
-    | |- (~ {{ ~_ ⊢a ~_ ⊆ ~_ }} -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }}) =>
+    | |- _ -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }} =>
         let H := fresh "H" in
         intros ? H;
-        inversion H;
+        directed dependent destruction H;
         functional_alg_type_infer_rewrite_clear;
         firstorder
-    | |- ((forall A : nf, ~ {{ ~_ ⊢a ~_ ⟹ ~_ }}) -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }}) =>
-        let H := fresh "H" in
-        intros ? H;
-        inversion H;
-        firstorder
+    | |- _ -> (forall A : nf, ~ {{ ~_ ⊢a ~_ ⟹ ~_ }}) =>
+        unfold not in *;
+        intros;
+        progressive_inversion;
+        functional_alg_type_infer_rewrite_clear;
+        solve [congruence | mautosolve 3]
     | |- type_infer_order _ => eassumption; fail 1
     | |- type_check_order _ => eassumption; fail 1
     | |- subtyping_order ?G ?A ?B =>
         enough (exists i, {{ G ⊢ A : ~n{{{ Type@i }}} }}) as [? [? []]%soundness_ty];
         only 1: enough (exists j, {{ G ⊢ B : ~n{{{ Type@j }}} }}) as [? [? []]%soundness_ty];
         only 1: solve [econstructor; eauto 3 using nbe_ty_order_sound];
         solve [mauto 4 using alg_type_infer_sound]
-    | _ =>
-        unfold not;
-        intros;
-        progressive_inversion;
-        functional_alg_type_infer_rewrite_clear;
-        solve [congruence | mautosolve 3]
-    | _ => idtac
+    | _ => try mautosolve 3
     end.
 
   #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
   Equations type_check G A (HA : (exists i, {{ G ⊢ A : Type@i }})) M (H : type_check_order M) : { {{ G ⊢a M ⟸ A }} } + { ~ {{ G ⊢a M ⟸ A }} } by struct H :=
   | G, A, HA, M, H =>
-      let*o->b (exist _ B _) := type_infer G _ M _ while _ in
-      let*b _ := subtyping_impl G B A _ while _ in
-      pureb _
+      let*pm (exist _ B _) := type_infer G _ M _ while _ in
+      let*pm _ := subtyping_impl G (nf_to_exp B) A _ while _ in
+      pure _
   with type_infer G (HG : {{ ⊢ G }}) M (H : type_infer_order M) : { A : nf | {{ G ⊢a M ⟹ A }} /\ (exists i, {{ G ⊢a A ⟹ Type@i }}) } + { forall A, ~ {{ G ⊢a M ⟹ A }} } by struct H :=
   | G, HG, M, H with M => {
     | {{{ Type@j }}} =>
-        pureo (exist _ n{{{ Type@(S j) }}} _)
-    | {{{ ℕ }}} => 
-        pureo (exist _ n{{{ Type@0 }}} _)
+        pure (exist _ n{{{ Type@(S j) }}} _)
+    | {{{ ℕ }}} =>
+        pure (exist _ n{{{ Type@0 }}} _)
     | {{{ zero }}} =>
-        pureo (exist _ n{{{ ℕ }}} _)
+        pure (exist _ n{{{ ℕ }}} _)
     | {{{ succ M' }}} =>
-        let*b->o _ := type_check G {{{ ℕ }}} _ M' _ while _ in
-        pureo (exist _ n{{{ ℕ }}} _)
+        let*pm _ := type_check G {{{ ℕ }}} _ M' _ while _ in
+        pure (exist _ n{{{ ℕ }}} _)
     | {{{ rec M' return A' | zero -> MZ | succ -> MS end }}} =>
-        let*b->o _ := type_check G {{{ ℕ }}} _ M' _ while _ in
-        let*o (exist _ UA' _) := type_infer {{{ G, ℕ }}} _ A' _ while _ in
-        let*o (exist _ i _) :=  get_level_of_type_nf UA' while _ in
-        let*b->o _ := type_check G {{{ A'[Id,,zero] }}} _ MZ _ while _ in
-        let*b->o _ := type_check {{{ G, ℕ, A' }}} {{{ A'[Wk∘Wk,,succ #1] }}} _ MS _ while _ in
+        let*pm _ := type_check G {{{ ℕ }}} _ M' _ while _ in
+        let*pm (exist _ UA' _) := type_infer {{{ G, ℕ }}} _ A' _ while _ in
+        let*pm (exist _ i _) :=  get_level_of_type_nf UA' while _ in
+        let*pm _ := type_check G {{{ A'[Id,,zero] }}} _ MZ _ while _ in
+        let*pm _ := type_check {{{ G, ℕ, A' }}} {{{ A'[Wk∘Wk,,succ #1] }}} _ MS _ while _ in
         let (A'', _) := nbe_ty_impl G {{{ A'[Id,,M'] }}} _ in
-        pureo (exist _ A'' _)
+        pure (exist _ A'' _)
     | {{{ Π B C }}} =>
-        let*o (exist _ UB _) := type_infer G _ B _ while _ in
-        let*o (exist _ i _) :=  get_level_of_type_nf UB while _ in
-        let*o (exist _ UC _) := type_infer {{{ G, B }}} _ C _ while _ in
-        let*o (exist _ j _) :=  get_level_of_type_nf UC while _ in
-        pureo (exist _ n{{{ Type@(max i j) }}} _)
+        let*pm (exist _ UB _) := type_infer G _ B _ while _ in
+        let*pm (exist _ i _) :=  get_level_of_type_nf UB while _ in
+        let*pm (exist _ UC _) := type_infer {{{ G, B }}} _ C _ while _ in
+        let*pm (exist _ j _) :=  get_level_of_type_nf UC while _ in
+        pure (exist _ n{{{ Type@(max i j) }}} _)
     | {{{ λ A' M' }}} =>
-        let*o (exist _ UA' _) := type_infer G _ A' _ while _ in
-        let*o (exist _ i _) :=  get_level_of_type_nf UA' while _ in
-        let*o (exist _ B' _) := type_infer {{{ G, A' }}} _ M' _ while _ in
+        let*pm (exist _ UA' _) := type_infer G _ A' _ while _ in
+        let*pm (exist _ i _) :=  get_level_of_type_nf UA' while _ in
+        let*pm (exist _ B' _) := type_infer {{{ G, A' }}} _ M' _ while _ in
         let (A'', _) := nbe_ty_impl G A' _ in
-        pureo (exist _ n{{{ Π A'' B' }}} _)
+        pure (exist _ n{{{ Π A'' B' }}} _)
     | {{{ M' N' }}} =>
-        let*o (exist _ C _) := type_infer G _ M' _ while _ in
-        let*o (existT _ A (exist _ B _)) := get_subterms_of_type_pi C while _ in
-        let*b->o _ := type_check G A _ N' _ while _ in
-        let (B', _) := nbe_ty_impl G {{{ B[Id,,N'] }}} _ in
-        pureo (exist _ B' _)
+        let*pm (exist _ C _) := type_infer G _ M' _ while _ in
+        let*pm (existT _ A (exist _ B _)) := get_subterms_of_type_pi C while _ in
+        let*pm _ := type_check G (A : nf) _ N' _ while _ in
+        let (B', _) := nbe_ty_impl G {{{ ~(B : nf)[Id,,N'] }}} _ in
+        pure (exist _ B' _)
     | {{{ #x }}} =>
-        let*o (exist _ A _) := lookup G _ x while _ in
+        let*pm (exist _ A _) := lookup G _ x while _ in
         let (A', _) := nbe_ty_impl G A _ in
-        pureo (exist _ A' _)
+        pure (exist _ A' _)
     | _ => inright _
     }
   .
@@ -214,7 +214,7 @@ Section type_check.
     clear_defs.
     mautosolve 4.
   Qed.
-  
+
   Next Obligation (* exists j, {{ G ⊢ A'[Id,,zero] : Type@j }} *).
     clear_defs.
     functional_alg_type_infer_rewrite_clear.
@@ -293,21 +293,21 @@ Section type_check.
     firstorder mauto 3.
   Qed.
 
-  Next Obligation. (* exists i : nat, {{ G ⊢ n : Type@i }} *)
+  Next Obligation. (* exists i : nat, {{ G ⊢ A : Type@i }} *)
     clear_defs.
     functional_alg_type_infer_rewrite_clear.
     progressive_inversion.
     eexists; mauto 4 using alg_type_infer_sound.
   Qed.
 
-  Next Obligation. (* nbe_ty_order G {{{ B[Id,,N'] }}} *)
+  Next Obligation. (* nbe_ty_order G {{{ y0[Id,,N'] }}} *)
     clear_defs.
     functional_alg_type_infer_rewrite_clear.
     progressive_inversion.
     assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G, ~(A : exp) ⊢ s : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G, ~(A : exp) ⊢ y0 : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
     assert {{ G ⊢ N' : A }} by mauto 3 using alg_type_check_sound.
-    assert {{ G ⊢ s[Id,,N'] : ~n{{{ Type@j }}} }} as [? []]%soundness_ty by mauto 3.
+    assert {{ G ⊢ y0[Id,,N'] : ~n{{{ Type@j }}} }} as [? []]%soundness_ty by mauto 3.
     mauto 3 using nbe_ty_order_sound.
   Qed.
 
@@ -317,8 +317,8 @@ Section type_check.
     progressive_inversion.
     split; [mauto 3 |].
     assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G, ~(A : exp) ⊢ s : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G ⊢ s[Id,,N'] ≈ B' : Type@j }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    assert {{ G, ~(A : exp) ⊢ y0 : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ y0[Id,,N'] ≈ B' : Type@j }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
     assert (user_exp B') by trivial using user_exp_nf.
     assert (exists k, {{ G ⊢a B' ⟹ Type@k }} /\ k <= j) as [? []] by (gen_presups; mauto 3).
     firstorder.
@@ -340,15 +340,18 @@ End type_check.
 
 Section type_check_closed.
   #[local]
-  Ltac impl_obl_tac := unfold not; intros; mauto 3 using user_exp_to_type_infer_order, type_check_order, type_infer_order.
+  Ltac impl_obl_tac :=
+    unfold not in *;
+    intros;
+    mauto 3 using user_exp_to_type_infer_order, type_check_order, type_infer_order.
 
   #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)]
   Equations type_check_closed A (HA : user_exp A) M (HM : user_exp M) : { {{ ⋅ ⊢ M : A }} } + { ~ {{ ⋅ ⊢ M : A }} } :=
   | A, HA, M, HM =>
-      let*o->b (exist _ UA _) := type_infer {{{ ⋅ }}} _ A _ while _ in
-      let*o->b (exist _ i _) :=  get_level_of_type_nf UA while _ in
-      let*b _ := type_check {{{ ⋅ }}} A _ M _ while _ in
-      pureb _
+      let*pm (exist _ UA _) := type_infer {{{ ⋅ }}} _ A _ while _ in
+      let*pm (exist _ i _) :=  get_level_of_type_nf UA while _ in
+      let*pm _ := type_check {{{ ⋅ }}} A _ M _ while _ in
+      pure _
   .
   Next Obligation. (* False *)
     assert {{ ⊢ ⋅ }} by mauto 2.