typeclasses shenanigans

CoqHott · Jan 28, 2025 · 17d31cb · 17d31cb
1 parent 42de86c
commit 17d31cb
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 18 deletions.
diff --git a/theories/Algorithmic/AlgorithmicTypingProperties.v b/theories/Algorithmic/AlgorithmicTypingProperties.v
@@ -397,30 +397,16 @@ End AlgorithmicTypingProperties.
 
 (** ** Consequences *)
 
-Import AlgorithmicTypingProperties.
-
-(** *** Completeness of algorithmic typing *)
-
-Import BundledTypingData AlgorithmicTypingProperties.
-
-From LogRel.TypingProperties Require Import LogRelConsequences.
-#[local] Existing Instances TypingSubstLogRel RedCompleteLogRel TypeConstructorsInjLogRel ConvCompleteLogRel TypingCompleteLogRel.
-
-#[deprecated(note="use the TypingComplete class instead")]Corollary algo_typing_complete Γ A t :
-  [Γ |-[de] t : A] ->
-  [Γ |-[bn] t : A].
-Proof.
-  now eintros ?%(tm_compl (ta' := bn)).
-Qed.
+Import AlgorithmicTypingData AlgorithmicTypingProperties.
 
 (** *** Uniqueness of types *)
 
-Lemma type_uniqueness Γ A A' t :
+Lemma type_uniqueness `{! TypingComplete (ta := de) (ta' := bn)} Γ A A' t :
   [Γ |-[de] t : A] ->
   [Γ |-[de] t : A'] ->
   [Γ |-[de] A ≅ A'].
 Proof.
-  intros [?? Hinf]%algo_typing_complete [?? Hinf']%algo_typing_complete.
+  intros [?? Hinf]%tm_compl [?? Hinf']%tm_compl.
   eapply algo_typing_det in Hinf.
   2: eassumption.
   subst.

diff --git a/theories/Decidability.v b/theories/Decidability.v
@@ -10,6 +10,8 @@ From PartialFun Require Import Monad PartialFun MonadExn.
 Import AlgorithmicTypingProperties DeclarativeTypingProperties.
 Set Universe Polymorphism.
 
+Import IntermediateTypingProperties BundledTypingData.
+
 #[local]Existing Instance TypingSubstLogRel.
 #[local]Existing Instance RedCompleteLogRel.
 #[local]Existing Instance TypeConstructorsInjLogRel.
@@ -37,7 +39,7 @@ Next Obligation.
   intros.
   apply typing_terminates ; tea.
   - apply implem_tconv_sound.
-  - apply tconv_terminates. 
+  - now intros ; eapply tconv_terminates.
 Qed.
 Next Obligation.
   intros * e ; cbn in *.
@@ -58,7 +60,10 @@ Next Obligation.
     eapply orec_graph_functional in Hgraph ; tea.
     assert (ok = exception e0) as [=] by (etransitivity ; eassumption).
   }
+
+  change [Γ |-[de] t : T] in Hty.
   eapply (tm_compl (ta' := bn)) in Hty as [].
+
   apply typing_complete.
   1: now apply implem_conv_complete.
   constructor ; tea.